The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

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