The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

> 
> I will try to make an exemple for that.
>
Ok, it is not a good one, and I probably could have make it shorter,
but it illustrates what I meant in my previous mail.
====================================================================
Require Import List.

Section X.

Variable A: Type.

Fixpoint last l (a: A) :=
 match l with
 | nil => a
 | a::l => last l a
 end.

Inductive constant: A -> list A -> Prop :=
| Cnil: forall a, constant a nil
| Ccons: forall a l, constant a l -> constant a (a::l).

Lemma Y: forall b a, a = b -> forall l, constant a l -> last l b = a.
Proof.
  intros b a Heq l H.
  induction H; simpl; auto.
  (*ok, the proof is easy, and quite artificial,
    but with the other definition of constant,
    it will be easier *)
  now subst; auto.
Qed.

Inductive constant2 (a: A): list A -> Prop :=
| Cnil2: constant2 a nil
| Ccons2: forall l, constant2 a l -> constant2 a (a::l).

Lemma Z: forall b a, a = b -> forall l, constant2 a l -> last l b = a.
Proof.
  intros b a Heq l H.
  induction H; simpl; auto.
  (*ok, the proof is easy, and quite artificial,
    but as we can see, Heq didn't have to be generalized *)
  now subst.
Qed.
End X.