The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sunday, November 20, 2011 03:11:00 PM Jesper Louis Andersen wrote:
> 2011/11/20 Victor Porton 
> <porton AT narod.ru>:
> > So I fail to understand what eq_rect means. Could you explain?
> 
> The simplest solution is to ask Coq:
> 
> Coq < About eq_rect.
> eq_rect :
> forall (A : Type) (x : A) (P : A -> Type), P x -> forall y : A, x = y -> P
> y
> 
> Argument A is implicit
> Argument scopes are [type_scope _ _ _ _ _]
> eq_rect is transparent
> Expands to: Constant Coq.Init.Logic.eq_rect
> 
> This tells you it is equivalent to eq_rect_r. There may be a reason
> for having the alternative name, but I don't know it unfortunately. My
> guess is the information can be found out by reading the source code.
> 
> Other likewise Vernacular commands are to be found here in the manual:
> http://coq.inria.fr/doc/Reference-Manual009.html
> 
> Especially the Search-commands are useful. They allow you to hunt for
> specific definitions and such in "reverse". You know there ought to be
> a theorem X, but you only know its statement, not its name for
> instance.

As the name indicates, eq_rect_r is the reverse of eq_rect (it assumes y = x 
instead of x = y).

In English, eq_rect is a conversion operator from P x to P y, given that x=y. 
 
eq_rect_r, given x=y, would do the reverse conversion from P y to P x.
-- 
Daniel Schepler