The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

If you have a suitable version of Coq, you can even have
something more focused, during the script:
  info rewrite p.

You can also manually replace "rewrite p" by:
pattern x; refine (paths_rew_r A x y _ _ p).

Now, paths_rew_r itself is no black magic, try
Print paths_rew_r.

You can even prove cow using case instead of rewrite
(rewrite <-, actually):

Proof.
  case q. case p. apply idpath.
Defined.

Or, shorter:

Proof.
  case q. exact p.
Defined.

Hope this helps,
JF

On Mon, Apr 02, 2012 at 11:43:44PM +0200, Andrej Bauer wrote:
> I forgot to mention that 8.4 is doing something, but it would be good
> to know what exactly. Witness this:
> 
> (* We define an inductive type which looks like [eq] but lives in [Type]. *)
> Inductive paths {A : Type} (x : A) : A -> Type := idpath : paths x x.
> 
> (* Let us try to rewrite with it. *)
> 
> Lemma cow {A} (x y z : A) (p : paths x y) (q : paths  y z) : paths x z.
> Proof.
>   rewrite p. (* It works! *)
>   rewrite q. (* It still works! *)
>   apply idpath.
> Defined.
> 
> Print cow.
> (* Output:
> test =
> fun (A : Type) (x y z : A) (p : paths x y) (q : paths y z) =>
> paths_rew_r A x y (fun x0 : A => paths x0 z)
>   (paths_rew_r A y z (fun y0 : A => paths y0 z) (idpath z) q) p
>      : forall (A : Type) (x y z : A), paths x y -> paths y z -> paths x z
> 
> Argument A is implicit and maximally inserted
> Argument scopes are [type_scope _ _ _ _ _]
> *)
> 
> (* Whoa, what is this [paths_rew_r]? Black magic? *)
> 
> (* We try the same with [eq]. *)
> Lemma bull {A} (x y z : A) (p : eq x y) (q : eq y z) : eq x z.
> Proof.
>   rewrite p.
>   rewrite q.
>   apply eq_refl.
> Defined.
> 
> Print bull.
> (* Output:
> bull =
> fun (A : Type) (x y z : A) (p : x = y) (q : y = z) =>
> eq_ind_r (fun x0 : A => x0 = z)
>   (eq_ind_r (fun y0 : A => y0 = z) (eq_refl z) q) p
>      : forall (A : Type) (x y z : A), x = y -> y = z -> x = z
> 
> Argument A is implicit and maximally inserted
> Argument scopes are [type_scope _ _ _ _ _]
> *)
> 
> (* So paths_rew_r is like eq_ind_r. More details please! *)
> 
> With kind regards,
> 
> Andrej
> 
> On Mon, Apr 2, 2012 at 11:31 PM, Andrej Bauer 
> <andrej.bauer AT andrej.com>
>  wrote:
> > What's the current status of having Coq "rewrite" working with an
> > identity type defined in Type rather than in Prop?
> >
> > There is a patch that accomplishes this, I think (but where)? Are
> > there plans to include it in a future version?
> >
> > With kind regards,
> >
> > Andrej
> 
> 

-- 
Jean-Francois Monin