Stream: Coq users

Topic: selection of variable


view this post on Zulip 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]

view this post on Zulip Julin S (Apr 30 2023 at 04:34):

Posting the coq code itself could make the question clearer.

view this post on Zulip Paolo Giarrusso (Apr 30 2023 at 05:03):

What Julin said, and depending on what f is, the goal might be unprovable or false

view this post on Zulip 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.

view this post on Zulip 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: Jun 20 2024 at 12:02 UTC