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/algebra/rat.v | 56 +++++++++++++++++++++++++++----------------------- 1 file changed, 30 insertions(+), 26 deletions(-) (limited to 'mathcomp/algebra/rat.v') diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 228a824..4ef050f 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -1,7 +1,8 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. -From mathcomp Require Import fintype bigop ssralg countalg div ssrnum ssrint. +From mathcomp Require Import fintype bigop order ssralg countalg div ssrnum. +From mathcomp Require Import ssrint. (******************************************************************************) (* This file defines a datatype for rational numbers and equips it with a *) @@ -18,8 +19,7 @@ From mathcomp Require Import fintype bigop ssralg countalg div ssrnum ssrint. (* ratr x == generic embedding of (r : R) into an arbitrary unitring. *) (******************************************************************************) -Import GRing.Theory. -Import Num.Theory. +Import Order.Theory GRing.Theory Num.Theory. Set Implicit Arguments. Unset Strict Implicit. @@ -51,16 +51,16 @@ Canonical rat_subCountType := [subCountType of rat]. Definition numq x := nosimpl ((valq x).1). Definition denq x := nosimpl ((valq x).2). -Lemma denq_gt0 x : 0 < denq x. +Lemma denq_gt0 x : 0 < denq x. Proof. by rewrite /denq; case: x=> [[a b] /= /andP []]. Qed. Hint Resolve denq_gt0 : core. -Definition denq_ge0 x := ltrW (denq_gt0 x). +Definition denq_ge0 x := ltW (denq_gt0 x). -Lemma denq_lt0 x : (denq x < 0) = false. Proof. by rewrite ltr_gtF. Qed. +Lemma denq_lt0 x : (denq x < 0) = false. Proof. by rewrite lt_gtF. Qed. Lemma denq_neq0 x : denq x != 0. -Proof. by rewrite /denq gtr_eqF ?denq_gt0. Qed. +Proof. by rewrite /denq gt_eqF ?denq_gt0. Qed. Hint Resolve denq_neq0 : core. Lemma denq_eq0 x : (denq x == 0) = false. @@ -99,7 +99,7 @@ Fact valqK x : fracq (valq x) = x. Proof. move: x => [[n d] /= Pnd]; apply: val_inj=> /=. move: Pnd; rewrite /coprime /fracq /= => /andP[] hd -/eqP hnd. -by rewrite ltr_gtF ?gtr_eqF //= hnd !divn1 mulz_sign_abs abszE gtr0_norm. +by rewrite lt_gtF ?gt_eqF //= hnd !divn1 mulz_sign_abs abszE gtr0_norm. Qed. Fact scalq_key : unit. Proof. by []. Qed. @@ -343,7 +343,7 @@ Canonical rat_comUnitRing := Eval hnf in [comUnitRingType of rat]. Fact rat_field_axiom : GRing.Field.mixin_of rat_unitRing. Proof. exact. Qed. Definition RatFieldIdomainMixin := (FieldIdomainMixin rat_field_axiom). -Canonical rat_iDomain := +Canonical rat_idomainType := Eval hnf in IdomainType rat (FieldIdomainMixin rat_field_axiom). Canonical rat_fieldType := FieldType rat rat_field_axiom. @@ -396,13 +396,13 @@ Lemma rat1 : 1%:Q = 1. Proof. by []. Qed. Lemma numqN x : numq (- x) = - numq x. Proof. rewrite /numq; case: x=> [[a b] /= /andP [hb]]; rewrite /coprime=> /eqP hab. -by rewrite ltr_gtF ?gtr_eqF // {2}abszN hab divn1 mulz_sign_abs. +by rewrite lt_gtF ?gt_eqF // {2}abszN hab divn1 mulz_sign_abs. Qed. Lemma denqN x : denq (- x) = denq x. Proof. rewrite /denq; case: x=> [[a b] /= /andP [hb]]; rewrite /coprime=> /eqP hab. -by rewrite gtr_eqF // abszN hab divn1 gtz0_abs. +by rewrite gt_eqF // abszN hab divn1 gtz0_abs. Qed. (* Will be subsumed by pnatr_eq0 *) @@ -502,7 +502,7 @@ Proof. rewrite !ge_rat0 => hnx hny. have hxy: (0 <= numq x * denq y + numq y * denq x). by rewrite addr_ge0 ?mulr_ge0. -by rewrite /numq /= -!/(denq _) ?mulf_eq0 ?denq_eq0 !ler_gtF ?mulr_ge0. +by rewrite /numq /= -!/(denq _) ?mulf_eq0 ?denq_eq0 !le_gtF ?mulr_ge0. Qed. Fact le_rat0M x y : le_rat 0 x -> le_rat 0 y -> le_rat 0 (x * y). @@ -510,12 +510,12 @@ Proof. rewrite !ge_rat0 => hnx hny. have hxy: (0 <= numq x * denq y + numq y * denq x). by rewrite addr_ge0 ?mulr_ge0. -by rewrite /numq /= -!/(denq _) ?mulf_eq0 ?denq_eq0 !ler_gtF ?mulr_ge0. +by rewrite /numq /= -!/(denq _) ?mulf_eq0 ?denq_eq0 !le_gtF ?mulr_ge0. Qed. Fact le_rat0_anti x : le_rat 0 x -> le_rat x 0 -> x = 0. Proof. -by move=> hx hy; apply/eqP; rewrite -numq_eq0 eqr_le -ge_rat0 -le_rat0 hx hy. +by move=> hx hy; apply/eqP; rewrite -numq_eq0 eq_le -ge_rat0 -le_rat0 hx hy. Qed. Lemma sgr_numq_div (n d : int) : sgr (numq (n%:Q / d%:Q)) = sgr n * sgr d. @@ -530,12 +530,12 @@ Proof. symmetry; rewrite ge_rat0 /le_rat -subr_ge0. case: ratP => nx dx cndx; case: ratP => ny dy cndy. rewrite -!mulNr addf_div ?intq_eq0 // !mulNr -!rmorphM -rmorphB /=. -symmetry; rewrite !lerNgt -sgr_cp0 sgr_numq_div mulrC gtr0_sg //. +symmetry; rewrite !leNgt -sgr_cp0 sgr_numq_div mulrC gtr0_sg //. by rewrite mul1r sgr_cp0. Qed. Fact le_rat_total : total le_rat. -Proof. by move=> x y; apply: ler_total. Qed. +Proof. by move=> x y; apply: le_total. Qed. Fact numq_sign_mul (b : bool) x : numq ((-1) ^+ b * x) = (-1) ^+ b * numq x. Proof. by case: b; rewrite ?(mul1r, mulN1r) // numqN. Qed. @@ -566,14 +566,19 @@ by rewrite /normq /= normr_num_div ?ger0_norm // divq_num_den. Qed. Fact lt_rat_def x y : (lt_rat x y) = (y != x) && (le_rat x y). -Proof. by rewrite /lt_rat ltr_def rat_eq. Qed. +Proof. by rewrite /lt_rat lt_def rat_eq. Qed. -Definition ratLeMixin := RealLeMixin le_rat0D le_rat0M le_rat0_anti - subq_ge0 (@le_rat_total 0) norm_ratN ge_rat0_norm lt_rat_def. +Definition ratLeMixin : realLeMixin rat_idomainType := + RealLeMixin le_rat0D le_rat0M le_rat0_anti subq_ge0 + (@le_rat_total 0) norm_ratN ge_rat0_norm lt_rat_def. +Canonical rat_porderType := POrderType ring_display rat ratLeMixin. +Canonical rat_latticeType := LatticeType rat ratLeMixin. +Canonical rat_orderType := OrderType rat le_rat_total. Canonical rat_numDomainType := NumDomainType rat ratLeMixin. +Canonical rat_normedDomainType := NormedDomainType rat rat ratLeMixin. Canonical rat_numFieldType := [numFieldType of rat]. -Canonical rat_realDomainType := RealDomainType rat (@le_rat_total 0). +Canonical rat_realDomainType := [realDomainType of rat]. Canonical rat_realFieldType := [realFieldType of rat]. Lemma numq_ge0 x : (0 <= numq x) = (0 <= x). @@ -585,10 +590,10 @@ Lemma numq_le0 x : (numq x <= 0) = (x <= 0). Proof. by rewrite -oppr_ge0 -numqN numq_ge0 oppr_ge0. Qed. Lemma numq_gt0 x : (0 < numq x) = (0 < x). -Proof. by rewrite !ltrNge numq_le0. Qed. +Proof. by rewrite !ltNge numq_le0. Qed. Lemma numq_lt0 x : (numq x < 0) = (x < 0). -Proof. by rewrite !ltrNge numq_ge0. Qed. +Proof. by rewrite !ltNge numq_ge0. Qed. Lemma sgr_numq x : sgz (numq x) = sgz x. Proof. @@ -605,7 +610,7 @@ Proof. by rewrite normrEsign denq_mulr_sign. Qed. Fact rat_archimedean : Num.archimedean_axiom [numDomainType of rat]. Proof. move=> x; exists `|numq x|.+1; rewrite mulrS ltr_spaddl //. -rewrite pmulrn abszE intr_norm numqE normrM ler_pemulr ?norm_ge0 //. +rewrite pmulrn abszE intr_norm numqE normrM ler_pemulr //. by rewrite -intr_norm ler1n absz_gt0 denq_eq0. Qed. @@ -758,7 +763,7 @@ by rewrite ![_ / _ * _]mulrAC !ler_pdivr_mulr ?ltr0z // -!rmorphM /= !ler_int. Qed. Lemma ltr_rat : {mono (@ratr F) : x y / x < y}. -Proof. exact: lerW_mono ler_rat. Qed. +Proof. exact: leW_mono ler_rat. Qed. Lemma ler0q x : (0 <= ratr F x) = (0 <= x). Proof. by rewrite (_ : 0 = ratr F 0) ?ler_rat ?rmorph0. Qed. @@ -777,8 +782,7 @@ Proof. by rewrite !sgr_def fmorph_eq0 ltrq0 rmorphMn rmorph_sign. Qed. Lemma ratr_norm x : ratr F `|x| = `|ratr F x|. Proof. -rewrite {2}[x]numEsign rmorphMsign normrMsign [`|ratr F _|]ger0_norm //. -by rewrite ler0q ?normr_ge0. +by rewrite {2}[x]numEsign rmorphMsign normrMsign [`|ratr F _|]ger0_norm ?ler0q. Qed. End InPrealField. -- 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/algebra/rat.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/algebra/rat.v') 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. -- 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/algebra/rat.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/algebra/rat.v') diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 8478d93..939046e 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -576,7 +576,7 @@ Canonical rat_porderType := POrderType ring_display rat ratLeMixin. Canonical rat_latticeType := LatticeType rat ratLeMixin. Canonical rat_orderType := OrderType rat le_rat_total. Canonical rat_numDomainType := NumDomainType rat ratLeMixin. -Canonical rat_normedDomainType := NormedDomainType rat rat ratLeMixin. +Canonical rat_normedZmodType := NormedZmoduleType rat rat ratLeMixin. Canonical rat_numFieldType := [numFieldType of rat]. Canonical rat_realDomainType := [realDomainType of rat]. Canonical rat_realFieldType := [realFieldType of rat]. -- cgit v1.2.3 From 44e8df83ad4e4394a96c15c787405cdea8931074 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 30 Oct 2019 14:40:23 +0100 Subject: Rename: (l|L)attice -> (d|D)istrLattice --- mathcomp/algebra/rat.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/algebra/rat.v') diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 939046e..15cc4fc 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -573,7 +573,7 @@ Definition ratLeMixin : realLeMixin rat_idomainType := (@le_rat_total 0) norm_ratN ge_rat0_norm lt_rat_def. Canonical rat_porderType := POrderType ring_display rat ratLeMixin. -Canonical rat_latticeType := LatticeType rat ratLeMixin. +Canonical rat_distrLatticeType := DistrLatticeType rat ratLeMixin. Canonical rat_orderType := OrderType rat le_rat_total. Canonical rat_numDomainType := NumDomainType rat ratLeMixin. Canonical rat_normedZmodType := NormedZmoduleType rat rat ratLeMixin. -- 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/algebra/rat.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mathcomp/algebra/rat.v') diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 15cc4fc..14b5035 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -576,7 +576,7 @@ Canonical rat_porderType := POrderType ring_display rat ratLeMixin. Canonical rat_distrLatticeType := DistrLatticeType rat ratLeMixin. Canonical rat_orderType := OrderType rat le_rat_total. Canonical rat_numDomainType := NumDomainType rat ratLeMixin. -Canonical rat_normedZmodType := NormedZmoduleType rat rat ratLeMixin. +Canonical rat_normedZmodType := NormedZmodType rat rat ratLeMixin. Canonical rat_numFieldType := [numFieldType of rat]. Canonical rat_realDomainType := [realDomainType of rat]. Canonical rat_realFieldType := [realFieldType of rat]. @@ -811,7 +811,7 @@ Qed. Require setoid_ring.Field_theory setoid_ring.Field_tac. -Lemma rat_field_theory : +Lemma rat_field_theory : Field_theory.field_theory 0%Q 1%Q addq mulq subq oppq divq invq eq. Proof. split => //; first exact rat_ring_theory. -- cgit v1.2.3