Stream: Coq users

Topic: Help from H


view this post on Zulip zohaze (Dec 16 2022 at 17:43):

H: l1=[b] ( l:list nat,b:nat)
In goal statement ,i have pattern matching on l1,like this
match l1 with
| []=>false
| h::t=>true
end true.
First , apply induction on l1,then it become
false=true.
statement is wrong because l1 cannot be empty,according to l1 it contains one element.How H can be helpful here?

view this post on Zulip Michael Soegtrop (Dec 16 2022 at 18:25):

You can do e.g.

view this post on Zulip zohaze (Mar 08 2023 at 03:31):

Thank you.

view this post on Zulip Dominique Larchey-Wendling (Mar 08 2023 at 08:18):

subst l1 or rewrite H could work as well.


Last updated: Jun 25 2024 at 14:01 UTC