The Coq mailing list

[Roman Beslik <beroal AT ukr.net>]

Hello everybody.

I'm trying to prove equality of tuples with dependent types (a type of 
'b' depends on a value of 'a'). Two 'Build_t ...'-s should be equal: a0 
= (fun a => a0 a) because of the first assumption and 'b' components are 
equal by definition. (It's just a simplified version for test purposes 
which does not make any sense.)

Record t:Type := {a:nat->Set; b:forall n, a n}.
Variable (a0:nat->Set) (b0:forall n, (fun a => a0 a) n).
Definition subst : forall (eq0:a0 = (fun a => a0 a)),
   Build_t a0 b0 = Build_t (fun a => a0 a) b0.
Proof.
refine (fun eq0 => _).
Set Printing All.
refine (match eq0 in _=dep
   return Build_t a0 b0 = Build_t dep b0
   with refl_equal => _ end).

I get

The term "b0" has type "forall n : nat, (fun a : nat => a0 a) n"
while it is expected to have type "forall n : nat, dep n"

But types in question are beta-convertible:

dep=(fun a => a0 a) \/ dep=a0
-> (forall n : nat, (fun a : nat => a0 a) n)
= (forall n : nat, a0 n)
= (forall n : nat, dep n)

Please can someone explain how Coq's type-checker works here? It is 
trickier than I thought.

--
Best regards,
 Roman Beslik.