The Coq mailing list

[vsiles AT lix.polytechnique.fr]

>
> Hi
>
> I've only used Coq for a few months so please forgive my ignorance.
>
> I am trying to do some formalization work in Coq and have ran across a
> problem, the essence of which can be summarized below:
>
> I have a type that's dependent on some other type, say nat for example:
> Record T (a:nat) : Type := { some_field : nat }.
>
> I have found that in order to state some theorems I need the following
> equality definition for T:
>
> Inductive T_eq (a:nat) (r1:T a) : forall b:nat, T b -> Prop :=
> | T_eq_intro : forall (r2:T a), r1 = r2 -> T_eq r1 r2.
>
> The intention is that for some r1:T a and r2:T b (where a and b might not
> be
> definitionally equal), T_eq r1 r2 iff a = b and r1 = r2.
> The point is that the only way to construct T_eq is to construct with (r1
> r2:T a) and a proof of r1 = r2.
>
> Which works fine until I want to make use of T_eq, ie what I want is the
> following theorem:
>
> forall (a:nat) (r1 r2:T a), T_eq r1 r2 -> r1 = r2.
>
> So if I have a proof of T_eq r1 r2, I want to get back the proof of r1=r2.
> But I can't seem to prove it.  I look at the elimination rule for T_eq:
>
> T_eq_ind =
> fun (a : nat) (r1 : T a) (P : forall b : nat, T b -> Prop)
>   (f : forall r2 : T a, r1 = r2 -> P a r2) (b : nat)
>   (t : T b) (t0 : T_eq r1 t) =>
> match t0 in (T_eq _ t1) return (P b0 t1) with
> | T_eq_intro x x0 => f x x0
> end
>
> The return type for the case analysis is (P b0 t1) for some P which, as
> far
> as I can see, cannot allow for the return type to be r1=r2, so how do I
> get
> back the proof of r1=r2?
>
> Thanks in advance.
>
> See
>
> --
> View this message in context:
> http://www.nabble.com/Newbie-question-%28Eliminating-some-dependent-types%29-tf3957584.html#a11229739
> Sent from the Coq mailing list archive at Nabble.com.
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
Hi !
I'm also quite new to coq but I've been playing with the equality on
dependant types lately, so I'll do my best.
The fact is when you have dependant equality, you can't always achieve the
transition to the liepniz equality for every dependant types. A well known
type family where this holds is when the equality is decidable. Can you
prove on your type that:
forall x y:T, {x=y}+{x<>y} ?

I invite you to read the Logiv/Eqdep_dec.v file (especially Theorem
eq_dep_eq_dec which I guess is what you're looking for)

I hope it will help you,

Regards

Vincent Siles,
master student (MPRI,Paris)