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]

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: Jun 20 2024 at 12:02 UTC