The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Hi everybody,

Thanks a lot for all comments and proofs. The proof that currently better fits my Coq knowledge is the one from Pierre. But it has some steps that I dont understand. Maybe you can help me fully understand it.

I rewrote Pierre's proof a little bit:

Theorem cons_t1 :

  forall A (l : list A) (a : A), l <> a :: l.

Proof.

  intros.

  induction l.

  discriminate.

  injection.

  intros.

  destruct IHl.

  rewrite H1 in H0.

  trivial.

Qed.

I understand all steps except the destruct IHl one. When Coq executes this step, it replaces False for l = a :: l in the goal. Why this happens?

Thanks,

Saulo

On Tue, Feb 10, 2015 at 10:41 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

2015-02-10 14:03 GMT+01:00 Saulo Araujo <saulo2 AT gmail.com>:

Thanks a lot Pierre!

On Tue, Feb 10, 2015 at 9:42 AM, Pierre Casteran <pierre.casteran AT labri.fr> wrote:

Hi,

 You can prove an auxiliary lemma by induction, using both discriminate and injection.
 Using list length leads you to use the fact that no natural number is eaual to its successor, which you can prove by the same technique.

Pierre

Well, you can also pose a definition like:

Definition same_length {A:Type} : list A -> list A -> Prop :=
  fix same_length (l : list A) : list A -> Prop :=
  match l with
  | nil => fun m => match m with nil => True | _ => False end
  | x::l => fun m => match m with y::m => same_length l m | _ => False end
  end.

From there, proving that "L1:forall l, same_length l l" can easily be done by induction.
Proving that "L2:forall l a, same_length l (a::l) -> False" is also trivial by induction on l.
From that two points, you can also easily prove your final goal with something like:

intros l a Heq; apply (L2 l a); case Heq; apply L1.
(or provide the full proof term: fun l a Heq => L2 l a (match Heq in _=x return same_length l x with eq_refl => L1 l end)).

This way, you have more things to prove, but if you are interested in the proof terms, they are likely to be more readable.

And this will also avoid the "n <> S n" proof.
 

Require Import List.

Goal forall A (l : list A) (a:A), l <> a::l.
induction l.
 -discriminate.
- injection 1.
  intros H0 _ ; now  destruct (IHl a).
Qed.


Le 10/02/2015 13:31, Saulo Araujo a écrit :

Hi,

I am trying to prove a theorem and got stuck. I have the following
hypothesis

H0 : l = (c, p) :: l

which says that a list is equal to the tail of another list. This, I
believe, is never true. Prooving another simpler theorem I also got in a
situation like this and, in that simpler case, I could end the proof
using the discriminate tactic, but in this case, Coq says:

Error: No primitive equality found.

Does anyone know what can I do?

Thanks in advance,
Saulo