experiment in removing internal_paths_*

Author: tabareau

test/bugs/github1794.v

@@ -283,6 +283,8 @@ Register paths as core.identity.type.
 Register idpath as core.identity.refl.
 Register paths_rect as core.identity.ind.
 Register paths_rec as core.identity.rec.
+Register paths_rec as core.identity.rect.
+Register paths_ind as core.identity.rect_dep.
 
 Notation "x = y :> A" := (@paths A x y) : type_scope.
 Notation "x = y" := (x = y :>_) : type_scope.
@@ -310,6 +312,13 @@ Proof.
   exact u.
 Defined.
 
+Definition paths_rect_r {A : Type} (a : A)
+           (P : A -> Type) (u : P a)
+  : forall (y : A) (p : y = a), P y := paths_ind_r a (fun b _ => P b) u.
+
+Register paths_ind_r as core.identity.rect_r_dep.
+Register paths_rect_r as core.identity.rect_r.
+
 Definition related_reflexive_path {A : Type} (R : Relation A) `{Reflexive A R}
   {a b : A} (p : a = b)
   : R a b.
@@ -398,16 +407,13 @@ Notation "p # u" := (transport _ p u) (only parsing) : path_scope.
 
 (** The first time [rewrite] is used in each direction, it creates transport lemmas called [internal_paths_rew] and [internal_paths_rew_r].  See ../Tactics.v for how these compare to [transport].  We use [rewrite] here to trigger the creation of these lemmas.  This ensures that they are defined outside of sections, so they are not unnecessarily polymorphic.  The lemmas below are not used in the library. *)
 (** TODO: Since Coq 8.20 has PR#18299, once that is our minimum version we can instead register wrappers for [transport] to be used for rewriting.  See the comment by Dan Christensen in that PR for how to do this.  Then the tactics [internal_paths_rew_to_transport] and [rewrite_to_transport] can be removed from ../Tactics.v. *)
+(** TODO DONE*)
 Local Lemma define_internal_paths_rew A x y P (u : P x) (H : x = y :> A) : P y.
 Proof. rewrite <- H. exact u. Defined.
 
 Local Lemma define_internal_paths_rew_r A x y P (u : P y) (H : x = y :> A) : P x.
 Proof. rewrite -> H. exact u. Defined.
 
-(* TODO: ": rename" is needed because the default names changed in Rocq 9.2.0.  When the minimum supported version is >= 9.2.0, the ": rename" can be removed. *)
-Arguments internal_paths_rew {A%_type_scope} {a} P%_function_scope f {a0} p : rename.
-Arguments internal_paths_rew_r {A%_type_scope} {a y} P%_function_scope HC X.
-
 (** Having defined transport, we can use it to talk about what a homotopy theorist might see as "paths in a fibration over paths in the base"; and what a type theorist might see as "heterogeneous equality in a dependent type".  We will first see this appearing in the type of [apD]. *)
 
 (** Functions act on paths: if [f : A -> B] and [p : x = y] is a path in [A], then [ap f p : f x = f y].  We typically pronounce [ap] as a single syllable, short for "application"; but it may also be considered as an acronym, "action on paths". *)

theories/Basics/Overture.v

@@ -405,20 +405,3 @@ Ltac context_to_lambda G :=
                                 let ret := context G[k] in
                                 exact ret)) in
   (eval cbv zeta in ret).
-
-(** The [rewrite <-] tactic uses [internal_paths_rew], which is definitionally equal to [transport], except for the order of the arguments.  The following replaces the former with the latter. *)
-Ltac internal_paths_rew_to_transport :=
-  repeat match goal with |- context [ internal_paths_rew ?P ?u ?p ] =>
-                           change (internal_paths_rew P u p) with (transport P p u) end.
-
-(** Unfortunately, the more common [rewrite ->] uses [internal_paths_rew_r], which is not definitionally equal to something involving [transport].  However, we do have a propositional equality. The arguments here match the arguments that [internal_paths_rew_r] takes. *)
-Definition internal_paths_rew_r_to_transport {A : Type} {x y : A} (P : A -> Type) (u : P y) (p : x = y)
-  : internal_paths_rew_r P u p = transport P p^ u.
-Proof.
-  destruct p; reflexivity.
-Defined.
-
-(** This tactic replaces both [internal_paths_rew] and [internal_paths_rew_r] with [transport], using [rewrite] for the latter. *)
-Ltac rewrite_to_transport :=
-  internal_paths_rew_to_transport;
-  rewrite ! internal_paths_rew_r_to_transport.