From 995dcae187c32d36c2191028567964116bcf0b70 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jul 2026 04:30:00 +0000 Subject: [PATCH 1/3] Adapt to Rocq dev: HB `of` clauses, mathcomp Nz* hierarchy, `^*` level Three unrelated breakages against Rocq 9.4+alpha / mathcomp dev: * Rocq now reserves `of` as a keyword (`constructor_binders` in g_vernac.mlg, "Add \"of _ & _ & _\" syntax for constructors"). coq-elpi parses HB's `of` clause as `IDENT "of"`, which no longer matches, so every `HB.mixin Record ... of ...`, `HB.factory Record ... of ...` and `HB.builders Context ... of ...` fails with a bare "Usage:" message. Use the equivalent `&` spelling, which is the form the HB usage message itself documents and works on older versions too. * mathcomp split its ring hierarchy: `SemiRing` no longer carries `1 != 0`, the nontrivial variant is `NzSemiRing`. Rename SemiRing -> NzSemiRing, ComSemiRing -> ComNzSemiRing, isSemiRing -> isNzSemiRing, SubSemiRing -> SubNzSemiRing, SubChoice_isSub[Com]SemiRing -> SubChoice_isSub[Com]NzSemiRing and SubSemiRing_isSubComSemiRing -> SubNzSemiRing_isSubComNzSemiRing, preserving the previous meaning of the dioid structures. * mathcomp's ssrfun now reserves `x ^*` at level 1 with left associativity; match that reservation instead of level 2. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- complete_dioid.v | 50 +++++++++++++++++++------------------- complete_lattice.v | 60 +++++++++++++++++++++++----------------------- dioid.v | 52 ++++++++++++++++++++-------------------- 3 files changed, 81 insertions(+), 81 deletions(-) diff --git a/complete_dioid.v b/complete_dioid.v index c2dbd9e..1e6b38d 100644 --- a/complete_dioid.v +++ b/complete_dioid.v @@ -59,7 +59,7 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Reserved Notation "x ^+" (at level 2, format "x ^+"). -Reserved Notation "x ^*" (at level 2, format "x ^*"). +Reserved Notation "x ^*" (at level 1, left associativity, format "x ^*"). Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -68,7 +68,7 @@ Local Open Scope dioid_scope. Import Order.Theory GRing.Theory. -HB.mixin Record isCompleteDioid d D of Dioid d D & CompleteLattice d D := { +HB.mixin Record isCompleteDioid d D & Dioid d D & CompleteLattice d D := { set_mulDl : forall (a : D) (B : set D), a * set_join B = set_join [set a * x | x in B]; set_mulDr : forall (a : D) (B : set D), @@ -435,15 +435,15 @@ Notation "a / b" := (div a b) : dioid_scope. #[short(type="comCompleteDioidType")] HB.structure Definition ComCompleteDioid d := - { D of GRing.ComSemiRing D & CompleteDioid d D }. + { D of GRing.ComNzSemiRing D & CompleteDioid d D }. HB.factory Record isComCompleteDioid d D - of ComDioid d D & CompleteLattice d D := { + & ComDioid d D & CompleteLattice d D := { set_mulDl : forall (a : D) (B : set D), a * set_join B = set_join [set a * x | x in B]; }. -HB.builders Context d D of isComCompleteDioid d D. +HB.builders Context d D & isComCompleteDioid d D. Lemma set_mulDr a (B : set D) : set_join B * a = set_join [set x * a | x in B]. Proof. @@ -454,7 +454,7 @@ HB.instance Definition _ := isCompleteDioid.Build d D set_mulDl set_mulDr. HB.end. HB.factory Record CompleteLattice_isComCompleteDioid d D - of CompleteLattice d D := { + & CompleteLattice d D := { zero : D; add : D -> D -> D; one : D; @@ -474,7 +474,7 @@ HB.factory Record CompleteLattice_isComCompleteDioid d D mul a (set_join B) = set_join [set mul a x | x in B]; }. -HB.builders Context d D of CompleteLattice_isComCompleteDioid d D. +HB.builders Context d D & CompleteLattice_isComCompleteDioid d D. HB.instance Definition _ := POrder_isComDioid.Build d D addA addC add0d adddd mulA mulC mul1d mulDl mul0d oner_neq0 le_def. HB.instance Definition _ := isComCompleteDioid.Build d D set_mulDl. @@ -552,10 +552,10 @@ HB.structure Definition SubCompleteDioid d (D : completeDioidType d) S d' := HB.factory Record SubDioid_JoinSubCompleteLattice_isJoinSubCompleteDioid d (D : completeDioidType d) S d' U - of @SubDioid d D S d' U & @JoinSubCompleteLattice d D S d' U := {}. + & @SubDioid d D S d' U & @JoinSubCompleteLattice d D S d' U := {}. HB.builders Context d D S d' U - of SubDioid_JoinSubCompleteLattice_isJoinSubCompleteDioid d D S d' U. + & SubDioid_JoinSubCompleteLattice_isJoinSubCompleteDioid d D S d' U. Lemma set_mulDl (a : U) (B : set U) : a * set_join B = set_join [set a * x | x in B]. Proof. @@ -573,12 +573,12 @@ HB.end. HB.factory Record SubDioid_SubPOrder_isJoinSubCompleteDioid d (D : completeDioidType d) S d' U - of @SubDioid d D S d' U & @Order.SubPOrder d D S d' U := { + & @SubDioid d D S d' U & @Order.SubPOrder d D S d' U := { opredSJ_subproof : set_join_closed S; }. HB.builders Context d D S d' U - of SubDioid_SubPOrder_isJoinSubCompleteDioid d D S d' U. + & SubDioid_SubPOrder_isJoinSubCompleteDioid d D S d' U. HB.instance Definition _ := SubPOrder_isJoinSubCompleteLattice.Build d D S d' U opredSJ_subproof. HB.instance Definition _ := @@ -586,12 +586,12 @@ HB.instance Definition _ := HB.end. HB.factory Record SubChoice_isJoinSubCompleteDioid d (D : completeDioidType d) - S (d' : Order.disp_t) U of SubChoice D S U := { + S (d' : Order.disp_t) U & SubChoice D S U := { semiring_closed_subproof : semiring_closed S; opredSJ_subproof : set_join_closed S; }. -HB.builders Context d D S d' U of SubChoice_isJoinSubCompleteDioid d D S d' U. +HB.builders Context d D S d' U & SubChoice_isJoinSubCompleteDioid d D S d' U. HB.instance Definition _ := SubChoice_isSubDioid.Build d D S d' U semiring_closed_subproof. HB.instance Definition _ := @@ -599,24 +599,24 @@ HB.instance Definition _ := HB.end. HB.factory Record SubChoice_isJoinSubComCompleteDioid d - (D : comCompleteDioidType d) S (d' : Order.disp_t) U of SubChoice D S U := { + (D : comCompleteDioidType d) S (d' : Order.disp_t) U & SubChoice D S U := { semiring_closed_subproof : semiring_closed S; opredSJ_subproof : set_join_closed S; }. HB.builders Context d D S d' U - of SubChoice_isJoinSubComCompleteDioid d D S d' U. + & SubChoice_isJoinSubComCompleteDioid d D S d' U. HB.instance Definition _ := SubChoice_isJoinSubCompleteDioid.Build d D S d' U semiring_closed_subproof opredSJ_subproof. -HB.instance Definition _ := GRing.SubSemiRing_isSubComSemiRing.Build D S U. +HB.instance Definition _ := GRing.SubNzSemiRing_isSubComNzSemiRing.Build D S U. HB.end. HB.factory Record SubDioid_SubCompleteLattice_isSubCompleteDioid d (D : completeDioidType d) S d' U - of @SubDioid d D S d' U & @SubCompleteLattice d D S d' U := {}. + & @SubDioid d D S d' U & @SubCompleteLattice d D S d' U := {}. HB.builders Context d D S d' U - of SubDioid_SubCompleteLattice_isSubCompleteDioid d D S d' U. + & SubDioid_SubCompleteLattice_isSubCompleteDioid d D S d' U. Lemma set_mulDl (a : U) (B : set U) : a * set_join B = set_join [set a * x | x in B]. Proof. @@ -634,13 +634,13 @@ HB.end. HB.factory Record SubDioid_SubPOrder_isSubCompleteDioid d (D : completeDioidType d) S d' U - of @SubDioid d D S d' U & @Order.SubPOrder d D S d' U := { + & @SubDioid d D S d' U & @Order.SubPOrder d D S d' U := { opredSM_subproof : set_meet_closed S; opredSJ_subproof : set_join_closed S; }. HB.builders Context d D S d' U - of SubDioid_SubPOrder_isSubCompleteDioid d D S d' U. + & SubDioid_SubPOrder_isSubCompleteDioid d D S d' U. HB.instance Definition _ := SubPOrder_isSubCompleteLattice.Build d D S d' U opredSM_subproof opredSJ_subproof. HB.instance Definition _ := @@ -648,13 +648,13 @@ HB.instance Definition _ := HB.end. HB.factory Record SubChoice_isSubCompleteDioid d (D : completeDioidType d) S - (d' : Order.disp_t) U of SubChoice D S U := { + (d' : Order.disp_t) U & SubChoice D S U := { semiring_closed_subproof : semiring_closed S; opredSM_subproof : set_meet_closed S; opredSJ_subproof : set_join_closed S; }. -HB.builders Context d D S d' U of SubChoice_isSubCompleteDioid d D S d' U. +HB.builders Context d D S d' U & SubChoice_isSubCompleteDioid d D S d' U. HB.instance Definition _ := SubChoice_isSubDioid.Build d D S d' U semiring_closed_subproof. HB.instance Definition _ := @@ -663,17 +663,17 @@ HB.instance Definition _ := HB.end. HB.factory Record SubChoice_isSubComCompleteDioid d - (D : comCompleteDioidType d) S (d' : Order.disp_t) U of SubChoice D S U := { + (D : comCompleteDioidType d) S (d' : Order.disp_t) U & SubChoice D S U := { semiring_closed_subproof : semiring_closed S; opredSM_subproof : set_meet_closed S; opredSJ_subproof : set_join_closed S; }. HB.builders Context d D S d' U - of SubChoice_isSubComCompleteDioid d D S d' U. + & SubChoice_isSubComCompleteDioid d D S d' U. HB.instance Definition _ := SubChoice_isSubCompleteDioid.Build d D S d' U semiring_closed_subproof opredSM_subproof opredSJ_subproof. -HB.instance Definition _ := GRing.SubSemiRing_isSubComSemiRing.Build D S U. +HB.instance Definition _ := GRing.SubNzSemiRing_isSubComNzSemiRing.Build D S U. HB.end. Notation "[ 'SubDioid_JoinSubCompleteLattice_isJoinSubCompleteDioid' 'of' U 'by' <: ]" := diff --git a/complete_lattice.v b/complete_lattice.v index da79d18..f8dc808 100644 --- a/complete_lattice.v +++ b/complete_lattice.v @@ -65,7 +65,7 @@ Definition set_f_is_glb d (T : porderType d) (set_f : set T -> T) := Definition set_f_is_lub d (T : porderType d) (set_f : set T -> T) := forall S, ubound S (set_f S) /\ forall x, ubound S x -> set_f S <= x. -HB.mixin Record isCompleteLattice d T of Order.POrder d T := { +HB.mixin Record isCompleteLattice d T & Order.POrder d T := { set_meet : set T -> T; set_meet_is_glb : set_f_is_glb set_meet; set_join : set T -> T; @@ -76,14 +76,14 @@ HB.mixin Record isCompleteLattice d T of Order.POrder d T := { HB.structure Definition CompleteLattice d := { T of Order.TBLattice d T & isCompleteLattice d T }. -HB.factory Record POrder_isCompleteLattice d T of Order.POrder d T := { +HB.factory Record POrder_isCompleteLattice d T & Order.POrder d T := { set_meet : set T -> T; set_meet_is_glb : set_f_is_glb set_meet; set_join : set T -> T; set_join_is_lub : set_f_is_lub set_join; }. -HB.builders Context d T of POrder_isCompleteLattice d T. +HB.builders Context d T & POrder_isCompleteLattice d T. Lemma set_join_ub S : ubound S (set_join S). Proof. exact: (set_join_is_lub S).1. Qed. @@ -231,12 +231,12 @@ HB.instance Definition _ := isCompleteLattice.Build d T HB.end. -HB.factory Record POrder_isMeetCompleteLattice d T of Order.POrder d T := { +HB.factory Record POrder_isMeetCompleteLattice d T & Order.POrder d T := { set_meet : set T -> T; set_meet_is_glb : set_f_is_glb set_meet; }. -HB.builders Context d T of POrder_isMeetCompleteLattice d T. +HB.builders Context d T & POrder_isMeetCompleteLattice d T. Definition set_join S := set_meet (ubound S). Lemma set_join_is_lub : set_f_is_lub set_join. Proof. @@ -247,12 +247,12 @@ HB.instance Definition _ := POrder_isCompleteLattice.Build d T set_meet_is_glb set_join_is_lub. HB.end. -HB.factory Record POrder_isJoinCompleteLattice d T of Order.POrder d T := { +HB.factory Record POrder_isJoinCompleteLattice d T & Order.POrder d T := { set_join : set T -> T; set_join_is_lub : set_f_is_lub set_join; }. -HB.builders Context d T of POrder_isJoinCompleteLattice d T. +HB.builders Context d T & POrder_isJoinCompleteLattice d T. Definition set_meet S := set_join (lbound S). Lemma set_meet_is_glb : set_f_is_glb set_meet. Proof. @@ -454,11 +454,11 @@ HB.structure Definition CompleteLatticeMorphism HB.factory Record isMeetCompleteLatticeMorphism d (L : completeLatticeType d) d' (L' : completeLatticeType d') (apply : L -> L') - of @Order.OrderMorphism d L d' L' apply := { + & @Order.OrderMorphism d L d' L' apply := { omorphSM : set_meet_morphism apply; }. -HB.builders Context d L d' L' f of isMeetCompleteLatticeMorphism d L d' L' f. +HB.builders Context d L d' L' f & isMeetCompleteLatticeMorphism d L d' L' f. Lemma omorphI : Order.meet_morphism f. Proof. by move=> x y; rewrite -!set_meet2 omorphSM !image_setU !image_set1. Qed. HB.instance Definition _ := Order.isMeetLatticeMorphism.Build d L d' L' f @@ -471,11 +471,11 @@ HB.end. HB.factory Record isJoinCompleteLatticeMorphism d (L : completeLatticeType d) d' (L' : completeLatticeType d') (apply : L -> L') - of @Order.OrderMorphism d L d' L' apply := { + & @Order.OrderMorphism d L d' L' apply := { omorphSJ : set_join_morphism apply; }. -HB.builders Context d L d' L' f of isJoinCompleteLatticeMorphism d L d' L' f. +HB.builders Context d L d' L' f & isJoinCompleteLatticeMorphism d L d' L' f. Lemma omorphU : Order.join_morphism f. Proof. by move=> x y; rewrite -!set_join2 omorphSJ !image_setU !image_set1. Qed. HB.instance Definition _ := Order.isJoinLatticeMorphism.Build d L d' L' f @@ -488,12 +488,12 @@ HB.end. HB.factory Record isCompleteLatticeMorphism d (L : completeLatticeType d) d' (L' : completeLatticeType d') (apply : L -> L') - of @Order.OrderMorphism d L d' L' apply := { + & @Order.OrderMorphism d L d' L' apply := { omorphSM : set_meet_morphism apply; omorphSJ : set_join_morphism apply; }. -HB.builders Context d L d' L' f of isCompleteLatticeMorphism d L d' L' f. +HB.builders Context d L d' L' f & isCompleteLatticeMorphism d L d' L' f. HB.instance Definition _ := isMeetCompleteLatticeMorphism.Build d L d' L' f omorphSM. HB.instance Definition _ := isJoinCompleteLatticeMorphism.Build d L d' L' f @@ -611,7 +611,7 @@ HB.factory Record isMeetCompleteLatticeClosed d (T : completeLatticeType d) opredSM : set_meet_closed S; }. -HB.builders Context d T S of isMeetCompleteLatticeClosed d T S. +HB.builders Context d T S & isMeetCompleteLatticeClosed d T S. Lemma opred1 : \top \in S. Proof. by rewrite -set_meet0 opredSM. Qed. HB.instance Definition _ := Order.isTLatticeClosed.Build d T S opred1. Lemma opredI : meet_closed S. @@ -625,7 +625,7 @@ HB.factory Record isJoinCompleteLatticeClosed d (T : completeLatticeType d) opredSJ : set_join_closed S; }. -HB.builders Context d T S of isJoinCompleteLatticeClosed d T S. +HB.builders Context d T S & isJoinCompleteLatticeClosed d T S. Lemma opred0 : \bot \in S. Proof. by rewrite -set_join0 opredSJ. Qed. HB.instance Definition _ := Order.isBLatticeClosed.Build d T S opred0. Lemma opredU : join_closed S. @@ -640,7 +640,7 @@ HB.factory Record isCompleteLatticeClosed d (T : completeLatticeType d) opredSJ : set_join_closed S; }. -HB.builders Context d T S of isCompleteLatticeClosed d T S. +HB.builders Context d T S & isCompleteLatticeClosed d T S. HB.instance Definition _ := isMeetCompleteLatticeClosed.Build d T S opredSM. HB.instance Definition _ := isJoinCompleteLatticeClosed.Build d T S opredSJ. HB.end. @@ -649,12 +649,12 @@ Arguments opredSM {d T} _. Arguments opredSJ {d T} _. HB.mixin Record isMeetSubCompleteLattice d (T : completeLatticeType d) - (S : pred T) d' U of SubType T S U & CompleteLattice d' U := { + (S : pred T) d' U & SubType T S U & CompleteLattice d' U := { valSM_subproof : set_meet_morphism (val : U -> T); }. HB.mixin Record isJoinSubCompleteLattice d (T : completeLatticeType d) - (S : pred T) d' U of SubType T S U & CompleteLattice d' U := { + (S : pred T) d' U & SubType T S U & CompleteLattice d' U := { valSJ_subproof : set_join_morphism (val : U -> T); }. @@ -691,11 +691,11 @@ HB.instance Definition _ (d : Order.disp_t) (T : completeLatticeType d) isJoinCompleteLatticeMorphism.Build d' U d T val valSJ_subproof. HB.factory Record SubPOrder_isMeetSubCompleteLattice d - (T : completeLatticeType d) S d' U of @Order.SubPOrder d T S d' U := { + (T : completeLatticeType d) S d' U & @Order.SubPOrder d T S d' U := { opredSM_subproof : set_meet_closed S; }. -HB.builders Context d T S d' U of SubPOrder_isMeetSubCompleteLattice d T S d' U. +HB.builders Context d T S d' U & SubPOrder_isMeetSubCompleteLattice d T S d' U. HB.instance Definition _ := isMeetCompleteLatticeClosed.Build d T S opredSM_subproof. @@ -735,22 +735,22 @@ HB.instance Definition _ := isMeetSubCompleteLattice.Build d T S d' U valSM. HB.end. HB.factory Record SubChoice_isMeetSubCompleteLattice d - (T : completeLatticeType d) S (d' : Order.disp_t) U of SubChoice T S U := { + (T : completeLatticeType d) S (d' : Order.disp_t) U & SubChoice T S U := { opredSM_subproof : set_meet_closed S; }. -HB.builders Context d T S d' U of SubChoice_isMeetSubCompleteLattice d T S d' U. +HB.builders Context d T S d' U & SubChoice_isMeetSubCompleteLattice d T S d' U. HB.instance Definition _ := Order.SubChoice_isSubPOrder.Build d T S d' U. HB.instance Definition _ := SubPOrder_isMeetSubCompleteLattice.Build d T S d' U opredSM_subproof. HB.end. HB.factory Record SubPOrder_isJoinSubCompleteLattice d - (T : completeLatticeType d) S d' U of @Order.SubPOrder d T S d' U := { + (T : completeLatticeType d) S d' U & @Order.SubPOrder d T S d' U := { opredSJ_subproof : set_join_closed S; }. -HB.builders Context d T S d' U of SubPOrder_isJoinSubCompleteLattice d T S d' U. +HB.builders Context d T S d' U & SubPOrder_isJoinSubCompleteLattice d T S d' U. HB.instance Definition _ := isJoinCompleteLatticeClosed.Build d T S opredSJ_subproof. @@ -788,23 +788,23 @@ HB.instance Definition _ := isJoinSubCompleteLattice.Build d T S d' U valSJ. HB.end. HB.factory Record SubChoice_isJoinSubCompleteLattice d - (T : completeLatticeType d) S (d' : Order.disp_t) U of SubChoice T S U := { + (T : completeLatticeType d) S (d' : Order.disp_t) U & SubChoice T S U := { opredSJ_subproof : set_join_closed S; }. -HB.builders Context d T S d' U of SubChoice_isJoinSubCompleteLattice d T S d' U. +HB.builders Context d T S d' U & SubChoice_isJoinSubCompleteLattice d T S d' U. HB.instance Definition _ := Order.SubChoice_isSubPOrder.Build d T S d' U. HB.instance Definition _ := SubPOrder_isJoinSubCompleteLattice.Build d T S d' U opredSJ_subproof. HB.end. HB.factory Record SubPOrder_isSubCompleteLattice d - (T : completeLatticeType d) S d' U of @Order.SubPOrder d T S d' U := { + (T : completeLatticeType d) S d' U & @Order.SubPOrder d T S d' U := { opredSM_subproof : set_meet_closed S; opredSJ_subproof : set_join_closed S; }. -HB.builders Context d T S d' U of SubPOrder_isSubCompleteLattice d T S d' U. +HB.builders Context d T S d' U & SubPOrder_isSubCompleteLattice d T S d' U. HB.instance Definition _ := isCompleteLatticeClosed.Build d T S opredSM_subproof opredSJ_subproof. @@ -866,12 +866,12 @@ HB.instance Definition _ := isJoinSubCompleteLattice.Build d T S d' U valSJ. HB.end. HB.factory Record SubChoice_isSubCompleteLattice d - (T : completeLatticeType d) S (d' : Order.disp_t) U of SubChoice T S U := { + (T : completeLatticeType d) S (d' : Order.disp_t) U & SubChoice T S U := { opredSM_subproof : set_meet_closed S; opredSJ_subproof : set_join_closed S; }. -HB.builders Context d T S d' U of SubChoice_isSubCompleteLattice d T S d' U. +HB.builders Context d T S d' U & SubChoice_isSubCompleteLattice d T S d' U. HB.instance Definition _ := Order.SubChoice_isSubPOrder.Build d T S d' U. HB.instance Definition _ := SubPOrder_isSubCompleteLattice.Build d T S d' U opredSM_subproof opredSJ_subproof. diff --git a/dioid.v b/dioid.v index b129e01..cfa3285 100644 --- a/dioid.v +++ b/dioid.v @@ -72,14 +72,14 @@ Local Open Scope dioid_scope. Import Order.Theory GRing.Theory. HB.mixin Record SemiRing_POrder_isDioid d D - of GRing.SemiRing D & Order.POrder d D := { + & GRing.NzSemiRing D & Order.POrder d D := { adddd : @idempotent_op D +%R; le_def : forall (a b : D), (a <= b) = (a + b == b); }. #[short(type="dioidType")] HB.structure Definition Dioid d := - { D of SemiRing_POrder_isDioid d D & GRing.SemiRing D & Order.POrder d D }. + { D of SemiRing_POrder_isDioid d D & GRing.NzSemiRing D & Order.POrder d D }. #[short(type="dioidLatticeType")] HB.structure Definition DioidLattice d := @@ -97,7 +97,7 @@ HB.structure Definition DioidTLattice d := HB.structure Definition DioidTBLattice d := { D of Dioid d D & Order.TBLattice d D }. -HB.factory Record POrder_isDioid d D of Order.POrder d D := { +HB.factory Record POrder_isDioid d D & Order.POrder d D := { zero : D; add : D -> D -> D; one : D; @@ -117,17 +117,17 @@ HB.factory Record POrder_isDioid d D of Order.POrder d D := { le_def : forall (a b : D), (a <= b) = (add a b == b); }. -HB.builders Context d D of POrder_isDioid d D. -HB.instance Definition _ := GRing.isSemiRing.Build D addA addC add0d +HB.builders Context d D & POrder_isDioid d D. +HB.instance Definition _ := GRing.isNzSemiRing.Build D addA addC add0d mulA mul1d muld1 mulDl mulDr mul0d muld0 oner_neq0. HB.instance Definition _ := SemiRing_POrder_isDioid.Build d D adddd le_def. HB.end. -HB.factory Record SemiRing_isDioid (d : Order.disp_t) D of GRing.SemiRing D := { +HB.factory Record SemiRing_isDioid (d : Order.disp_t) D & GRing.NzSemiRing D := { adddd : @idempotent_op D +%R; }. -HB.builders Context d D of SemiRing_isDioid d D. +HB.builders Context d D & SemiRing_isDioid d D. Definition le_dioid (a b : D) := a + b == b. @@ -160,7 +160,7 @@ HB.instance Definition _ := SemiRing_POrder_isDioid.Build d D adddd le_def. HB.end. -HB.factory Record Choice_isDioid (d : Order.disp_t) D of Choice D := { +HB.factory Record Choice_isDioid (d : Order.disp_t) D & Choice D := { zero : D; add : D -> D -> D; one : D; @@ -179,8 +179,8 @@ HB.factory Record Choice_isDioid (d : Order.disp_t) D of Choice D := { oner_neq0 : one != zero; }. -HB.builders Context d D of Choice_isDioid d D. -HB.instance Definition _ := GRing.isSemiRing.Build D addA addC add0d +HB.builders Context d D & Choice_isDioid d D. +HB.instance Definition _ := GRing.isNzSemiRing.Build D addA addC add0d mulA mul1d muld1 mulDl mulDr mul0d muld0 oner_neq0. HB.instance Definition _ := SemiRing_isDioid.Build d D adddd. HB.end. @@ -231,9 +231,9 @@ Proof. move=> ac bd; exact/(le_trans (led_mul2r _ ac))/led_mul2l. Qed. End DioidTheory. #[short(type="comDioidType")] -HB.structure Definition ComDioid d := { D of GRing.ComSemiRing D & Dioid d D }. +HB.structure Definition ComDioid d := { D of GRing.ComNzSemiRing D & Dioid d D }. -HB.factory Record POrder_isComDioid d D of Order.POrder d D := { +HB.factory Record POrder_isComDioid d D & Order.POrder d D := { zero : D; add : D -> D -> D; one : D; @@ -251,7 +251,7 @@ HB.factory Record POrder_isComDioid d D of Order.POrder d D := { le_def : forall (a b : D), (a <= b) = (add a b == b); }. -HB.builders Context d D of POrder_isComDioid d D. +HB.builders Context d D & POrder_isComDioid d D. Lemma muld1 : right_id one mul. Proof. by move=> x; rewrite mulC mul1d. Qed. @@ -269,7 +269,7 @@ HB.instance Definition _ := GRing.SemiRing_hasCommutativeMul.Build D mulC. HB.end. -HB.factory Record Choice_isComDioid (d : Order.disp_t) D of Choice D := { +HB.factory Record Choice_isComDioid (d : Order.disp_t) D & Choice D := { zero : D; add : D -> D -> D; one : D; @@ -286,7 +286,7 @@ HB.factory Record Choice_isComDioid (d : Order.disp_t) D of Choice D := { oner_neq0 : one != zero; }. -HB.builders Context d D of Choice_isComDioid d D. +HB.builders Context d D & Choice_isComDioid d D. Lemma muld1 : right_id one mul. Proof. by move=> x; rewrite mulC mul1d. Qed. @@ -306,7 +306,7 @@ HB.end. #[short(type="subDioidType")] HB.structure Definition SubDioid d (D : dioidType d) (S : pred D) d' := - { U of GRing.SubSemiRing D S U & @Order.SubPOrder d D S d' U & Dioid d' U }. + { U of GRing.SubNzSemiRing D S U & @Order.SubPOrder d D S d' U & Dioid d' U }. #[short(type="subDioidLatticeType")] HB.structure Definition SubDioidLattice d (D : dioidLatticeType d) S d' := @@ -325,9 +325,9 @@ HB.structure Definition SubDioidTBLattice d (D : dioidLatticeType d) S d' := { U of @SubDioid d D S d' U & @Order.TBLattice d' U }. HB.factory Record SubSemiRing_SubPOrder_isSubDioid d (D : dioidType d) S d' U - of GRing.SubSemiRing D S U & @Order.SubPOrder d D S d' U := {}. + & GRing.SubNzSemiRing D S U & @Order.SubPOrder d D S d' U := {}. -HB.builders Context d D S d' U of SubSemiRing_SubPOrder_isSubDioid d D S d' U. +HB.builders Context d D S d' U & SubSemiRing_SubPOrder_isSubDioid d D S d' U. Lemma adddd : @idempotent_op U +%R. Proof. by move=> x; apply: val_inj; rewrite raddfD adddd. Qed. Lemma le_def (a b : U) : (a <= b) = (a + b == b). @@ -336,13 +336,13 @@ HB.instance Definition _ := SemiRing_POrder_isDioid.Build d' U adddd le_def. HB.end. HB.factory Record SubChoice_isSubDioid d (D : dioidType d) S (d' : Order.disp_t) - U of SubChoice D S U := { + U & SubChoice D S U := { semiring_closed_subproof : semiring_closed S; }. HB.builders Context d (D : dioidType d) S d' U - of SubChoice_isSubDioid d D S d' U. -HB.instance Definition _ := GRing.SubChoice_isSubSemiRing.Build D S U + & SubChoice_isSubDioid d D S d' U. +HB.instance Definition _ := GRing.SubChoice_isSubNzSemiRing.Build D S U semiring_closed_subproof. HB.instance Definition _ := Order.SubChoice_isSubPOrder.Build d D S d' U. HB.instance Definition _ := SubSemiRing_SubPOrder_isSubDioid.Build d D S d' U. @@ -353,22 +353,22 @@ HB.structure Definition SubComDioid d (D : comDioidType d) (S : pred D) d' := {U of @SubDioid d D S d' U & ComDioid d' U}. HB.factory Record SubComSemiRing_SubPOrder_isSubComDioid d (D : comDioidType d) - S (d' : Order.disp_t) U of GRing.SubComSemiRing D S U & @Order.SubPOrder d D S + S (d' : Order.disp_t) U & GRing.SubComNzSemiRing D S U & @Order.SubPOrder d D S d' U := {}. HB.builders Context d D S d' U - of SubComSemiRing_SubPOrder_isSubComDioid d D S d' U. + & SubComSemiRing_SubPOrder_isSubComDioid d D S d' U. HB.instance Definition _ := SubSemiRing_SubPOrder_isSubDioid.Build d D S d' U. HB.end. HB.factory Record SubChoice_isSubComDioid d (D : comDioidType d) S - (d' : Order.disp_t) U of SubChoice D S U := { + (d' : Order.disp_t) U & SubChoice D S U := { semiring_closed_subproof : semiring_closed S }. HB.builders Context d (D : comDioidType d) S d' U - of SubChoice_isSubComDioid d D S d' U. -HB.instance Definition _ := GRing.SubChoice_isSubComSemiRing.Build D S U + & SubChoice_isSubComDioid d D S d' U. +HB.instance Definition _ := GRing.SubChoice_isSubComNzSemiRing.Build D S U semiring_closed_subproof. HB.instance Definition _ := Order.SubChoice_isSubPOrder.Build d D S d' U. HB.instance Definition _ := SubSemiRing_SubPOrder_isSubDioid.Build d D S d' U. From 761d4407d380879fde0e809955634534605d2b11 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jul 2026 04:36:41 +0000 Subject: [PATCH 2/3] Adapt to the mathcomp 2.6 ssreflect `rewrite (_ : A = B)` goal order MathComp 2.5.0's mathcomp/boot/ssreflect.v carried `Global Set SsrOldRewriteGoalsOrder.`; mathcomp dev (2.6+, PR #1545) removed it, so the Rocq option reverts to its default and the side condition produced by `rewrite (_ : A = B)` is now left as the FIRST goal instead of the last. That is what the `; last first.` idiom in these proofs was compensating for. This is a mathcomp change, not a Rocq one: the flag itself is permanent and undeprecated. Swap the idiom at each of the five affected sites -- drop `; last first.` where it was present and add it where it was not -- leaving the proof scripts themselves untouched. With only five sites this is cheaper than adding a per-file `Set SsrOldRewriteGoalsOrder.`, and it is step (2) of the ladder mathcomp's own 2.6.0 CHANGELOG describes, so it does not have to be undone later. The cost is that the file now requires mathcomp >= 2.6, which the opam bounds state. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b --- .github/workflows/coq-action.yml | 2 +- README.md | 9 ++++----- complete_dioid.v | 14 +++++++------- coq-mathcomp-dioid.opam | 7 +++---- 4 files changed, 15 insertions(+), 17 deletions(-) diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml index b3541b5..eacc522 100644 --- a/.github/workflows/coq-action.yml +++ b/.github/workflows/coq-action.yml @@ -15,7 +15,7 @@ jobs: strategy: matrix: image: - - mathcomp/mathcomp:2.3.0-coq-8.20 + - mathcomp/mathcomp:2.6.0-rocq-prover-9.2 fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/README.md b/README.md index 48d17ac..b332975 100644 --- a/README.md +++ b/README.md @@ -17,16 +17,15 @@ Installation Dependencies ------------ -* Coq (>= 8.20) -* The Mathcomp library (>= 2.3.0) -* Hierarchy Builder (= 1.8.0) -* Mathcomp classical (= 1.8.0) +* Rocq (>= 9.2) +* The Mathcomp library (>= 2.6.0) +* Mathcomp classical (>= 1.17.0) Dependencies can be installed with OPAM (>= 2.0) by typing: ``` % opam repo add coq-released https://coq.inria.fr/opam/released -% opam install coq.8.20.1 coq-mathcomp-algebra.2.3.0 coq-mathcomp-classical.1.8.0 +% opam install coq-core.9.0.1 rocq-mathcomp-algebra.2.6.0 rocq-mathcomp-classical ``` Compilation diff --git a/complete_dioid.v b/complete_dioid.v index 1e6b38d..6912d49 100644 --- a/complete_dioid.v +++ b/complete_dioid.v @@ -253,7 +253,7 @@ suff Hyp : forall i, (a + 1) ^ i = set_add [set a ^ j | j in [set x | 'I_i.+1 x] elim=> [ | i IHi]; [by rewrite set_add1 !exp0|]. rewrite expS mulrDl mul1r IHi set_mulDl. set B' := [set a ^ j | j in [set j | (1 <= j <= i)%N]]. -rewrite [X in set_join X](_ : _ = a ^ i.+1 |` B'); last first. +rewrite [X in set_join X](_ : _ = a ^ i.+1 |` B'). { rewrite predeqP => x; split. - move=> -[y [[j Hj] _ <-] <-]. rewrite expS /= -!expS. @@ -263,7 +263,7 @@ rewrite [X in set_join X](_ : _ = a ^ i.+1 |` B'); last first. move=> -[[//|j] /andP [Hj Hji] <-]; rewrite expS; exists (a ^ j) => //. by move: Hji => /ltnW; rewrite -ltnS => Hji; exists (Ordinal Hji). } rewrite -[set_join]/set_add set_addDl. -rewrite (_ : image _ _ = (1%R |` B')); last first. +rewrite (_ : image _ _ = (1%R |` B')). { rewrite predeqP => x; split. { move=> -[[[|j] Hj] _ <-]; [by left; rewrite exp0|]. by right; exists (Ordinal Hj). } @@ -286,7 +286,7 @@ Lemma kleene_sqr a : a^* * a^* = a^*. Proof. rewrite {1}/op_kleene set_mulDr. set B' := (a ^* |` (range (fun i => a ^ i.+1 * a ^*))). -rewrite (_ : image _ _ = B'); last first. +rewrite (_ : image _ _ = B'). { rewrite predeqP => x; split. - by move=> -[_ [[|i] _ <-] <-]; [left; rewrite exp0 mul1r|right; exists i]. - move=> [-> | [i _ <-]]; [by exists 1%R; [exists O|rewrite mul1r]|]. @@ -310,7 +310,7 @@ Qed. Lemma kleene_kleene a : (a ^*) ^* = a ^*. Proof. rewrite kleeneSr /op_plus. -rewrite (_ : image _ _ = a ^* |` set0). +rewrite (_ : image _ _ = a ^* |` set0); last first. by rewrite setU0 set_join1 kleeneSr addrA adddd. rewrite predeqP => x; split. - move=> [i _ <-]; left; exact: kleene_exp. @@ -324,7 +324,7 @@ Theorem kleene_star_least a b : forall x, (x = a * x + b) -> a ^* * b <= x. Proof. move=> x Hx. rewrite set_mulDr. -rewrite [X in set_join X](_ : _ = [set (a ^ i) * b | i in setT]); last first. +rewrite [X in set_join X](_ : _ = [set (a ^ i) * b | i in setT]). rewrite predeqP => y; split. - by move=> [_ [i _ <-] <-]; exists i. - by move=> [i _ <-]; exists (a ^ i); [exists i|]. @@ -608,7 +608,7 @@ HB.builders Context d D S d' U & SubChoice_isJoinSubComCompleteDioid d D S d' U. HB.instance Definition _ := SubChoice_isJoinSubCompleteDioid.Build d D S d' U semiring_closed_subproof opredSJ_subproof. -HB.instance Definition _ := GRing.SubNzSemiRing_isSubComNzSemiRing.Build D S U. +HB.instance Definition _ := GRing.SubSemiRing_isSubComSemiRing.Build D S U. HB.end. HB.factory Record SubDioid_SubCompleteLattice_isSubCompleteDioid @@ -673,7 +673,7 @@ HB.builders Context d D S d' U & SubChoice_isSubComCompleteDioid d D S d' U. HB.instance Definition _ := SubChoice_isSubCompleteDioid.Build d D S d' U semiring_closed_subproof opredSM_subproof opredSJ_subproof. -HB.instance Definition _ := GRing.SubNzSemiRing_isSubComNzSemiRing.Build D S U. +HB.instance Definition _ := GRing.SubSemiRing_isSubComSemiRing.Build D S U. HB.end. Notation "[ 'SubDioid_JoinSubCompleteLattice_isJoinSubCompleteDioid' 'of' U 'by' <: ]" := diff --git a/coq-mathcomp-dioid.opam b/coq-mathcomp-dioid.opam index 499a15d..9d2d0ce 100644 --- a/coq-mathcomp-dioid.opam +++ b/coq-mathcomp-dioid.opam @@ -15,10 +15,9 @@ build: [ install: [make "install"] depends: [ - "coq" { >= "8.20" & < "8.21~" } - "coq-mathcomp-algebra" { >= "2.3" & < "2.4~" } - "coq-mathcomp-classical" { >= "1.8" & < "1.9~" } - "coq-hierarchy-builder" { >= "1.8.0" } + "coq-core" { >= "9.2" } + "rocq-mathcomp-algebra" { >= "2.6" } + "rocq-mathcomp-classical" { >= "1.17" } ] synopsis: "Dioid" description: """ From 194623107a8dde3ff167ee8c73996f01eb0117d5 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 21 Aug 2026 11:48:31 +0200 Subject: [PATCH 3/3] Compile without coq shims --- .github/workflows/coq-action.yml | 16 +++++----- .gitignore | 6 ++-- Makefile | 28 +++++++++--------- coq-mathcomp-dioid.opam | 41 ++----------------------- rocq-mathcomp-dioid.opam | 51 ++++++++++++++++++++++++++++++++ 5 files changed, 79 insertions(+), 63 deletions(-) create mode 100644 rocq-mathcomp-dioid.opam diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml index eacc522..e18f421 100644 --- a/.github/workflows/coq-action.yml +++ b/.github/workflows/coq-action.yml @@ -21,7 +21,7 @@ jobs: - uses: actions/checkout@v2 - uses: coq-community/docker-coq-action@v1 with: - opam_file: 'coq-mathcomp-dioid.opam' + opam_file: 'rocq-mathcomp-dioid.opam' custom_image: ${{ matrix.image }} custom_script: | startGroup Print opam config @@ -31,18 +31,18 @@ jobs: startGroup Update opam cache opam update -y endGroup - startGroup Build coq-mathcomp-dioid dependencies - opam pin add -n -y -k path coq-mathcomp-dioid . - opam remove coq-mathcomp-character coq-mathcomp-field coq-mathcomp-solvable # coq-mathcomp-algebra is enough - opam install -y -j ${NJOBS} coq-mathcomp-dioid --deps-only + startGroup Build rocq-mathcomp-dioid dependencies + opam pin add -n -y -k path rocq-mathcomp-dioid . + opam remove -y rocq-mathcomp-character rocq-mathcomp-field rocq-mathcomp-solvable # rocq-mathcomp-algebra is enough + opam install -y -j ${NJOBS} rocq-mathcomp-dioid --deps-only opam list endGroup - startGroup Build coq-mathcomp-dioid - opam install -y -v -j ${NJOBS} coq-mathcomp-dioid + startGroup Build rocq-mathcomp-dioid + opam install -y -v -j ${NJOBS} rocq-mathcomp-dioid opam list endGroup startGroup Uninstallation test - opam remove -y coq-mathcomp-dioid + opam remove -y rocq-mathcomp-dioid endGroup # See also: diff --git a/.gitignore b/.gitignore index d56168e..1dc190c 100644 --- a/.gitignore +++ b/.gitignore @@ -1,7 +1,7 @@ *~ -Makefile.coq -Makefile.coq.conf -.Makefile.coq.d +Makefile.rocq +Makefile.rocq.conf +.Makefile.rocq.d .*.aux *.glob *.vo diff --git a/Makefile b/Makefile index ce9102b..04618b7 100644 --- a/Makefile +++ b/Makefile @@ -1,33 +1,33 @@ # Makefile for dioid COQ_PROJ := _CoqProject -COQ_MAKEFILE := Makefile.coq -COQ_MAKE := +$(MAKE) -f $(COQ_MAKEFILE) +ROCQ_MAKEFILE := Makefile.rocq +ROCQ_MAKE := +$(MAKE) -f $(ROCQ_MAKEFILE) -ifneq "$(COQBIN)" "" - COQBIN := $(COQBIN)/ +ifneq "$(ROCQBIN)" "" + ROCQBIN := $(ROCQBIN)/ else - COQBIN := $(dir $(shell which coqc)) + ROCQBIN := $(dir $(shell which coqc)) endif -export COQBIN +export ROCQBIN -all install html gallinahtml: $(COQ_MAKEFILE) Makefile - $(COQ_MAKE) $@ +all install html gallinahtml: $(ROCQ_MAKEFILE) Makefile + $(ROCQ_MAKE) $@ %.vo: %.v - $(COQ_MAKE) $@ + $(ROCQ_MAKE) $@ -$(COQ_MAKEFILE): $(COQ_PROJ) - $(COQBIN)coq_makefile -f $< -o $@ +$(ROCQ_MAKEFILE): $(COQ_PROJ) + $(ROCQBIN)rocq makefile -f $< -o $@ clean: - -$(COQ_MAKE) clean + -$(ROCQ_MAKE) clean distclean: clean - $(RM) $(COQ_MAKEFILE) $(COQ_MAKEFILE).conf + $(RM) $(ROCQ_MAKEFILE) $(ROCQ_MAKEFILE).conf $(RM) *~ .*.aux .lia.cache --include $(COQ_MAKEFILE).conf +-include $(ROCQ_MAKEFILE).conf .PHONY: all install html gallinahtml clean distclean diff --git a/coq-mathcomp-dioid.opam b/coq-mathcomp-dioid.opam index 9d2d0ce..be8990a 100644 --- a/coq-mathcomp-dioid.opam +++ b/coq-mathcomp-dioid.opam @@ -9,43 +9,8 @@ dev-repo: "git+https://github.com/math-comp/dioid.git" bug-reports: "https://github.com/math-comp/dioid/issues" license: "CECILL-B" -build: [ - [make "-j%{jobs}%"] -] -install: [make "install"] - depends: [ - "coq-core" { >= "9.2" } - "rocq-mathcomp-algebra" { >= "2.6" } - "rocq-mathcomp-classical" { >= "1.17" } -] -synopsis: "Dioid" -description: """ -Definitions of the algebraic structure of dioid following the style of -ssralg in the Mathcomp library. - -The main algebraic structures defined are: -* semirings: rings without opposite for the additive law -* dioids: idempotent semirings (i.e., forall x, x + x = x) -* complete dioids: dioids whose canonical order (x <= y wen x + y = y) - yields a complete lattice -* commutative variants (multiplicative law is commutative) - -More details can be found in comments at the beginning of each file. -""" - -tags: [ - "keyword:dioid" - "keyword:semiring" - "keyword:complete dioid" - "category:Miscellaneous/Coq Extensions" - "logpath:mathcomp.dioid" -] -authors: [ - "Lucien Rakotomalala " - "Pierre Roux " + "coq-core" + "rocq-mathcomp-diod" ] -#url { -# src: "https://github.com/validsdp/validsdp/releases/download/v0.8.0/validsdp-0.8.0.tar.gz" -# checksum: "sha256=TODO curl -L archive | sha256sum" -#} +synopsis: "Compatibility package for rocq-mathcomp-dioid" diff --git a/rocq-mathcomp-dioid.opam b/rocq-mathcomp-dioid.opam new file mode 100644 index 0000000..caac1e7 --- /dev/null +++ b/rocq-mathcomp-dioid.opam @@ -0,0 +1,51 @@ +opam-version: "2.0" +version: "dev" +maintainer: [ + "Pierre Roux " +] + +homepage: "https://github.com/math-comp/dioid" +dev-repo: "git+https://github.com/math-comp/dioid.git" +bug-reports: "https://github.com/math-comp/dioid/issues" +license: "CECILL-B" + +build: [ + [make "-j%{jobs}%"] +] +install: [make "install"] + +depends: [ + "rocq-core" { >= "9.2" } + "rocq-mathcomp-algebra" { >= "2.6" } + "rocq-mathcomp-classical" { >= "1.17" } +] +synopsis: "Dioid" +description: """ +Definitions of the algebraic structure of dioid following the style of +ssralg in the Mathcomp library. + +The main algebraic structures defined are: +* semirings: rings without opposite for the additive law +* dioids: idempotent semirings (i.e., forall x, x + x = x) +* complete dioids: dioids whose canonical order (x <= y wen x + y = y) + yields a complete lattice +* commutative variants (multiplicative law is commutative) + +More details can be found in comments at the beginning of each file. +""" + +tags: [ + "keyword:dioid" + "keyword:semiring" + "keyword:complete dioid" + "category:Miscellaneous/Coq Extensions" + "logpath:mathcomp.dioid" +] +authors: [ + "Lucien Rakotomalala " + "Pierre Roux " +] +#url { +# src: "https://github.com/validsdp/validsdp/releases/download/v0.8.0/validsdp-0.8.0.tar.gz" +# checksum: "sha256=TODO curl -L archive | sha256sum" +#}