pianke (Apr 08 2023 at 11:28): pianke (Apr 08 2023 at 11:28):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.
Pierre Castéran (Apr 08 2023 at 12:02):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.
H1: l<>nil
H2: NoDup l=true or H2: NoDup (a::l)=true
I mean in hypothesis write it as above. To avoid the cases of repeation.
Laurent Théry (Apr 09 2023 at 07:30):What is a?
Pierre Castéran (Apr 09 2023 at 09:41):Looks to be some confusion between propositions and Booleans in your statements of H2. If you use Standard library’s Nodup, NoDup l is not a Boolean, but a proposition.
pianke (Apr 11 2023 at 03:06):After induction on l, a is the first element of l.
Laurent Théry (Apr 11 2023 at 12:04):so why you don't give us exactly the goal you have?
Last updated: Apr 19 2024 at 00:02 UTC