The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Note that induction is really needed:
l = x :: l makes sense for circular lists,
as well as n = S n for infinite numbers.

JF

On Tue, Feb 10, 2015 at 10:03:41AM -0300, Saulo Araujo wrote:
>    Thanks a lot Pierre!
>    On Tue, Feb 10, 2015 at 9:42 AM, Pierre Casteran
>    
> <[1]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
> 
>      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
>