The Coq mailing list

[Roman Beslik <beroal AT ukr.net>]

Adam Chlipala wrote:
> Roman Beslik wrote:
> > 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"
>
> The important point here is that the [return] clause must be 
> type-checked independently before it can be used.  During that 
> checking, nothing is known about the variable [dep] but its type, and 
> that type does not imply the equality that you wish held.
>
> Here's a proof that I came up with:
>
> Theorem subst : forall (eq0:a0 = (fun a => a0 a)),
>  Build_t a0 b0 = Build_t (fun a => a0 a) b0.
>  intros.
>  generalize b0.
>  rewrite eq0.
>  reflexivity.
> Qed.
>
> There is more discussion of the importance of generalization in my 
> draft textbook:
>    http://adam.chlipala.net/cpdt/
> though I'm planning to add more coverage of the subject in the next 
> few months.
Thanks for your explanation. If I don't use 'dep' on both sides of '=' 
in 'return' clause than their types don't match.

Though I use
refine (f_equal (fun a => a b0) _).
instead of
generalize b0.
Are they the same?

--
Best regards,
 Roman Beslik.