val:nat l:list nat
I am confuse here ,i should apply destruct command on l or val ?
If i apply induction on l then f will be 0.
val=0 val>0 is contradiction.
In second case
On the other hand val=0 & val>0 also gives same result.
In this case what would be better option to apply destruct command on l or val which leads contradiction.
Posting the coq code itself could make the question clearer.
What Julin said, and depending on what f is, the goal might be unprovable or false
Also, a mistake: if you apply induction on l, you'll get val = 0 -> val > 0 which isn't a contradiction (that lets you close the goal), just an unprovable goal.
In fact, if f  = 0, then l :=  is a case where your goal is false.
Last updated: Oct 04 2023 at 20:01 UTC