The Coq mailing list

[Damien Pous <Damien.Pous AT inrialpes.fr>]

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

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