From f139173fb8b1238ded4d100311adb0e8537c0c46 Mon Sep 17 00:00:00 2001 From: nicolas tabareau Date: Fri, 28 Nov 2025 15:33:46 +0100 Subject: [PATCH 1/3] Revert "Merge pull request #2331 from tabareau/sortpoly-equality" This reverts commit 28c8d19d07da01ce6e6b8f8ce79ae6aedf940192, reversing changes made to 42b956c1c4c36ea1ec5adc40baf3b61d3eb829c2. --- test/bugs/github1794.v | 5 +---- theories/Basics/Overture.v | 31 ++++++++++--------------------- theories/Tactics.v | 6 +++--- 3 files changed, 14 insertions(+), 28 deletions(-) diff --git a/test/bugs/github1794.v b/test/bugs/github1794.v index 3f40521a852..6f1d497f2a1 100644 --- a/test/bugs/github1794.v +++ b/test/bugs/github1794.v @@ -1,9 +1,6 @@ From HoTT Require Import Basics.Overture. +(** When [rewrite] is first used, it defines helper lemmas. If the first use is in a Section that has universe variables, then these lemmas get unnecessary universe variables. Overture uses [rewrite] outside of a section to ensure that they have the expected number of universe variables, and we test that here. *) -(** After PR#21098, helper lemmas are not generated as rewrite now relies on typeclass instances *) - -(* Check internal_paths_rew@{u1 u2}. Check internal_paths_rew_r@{u1 u2}. -*) \ No newline at end of file diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v index 95022b93e46..44dbce3f758 100644 --- a/theories/Basics/Overture.v +++ b/theories/Basics/Overture.v @@ -3,8 +3,8 @@ (** This file defines some of the most basic types and type formers, such as sums, products, Sigma types and path types. It defines the action of functions on paths [ap], transport, equivalences, and function extensionality. It also defines truncatedness, and a number of other fundamental definitions used throughout the library. *) (** Import the file of reserved notations so we maintain consistent level notations throughout the library. *) -Require Export Equality. Require Export Basics.Settings Basics.Notations. + Local Set Polymorphic Inductive Cumulativity. (** This command prevents Coq from automatically defining the eliminator functions for inductive types. We will define them ourselves to match the naming scheme of the HoTT Book. In principle we ought to make this [Global], but unfortunately the tactics [induction] and [elim] assume that the eliminators are named in Coq's way, e.g. [thing_rect], so making it global could cause unpleasant surprises for people defining new inductive types. However, when you do define your own inductive types you are encouraged to also do [Local Unset Elimination Schemes] and then use [Scheme] to define [thing_ind], [thing_rec], and (for compatibility with [induction] and [elim]) [thing_rect], as we have done below for [paths], [Empty], [Unit], etc. We are hoping that this will be fixed eventually; see https://github.com/coq/coq/issues/3745. *) @@ -395,28 +395,17 @@ Arguments transport {A}%_type_scope P%_function_scope {x y} p%_path_scope u : si (** Transport is very common so it is worth introducing a parsing notation for it. However, we do not use the notation for output because it hides the fibration, and so makes it very hard to read involved transport expression. *) Notation "p # u" := (transport _ p u) (only parsing) : path_scope. -Instance path_Has_refl@{l} : Has_refl@{Type Type;l l} (@paths@{l}) - := @idpath. - -Definition path_Has_J_elim@{l l'} : Has_J@{Type Type Type; l l l'} (@paths) _ - := paths_rect. - -Hint Resolve path_Has_J_elim : rewrite_instances. - -Definition path_Has_Leibniz_elim@{l l'} : Has_Leibniz@{Type Type Type;l l l'} (@paths) - := @paths_rec. +(** 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. *) +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. -Hint Resolve path_Has_Leibniz_elim : rewrite_instances. +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. -Definition path_Has_J_r_elim@{l l'} : Has_J_r@{Type Type Type; l l l'} (@paths) _ - := @paths_ind_r. - -Hint Resolve path_Has_J_r_elim : rewrite_instances. - -Definition path_Has_Leibniz_r_elim@{l l'} : Has_Leibniz_r@{Type Type s;l l l'} (@paths) := - fun A x P t y e => @paths_ind_r A x (fun a _ => P a) t y e. - -Hint Resolve path_Has_Leibniz_r_elim : rewrite_instances. +(* 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]. *) diff --git a/theories/Tactics.v b/theories/Tactics.v index e1227131184..b5af72b0c25 100644 --- a/theories/Tactics.v +++ b/theories/Tactics.v @@ -408,12 +408,12 @@ Ltac context_to_lambda G := (** 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 [ path_Has_Leibniz_elim ?A ?x ?P ?u ?y ?p ] => - change (path_Has_Leibniz_elim A x P u y p) with (transport P p u) end. + 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) - : path_Has_Leibniz_r_elim _ _ P u _ p = transport P p^ u. + : internal_paths_rew_r P u p = transport P p^ u. Proof. destruct p; reflexivity. Defined. From 52f1d59ff09a27ad9bac45dcbf1f844967db4497 Mon Sep 17 00:00:00 2001 From: nicolas tabareau Date: Fri, 28 Nov 2025 15:35:18 +0100 Subject: [PATCH 2/3] Add overlay after PR #21371 --- theories/Basics/Overture.v | 1 + 1 file changed, 1 insertion(+) diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v index 44dbce3f758..968fae98b65 100644 --- a/theories/Basics/Overture.v +++ b/theories/Basics/Overture.v @@ -282,6 +282,7 @@ Definition paths_rect := paths_ind. 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. Notation "x = y :> A" := (@paths A x y) : type_scope. Notation "x = y" := (x = y :>_) : type_scope. From 704649d16346b8cbfaf501039048d576581f2d0b Mon Sep 17 00:00:00 2001 From: Dan Christensen Date: Sat, 29 Nov 2025 08:41:03 -0500 Subject: [PATCH 3/3] Overture.v: update TODO about registering lemmas for rewriting --- theories/Basics/Overture.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Basics/Overture.v b/theories/Basics/Overture.v index 968fae98b65..e230cb715e3 100644 --- a/theories/Basics/Overture.v +++ b/theories/Basics/Overture.v @@ -397,7 +397,7 @@ Arguments transport {A}%_type_scope P%_function_scope {x y} p%_path_scope u : si 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: 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. Rocq 9.2 will contain PR#21098 which adds further registration options. It should be possible to do things in a way that works across these versions. See #2332 for a discussion of this. *) 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.