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: Jun 23 2024 at 23:01 UTC