The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

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

Thanks again Pierre!

On Tue, Feb 10, 2015 at 12:35 PM, Pierre Casteran <pierre.casteran AT labri.fr> wrote:

Ah, it's just using negation elimination rule.

IHL's statement is  l <> a :: l, that is   ~ (l = a::l)

Negation elimination works as follows:

if you have a goal like
Gamma, H: ~A  |- B
the tactic  "destruct H"  generates a new goal of the form
Gamma |- A.

Well, more generally, if you have a term "t" of type "A->B" and B is an inductive type, "destruct t." is equivalent to "assert (a:A); [|destruct (t a)]." That is: you will be requested to prove existence of something in "A", then this some thing can be applied to "t" to get an inductive value which can be destructured.

False being an inductive, it works in your case.
An other example is when you have something like "H : P x -> a = b", then as "a = b" is an inductive, "destruct H." will also request to prove "P x" and then will replace all occurrences of "b" with "a". I think that "rewrite <- H." also works in this case.
 

In your example, doing "apply IHl" instead of "destruct IHl" works too,
since IHl's type is convertible to  (l = a::l -> False).


Best regards,

Pierre






Le 10/02/2015 15:32, Saulo Araujo a écrit :

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
<mailto:sedrikov AT gmail.com>> wrote:



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

        Thanks a lot Pierre!

        On Tue, Feb 10, 2015 at 9:42 AM, Pierre Casteran

        <pierre.casteran AT labri.fr <mailto:pierre.casteran@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