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/intdiv.v | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) (limited to 'mathcomp/algebra/intdiv.v') diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 7663e63..eaa256c 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -1,7 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path. -From mathcomp Require Import div choice fintype tuple finfun bigop prime. +From mathcomp Require Import div choice fintype tuple finfun bigop prime order. From mathcomp Require Import ssralg poly ssrnum ssrint rat matrix. From mathcomp Require Import polydiv finalg perm zmodp mxalgebra vector. @@ -46,7 +46,7 @@ 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. Definition divz (m d : int) := @@ -79,7 +79,7 @@ Proof. by case: d => // d; rewrite /divz /= mul1r. Qed. Lemma divzN m d : (m %/ - d)%Z = - (m %/ d)%Z. Proof. by case: m => n; rewrite /divz /= sgzN abszN mulNr. Qed. -Lemma divz_abs m d : (m %/ `|d|)%Z = (-1) ^+ (d < 0)%R * (m %/ d)%Z. +Lemma divz_abs (m d : int) : (m %/ `|d|)%Z = (-1) ^+ (d < 0)%R * (m %/ d)%Z. Proof. by rewrite {3}[d]intEsign !mulr_sign; case: ifP => -> //; rewrite divzN opprK. Qed. @@ -132,7 +132,7 @@ Qed. Lemma divzMDl q m d : d != 0 -> ((q * d + m) %/ d)%Z = q + (m %/ d)%Z. Proof. -rewrite neqr_lt -oppr_gt0 => nz_d. +rewrite neq_lt -oppr_gt0 => nz_d. wlog{nz_d} d_gt0: q d / d > 0; last case: d => // d in d_gt0 *. move=> IH; case/orP: nz_d => /IH// /(_ (- q)). by rewrite mulrNN !divzN -opprD => /oppr_inj. @@ -179,8 +179,8 @@ Lemma divzMpl p m d : p > 0 -> (p * m %/ (p * d) = m %/ d)%Z. Proof. case: p => // p p_gt0; wlog d_gt0: d / d > 0; last case: d => // d in d_gt0 *. by move=> IH; case/intP: d => [|d|d]; rewrite ?mulr0 ?divz0 ?mulrN ?divzN ?IH. -rewrite {1}(divz_eq m d) mulrDr mulrCA divzMDl ?mulf_neq0 ?gtr_eqF // addrC. -rewrite divz_small ?add0r // PoszM pmulr_rge0 ?modz_ge0 ?gtr_eqF //=. +rewrite {1}(divz_eq m d) mulrDr mulrCA divzMDl ?mulf_neq0 ?gt_eqF // addrC. +rewrite divz_small ?add0r // PoszM pmulr_rge0 ?modz_ge0 ?gt_eqF //=. by rewrite ltr_pmul2l ?ltz_pmod. Qed. Arguments divzMpl [p m d]. @@ -203,19 +203,20 @@ Qed. Lemma ltz_ceil m d : d > 0 -> m < ((m %/ d)%Z + 1) * d. Proof. -by case: d => // d d_gt0; rewrite mulrDl mul1r -ltr_subl_addl ltz_mod ?gtr_eqF. +by case: d => // d d_gt0; rewrite mulrDl mul1r -ltr_subl_addl ltz_mod ?gt_eqF. Qed. Lemma ltz_divLR m n d : d > 0 -> ((m %/ d)%Z < n) = (m < n * d). Proof. move=> d_gt0; apply/idP/idP. - by rewrite -lez_addr1 -(ler_pmul2r d_gt0); apply: ltr_le_trans (ltz_ceil _ _). -rewrite -(ltr_pmul2r d_gt0 _ n) //; apply: ler_lt_trans (lez_floor _ _). -by rewrite gtr_eqF. + by rewrite -[_ < n]lez_addr1 -(ler_pmul2r d_gt0); + apply: lt_le_trans (ltz_ceil _ _). +rewrite -(ltr_pmul2r d_gt0 _ n) //; apply: le_lt_trans (lez_floor _ _). +by rewrite gt_eqF. Qed. Lemma lez_divRL m n d : d > 0 -> (m <= (n %/ d)%Z) = (m * d <= n). -Proof. by move=> d_gt0; rewrite !lerNgt ltz_divLR. Qed. +Proof. by move=> d_gt0; rewrite !leNgt ltz_divLR. Qed. Lemma divz_ge0 m d : d > 0 -> ((m %/ d)%Z >= 0) = (m >= 0). Proof. by case: d m => // d [] n d_gt0; rewrite (divz_nat, divNz_nat). Qed. @@ -225,9 +226,9 @@ Proof. case: n => // [[|n]] _; first by rewrite mul0r !divz0 div0z. wlog p_gt0: p / p > 0; last case: p => // p in p_gt0 *. by case/intP: p => [|p|p] IH; rewrite ?mulr0 ?divz0 ?mulrN ?divzN // IH. -rewrite {2}(divz_eq m (n.+1%:Z * p)) mulrA mulrAC !divzMDl // ?gtr_eqF //. +rewrite {2}(divz_eq m (n.+1%:Z * p)) mulrA mulrAC !divzMDl // ?gt_eqF //. rewrite [rhs in _ + rhs]divz_small ?addr0 // ltz_divLR // divz_ge0 //. -by rewrite mulrC ltz_pmod ?modz_ge0 ?gtr_eqF ?pmulr_lgt0. +by rewrite mulrC ltz_pmod ?modz_ge0 ?gt_eqF ?pmulr_lgt0. Qed. Lemma modz_small m d : 0 <= m < d -> (m %% d)%Z = m. @@ -1073,4 +1074,3 @@ rewrite -defS -2!mulmxA; have ->: T *m pinvmx T = 1%:M. by apply: (row_free_inj uT); rewrite mul1mx mulmxKpV. by move=> i; rewrite mulmx1 -map_mxM 2!mxE denq_int mxE. 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/algebra/intdiv.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/algebra/intdiv.v') 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) := -- cgit v1.2.3