The Coq mailing list

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

Hello, Cedric, Damien and Thorsten,

  Thank you for your answers.

I could prove the decidability of equality on finite lists (assuming 
this property on A).

Lemma  LList_eq_dec: forall h :LList, Finite h -> forall k, Finite k -> 
{h=k}+{h<>k}.

Then I try to use eq_dep_eq_dec, but it  requires the decidability of 
equality
over the considered type Llist A.

 - Is there any version  of this theorem allowing me to apply 
Llist_eq_dec instead
of decidability of equality on LList A ? In Logic.Eqdep_dec ? In the 
litterature ?

Pierre



Le 20/05/2011 09:49, AUGER Cedric a écrit :
> 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
> > >
> > >
> > >
> > >
> > >
> > >
> > >        
> >      
>