Extend Scheme command to support custom schemes#21271
Closed
felixL-K wants to merge 6 commits intorocq-prover:masterfrom
Closed
Extend Scheme command to support custom schemes#21271felixL-K wants to merge 6 commits intorocq-prover:masterfrom
felixL-K wants to merge 6 commits intorocq-prover:masterfrom
Conversation
coqbot-app
bot
added
the
needs: full CI
Contributor
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
github-actions
bot
added
the
needs: rebase
Contributor
|
Doesn't build & needs a rebase to fix conflicts (I guess conflicts from #21241) |
felixL-K
force-pushed
the
generalize_schemes_try_rebase
branch
from
50fa022 to
e22a90f
Compare
coqbot-app
bot
added
needs: full CI
SkySkimmer
added
needs: squashing
felixL-K
force-pushed
the
generalize_schemes_try_rebase
branch
from
e22a90f to
daa1773
Compare
SkySkimmer
removed
the
needs: squashing
Contributor
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
SkySkimmer
reviewed
Nov 18, 2025
SkySkimmer
reviewed
Nov 18, 2025
SkySkimmer
reviewed
Nov 18, 2025
test-suite/success/RegisterScheme.v
Outdated
|
|
||
| Module TestExport. | ||
| #[export] Register Scheme paths_rew_r_dep as rew_r_dep for eq. | ||
| #[export] Register Scheme paths_rew_r_dep as Left2Right Dependent Rewrite for eq. |
Contributor
There was a problem hiding this comment.
we probably want to provide some compatibility mapping for Register Scheme so that the old scheme names keep working alongside the new ones for at least version
Author
There was a problem hiding this comment.
Do I add a function like:
let old_scheme_name_to_new sch =
match sch with
| ["rew_r_dep"] -> ["Left2Right"; "Dependent"; "Rewrite"]
| ["rect_dep"] | ["rec_dep"] -> ["Induction"]
| …
| _ -> CErrors.user_err Pp.(str ("unknown scheme kind " ^ String.concat " " sch))
and wrap it in a deprecation warning?
Right now I changed the Register command so that it always requires Sort @qualid at the end, so maybe compatibility for old scheme names is no longer necessary ?
Contributor
There was a problem hiding this comment.
The old syntax should keep working (deprecated) for at least a version
so yes there should be some old_scheme_name_to_new translation, but it should also return the sort (and Register shouldn't be given a sort when called with old scheme names)
SkySkimmer
reviewed
Nov 18, 2025
SkySkimmer
reviewed
Nov 18, 2025
| val all_schemes : unit -> Constant.t CString.Map.t Indmap_env.t | ||
| module Key : sig | ||
|
|
||
| type t = (string list * UnivGen.QualityOrSet.t option * bool) |
Contributor
There was a problem hiding this comment.
not entirely sure QualityOrSet is the right type for this, we may want a type which does not include sort variables
Author
There was a problem hiding this comment.
@herbelin what do you think about this ?
What type should we use ? Should I create a new type or keep QualityOrSet ?
Contributor
There was a problem hiding this comment.
And yet, you want to be able to distinguish SortPoly or Not.
A basic algebraic type would probably suffice
SkySkimmer
reviewed
Nov 18, 2025
SkySkimmer
reviewed
Nov 18, 2025
Contributor
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/hott/theories/Limits/Pullback.v in 50m 27s (from ci-hott) (full log on GitHub Actions - verbose log) We are collecting data on the user experience of the Coq Bug Minimizer. 🌟 Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-noinit" "-indices-matter" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/theories" "HoTT" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/contrib" "HoTT.Contrib" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/test" "HoTT.Tests" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Ltac2" "Ltac2" "-top" "HoTT.Limits.Pullback") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 498 lines to 67 lines, then from 81 lines to 723 lines, then from 729 lines to 118 lines, then from 129 lines to 182 lines, then from 189 lines to 122 lines, then from 133 lines to 924 lines, then from 931 lines to 146 lines, then from 156 lines to 196 lines, then from 203 lines to 157 lines, then from 168 lines to 1050 lines, then from 1056 lines to 221 lines, then from 232 lines to 371 lines, then from 378 lines to 231 lines, then from 242 lines to 1803 lines, then from 1809 lines to 246 lines, then from 257 lines to 969 lines, then from 973 lines to 305 lines, then from 316 lines to 1129 lines, then from 1135 lines to 434 lines, then from 445 lines to 532 lines, then from 539 lines to 447 lines, then from 457 lines to 772 lines, then from 776 lines to 478 lines, then from 489 lines to 477 lines, then from 489 lines to 378 lines, then from 390 lines to 378 lines *)
(* coqc version 9.2+alpha compiled with OCaml 4.14.2
coqtop version 9.2+alpha
Expected coqc runtime on this file: 1.262 sec
Expected coqc peak memory usage on this file: 370688.0 kb *)
Require Corelib.Init.Ltac.
Inductive False : Prop := .
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
Reserved Notation "x = y :> T"
(at level 70, y at next level, no associativity).
Reserved Notation "{ x : A & P }" (at level 0, x at level 99).
Reserved Notation "p @ q" (at level 20).
Reserved Notation "f == g" (at level 70, no associativity).
Reserved Notation "A <~> B" (at level 85).
Reserved Notation "g 'oE' f" (at level 40, left associativity).
Reserved Notation "g 'o' f" (at level 40, left associativity).
Declare Scope fibration_scope.
Delimit Scope function_scope with function.
Delimit Scope type_scope with type.
Delimit Scope equiv_scope with equiv.
Delimit Scope path_scope with path.
Global Open Scope equiv_scope.
Global Open Scope path_scope.
Global Open Scope fibration_scope.
Global Open Scope type_scope.
Declare ML Module "ltac_plugin:coq-core.plugins.ltac".
Global Set Default Proof Mode "Classic".
Global Set Universe Polymorphism.
Global Unset Strict Universe Declaration.
Global Set Keyed Unification.
Create HintDb typeclass_instances discriminated.
Notation "A -> B" := (forall (_ : A), B) : type_scope.
Definition Relation (A : Type) := A -> A -> Type.
Class Reflexive {A} (R : Relation A) :=
reflexivity : forall x : A, R x x.
Class Symmetric {A} (R : Relation A) :=
symmetry : forall x y, R x y -> R y x.
Ltac old_reflexivity := reflexivity.
Tactic Notation "reflexivity" :=
old_reflexivity
|| (intros;
let R := match goal with |- ?R ?x ?y => constr:(R) end in
let pre_proof_term_head := constr:(@reflexivity _ R _) in
let proof_term_head := (eval cbn in pre_proof_term_head) in
apply (proof_term_head : forall x, R x x)).
Tactic Notation "symmetry" :=
let R := match goal with |- ?R ?x ?y => constr:(R) end in
let x := match goal with |- ?R ?x ?y => constr:(x) end in
let y := match goal with |- ?R ?x ?y => constr:(y) end in
let pre_proof_term_head := constr:(@symmetry _ R _) in
let proof_term_head := (eval cbn in pre_proof_term_head) in
refine (proof_term_head y x _); change (R y x).
Notation Type0 := Set.
Record sig {A} (P : A -> Type) := exist {
proj1 : A ;
proj2 : P proj1 ;
}.
Arguments exist {A}%_type P%_type _ _.
Arguments proj1 {A P} _ / .
Arguments proj2 {A P} _ / .
Notation "{ x : A & P }" := (sig (fun x:A => P)) : type_scope.
Notation "( x ; y )" := (exist _ x y) : fibration_scope.
Notation pr1 := proj1.
Notation pr2 := proj2.
Notation "x .1" := (pr1 x) : fibration_scope.
Notation "x .2" := (pr2 x) : fibration_scope.
Notation idmap := (fun x => x).
Notation compose := (fun g f x => g (f x)).
Notation "g 'o' f" := (compose g%function f%function) : function_scope.
Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Arguments idpath {A a} , [A] a.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.
Definition inverse {A : Type} {x y : A} (p : x = y) : y = x.
Admitted.
Instance symmetric_paths {A} : Symmetric (@paths A) | 0.
exact (@inverse A).
Defined.
Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
match p, q with idpath, idpath => idpath end.
Notation "1" := idpath : path_scope.
Notation "p @ q" := (concat p%path q%path) : path_scope.
Notation "p ^" := (inverse p%path) : path_scope.
Definition ap {A B : Type} (f : A -> B) {x y : A} (p : x = y) : f x = f y.
Admitted.
Definition pointwise_paths A (P : A -> Type) (f g : forall x, P x)
:= forall x, f x = g x.
Instance symmetric_pointwise_paths A P
: Symmetric (pointwise_paths A P).
Proof.
intros ? ? p ?; symmetry; apply p.
Defined.
Global Arguments pointwise_paths {A}%_type_scope {P} (f g)%_function_scope.
Notation "f == g" := (pointwise_paths f g) : type_scope.
Class IsEquiv {A B : Type} (f : A -> B) := {
equiv_inv : B -> A ;
eisretr : f o equiv_inv == idmap ;
eissect : equiv_inv o f == idmap ;
eisadj : forall x : A, eisretr (f x) = ap f (eissect x) ;
}.
Record Equiv A B := {
equiv_fun : A -> B ;
equiv_isequiv :: IsEquiv equiv_fun
}.
Notation "A <~> B" := (Equiv A B) : type_scope.
Inductive trunc_index : Type0 :=
| minus_two : trunc_index
| trunc_S : trunc_index -> trunc_index.
Inductive IsTrunc_internal (A : Type@{u}) : trunc_index -> Type@{u} :=
| Build_Contr : forall (center : A) (contr : forall y, center = y), IsTrunc_internal A minus_two
| istrunc_S : forall {n:trunc_index}, (forall x y:A, IsTrunc_internal (x = y) n) -> IsTrunc_internal A (trunc_S n).
Notation IsTrunc n A := (IsTrunc_internal A n).
Notation Contr A := (IsTrunc minus_two A).
Tactic Notation "do_with_holes" tactic3(x) uconstr(p) :=
x uconstr:(p) ||
x uconstr:(p _) ||
x uconstr:(p _ _) ||
x uconstr:(p _ _ _) ||
x uconstr:(p _ _ _ _) ||
x uconstr:(p _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).
Class IsGlobalAxiom (A : Type) : Type0 := {}.
Ltac is_global_axiom A := let _ := constr:(_ : IsGlobalAxiom A) in idtac.
Ltac global_axiom := try match goal with
| |- ?G => is_global_axiom G; exact _
end.
Tactic Notation "nrefine" uconstr(term) := notypeclasses refine term; global_axiom.
Tactic Notation "snrefine" uconstr(term) := simple notypeclasses refine term; global_axiom.
Tactic Notation "rapply" uconstr(term)
:= do_with_holes ltac:(fun x => assert_succeeds (nrefine x); refine x) term.
Definition inv_V {A : Type} {x y : A} (p : x = y) :
p^^ = p.
Admitted.
Definition Contr_ind@{u v|} (A : Type@{u}) (P : Contr A -> Type@{v})
(H : forall (center : A) (contr : forall y, center = y), P (Build_Contr A center contr))
(C : Contr A)
: P C.
Admitted.
Instance reflexive_equiv : Reflexive Equiv | 0.
Admitted.
Definition equiv_compose' {A B C : Type} (g : B <~> C) (f : A <~> B)
: A <~> C.
Admitted.
Notation "g 'oE' f" := (equiv_compose' g%equiv f%equiv) : equiv_scope.
Section Adjointify.
Context {A B : Type} (f : A -> B) (g : B -> A).
Context (isretr : f o g == idmap) (issect : g o f == idmap).
Definition equiv_adjointify : A <~> B.
Admitted.
End Adjointify.
Theorem equiv_inverse {A B : Type} : (A <~> B) -> (B <~> A).
Admitted.
Notation "e ^-1" := (@equiv_inverse _ _ e) : equiv_scope.
Instance symmetric_equiv : Symmetric Equiv | 0.
Admitted.
Ltac decomposing_intros :=
let x := fresh in
intros x; hnf in x; cbn in x;
try lazymatch type of x with
| ?a = ?b => idtac
| forall y:?A, ?B => idtac
| Contr ?A => revert x; match goal with |- (forall y, ?P y) => snrefine (Contr_ind A P _) end
| _ => elim x; clear x
end;
try decomposing_intros.
Ltac multi_assumption :=
multimatch goal with
[ H : ?A |- _ ] => exact H
end.
Ltac build_record :=
cbn; multi_assumption + (unshelve econstructor; build_record).
Ltac make_equiv :=
snrefine (equiv_adjointify _ _ _ _);
[ decomposing_intros; build_record
| decomposing_intros; build_record
| decomposing_intros; exact idpath
| decomposing_intros; exact idpath ].
Generalizable Variables X A B C f g n.
Definition functor_sigma `{P : A -> Type} `{Q : B -> Type}
(f : A -> B) (g : forall a, P a -> Q (f a))
: sig P -> sig Q.
exact (fun u => (f u.1 ; g u.1 u.2)).
Defined.
Definition equiv_functor_sigma_id `{P : A -> Type} `{Q : A -> Type}
(g : forall a, P a <~> Q a)
: sig P <~> sig Q.
Admitted.
Local Unset Elimination Schemes.
Cumulative Inductive PathSquare {A} : forall a00 {a10 a01 a11 : A},
a00 = a10 -> a01 = a11 -> a00 = a01 -> a10 = a11 -> Type
:= sq_id : forall {x : A},
PathSquare x 1 1 1 1.
Arguments PathSquare {A _ _ _ _}.
#[warnings="-unsupported-attributes",register=no] Scheme PathSquare_ind := Induction for PathSquare Sort Type.
Definition equiv_sq_tr {A : Type} {a00 a10 a01 a11 : A}
{px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11}
: PathSquare px0 px1 p0x p1x <~> PathSquare p0x p1x px0 px1.
Admitted.
Notation sq_tr := equiv_sq_tr.
Section MovePaths.
Context {A : Type} {x x00 x20 x02 x22 : A}
{f10 : x00 = x20} {f12 : x02 = x22} {f01 : x00 = x02} {f21 : x20 = x22}.
Definition equiv_sq_move_23 {f12'' : x02 = x} {f12' : x = x22}
: PathSquare f10 (f12'' @ f12') f01 f21 <~> PathSquare f10 f12' (f01 @ f12'') f21.
admit.
Defined.
Definition equiv_sq_move_14 {f10'' : x00 = x} {f10' : x = x20}
: PathSquare (f10'' @ f10') f12 f01 f21 <~> PathSquare f10'' f12 f01 (f10' @ f21).
admit.
Defined.
Definition equiv_sq_move_24 {f12'' : x02 = x} {f12' : x22 = x}
: PathSquare f10 (f12'' @ f12'^) f01 f21 <~> PathSquare f10 f12'' f01 (f21 @ f12').
admit.
Defined.
Definition equiv_sq_move_31 {f10'' : x00 = x} {f10' : x = x20}
: PathSquare f10' f12 (f10''^ @ f01) f21 <~> PathSquare (f10'' @ f10') f12 f01 f21.
admit.
Defined.
End MovePaths.
Notation sq_move_23 := equiv_sq_move_23.
Notation sq_move_14 := equiv_sq_move_14.
Notation sq_move_24 := equiv_sq_move_24.
Notation sq_move_31 := equiv_sq_move_31.
Definition Pullback {A B C} (f : B -> A) (g : C -> A)
:= { b : B & { c : C & f b = g c }}.
Section Functor_Pullback.
Context {A1 B1 C1 A2 B2 C2}
(f1 : B1 -> A1) (g1 : C1 -> A1)
(f2 : B2 -> A2) (g2 : C2 -> A2)
(h : A1 -> A2) (k : B1 -> B2) (l : C1 -> C2)
(p : f2 o k == h o f1) (q : g2 o l == h o g1).
Definition functor_pullback : Pullback f1 g1 -> Pullback f2 g2.
exact (functor_sigma k
(fun b1 => (functor_sigma l
(fun c1 e1 => p b1 @ ap h e1 @ (q c1)^)))).
Defined.
End Functor_Pullback.
Definition equiv_path_pullback {A B C} (f : B -> A) (g : C -> A)
(x y : Pullback f g)
: { p : x.1 = y.1 & { q : x.2.1 = y.2.1 & PathSquare (ap f p) (ap g q) x.2.2 y.2.2 } }
<~> (x = y).
Admitted.
Section Pullback3x3.
Context
(A00 A02 A04 A20 A22 A24 A40 A42 A44 : Type)
(f01 : A00 -> A02) (f03 : A04 -> A02)
(f10 : A00 -> A20) (f12 : A02 -> A22) (f14 : A04 -> A24)
(f21 : A20 -> A22) (f23 : A24 -> A22)
(f30 : A40 -> A20) (f32 : A42 -> A22) (f34 : A44 -> A24)
(f41 : A40 -> A42) (f43 : A44 -> A42)
(H11 : f12 o f01 == f21 o f10) (H13 : f12 o f03 == f23 o f14)
(H31 : f32 o f41 == f21 o f30) (H33 : f32 o f43 == f23 o f34).
Let fX1 := functor_pullback f10 f30 f12 f32 f21 f01 f41 H11 H31.
Let fX3 := functor_pullback f14 f34 f12 f32 f23 f03 f43 H13 H33.
Let f1X := functor_pullback f01 f03 f21 f23 f12 f10 f14 (symmetry _ _ H11) (symmetry _ _ H13).
Let f3X := functor_pullback f41 f43 f21 f23 f32 f30 f34 (symmetry _ _ H31) (symmetry _ _ H33).
Theorem pullback3x3 : Pullback fX1 fX3 <~> Pullback f1X f3X.
Proof.
refine (_ oE _ oE _).
1,3:do 2 (rapply equiv_functor_sigma_id; intro).
1:apply equiv_path_pullback.
1:symmetry; apply equiv_path_pullback.
refine (_ oE _).
{
do 4 (rapply equiv_functor_sigma_id; intro).
refine (sq_tr oE _).
refine (sq_move_14^-1 oE _).
refine (sq_move_31 oE _).
refine (sq_move_24^-1 oE _).
refine (sq_move_23^-1 oE _).
rewrite 2 inv_V.
reflexivity.
}
make_equiv.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 2.9MiB file on GitHub Actions Artifacts under
|
SkySkimmer
reviewed
Nov 18, 2025
|
|
||
| (newref,sch_type, ind, sch_sort) | ||
|
|
||
| let do_scheme ~register ?(force_mutual=false) env l = |
Contributor
There was a problem hiding this comment.
register is ignored, this causes HoTT to fail as #[warnings="unsupported-attributes",register=no] Scheme PathSquare_ind := Induction for PathSquare Sort Type. is registering the scheme when they don't want it registered.
Contributor
|
@coqbot ci minimize ci-fiat_parsers ci-metarocq |
Contributor
|
I am now running minimization at commit daa1773 on requested targets ci-fiat_parsers, ci-metarocq. I'll come back to you with the results once it's done. |
SkySkimmer
reviewed
Nov 18, 2025
github-actions
bot
added
the
needs: rebase
Contributor
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metarocq/erasure/theories/EWcbvEval.v in 5h 15m 7s (from ci-metarocq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout) (truncated to first and last 32KiB; full 113KiB file on GitHub Actions Artifacts under
|
Contributor
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metarocq/erasure/theories/EWcbvEval.v in 5h 15m 7s (from ci-metarocq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout) (truncated to first and last 32KiB; full 61KiB file on GitHub Actions Artifacts under
|
felixL-K
force-pushed
the
generalize_schemes_try_rebase
branch
from
daa1773 to
e257755
Compare
coqbot-app
bot
added
needs: full CI
github-actions
bot
added
the
needs: rebase
felixL-K
force-pushed
the
generalize_schemes_try_rebase
branch
from
b062970 to
72951dc
Compare
coqbot-app
bot
removed
the
needs: rebase
thomas-lamiaux
requested changes
Dec 23, 2025
Contributor
thomas-lamiaux
left a comment
thomas-lamiaux
left a comment
There was a problem hiding this comment.
I don't have much to say except that I do not think it is a good practice to make types more specific for instance by adding a bool here and there.
We want generic type we understand and that are not ad-hoc and instantiate them appropriately when needed.
Comment on lines
+24
to
+26
| val declare_scheme : Libobject.locality -> Key.t -> (inductive * GlobRef.t) -> unit | ||
| val lookup_scheme : (string list * UnivGen.QualityOrSet.t option * bool) -> inductive -> GlobRef.t | ||
| val all_schemes : unit -> GlobRef.t Key.Map.t Indmap_env.t |
Contributor
There was a problem hiding this comment.
While I understand the idea not to really on string, I am not sure whether it is any better to really on sth as ad-hoc as:
string list * UnivGen.QualityOrSet.t option * bool
What if we later want to differentiate regular definition from template polymorphic one ? Or any variant of that ?
Would we add one more boolean ?
Contributor
There was a problem hiding this comment.
I would probably prefer a string with a well-written function to compute it that can be easily extended rather than extending the type ? What do you think ?
|
|
||
| type is_mutual = bool | ||
|
|
||
| type t = (string list * UnivGen.QualityOrSet.t option * is_mutual) |
Contributor
There was a problem hiding this comment.
Why use a list of string and not just a String ?
| with_context_set ctx (UnivGen.fresh_global_instance env sym_scheme) | ||
|
|
||
| let build_sym_involutive_scheme env handle ind = | ||
| let build_sym_involutive_scheme env handle ind _ = |
Contributor
There was a problem hiding this comment.
I don't know what is the standard in Ocaml, but I personally think it is much better to add an eta-expansion when the function needs to be applied like fun x y _ -> f x y than to add an unnamed variable at the definition f x y _.
It is not the end of the world as build_sym_involutive_scheme is not exposed in the .mli file, but it still makes it harder to maintain the code as you don't get why there is an extra-variable until you find where it is applied
| (* Scheme builders. [bool] = is_dep. [None] = silent failure. *) | ||
| type mutual_scheme_object_function = | ||
| Environ.env -> handle -> MutInd.t -> constr array Evd.in_ustate | ||
| Environ.env -> handle -> inductive list -> bool -> constr array Evd.in_ustate option |
Contributor
There was a problem hiding this comment.
I don't think a boolean should be added here. This is too specific.
To me a function instantiate to true should be given as an argument when needed.
Why is there an addition of the type option ?
| let is_declared_scheme_object key = Hashtbl.mem scheme_object_table key | ||
|
|
||
| let scheme_kind_name (key : _ scheme_kind) : string = key | ||
| let get_suff sch_type sch_sort = |
Contributor
There was a problem hiding this comment.
Please name this get_suffix or whatever it is supposed to mean.
suff really does not mean anything. It could be a typo for stuff for instance.
| ?suff:string -> | ||
| ?deps:(Environ.env -> MutInd.t -> scheme_dependency list) -> | ||
| val declare_mutual_scheme_object : string list * UnivGen.QualityOrSet.t option -> | ||
| (Declarations.one_inductive_body option -> string) -> |
| val all_schemes : unit -> Constant.t CString.Map.t Indmap_env.t | ||
| module Key : sig | ||
|
|
||
| type t = (string list * UnivGen.QualityOrSet.t option * bool) |
Contributor
There was a problem hiding this comment.
And yet, you want to be able to distinguish SortPoly or Not.
A basic algebraic type would probably suffice
| let sigma = Evd.emit_side_effects eff sigma in | ||
| Proofview.Unsafe.tclEVARS sigma | ||
|
|
||
| (* Scheme builders. [bool] = is_dep. [None] = silent failure. *) |
Contributor
There was a problem hiding this comment.
[None] = silent failure.
What do you mean ?
Comment on lines
+62
to
+63
| | SchemeMutualDep of Names.MutInd.t * mutual scheme_kind * bool | ||
| | SchemeIndividualDep of inductive * individual scheme_kind * bool |
Contributor
There was a problem hiding this comment.
why add tabs ? (and Names. btw )
| with Not_found -> CErrors.user_err Pp.(str "Mutually defined schemes should be recursive.")) | ||
| | _ -> (failwith "do_mutual_scheme expects a non empty list of inductive types.") | ||
|
|
||
| (* TODO : redifine do_mutual_induction_scheme using do_mutual_scheme *) |
Contributor
|
@felixL-K just to be clear, they are many design choices possible. I am questioning a few one that have been made, but I am not saying to change it. It should only be changed if, after discussing with the others like @SkySkimmer, we agree that this one or that one is better. |
github-actions
bot
added
the
needs: rebase
Contributor
|
The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed. |
Contributor
|
This PR was not rebased after 30 days despite the warning, it is now closed. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This pull request comes at the conclusion of my internship with Hugo Herbelin and aims to extend the
Schemecommand in Rocq to allow users to define new schemes beyond the built-in ones(
Induction,Minimality,Elimination,Case, etc.).It also unifies the previously distinct implementations of
EqualityandBoolean Equalityschemes,bringing them into the generalised scheme mechanism.
Previously, the compiler only allowed a fixed set of elimination schemes, by generalising them, we
open the door for user-defined schemes.
You can now also define schemes that weren’t accessible before.
For example:
Scheme Right2Left Dependent Rewrite for ind Sort TypeTo do that :
string listrepresenting the scheme name (e.g.,["Induction"],["Boolean";"Equality"], …)UnivGen.QualityOrSet.t optionrepresenting the universe sort/type on which the scheme operatesboolflag indicating whether the scheme is mutual (true) or individual (false)do_mutual_induction_schemein vernac/indschemes.ml with a newdo_schemefunctionthat handles both individual and mutual schemes.
EqualityandBoolean Equalityschemes into the general scheme machinery,no longer special-cased.Rewritingscheme into the general scheme machineryPlease review especially the new scheme registration logic and the handling of mutual vs individual
cases.
make doc_gram_rsts.