The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

In the development version (8.5), there is a set of "standard"
notations for eq_rect and eq_rect_r to "get it right" quicklier:

Import EqNotations. (* From Logic.v *)
Definition test0 {A B:Type} {H:A=B} (a:A) : B := rew [fun X => X] H in a.

or even:

Import EqNotations.
Definition test0 {A B:Type} {H:A=B} (a:A) : B := rew H in a.

To achieve this in 8.4, one would need the following

Import EqNotations.
Notation "'rew' [ P ] H 'in' H'" := (eq_rect _ P H' _ H)
    (at level 10, H' at level 10,
     format "'[' 'rew'  [ P ]  '/    ' H  in  '/' H' ']'").
Definition test0 {A B:Type} {H:A=B} (a:A) : B := rew [fun X => X] H in a.

Happy 2015,

Hugo

On Tue, Dec 30, 2014 at 10:44:24PM +0100, Cedric Auger wrote:
> You can also be more low level by unfolding eq_rect.
> 
> I did not tried it, but I guess that the following would work:
> 
> Definition test0 {A B:Type} {H:A=B} (a:A) : B :=
>   match H in _=T return T with eq_refl => a end.
> 
> I do not know if coq has improved annotations inference. Maybe the following
> would also work:
> 
> Definition test0 {A B:Type} {H:A=B} (a:A) : B := let () := H in a.
> 
> 
> 
> 2014-12-30 20:21 GMT+01:00 Guillaume Melquiond 
> <guillaume.melquiond AT inria.fr>:
> 
>     On 30/12/2014 20:01, Vadim Zaliva wrote:
> 
>         Is it possible to do something like this:
> 
>         Program Definition test0 {A B:Type} {H:A=B} (a:A) : B := a.
> 
>         I would like using 'H' cast (coerce?) 'a' to type 'B'.
> 
> 
>     Definition test0 {A B:Type} {H:A=B} (a:A) : B :=
>       eq_rect A (fun C => C) a B H.
> 
>     Note that, except for a few people, I don't expect anyone to get the
>     formula right on the first try. Here is how I obtained it:
> 
>     Definition test0 {A B:Type} {H:A=B} (a:A) : B.
>     Proof.
>       rewrite <- H.
>       exact a.
>     Defined.
> 
>     Best regards,
> 
>     Guillaume
> 
>