The Coq mailing list

[Brian Aydemir <baydemir AT cis.upenn.edu>]

To expand on Andrew's remark, p and q in prop_eq are inferred to have  
type Type.  Thus, the eq argument to prop_eq is at Type, not at Prop.

As a general remark: Enabling the printing of implicit arguments is a  
good way to debug problems where Coq refuses to match or unify terms  
that look identical to the user.

-Brian

On Jul 30, 2008, at 4:34 PM, Andrew McCreight wrote:

> Doing "Set Printing All" reveals what the problem is:
>
> Toplevel input, characters 54-73:
> Error: The term "@f_equal2 nat nat Prop lt x1 y1 x2 y2 eq1 eq2" has  
> type
>  "@eq Prop (lt x1 x2) (lt y1 y2)" while it is expected to have type
>  "@eq Type (lt x1 x2) (lt y1 y2)".
>
>
> -Andrew
>
> On Mon, Jul 28, 2008 at 4:08 PM, see tolearn <seetolearn AT mail.ru>  
> wrote:
> Consider theorem 'prop_eq':
> > Definition prop_eq := fun p q (eq1:p=q)
>        => (match eq1 in _=qdep return p->qdep
>        with refl_equal => fun p=>p
>        end) : p->q.
>
> Then:
> > Variable (x1 x2 y1 y2:nat) (eq1:x1=y1) (eq2:x2=y2) (lt1:x1<x2).
> > Check prop_eq (x1 < x2) (y1 < y2) (f_equal2 lt eq1 eq2) lt1.
> gives an error message:
> {{{
> Error: The term "f_equal2 lt eq1 eq2" has type "(x1 < x2) = (y1 < y2)"
>  while it is expected to have type "(x1 < x2) = (y1 < y2)"
> }}}
> The terms actually are identic. Am I missing something? I'm
> using CoqIde, coqtop version 8.1pl1 (Jul. 2007), Linux.
>
> Best regards,
> Roman Beslik.
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/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