The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

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




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