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?
You may execute exfalso; discriminate
.
Pierre Castéran said:
You may execute
exfalso; discriminate
.
Thanks! that worked!
Roland Coeurjoly has marked this topic as resolved.
Last updated: Sep 23 2023 at 13:01 UTC