From 0e6e3c982a9cb90e797ff3b6e84d4592e1ec05ab Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 24 Feb 2025 15:32:49 +0100 Subject: [PATCH] Compile with mathcomp 2.3.0 --- .github/workflows/coq-action.yml | 5 +-- README.md | 33 +++----------- complete_dioid.v | 32 +++++++------- complete_lattice.v | 76 ++++++++++++++++---------------- coq-mathcomp-dioid.opam | 8 ++-- dioid.v | 28 ++++++------ 6 files changed, 81 insertions(+), 101 deletions(-) diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml index 33a2d96..b3541b5 100644 --- a/.github/workflows/coq-action.yml +++ b/.github/workflows/coq-action.yml @@ -15,8 +15,7 @@ jobs: strategy: matrix: image: - - mathcomp/mathcomp:1.13.0-coq-8.13 - - mathcomp/mathcomp:1.12.0-coq-8.13 + - mathcomp/mathcomp:2.3.0-coq-8.20 fail-fast: false steps: - uses: actions/checkout@v2 @@ -34,7 +33,7 @@ jobs: endGroup startGroup Build coq-mathcomp-dioid dependencies opam pin add -n -y -k path coq-mathcomp-dioid . - opam remove coq-mathcomp-algebra coq-mathcomp-character coq-mathcomp-field coq-mathcomp-fingroup coq-mathcomp-solvable # coq-mathcomp-ssreflect is enough + 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 opam list endGroup diff --git a/README.md b/README.md index a468451..48d17ac 100644 --- a/README.md +++ b/README.md @@ -12,41 +12,21 @@ The main algebraic structures defined are: More details can be found in comments at the beginning of each .v file. Installation ------------- - -This is currently not available as an OPAM (>= 2.0) package: - -When MathComp Analysis for MathComp 2 will be released, this will be -installable by typing: - -``` -% opam repo add coq-released https://coq.inria.fr/opam/released -% opam install coq-mathcomp-dioid -``` +============ Dependencies ------------ -* Coq (>= 8.16) -* The Mathcomp library (>= 2.0.0) -* Hierarchy Builder (= 1.4.0) -* Mathcomp Analysis (hierarchy-builder branch) +* Coq (>= 8.20) +* The Mathcomp library (>= 2.3.0) +* Hierarchy Builder (= 1.8.0) +* Mathcomp classical (= 1.8.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-mathcomp-algebra.2.0.0 -``` - -Except MathComp Analysis (or only its mathcomp-classical package) that -must currently be installed from source: - -``` -% git clone https://github.com/math-comp/analysis -% git checkout hierarchy-builder -% make -j4 -C classical -% make -C classical install +% opam install coq.8.20.1 coq-mathcomp-algebra.2.3.0 coq-mathcomp-classical.1.8.0 ``` Compilation @@ -56,4 +36,5 @@ Just type ``` % make +% make install ``` diff --git a/complete_dioid.v b/complete_dioid.v index 4c28b1f..f7ad264 100644 --- a/complete_dioid.v +++ b/complete_dioid.v @@ -85,14 +85,14 @@ HB.structure Definition CompleteDioid d := Section CompleteDioidTheory. -Variables (disp : unit) (D : completeDioidType disp). +Variables (disp : Order.disp_t) (D : completeDioidType disp). Implicit Types a b c : D. Implicit Types B : set D. Notation set_add := set_join. -Lemma bottom_zero : 0%O = 0%R :> D. +Lemma bottom_zero : \bot = 0%R :> D. Proof. by apply/le_anti; rewrite le0x le0d. Qed. Lemma set_addDl a B : set_add (a |` B) = a + set_add B. @@ -109,10 +109,10 @@ Proof. by rewrite -[in LHS](set_join1 b) -set_addDl set_joinU !set_join1. Qed. Lemma set_addU A B : set_add (A `|` B) = set_add A + set_add B. Proof. by rewrite set_joinU add_join. Qed. -Lemma add_d1 : @right_zero D D 1%O +%R. +Lemma add_d1 : @right_zero D D \top +%R. Proof. by move=> x; apply/eqP; rewrite -le_def lex1. Qed. -Lemma add_1d : @left_zero D D 1%O +%R. +Lemma add_1d : @left_zero D D \top +%R. Proof. by move=> x; rewrite addrC add_d1. Qed. Lemma set_add0 (F : nat -> D) : set_add [set F i | i in [set x | 'I_0 x]] = 0%R. @@ -353,7 +353,7 @@ apply/idP/idP => H; [exact: set_join_ub|]. by move: (div_mul_le b a); apply/le_trans/led_mul2r. Qed. -Lemma div_top x : 1%O / x = 1%O. +Lemma div_top x : \top / x = \top. Proof. apply/le_anti /andP; split; [|rewrite -mul_div_equiv]; exact: lex1. Qed. Lemma led_divl a b c : a <= b -> a / c <= b / c. @@ -482,7 +482,7 @@ HB.end. Section ComCompleteDioidTheory. -Variables (disp : unit) (D : comCompleteDioidType disp). +Variables (disp : Order.disp_t) (D : comCompleteDioidType disp). Implicit Types a b : D. @@ -586,7 +586,7 @@ HB.instance Definition _ := HB.end. HB.factory Record SubChoice_isJoinSubCompleteDioid d (D : completeDioidType d) - S (d' : unit) U of SubChoice D S U := { + S (d' : Order.disp_t) U of SubChoice D S U := { semiring_closed_subproof : semiring_closed S; opredSJ_subproof : set_join_closed S; }. @@ -598,8 +598,8 @@ HB.instance Definition _ := SubDioid_SubPOrder_isJoinSubCompleteDioid.Build d D S d' U opredSJ_subproof. HB.end. -HB.factory Record SubChoice_isJoinSubComCompleteDioid - d (D : comCompleteDioidType d) S (d' : unit) U of SubChoice D S U := { +HB.factory Record SubChoice_isJoinSubComCompleteDioid d + (D : comCompleteDioidType d) S (d' : Order.disp_t) U of SubChoice D S U := { semiring_closed_subproof : semiring_closed S; opredSJ_subproof : set_join_closed S; }. @@ -648,7 +648,7 @@ HB.instance Definition _ := HB.end. HB.factory Record SubChoice_isSubCompleteDioid d (D : completeDioidType d) S - (d' : unit) U of SubChoice D S U := { + (d' : Order.disp_t) U of SubChoice D S U := { semiring_closed_subproof : semiring_closed S; opredSM_subproof : set_meet_closed S; opredSJ_subproof : set_join_closed S; @@ -662,8 +662,8 @@ HB.instance Definition _ := opredSM_subproof opredSJ_subproof. HB.end. -HB.factory Record SubChoice_isSubComCompleteDioid - d (D : comCompleteDioidType d) S (d' : unit) U of SubChoice D S U := { +HB.factory Record SubChoice_isSubComCompleteDioid d + (D : comCompleteDioidType d) S (d' : Order.disp_t) U of SubChoice D S U := { semiring_closed_subproof : semiring_closed S; opredSM_subproof : set_meet_closed S; opredSJ_subproof : set_join_closed S; @@ -746,7 +746,7 @@ Notation "[ 'SubChoice_isSubComCompleteDioid' 'of' U 'by' <: 'with' disp ]" := (* Testing subtype hierarchy Section Test0. -Variables (d : unit) (T : choiceType) (S : {pred T}). +Variables (d : Order.disp_t) (T : choiceType) (S : {pred T}). Inductive B := mkB x & x \in S. Definition vB u := let: mkB x _ := u in x. @@ -759,7 +759,7 @@ End Test0. Module Test1. Section Test1. -Variables (d : unit) (D : completeDioidType d) (S : semiringClosed D). +Variables (d : Order.disp_t) (D : completeDioidType d) (S : semiringClosed D). Hypothesis SSJ : set_join_closed S. HB.instance Definition _ := isJoinCompleteLatticeClosed.Build d D S SSJ. @@ -773,7 +773,7 @@ End Test1. Module Test2. Section Test2. -Variables (d : unit) (D : completeDioidType d) (S : semiringClosed D). +Variables (d : Order.disp_t) (D : completeDioidType d) (S : semiringClosed D). Hypothesis SSM : set_meet_closed S. Hypothesis SSJ : set_join_closed S. @@ -787,7 +787,7 @@ End Test2. Module Test3. Section Test3. -Variables (d : unit) (D : comCompleteDioidType d) (S : semiringClosed D). +Variables (d : Order.disp_t) (D : comCompleteDioidType d) (S : semiringClosed D). Hypothesis SSJ : set_join_closed S. HB.instance Definition _ := isJoinCompleteLatticeClosed.Build d D S SSJ. diff --git a/complete_lattice.v b/complete_lattice.v index b07a853..e0d8a6b 100644 --- a/complete_lattice.v +++ b/complete_lattice.v @@ -263,7 +263,7 @@ HB.end. Section CompleteLatticeTheory. -Variables (d : unit) (L : completeLatticeType d). +Variables (d : Order.disp_t) (L : completeLatticeType d). Implicit Types S : set L. Implicit Types x : L. @@ -355,16 +355,16 @@ move=> xmS xmS'; apply: set_meet_ge_lb => y [] Sy. - exact/(le_trans xmS')/set_meet_lb. Qed. -Lemma set_joinT : set_join setT = 1%O :> L. +Lemma set_joinT : set_join setT = \top :> L. Proof. by apply/le_anti; rewrite lex1 set_join_ub. Qed. -Lemma set_join0 : set_join set0 = 0%O :> L. +Lemma set_join0 : set_join set0 = \bot :> L. Proof. by apply/le_anti; rewrite le0x set_join_le_ub. Qed. -Lemma set_meetT : set_meet setT = 0%O :> L. +Lemma set_meetT : set_meet setT = \bot :> L. Proof. by apply/le_anti; rewrite le0x set_meet_lb. Qed. -Lemma set_meet0 : set_meet set0 = 1%O :> L. +Lemma set_meet0 : set_meet set0 = \top :> L. Proof. by apply/le_anti; rewrite lex1 set_meet_ge_lb. Qed. Lemma set_join2 x y : set_join [set x; y] = x `|` y. @@ -530,9 +530,9 @@ Section CompleteLatticeMorphismTheory. Section IdCompFun. -Variables (d : unit) (T : completeLatticeType d). -Variables (d' : unit) (T' : completeLatticeType d'). -Variables (d'' : unit) (T'' : completeLatticeType d''). +Variables (d : Order.disp_t) (T : completeLatticeType d). +Variables (d' : Order.disp_t) (T' : completeLatticeType d'). +Variables (d'' : Order.disp_t) (T'' : completeLatticeType d''). Section MeetCompFun. @@ -679,13 +679,13 @@ HB.structure Definition SubCompleteLattice d (T : completeLatticeType d) S & @JoinSubCompleteLattice d T S d' U }. #[export] -HB.instance Definition _ (d : unit) (T : completeLatticeType d) (S : pred T) - d' (U : MeetSubCompleteLattice.type S d') := +HB.instance Definition _ (d : Order.disp_t) (T : completeLatticeType d) + (S : pred T) d' (U : MeetSubCompleteLattice.type S d') := isMeetCompleteLatticeMorphism.Build d' U d T val valSM_subproof. #[export] -HB.instance Definition _ (d : unit) (T : completeLatticeType d) (S : pred T) - d' (U : JoinSubCompleteLattice.type S d') := +HB.instance Definition _ (d : Order.disp_t) (T : completeLatticeType d) + (S : pred T) d' (U : JoinSubCompleteLattice.type S d') := isJoinCompleteLatticeMorphism.Build d' U d T val valSJ_subproof. HB.factory Record SubPOrder_isMeetSubCompleteLattice d @@ -701,14 +701,14 @@ HB.instance Definition _ := isMeetCompleteLatticeClosed.Build d T S Lemma opredSM (B : set U) : set_meet (val @` B) \in S. Proof. by apply: opredSM => _ [y By] <- /=; apply: valP. Qed. -Let inU v Sv : U := eqtype.sub v Sv. +Let inU v Sv : U := eqtype.Sub v Sv. Let set_meetU (B : set U) := inU (opredSM B). Lemma set_meetU_is_glb : set_f_is_glb set_meetU. Proof. move=> B; split. -- by move=> x Bx; rewrite leEsub subK set_meet_lb//; exists x. -- move=> x ubx; rewrite leEsub subK set_meet_ge_lb// => _ [y By <-]. +- by move=> x Bx; rewrite leEsub SubK set_meet_lb//; exists x. +- move=> x ubx; rewrite leEsub SubK set_meet_ge_lb// => _ [y By <-]. by rewrite -leEsub ubx. Qed. @@ -716,21 +716,21 @@ HB.instance Definition _ := POrder_isMeetCompleteLattice.Build d' U set_meetU_is_glb. Lemma val1 : (val : U -> T) \top = \top. -Proof. by rewrite subK image_set0 set_meet0. Qed. +Proof. by rewrite SubK image_set0 set_meet0. Qed. HB.instance Definition _ := Order.isTSubLattice.Build d T S d' U val1. Lemma valI : Order.meet_morphism (val : U -> T). -Proof. by move=> x y; rewrite subK !image_setU !image_set1 set_meet2. Qed. +Proof. by move=> x y; rewrite SubK !image_setU !image_set1 set_meet2. Qed. HB.instance Definition _ := Order.isMeetSubLattice.Build d T S d' U valI. Lemma valSM : set_meet_morphism (val : U -> T). -Proof. by move=> B; rewrite subK. Qed. +Proof. by move=> B; rewrite SubK. Qed. HB.instance Definition _ := isMeetSubCompleteLattice.Build d T S d' U valSM. HB.end. HB.factory Record SubChoice_isMeetSubCompleteLattice d - (T : completeLatticeType d) S (d' : unit) U of SubChoice T S U := { + (T : completeLatticeType d) S (d' : Order.disp_t) U of SubChoice T S U := { opredSM_subproof : set_meet_closed S; }. @@ -753,14 +753,14 @@ HB.instance Definition _ := isJoinCompleteLatticeClosed.Build d T S Lemma opredSJ (B : set U) : set_join (val @` B) \in S. Proof. by apply: opredSJ => _ [y By] <- /=; apply: valP. Qed. -Let inU v Sv : U := eqtype.sub v Sv. +Let inU v Sv : U := eqtype.Sub v Sv. Let set_joinU (B : set U) := inU (opredSJ B). Lemma set_joinU_is_lub : set_f_is_lub set_joinU. Proof. move=> B; split. -- by move=> x Bx; rewrite leEsub subK set_join_ub//; exists x. -- move=> x ubx; rewrite leEsub subK set_join_le_ub// => _ [y By <-]. +- by move=> x Bx; rewrite leEsub SubK set_join_ub//; exists x. +- move=> x ubx; rewrite leEsub SubK set_join_le_ub// => _ [y By <-]. by rewrite -leEsub ubx. Qed. @@ -768,21 +768,21 @@ HB.instance Definition _ := POrder_isJoinCompleteLattice.Build d' U set_joinU_is_lub. Lemma val0 : (val : U -> T) \bot = \bot. -Proof. by rewrite subK image_set0 set_join0. Qed. +Proof. by rewrite SubK image_set0 set_join0. Qed. HB.instance Definition _ := Order.isBSubLattice.Build d T S d' U val0. Lemma valU : Order.join_morphism (val : U -> T). -Proof. by move=> x y; rewrite subK !image_setU !image_set1 set_join2. Qed. +Proof. by move=> x y; rewrite SubK !image_setU !image_set1 set_join2. Qed. HB.instance Definition _ := Order.isJoinSubLattice.Build d T S d' U valU. Lemma valSJ : set_join_morphism (val : U -> T). -Proof. by move=> B; rewrite subK. Qed. +Proof. by move=> B; rewrite SubK. Qed. HB.instance Definition _ := isJoinSubCompleteLattice.Build d T S d' U valSJ. HB.end. HB.factory Record SubChoice_isJoinSubCompleteLattice d - (T : completeLatticeType d) S (d' : unit) U of SubChoice T S U := { + (T : completeLatticeType d) S (d' : Order.disp_t) U of SubChoice T S U := { opredSJ_subproof : set_join_closed S; }. @@ -809,23 +809,23 @@ Proof. by apply: opredSM => _ [y By] <- /=; apply: valP. Qed. Lemma opredSJ (B : set U) : set_join (val @` B) \in S. Proof. by apply: opredSJ => _ [y By] <- /=; apply: valP. Qed. -Let inU v Sv : U := eqtype.sub v Sv. +Let inU v Sv : U := eqtype.Sub v Sv. Let set_meetU (B : set U) := inU (opredSM B). Let set_joinU (B : set U) := inU (opredSJ B). Lemma set_meetU_is_glb : set_f_is_glb set_meetU. Proof. move=> B; split. -- by move=> x Bx; rewrite leEsub subK set_meet_lb//; exists x. -- move=> x lbx; rewrite leEsub subK set_meet_ge_lb// => _ [y By <-]. +- by move=> x Bx; rewrite leEsub SubK set_meet_lb//; exists x. +- move=> x lbx; rewrite leEsub SubK set_meet_ge_lb// => _ [y By <-]. by rewrite -leEsub lbx. Qed. Lemma set_joinU_is_lub : set_f_is_lub set_joinU. Proof. move=> B; split. -- by move=> x Bx; rewrite leEsub subK set_join_ub//; exists x. -- move=> x ubx; rewrite leEsub subK set_join_le_ub// => _ [y By <-]. +- by move=> x Bx; rewrite leEsub SubK set_join_ub//; exists x. +- move=> x ubx; rewrite leEsub SubK set_join_le_ub// => _ [y By <-]. by rewrite -leEsub ubx. Qed. @@ -833,33 +833,33 @@ HB.instance Definition _ := POrder_isCompleteLattice.Build d' U set_meetU_is_glb set_joinU_is_lub. Lemma val0 : (val : U -> T) \bot = \bot. -Proof. by rewrite subK image_set0 set_join0. Qed. +Proof. by rewrite SubK image_set0 set_join0. Qed. HB.instance Definition _ := Order.isBSubLattice.Build d T S d' U val0. Lemma val1 : (val : U -> T) \top = \top. -Proof. by rewrite subK image_set0 set_meet0. Qed. +Proof. by rewrite SubK image_set0 set_meet0. Qed. HB.instance Definition _ := Order.isTSubLattice.Build d T S d' U val1. Lemma valI : Order.meet_morphism (val : U -> T). -Proof. by move=> x y; rewrite subK !image_setU !image_set1 set_meet2. Qed. +Proof. by move=> x y; rewrite SubK !image_setU !image_set1 set_meet2. Qed. HB.instance Definition _ := Order.isMeetSubLattice.Build d T S d' U valI. Lemma valU : Order.join_morphism (val : U -> T). -Proof. by move=> x y; rewrite subK !image_setU !image_set1 set_join2. Qed. +Proof. by move=> x y; rewrite SubK !image_setU !image_set1 set_join2. Qed. HB.instance Definition _ := Order.isJoinSubLattice.Build d T S d' U valU. Lemma valSM : set_meet_morphism (val : U -> T). -Proof. by move=> B; rewrite subK. Qed. +Proof. by move=> B; rewrite SubK. Qed. HB.instance Definition _ := isMeetSubCompleteLattice.Build d T S d' U valSM. Lemma valSJ : set_join_morphism (val : U -> T). -Proof. by move=> B; rewrite subK. Qed. +Proof. by move=> B; rewrite SubK. Qed. HB.instance Definition _ := isJoinSubCompleteLattice.Build d T S d' U valSJ. HB.end. HB.factory Record SubChoice_isSubCompleteLattice d - (T : completeLatticeType d) S (d' : unit) U of SubChoice T S U := { + (T : completeLatticeType d) S (d' : Order.disp_t) U of SubChoice T S U := { opredSM_subproof : set_meet_closed S; opredSJ_subproof : set_join_closed S; }. diff --git a/coq-mathcomp-dioid.opam b/coq-mathcomp-dioid.opam index 5047765..499a15d 100644 --- a/coq-mathcomp-dioid.opam +++ b/coq-mathcomp-dioid.opam @@ -15,10 +15,10 @@ build: [ install: [make "install"] depends: [ - "coq" { >= "8.16" & < "8.18~" } - "coq-mathcomp-algebra" { >= "2.0" & < "2.1~" } - "coq-mathcomp-classical" { >= "1.0" & < "1.1~" } - "coq-hierarchy-builder" { >= "1.4.0" } + "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" } ] synopsis: "Dioid" description: """ diff --git a/dioid.v b/dioid.v index f501107..03d404a 100644 --- a/dioid.v +++ b/dioid.v @@ -123,7 +123,7 @@ HB.instance Definition _ := GRing.isSemiRing.Build D addA addC add0d HB.instance Definition _ := SemiRing_POrder_isDioid.Build d D adddd le_def. HB.end. -HB.factory Record SemiRing_isDioid (d : unit) D of GRing.SemiRing D := { +HB.factory Record SemiRing_isDioid (d : Order.disp_t) D of GRing.SemiRing D := { adddd : @idempotent D +%R; }. @@ -160,7 +160,7 @@ HB.instance Definition _ := SemiRing_POrder_isDioid.Build d D adddd le_def. HB.end. -HB.factory Record Choice_isDioid (d : unit) D of Choice D := { +HB.factory Record Choice_isDioid (d : Order.disp_t) D of Choice D := { zero : D; add : D -> D -> D; one : D; @@ -187,7 +187,7 @@ HB.end. Section DioidTheory. -Variables (disp : unit) (D : dioidType disp). +Variables (disp : Order.disp_t) (D : dioidType disp). Implicit Type a b c : D. @@ -269,7 +269,7 @@ HB.instance Definition _ := GRing.SemiRing_hasCommutativeMul.Build D mulC. HB.end. -HB.factory Record Choice_isComDioid (d : unit) D of Choice D := { +HB.factory Record Choice_isComDioid (d : Order.disp_t) D of Choice D := { zero : D; add : D -> D -> D; one : D; @@ -305,7 +305,7 @@ HB.instance Definition _ := GRing.SemiRing_hasCommutativeMul.Build D mulC. HB.end. #[short(type="subDioidType")] -HB.structure Definition SubDioid d (D : dioidType d) (S : pred D) (d' : unit) := +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 }. #[short(type="subDioidLatticeType")] @@ -335,8 +335,8 @@ Proof. by rewrite leEsub le_def -rmorphD /= (inj_eq val_inj). Qed. 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' : unit) U - of SubChoice D S U := { +HB.factory Record SubChoice_isSubDioid d (D : dioidType d) S (d' : Order.disp_t) + U of SubChoice D S U := { semiring_closed_subproof : semiring_closed S; }. @@ -353,16 +353,16 @@ 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' : unit) U of GRing.SubComSemiRing D S U & @Order.SubPOrder d D S d' U := - {}. + S (d' : Order.disp_t) U of GRing.SubComSemiRing 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. 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' : unit) U - of SubChoice D S U := { +HB.factory Record SubChoice_isSubComDioid d (D : comDioidType d) S + (d' : Order.disp_t) U of SubChoice D S U := { semiring_closed_subproof : semiring_closed S }. @@ -412,7 +412,7 @@ Notation "[ 'SubChoice_isSubComDioid' 'of' U 'by' <: 'with' disp ]" := (* Testing subtype hierarchy Section Test0. -Variables (d : unit) (T : choiceType) (S : {pred T}). +Variables (d : Order.disp_t) (T : choiceType) (S : {pred T}). Inductive B := mkB x & x \in S. Definition vB u := let: mkB x _ := u in x. @@ -424,7 +424,7 @@ End Test0. Section Test1. -Variables (d : unit) (R : dioidType d) (S : semiringClosed R). +Variables (d : Order.disp_t) (R : dioidType d) (S : semiringClosed R). HB.instance Definition _ := [SubChoice_isSubDioid of B S by <: with tt]. @@ -432,7 +432,7 @@ End Test1. Section Test2. -Variables (d : unit) (R : comDioidType d) (S : semiringClosed R). +Variables (d : Order.disp_t) (R : comDioidType d) (S : semiringClosed R). HB.instance Definition _ := [SubChoice_isSubComDioid of B S by <: with tt].