Stream: Coq users

Topic: no similarity


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

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

view this post on Zulip pianke (Apr 09 2023 at 06:30):

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.

view this post on Zulip Laurent Théry (Apr 09 2023 at 07:30):

What is a?

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

view this post on Zulip pianke (Apr 11 2023 at 03:06):

After induction on l, a is the first element of l.

view this post on Zulip Laurent Théry (Apr 11 2023 at 12:04):

so why you don't give us exactly the goal you have?


Last updated: Oct 04 2023 at 21:01 UTC