The Coq mailing list

[See <wongsee AT gmail.com>]

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.