zohaze (Apr 30 2023 at 04:34): zohaze (Apr 30 2023 at 04:34):val:nat l:list nat
val=f l->
val>0.
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
val= f[n::t]
val>0.
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.
& f[n::t]
Julin S (Apr 30 2023 at 04:34):Posting the coq code itself could make the question clearer.
Paolo Giarrusso (Apr 30 2023 at 05:03):What Julin said, and depending on what f is, the goal might be unprovable or false
Paolo Giarrusso (Apr 30 2023 at 05:09):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.
Paolo Giarrusso (Apr 30 2023 at 05:09):In fact, if f [] = 0, then l := [] is a case where your goal is false.
Last updated: Oct 04 2023 at 20:01 UTC