I want to add a constraint on natural number list that no element is repeated in the list. To solve the lemma related to this list how i should add this in hypothesis(no duplication) .I have a list c1::c2::t & H1:d1=c1 H2: d2=c2 . When i compare two elements of list then i could be able to derive beq_nat c1 c2=false.
You may apply the following lemma:
Require Import List . Lemma NoDup_xy_inv: forall x y (l: list nat), NoDup (x::y::l) -> x <> y. Proof. intros x y l H Heq; inversion_clear H; subst; apply H0; now constructor. Qed.
H2: NoDup l=true or H2: NoDup (a::l)=true
I mean in hypothesis write it as above. To avoid the cases of repeation.
Looks to be some confusion between propositions and Booleans in your statements of
H2. If you use Standard library’s
NoDup l is not a Boolean, but a proposition.
After induction on l, a is the first element of l.
so why you don't give us exactly the goal you have?
Last updated: Oct 04 2023 at 21:01 UTC