Stream: Coq users

Topic: Help from H

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?

Michael Soegtrop (Dec 16 2022 at 18:25):

You can do e.g.

• inversion H1 which splits the goal into all ways in which H1 could be valid - which are none
• congruence which is a decision procedure for equalities

zohaze (Mar 08 2023 at 03:31):

Thank you.

Dominique Larchey-Wendling (Mar 08 2023 at 08:18):

subst l1 or rewrite H could work as well.

Last updated: Oct 13 2024 at 01:02 UTC