The Coq mailing list

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

Le Fri, 20 May 2011 09:41:35 +0200,
Damien Pous 
<Damien.Pous AT inrialpes.fr>
 a écrit :

> Bonjour Pierre,
> 
> Here is a proof assuming that equality is decidable on streams (which
> is certainly not the case).
> This is because I use the lemma eq_dep_eq_dec to transform an eq_dep
> into a plain eq.
> Would a similar lemma about eq_dep hold assuming proof irrelevance on
> A rather than decidability on LList A ?
> 
> Best,
> Damien
> ---

I got this proof which always require an axiom, but simply using
eq_dep_eq (what is the command to know all the axioms a definition
depends on?)


Variable (A:Type).

CoInductive LList :=
   | LNil: LList
   | LCons : A -> LList -> LList.


Inductive Finite : LList -> Prop :=
   |Finite_LNil: Finite LNil
   |Finite_LCons   : forall a l, Finite l-> Finite (LCons a l).

Require Import Eqdep.

Goal forall l (H H0:Finite l), H=H0.
 (* as I guess it won't be proved without dependant equality,
    I change the goal to make it provable using an axiom *)
 intros l H H0; apply eq_dep_eq.
 (* OK, now we can proceed by first "unrelating" H and H0 *)
 generalize (eq_refl l); revert H0; generalize l at 1 3 5.
 (* OK, now the induction can start;
    as induction doesn't work here, I use fix *)
 revert l H; fix 2; intros _ [] _ [] Heq.
 (*-> LNil vs LNil*)
      split.
 (*-> LNil vs LCons*)
      discriminate.
 (*-> LCons vs LNil*)
      discriminate.
 (*-> LCons vs LCons*)
      (* as always, fist thing to do is get rid of the recursive call *)
      generalize (Unnamed_thm l0 f l2 f0); clear -Heq.
      (* now we eliminate our equality *)
      revert f; inversion_clear Heq; clear.
      (* we simplify our recursive call *)
      intros; generalize (H (eq_refl _)); clear.
      (* we prepare our last equality for elimination *)
      revert f0; generalize l2 at 1 3 6 7; intros.
      (* we eliminate our equality *)
      destruct H.
      (* we conclude *)
      split.
Qed.

> 
> Set Implicit Arguments.
> Require Import Eqdep Eqdep_dec.
> 
> Section s.
> 
> Variable (A:Type).
> 
> CoInductive LList :=
>  | LNil: LList
>  | LCons : A -> LList -> LList.
> 
> 
> Inductive Finite : LList -> Prop :=
>  |Finite_LNil: Finite LNil
>  |Finite_LCons   : forall a l, Finite l -> Finite (LCons a l).
> 
> Notation "H == K" := (eq_dep _ Finite _ H _ K) (at level 80).
> 
> Fixpoint dep h (H: Finite h): forall k (K: Finite k), h = k -> H == K.
>   destruct H; destruct K.
>    reflexivity.
>    discriminate.
>    discriminate.
>    intro E. injection E. intros E1 E2.
>    rewrite (dep _ H _ K E1). subst. reflexivity.
> Defined.
> 
> Goal forall l (H K:Finite l), H==K.
> Proof.
>   intros. apply dep. reflexivity.
> Qed.
> 
> Axiom LList_dec: forall h k: LList, {h=k}+{h<>k}.
> 
> Goal forall l (H K:Finite l), H=K.
> Proof.
>   intros. apply Eqdep_dec.eq_dep_eq_dec.
>    apply LList_dec.
>    apply dep. reflexivity.
> Qed.
> 
> 
> 
> 
> 
> 2011/5/20 Pierre Casteran 
> <pierre.casteran AT labri.fr>:
> > Hello,
> >
> >  Let us consider a type of finite or infinite lists :
> >
> > Variable (A:Type).
> >
> > CoInductive LList :=
> >  | LNil: LList
> >  | LCons : A -> LList -> LList.
> >
> >
> > Inductive Finite : LList -> Prop :=
> >  |Finite_LNil: Finite LNil
> >  |Finite_LCons   : forall a l, Finite l-> Finite (LCons a l).
> >
> >
> > Is it possible to prove unicity of proofs of Finite ?
> >
> > Goal forall l (H H0:Finite l), H=H0 ?
> >
> > Pierre
> >
> >
> >
> >
> >
> >
>