The Coq mailing list

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

Le Fri, 20 May 2011 11:20:34 +0200,
Pierre Casteran 
<pierre.casteran AT labri.fr>
 a écrit :

> 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
> 

Maybe you should reread my post.

You do not require anything on decidability of equalities on A.
The only thing is that what you want is equivalent to prove:

1. forall (H H0: Finite LNil), H = H0.
2. forall l, (forall (H H0: Finite l), H = H0) ->
   forall a, (H H0: Finite (LCons a l)), H = H0.

or to prove:
1. forall H, H = Finite_LNil.
2. forall a l (f: Finite l) H, H = Finite_LCons a l f.

What I meant was that eq_dep_eq is an axiom sufficient to prove
that but if you have a way to prove that freely, then you have a way to
prove your goal.

Note that there is no matter of being or not coinductive for this case.

> 
> 
> 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
> >>>
> >>>
> >>>
> >>>
> >>>
> >>>
> >>>        
> >>      
> >    
>