From fbf0b7568b8d6231671954cba8bcae4120e591cc Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 5 Feb 2019 15:38:39 +0100 Subject: Make an appropriate use of the order library everywhere (#278, #280, #282, #283, #285, #286, #288, #296, #330, #334, and #341) ssrnum related changes: - Redefine the intermediate structure between `idomainType` and `numDomainType`, which is `normedDomainType` (normed integral domain without an order). - Generalize (by using `normedDomainType` or the order structures), relocate (to order.v), and rename ssrnum related definitions and lemmas. - Add a compatibility module `Num.mc_1_9` and export it to check compilation. - Remove the use of the deprecated definitions and lemmas from entire theories. - Implement factories mechanism to construct several ordered and num structures from fewer axioms. order related changes: - Reorganize the hierarchy of finite lattice structures. Finite lattices have top and bottom elements except for empty set. Therefore we removed finite lattice structures without top and bottom. - Reorganize the theory modules in order.v: + `LTheory` (lattice and partial order, without complement and totality) + `CTheory` (`LTheory` + complement) + `Theory` (all) - Give a unique head symbol for `Total.mixin_of`. - Replace reverse and `^r` with converse and `^c` respectively. - Fix packing and cloning functions and notations. - Provide more ordered type instances: Products and lists can be ordered in two different ways: the lexicographical ordering and the pointwise ordering. Now their canonical instances are not exported to make the users choose them. - Export `Order.*.Exports` modules by default. - Specify the core hint database explicitly in order.v. (see #252) - Apply 80 chars per line restriction. General changes: - Give consistency to shape of formulae and namings of `lt_def` and `lt_neqAle` like lemmas: lt_def x y : (x < y) = (y != x) && (x <= y), lt_neqAle x y : (x < y) = (x != y) && (x <= y). - Enable notation overloading by using scopes and displays: + Define `min` and `max` notations (`minr` and `maxr` for `ring_display`) as aliases of `meet` and `join` specialized for `total_display`. + Provide the `ring_display` version of `le`, `lt`, `ge`, `gt`, `leif`, and `comparable` notations and their explicit variants in `Num.Def`. + Define 3 variants of `[arg min_(i < n | P) F]` and `[arg max_(i < n | P) F]` notations in `nat_scope` (specialized for nat), `order_scope` (general version), and `ring_scope` (specialized for `ring_display`). - Update documents and put CHANGELOG entries. --- mathcomp/field/algC.v | 64 +++++++++++++++++++++++++++------------------------ 1 file changed, 34 insertions(+), 30 deletions(-) (limited to 'mathcomp/field/algC.v') diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index e1fd4d1..8c1fd96 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -1,9 +1,9 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq choice. -From mathcomp Require Import div fintype path bigop finset prime ssralg poly. -From mathcomp Require Import polydiv mxpoly generic_quotient countalg ssrnum. -From mathcomp Require Import closed_field ssrint rat intdiv. +From mathcomp Require Import div fintype path bigop finset prime order ssralg. +From mathcomp Require Import poly polydiv mxpoly generic_quotient countalg. +From mathcomp Require Import ssrnum closed_field ssrint rat intdiv. From mathcomp Require Import algebraics_fundamentals. (******************************************************************************) @@ -53,14 +53,14 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Import GRing.Theory Num.Theory. +Import Order.Theory GRing.Theory Num.Theory. Local Open Scope ring_scope. (* The Num mixin for an algebraically closed field with an automorphism of *) (* order 2, making it into a field of complex numbers. *) Lemma ComplexNumMixin (L : closedFieldType) (conj : {rmorphism L -> L}) : involutive conj -> ~ conj =1 id -> - {numL | forall x : NumDomainType L numL, `|x| ^+ 2 = x * conj x}. + {numL : numMixin L | forall x : NumDomainType L numL, `|x| ^+ 2 = x * conj x}. Proof. move=> conjK conj_nt. have nz2: 2%:R != 0 :> L. @@ -184,7 +184,7 @@ have normD x y : le (norm (x + y)) (norm x + norm y). apply/posP; exists (i * (x * conj y - y * conj x)); congr (_ * _). rewrite !(rmorphM, rmorphB) iJ !conjK mulNr -mulrN opprB. by rewrite (mulrC x) (mulrC y). -by exists (Num.Mixin normD sposD norm_eq0 pos_linear normM (rrefl _) (rrefl _)). +by exists (NumMixin normD sposD norm_eq0 pos_linear normM (rrefl _) (rrefl _)). Qed. Module Algebraics. @@ -229,8 +229,10 @@ Canonical decFieldType := DecFieldType type decFieldMixin. Axiom closedFieldAxiom : GRing.ClosedField.axiom ringType. Canonical closedFieldType := ClosedFieldType type closedFieldAxiom. -Parameter numMixin : Num.mixin_of ringType. +Parameter numMixin : numMixin idomainType. +Canonical porderType := POrderType ring_display type numMixin. Canonical numDomainType := NumDomainType type numMixin. +Canonical normedDomainType := NormedDomainType type type numMixin. Canonical numFieldType := [numFieldType of type]. Parameter conjMixin : Num.ClosedField.imaginary_mixin_of numDomainType. @@ -422,13 +424,15 @@ have [i i2]: exists i : type, i ^+ 2 = -1. have [i] := @solve_monicpoly _ 2 (nth 0 [:: -1 : type]) isT. by rewrite !big_ord_recl big_ord0 /= mul0r mulr1 !addr0; exists i. move/(_ i)/(congr1 CtoL); rewrite LtoC_K => iL_J. -have/ltr_geF/idP[] := @ltr01 Lnum; rewrite -oppr_ge0 -(rmorphN1 CtoL_rmorphism). -rewrite -i2 rmorphX /= expr2 -{2}iL_J -(svalP LnumMixin). -by rewrite exprn_ge0 ?normr_ge0. +have/lt_geF/idP[] := @ltr01 Lnum; rewrite -oppr_ge0 -(rmorphN1 CtoL_rmorphism). +by rewrite -i2 rmorphX /= expr2 -{2}iL_J -(svalP LnumMixin) exprn_ge0. Qed. -Definition numMixin := sval (ComplexNumMixin conjK conj_nt). +Definition numMixin : numMixin closedFieldType := + sval (ComplexNumMixin conjK conj_nt). +Canonical porderType := POrderType ring_display type numMixin. Canonical numDomainType := NumDomainType type numMixin. +Canonical normedDomainType := NormedDomainType type type numMixin. Canonical numFieldType := [numFieldType of type]. Lemma normK u : `|u| ^+ 2 = u * conj u. @@ -480,18 +484,18 @@ Fact floorC_subproof x : {m | x \is Creal -> ZtoC m <= x < ZtoC (m + 1)}. Proof. have [Rx | _] := boolP (x \is Creal); last by exists 0. without loss x_ge0: x Rx / x >= 0. - have [x_ge0 | /ltrW x_le0] := real_ger0P Rx; first exact. + have [x_ge0 | /ltW x_le0] := real_ge0P Rx; first exact. case/(_ (- x)) => [||m /(_ isT)]; rewrite ?rpredN ?oppr_ge0 //. - rewrite ler_oppr ltr_oppl -!rmorphN opprD /= ltr_neqAle ler_eqVlt. + rewrite ler_oppr ltr_oppl -!rmorphN opprD /= lt_neqAle le_eqVlt. case: eqP => [-> _ | _ /and3P[lt_x_m _ le_m_x]]. - by exists (- m) => _; rewrite lerr rmorphD ltr_addl ltr01. + by exists (- m) => _; rewrite lexx rmorphD ltr_addl ltr01. by exists (- m - 1); rewrite le_m_x subrK. have /ex_minnP[n lt_x_n1 min_n]: exists n, x < n.+1%:R. have [n le_x_n] := rat_algebraic_archimedean algebraic x. - by exists n; rewrite -(ger0_norm x_ge0) (ltr_trans le_x_n) ?ltr_nat. + by exists n; rewrite -(ger0_norm x_ge0) (lt_trans le_x_n) ?ltr_nat. exists n%:Z => _; rewrite addrC -intS lt_x_n1 andbT. case Dn: n => // [n1]; rewrite -Dn. -have [||//|] := @real_lerP _ n%:R x; rewrite ?rpred_nat //. +have [||//|] := @real_leP _ n%:R x; rewrite ?rpred_nat //. by rewrite Dn => /min_n; rewrite Dn ltnn. Qed. @@ -535,7 +539,9 @@ Canonical unitRingType. Canonical comRingType. Canonical comUnitRingType. Canonical idomainType. +Canonical porderType. Canonical numDomainType. +Canonical normedDomainType. Canonical fieldType. Canonical numFieldType. Canonical decFieldType. @@ -663,15 +669,15 @@ Proof. by rewrite /floorC => Rx; case: (floorC_subproof x) => //= m; apply. Qed. Lemma floorC_def x m : m%:~R <= x < (m + 1)%:~R -> floorC x = m. Proof. -case/andP=> lemx ltxm1; apply/eqP; rewrite eqr_le -!ltz_addr1. +case/andP=> lemx ltxm1; apply/eqP; rewrite eq_le -!ltz_addr1. have /floorC_itv/andP[lefx ltxf1]: x \is Creal. by rewrite -[x](subrK m%:~R) rpredD ?realz ?ler_sub_real. -by rewrite -!(ltr_int [numFieldType of algC]) 2?(@ler_lt_trans _ x). +by rewrite -!(ltr_int [numFieldType of algC]) 2?(@le_lt_trans _ _ x). Qed. Lemma intCK : cancel intr floorC. Proof. -by move=> m; apply: floorC_def; rewrite ler_int ltr_int ltz_addr1 lerr. +by move=> m; apply: floorC_def; rewrite ler_int ltr_int ltz_addr1 lexx. Qed. Lemma floorCK : {in Cint, cancel floorC intr}. Proof. by move=> z /eqP. Qed. @@ -757,17 +763,17 @@ Lemma truncC_itv x : 0 <= x -> (truncC x)%:R <= x < (truncC x).+1%:R. Proof. move=> x_ge0; have /andP[lemx ltxm1] := floorC_itv (ger0_real x_ge0). rewrite /truncC x_ge0 -addn1 !pmulrn PoszD gez0_abs ?lemx //. -by rewrite -ltz_addr1 -(ltr_int [numFieldType of algC]) (ler_lt_trans x_ge0). +by rewrite -ltz_addr1 -(ltr_int [numFieldType of algC]) (le_lt_trans x_ge0). Qed. Lemma truncC_def x n : n%:R <= x < n.+1%:R -> truncC x = n. Proof. move=> ivt_n_x; have /andP[lenx _] := ivt_n_x. -by rewrite /truncC (ler_trans (ler0n _ n)) // (@floorC_def _ n) // addrC -intS. +by rewrite /truncC (le_trans (ler0n _ n)) // (@floorC_def _ n) // addrC -intS. Qed. Lemma natCK n : truncC n%:R = n. -Proof. by apply: truncC_def; rewrite lerr ltr_nat /=. Qed. +Proof. by apply: truncC_def; rewrite lexx ltr_nat /=. Qed. Lemma CnatP x : reflect (exists n, x = n%:R) (x \in Cnat). Proof. @@ -782,9 +788,9 @@ Proof. apply/idP/idP=> [m_gt0 | x_ge1]. have /truncC_itv/andP[lemx _]: 0 <= x. by move: m_gt0; rewrite /truncC; case: ifP. - by apply: ler_trans lemx; rewrite ler1n. -have /truncC_itv/andP[_ ltxm1]:= ler_trans ler01 x_ge1. -by rewrite -ltnS -ltC_nat (ler_lt_trans x_ge1). + by apply: le_trans lemx; rewrite ler1n. +have /truncC_itv/andP[_ ltxm1]:= le_trans ler01 x_ge1. +by rewrite -ltnS -ltC_nat (le_lt_trans x_ge1). Qed. Lemma truncC0Pn x : reflect (truncC x = 0%N) (~~ (1 <= x)). @@ -912,14 +918,12 @@ by rewrite pnatr_eq0 ler1n lt0n. Qed. Lemma sqr_Cint_ge1 x : x \in Cint -> x != 0 -> 1 <= x ^+ 2. -Proof. -by move=> Zx nz_x; rewrite -Cint_normK // expr_ge1 ?normr_ge0 ?norm_Cint_ge1. -Qed. +Proof. by move=> Zx nz_x; rewrite -Cint_normK // expr_ge1 ?norm_Cint_ge1. Qed. Lemma Cint_ler_sqr x : x \in Cint -> x <= x ^+ 2. Proof. move=> Zx; have [-> | nz_x] := eqVneq x 0; first by rewrite expr0n. -apply: ler_trans (_ : `|x| <= _); first by rewrite real_ler_norm ?Creal_Cint. +apply: le_trans (_ : `|x| <= _); first by rewrite real_ler_norm ?Creal_Cint. by rewrite -Cint_normK // ler_eexpr // norm_Cint_ge1. Qed. @@ -937,7 +941,7 @@ Lemma dvdCP_nat x y : 0 <= x -> 0 <= y -> (x %| y)%C -> {n | y = n%:R * x}. Proof. move=> x_ge0 y_ge0 x_dv_y; apply: sig_eqW. case/dvdCP: x_dv_y => z Zz -> in y_ge0 *; move: x_ge0 y_ge0 Zz. -rewrite ler_eqVlt => /predU1P[<- | ]; first by exists 22; rewrite !mulr0. +rewrite le_eqVlt => /predU1P[<- | ]; first by exists 22; rewrite !mulr0. by move=> /pmulr_lge0-> /CintEge0-> /CnatP[n ->]; exists n. Qed. -- cgit v1.2.3 From b0a01acd904cbfcaf47d821b3b5e72098b9efb07 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 3 Sep 2019 17:07:44 +0200 Subject: Add (meet|join)_(l|r), some renamings, and small cleanups New lemmas: - meet_l, meet_r, join_l, join_r. Renamings: - Order.BLatticeTheory.lexUl -> disjoint_lexUl, - Order.BLatticeTheory.lexUr -> disjoint_lexUr, - Order.TBLatticeTheory.lexIl -> cover_leIxl, - Order.TBLatticeTheory.lexIr -> cover_leIxr. Use `Order.TTheory` instead of `Order.Theory` if applicable --- mathcomp/field/algC.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/field/algC.v') 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 *) -- cgit v1.2.3 From e7df10a74264f52a17f54f87b8a89c9360a46926 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 16 Oct 2019 10:26:35 +0200 Subject: Redefine `normedDomainType` (now `normedZmodType`) (#392) * Redefine `normedDomainType` (now `normedZmodType`) - Redefine `normedDomainType` to drop ring and integral domain axioms. - Add canonical instance of `normedZmodType` for `prod`.--- mathcomp/field/algC.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'mathcomp/field/algC.v') diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index d41c6d8..aee2b85 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -232,7 +232,7 @@ Canonical closedFieldType := ClosedFieldType type closedFieldAxiom. Parameter numMixin : numMixin idomainType. Canonical porderType := POrderType ring_display type numMixin. Canonical numDomainType := NumDomainType type numMixin. -Canonical normedDomainType := NormedDomainType type type numMixin. +Canonical normedZmodType := NormedZmoduleType type type numMixin. Canonical numFieldType := [numFieldType of type]. Parameter conjMixin : Num.ClosedField.imaginary_mixin_of numDomainType. @@ -432,7 +432,7 @@ Definition numMixin : numMixin closedFieldType := sval (ComplexNumMixin conjK conj_nt). Canonical porderType := POrderType ring_display type numMixin. Canonical numDomainType := NumDomainType type numMixin. -Canonical normedDomainType := NormedDomainType type type numMixin. +Canonical normedZmodType := NormedZmoduleType type type numMixin. Canonical numFieldType := [numFieldType of type]. Lemma normK u : `|u| ^+ 2 = u * conj u. @@ -541,7 +541,7 @@ Canonical comUnitRingType. Canonical idomainType. Canonical porderType. Canonical numDomainType. -Canonical normedDomainType. +Canonical normedZmodType. Canonical fieldType. Canonical numFieldType. Canonical decFieldType. -- cgit v1.2.3 From b3261c9020105f3c6667697b22ca8a542271bc4c Mon Sep 17 00:00:00 2001 From: affeldt-aist Date: Thu, 14 Nov 2019 20:49:44 +0900 Subject: renaming NormedZmoduleType and NormedZmoduleMixin (#416) * renaming NormedZmoduleType -> NormedZmodType NormedZmoduleMixin -> NormedZmodMixin that looks more homogeneous with regard to naming conventions used so far * update .gitlab-ci.yml * typo --- mathcomp/field/algC.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp/field/algC.v') diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index aee2b85..0e3005d 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.v @@ -232,7 +232,7 @@ Canonical closedFieldType := ClosedFieldType type closedFieldAxiom. Parameter numMixin : numMixin idomainType. Canonical porderType := POrderType ring_display type numMixin. Canonical numDomainType := NumDomainType type numMixin. -Canonical normedZmodType := NormedZmoduleType type type numMixin. +Canonical normedZmodType := NormedZmodType type type numMixin. Canonical numFieldType := [numFieldType of type]. Parameter conjMixin : Num.ClosedField.imaginary_mixin_of numDomainType. @@ -432,7 +432,7 @@ Definition numMixin : numMixin closedFieldType := sval (ComplexNumMixin conjK conj_nt). Canonical porderType := POrderType ring_display type numMixin. Canonical numDomainType := NumDomainType type numMixin. -Canonical normedZmodType := NormedZmoduleType type type numMixin. +Canonical normedZmodType := NormedZmodType type type numMixin. Canonical numFieldType := [numFieldType of type]. Lemma normK u : `|u| ^+ 2 = u * conj u. -- cgit v1.2.3