Stream: Coq users

Topic: ✔ Reason about head of empty list

Roland Coeurjoly Lechuga (Jun 06 2022 at 16:45):

I have the following context and proof obligations
1 goal (ID 696)

correctness0 : Correctness
generic_debugging_algorithm : forall n : Node,
weight n <
weight
{|
correctness :=
correctness0;
children := []
|} -> Node
head : Node
tail : list Node
Heq_anonymous : head :: tail =
{|
correctness := correctness0;
children := []
|}.(children)
H : head :: tail = []
============================
match head.(children) with
| [] => 1
| n :: l =>
S
(weight n +
list_sum
(map (fun child : Node => weight child) l))
end < 1

There is the hypotheiss H: head :: tail = [], therefore, it is not possible to match head.(children) with anything.
Is it possible to prove this or I have to undo?

Pierre Castéran (Jun 06 2022 at 18:10):

You may execute exfalso; discriminate.

Roland Coeurjoly Lechuga (Jun 06 2022 at 18:13):

Pierre Castéran said:

You may execute exfalso; discriminate.

Thanks! that worked!

Notification Bot (Jun 06 2022 at 18:13):

Roland Coeurjoly has marked this topic as resolved.

Last updated: Sep 23 2023 at 13:01 UTC