diff options
| -rw-r--r-- | .gitlab-ci.yml | 60 | ||||
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 6 | ||||
| -rw-r--r-- | mathcomp/algebra/intdiv.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/interval.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/rat.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 12 | ||||
| -rw-r--r-- | mathcomp/character/vcharacter.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/algC.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/algebraics_fundamentals.v | 2 | ||||
| -rw-r--r-- | mathcomp/field/finfield.v | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 41 |
12 files changed, 98 insertions, 37 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ef0b240..b366d39 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -143,6 +143,9 @@ coq-dev: script: - make -j "${NJOBS}" - make install + except: + - /^experiment\/order$/ + - /^pr-(270|383)$/ ci-fourcolor-8.7: extends: .ci-fourcolor @@ -169,6 +172,33 @@ ci-fourcolor-dev: variables: COQ_VERSION: "dev" +.ci-fourcolor-270: + extends: .ci + variables: + CONTRIB_URL: "https://github.com/pi8027/fourcolor.git" + CONTRIB_VERSION: fix-mathcomp-270 + script: + - make -j "${NJOBS}" + - make install + only: + - /^experiment\/order$/ + - /^pr-(270|383)$/ + +ci-fourcolor-8.7-270: + extends: .ci-fourcolor-270 + variables: + COQ_VERSION: "8.7" + +ci-fourcolor-8.8-270: + extends: .ci-fourcolor-270 + variables: + COQ_VERSION: "8.8" + +ci-fourcolor-dev-270: + extends: .ci-fourcolor-270 + variables: + COQ_VERSION: "dev" + # The Odd Order Theorem .ci-odd-order: extends: .ci @@ -178,6 +208,9 @@ ci-fourcolor-dev: script: - make -j "${NJOBS}" - make install + except: + - /^experiment\/order$/ + - /^pr-(270|383)$/ ci-odd-order-8.7: extends: .ci-odd-order @@ -204,6 +237,33 @@ ci-odd-order-dev: variables: COQ_VERSION: "dev" +.ci-odd-order-270: + extends: .ci + variables: + CONTRIB_URL: "https://github.com/pi8027/odd-order.git" + CONTRIB_VERSION: fix-mathcomp-270 + script: + - make -j "${NJOBS}" + - make install + only: + - /^experiment\/order$/ + - /^pr-(270|383)$/ + +ci-odd-order-8.7-270: + extends: .ci-odd-order-270 + variables: + COQ_VERSION: "8.7" + +ci-odd-order-8.8-270: + extends: .ci-odd-order-270 + variables: + COQ_VERSION: "8.8" + +ci-odd-order-dev-270: + extends: .ci-odd-order-270 + variables: + COQ_VERSION: "dev" + # The Lemma Overloading library .ci-lemma-overloading: extends: .ci diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ca4c118..9624885 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -73,10 +73,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). * `minr_max(l|r)` -> `meetU(l|r)` * `minrP`, `maxrP` -> `leP`, `ltP` * `(minr|maxr)(r|C|A|CA|AC)` -> `(meet|join)(xx|C|A|CA|AC)` - * `minr_l` -> `elimT meet_idPl` - * `minr_r` -> `elimT meet_idPr` - * `maxr_l` -> `elimT join_idPr` - * `maxr_r` -> `elimT join_idPl` + * `minr_(l|r)` -> `meet_(l|r)` + * `maxr_(l|r)` -> `join_(l|r)` * `arg_minrP` -> `arg_minP` * `arg_maxrP` -> `arg_maxP` + Generalized the following lemmas as properties of `normedDomainType`: diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index eaa256c..2a485fd 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -46,7 +46,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import Order.Theory GRing.Theory Num.Theory. +Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope ring_scope. Definition divz (m d : int) := diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 48d5254..b34c1ad 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -40,7 +40,7 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Local Open Scope ring_scope. -Import Order.Theory Order.Syntax GRing.Theory Num.Theory. +Import Order.TTheory Order.Syntax GRing.Theory Num.Theory. Local Notation mid x y := ((x + y) / 2%:R). diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 4ef050f..8478d93 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -19,7 +19,7 @@ From mathcomp Require Import ssrint. (* ratr x == generic embedding of (r : R) into an arbitrary unitring. *) (******************************************************************************) -Import Order.Theory GRing.Theory Num.Theory. +Import Order.TTheory GRing.Theory Num.Theory. Set Implicit Arguments. Unset Strict Implicit. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index cbd6fa1..b408f9d 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -40,7 +40,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import Order.Theory GRing.Theory Num.Theory. +Import Order.TTheory GRing.Theory Num.Theory. Delimit Scope int_scope with Z. Local Open Scope int_scope. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index d068135..2906412 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -125,7 +125,7 @@ Unset Printing Implicit Defensive. Local Open Scope order_scope. Local Open Scope ring_scope. -Import Order.Theory Order.Def Order.Syntax GRing.Theory. +Import Order.TTheory Order.Def Order.Syntax GRing.Theory. Reserved Notation "<= y" (at level 35). Reserved Notation ">= y" (at level 35). @@ -5478,12 +5478,12 @@ Implicit Types x y z : R. Section MinMax. Definition minrC : @commutative R R min := @meetC _ R. Definition minrr : @idempotent R min := @meetxx _ R. -Definition minr_l x y : x <= y -> min x y = x := elimT meet_idPl. -Definition minr_r x y : y <= x -> min x y = y := elimT meet_idPr. +Definition minr_l x y : x <= y -> min x y = x := @meet_l _ _ x y. +Definition minr_r x y : y <= x -> min x y = y := @meet_r _ _ x y. Definition maxrC : @commutative R R max := @joinC _ R. Definition maxrr : @idempotent R max := @joinxx _ R. -Definition maxr_l x y : y <= x -> max x y = x := elimT join_idPr. -Definition maxr_r x y : x <= y -> max x y = y := elimT join_idPl. +Definition maxr_l x y : y <= x -> max x y = x := @join_l _ _ x y. +Definition maxr_r x y : x <= y -> max x y = y := @join_r _ _ x y. Definition minrA x y z : min x (min y z) = min (min x y) z := meetA x y z. Definition minrCA : @left_commutative R R min := meetCA. Definition minrAC : @right_commutative R R min := meetAC. @@ -5674,5 +5674,3 @@ Notation "[ 'arg' 'maxr_' ( i > i0 ) F ]" := [arg maxr_(i > i0 | true) F] End Num. End mc_1_9. - -Export mc_1_9 mc_1_9.Num.Syntax. diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v index e886c5a..faecc02 100644 --- a/mathcomp/character/vcharacter.v +++ b/mathcomp/character/vcharacter.v @@ -40,7 +40,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import Order.Theory GroupScope GRing.Theory Num.Theory. +Import Order.TTheory GroupScope GRing.Theory Num.Theory. Local Open Scope ring_scope. Section Basics. diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index 8c1fd96..d41c6d8 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -53,7 +53,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import Order.Theory GRing.Theory Num.Theory. +Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope ring_scope. (* The Num mixin for an algebraically closed field with an automorphism of *) diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index e8521ec..613dd91 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.v @@ -112,7 +112,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import Order.Theory Order.Syntax GroupScope GRing.Theory Num.Theory. +Import Order.TTheory Order.Syntax GroupScope GRing.Theory Num.Theory. Local Open Scope ring_scope. Local Notation "p ^ f" := (map_poly f p) : ring_scope. diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v index efe5cea..f0d432f 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/field/finfield.v @@ -568,7 +568,7 @@ End FinFieldExists. Section FinDomain. -Import order ssrnum ssrint algC cyclotomic Order.Theory Num.Theory. +Import order ssrnum ssrint algC cyclotomic Order.TTheory Num.Theory. Local Infix "%|" := dvdn. (* Hide polynomial divisibility. *) Variable R : finUnitRingType. diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index fd0f663..554ae72 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -783,14 +783,13 @@ Variable (disp : unit). Local Notation porderType := (porderType disp). Variable (T : porderType). -Definition le (R : porderType) : rel R := POrder.le (POrder.class R). +Definition le : rel T := POrder.le (POrder.class T). Local Notation "x <= y" := (le x y) : order_scope. -Definition lt (R : porderType) : rel R := POrder.lt (POrder.class R). +Definition lt : rel T := POrder.lt (POrder.class T). Local Notation "x < y" := (lt x y) : order_scope. -Definition comparable (R : porderType) : rel R := - fun (x y : R) => (x <= y) || (y <= x). +Definition comparable : rel T := fun (x y : T) => (x <= y) || (y <= x). Local Notation "x >=< y" := (comparable x y) : order_scope. Local Notation "x >< y" := (~~ (x >=< y)) : order_scope. @@ -1487,11 +1486,11 @@ Module Import TotalSyntax. Fact total_display : unit. Proof. exact: tt. Qed. Notation max := (@join total_display _). -Notation "@ 'max' R" := - (@join total_display R) (at level 10, R at level 8, only parsing). +Notation "@ 'max' T" := + (@join total_display T) (at level 10, T at level 8, only parsing). Notation min := (@meet total_display _). -Notation "@ 'min' R" := - (@meet total_display R) (at level 10, R at level 8, only parsing). +Notation "@ 'min' T" := + (@meet total_display T) (at level 10, T at level 8, only parsing). Notation "\max_ ( i <- r | P ) F" := (\big[max/0%O]_(i <- r | P%B) F%O) : order_scope. @@ -1967,7 +1966,7 @@ Notation "x <=^c y <^c z" := ((x <=^c y) && (y <^c z)) : order_scope. Notation "x <^c y <^c z" := ((x <^c y) && (y <^c z)) : order_scope. Notation "x <=^c y ?= 'iff' C" := (<?=^c%O x y C) : order_scope. -Notation "x <=^c y ?= 'iff' C :> R" := ((x : R) <=^c (y : R) ?= iff C) +Notation "x <=^c y ?= 'iff' C :> T" := ((x : T) <=^c (y : T) ?= iff C) (only parsing) : order_scope. Notation ">=<^c x" := (>=<^c%O x) : order_scope. @@ -2517,6 +2516,9 @@ Proof. by rewrite leEmeet; apply/eqP. Qed. Lemma meet_idPr {x y} : reflect (y `&` x = x) (x <= y). Proof. by rewrite meetC; apply/meet_idPl. Qed. +Lemma meet_l x y : x <= y -> x `&` y = x. Proof. exact/meet_idPl. Qed. +Lemma meet_r x y : y <= x -> x `&` y = y. Proof. exact/meet_idPr. Qed. + Lemma leIidl x y : (x <= x `&` y) = (x <= y). Proof. by rewrite !leEmeet meetKI. Qed. Lemma leIidr x y : (x <= y `&` x) = (x <= y). @@ -2582,6 +2584,9 @@ Proof. exact: (@meet_idPr _ [latticeType of L^c]). Qed. Lemma join_idPr {x y} : reflect (y `|` x = y) (x <= y). Proof. exact: (@meet_idPl _ [latticeType of L^c]). Qed. +Lemma join_l x y : y <= x -> x `|` y = x. Proof. exact/join_idPr. Qed. +Lemma join_r x y : x <= y -> x `|` y = y. Proof. exact/join_idPl. Qed. + Lemma leUidl x y : (x `|` y <= y) = (x <= y). Proof. exact: (@leIidr _ [latticeType of L^c]). Qed. Lemma leUidr x y : (y `|` x <= y) = (x <= y). @@ -2809,14 +2814,14 @@ Qed. Lemma leU2r_le y t x z : x `&` t = 0 -> y `|` x <= t `|` z -> x <= z. Proof. by rewrite joinC [_ `|` z]joinC => /leU2l_le H /H. Qed. -Lemma lexUl z x y : x `&` z = 0 -> (x <= y `|` z) = (x <= y). +Lemma disjoint_lexUl z x y : x `&` z = 0 -> (x <= y `|` z) = (x <= y). Proof. move=> xz0; apply/idP/idP=> xy; last by rewrite lexU2 ?xy. by apply: (@leU2l_le x z); rewrite ?joinxx. Qed. -Lemma lexUr z x y : x `&` z = 0 -> (x <= z `|` y) = (x <= y). -Proof. by move=> xz0; rewrite joinC; rewrite lexUl. Qed. +Lemma disjoint_lexUr z x y : x `&` z = 0 -> (x <= z `|` y) = (x <= y). +Proof. by move=> xz0; rewrite joinC; rewrite disjoint_lexUl. Qed. Lemma leU2E x y z t : x `&` t = 0 -> y `&` z = 0 -> (x `|` y <= z `|` t) = (x <= z) && (y <= t). @@ -2970,11 +2975,11 @@ Proof. rewrite joinC; exact: (@leU2l_le _ [tblatticeType of L^c]). Qed. Lemma leI2r_le y t x z : y `|` z = 1 -> y `&` x <= t `&` z -> x <= z. Proof. rewrite joinC; exact: (@leU2r_le _ [tblatticeType of L^c]). Qed. -Lemma lexIl z x y : z `|` y = 1 -> (x `&` z <= y) = (x <= y). -Proof. rewrite joinC; exact: (@lexUl _ [tblatticeType of L^c]). Qed. +Lemma cover_leIxl z x y : z `|` y = 1 -> (x `&` z <= y) = (x <= y). +Proof. rewrite joinC; exact: (@disjoint_lexUl _ [tblatticeType of L^c]). Qed. -Lemma lexIr z x y : z `|` y = 1 -> (z `&` x <= y) = (x <= y). -Proof. rewrite joinC; exact: (@lexUr _ [tblatticeType of L^c]). Qed. +Lemma cover_leIxr z x y : z `|` y = 1 -> (z `&` x <= y) = (x <= y). +Proof. rewrite joinC; exact: (@disjoint_lexUr _ [tblatticeType of L^c]). Qed. Lemma leI2E x y z t : x `|` t = 1 -> y `|` z = 1 -> (x `&` y <= z `&` t) = (x <= z) && (y <= t). @@ -3943,7 +3948,7 @@ Notation "x <=^p y <^p z" := ((x <=^p y) && (y <^p z)) : order_scope. Notation "x <^p y <^p z" := ((x <^p y) && (y <^p z)) : order_scope. Notation "x <=^p y ?= 'iff' C" := (<?=^p%O x y C) : order_scope. -Notation "x <=^p y ?= 'iff' C :> R" := ((x : R) <=^p (y : R) ?= iff C) +Notation "x <=^p y ?= 'iff' C :> T" := ((x : T) <=^p (y : T) ?= iff C) (only parsing) : order_scope. Notation ">=<^p x" := (>=<^p%O x) : order_scope. @@ -4052,7 +4057,7 @@ Notation "x <=^l y <^l z" := ((x <=^l y) && (y <^l z)) : order_scope. Notation "x <^l y <^l z" := ((x <^l y) && (y <^l z)) : order_scope. Notation "x <=^l y ?= 'iff' C" := (<?=^l%O x y C) : order_scope. -Notation "x <=^l y ?= 'iff' C :> R" := ((x : R) <=^l (y : R) ?= iff C) +Notation "x <=^l y ?= 'iff' C :> T" := ((x : T) <=^l (y : T) ?= iff C) (only parsing) : order_scope. Notation ">=<^l x" := (>=<^l%O x) : order_scope. |