Library mathcomp.algebra.ssrint
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
From mathcomp Require Import fintype finfun bigop order ssralg countalg ssrnum.
From mathcomp Require Import poly.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
From mathcomp Require Import fintype finfun bigop order ssralg countalg ssrnum.
From mathcomp Require Import poly.
This file develops a basic theory of signed integers, defining:
int == the type of signed integers, with two constructors Posz for
non-negative integers and Negz for negative integers. It
supports the realDomainType interface (and its parents).
n%:Z == explicit cast from nat to int (:= Posz n); displayed as n.
However (Posz m = Posz n) is displayed as (m = n :> int)
(and so are ==, != and <>)
Lemma NegzE : turns (Negz n) into - n.+1%:Z.
x *~ m == m times x, with m : int;
convertible to x *+ n if m is Posz n
convertible to x *- n.+1 if m is Negz n.
m%:~R == the image of m : int in a generic ring (:= 1 *~ m).
x ^ m == x to the m, with m : int;
convertible to x ^+ n if m is Posz n
convertible to x ^- n.+1 if m is Negz n.
sgz x == sign of x : R,
equals (0 : int) if and only x == 0,
equals (1 : int) if x is positive
and (-1 : int) otherwise.
`|m|%N == the n : nat such that `|m|%R = n%:Z, for m : int.
`|m - n|%N == the distance between m and n; the '-' is specialized to
the int type, so m and n can be either of type nat or int
thanks to the Posz coercion; m and n are however parsed in
the %N scope. The IntDist submodule provides this notation
and the corresponding theory independently of the rest of
of the int and ssralg libraries (and notations).
Warning: due to the declaration of Posz as a coercion, two terms might be
displayed the same while not being convertible, for instance:
(Posz (x - y)) and (Posz x) - (Posz y) for x, y : nat.
Set Implicit Arguments.
Declare Scope int_scope.
Declare Scope distn_scope.
Declare Scope rat_scope.
Reserved Notation "n %:Z" (at level 2, left associativity, format "n %:Z").
Reserved Notation "n = m :> 'int'"
(at level 70, m at next level, format "n = m :> 'int'", only printing).
Reserved Notation "n == m :> 'int'"
(at level 70, m at next level, format "n == m :> 'int'", only printing).
Reserved Notation "n != m :> 'int'"
(at level 70, m at next level, format "n != m :> 'int'", only printing).
Reserved Notation "n <> m :> 'int'"
(at level 70, m at next level, format "n <> m :> 'int'", only printing).
Import Order.TTheory GRing.Theory Num.Theory.
Delimit Scope int_scope with Z.
Local Open Scope int_scope.
Defining int
This must be deferred to module DistInt to work around the design flaws of
the Coq module system.
Coercion Posz : nat >-> int.
Notation "n %:Z" := (Posz n) (only parsing) : int_scope.
Notation "n %:Z" := (Posz n) (only parsing) : ring_scope.
Notation "n = m :> 'int'" := (Posz n = Posz m) (only printing) : ring_scope.
Notation "n == m :> 'int'" := (Posz n == Posz m) (only printing) : ring_scope.
Notation "n != m :> 'int'" := (Posz n != Posz m) (only printing) : ring_scope.
Notation "n <> m :> 'int'" := (Posz n ≠ Posz m) (only printing) : ring_scope.
Definition natsum_of_int (m : int) : nat + nat :=
match m with Posz p ⇒ inl _ p | Negz n ⇒ inr _ n end.
Definition int_of_natsum (m : nat + nat) :=
match m with inl p ⇒ Posz p | inr n ⇒ Negz n end.
Lemma natsum_of_intK : cancel natsum_of_int int_of_natsum.
Definition int_eqMixin := CanEqMixin natsum_of_intK.
Definition int_countMixin := CanCountMixin natsum_of_intK.
Definition int_choiceMixin := CountChoiceMixin int_countMixin.
Canonical int_eqType := Eval hnf in EqType int int_eqMixin.
Canonical int_choiceType := Eval hnf in ChoiceType int int_choiceMixin.
Canonical int_countType := Eval hnf in CountType int int_countMixin.
Lemma eqz_nat (m n : nat) : (m%:Z == n%:Z) = (m == n).
Module intZmod.
Section intZmod.
Definition addz (m n : int) :=
match m, n with
| Posz m', Posz n' ⇒ Posz (m' + n')
| Negz m', Negz n' ⇒ Negz (m' + n').+1
| Posz m', Negz n' ⇒ if n' < m' then Posz (m' - n'.+1) else Negz (n' - m')
| Negz n', Posz m' ⇒ if n' < m' then Posz (m' - n'.+1) else Negz (n' - m')
end.
Definition oppz m := nosimpl
match m with
| Posz n ⇒ if n is (n'.+1)%N then Negz n' else Posz 0
| Negz n ⇒ Posz (n.+1)%N
end.
Lemma PoszD : {morph Posz : m n / (m + n)%N >-> m + n}.
Lemma NegzE (n : nat) : Negz n = - n.+1.
Lemma int_rect (P : int → Type) :
P 0 → (∀ n : nat, P n → P (n.+1))
→ (∀ n : nat, P (- n) → P (- (n.+1)))
→ ∀ n : int, P n.
Definition int_rec := int_rect.
Definition int_ind := int_rect.
Variant int_spec (x : int) : int → Type :=
| ZintNull of x = 0 : int_spec x 0
| ZintPos n of x = n.+1 : int_spec x n.+1
| ZintNeg n of x = - (n.+1)%:Z : int_spec x (- n.+1).
Lemma intP x : int_spec x x.
Lemma addzC : commutative addz.
Lemma add0z : left_id 0 addz.
Lemma oppzK : involutive oppz.
Lemma oppz_add : {morph oppz : m n / m + n}.
Lemma add1Pz (n : int) : 1 + (n - 1) = n.
Lemma subSz1 (n : int) : 1 + n - 1 = n.
Lemma addSnz (m : nat) (n : int) : (m.+1%N) + n = 1 + (m + n).
Lemma addSz (m n : int) : (1 + m) + n = 1 + (m + n).
Lemma addPz (m n : int) : (m - 1) + n = (m + n) - 1.
Lemma addzA : associative addz.
Lemma addNz : left_inverse (0:int) oppz addz.
Lemma predn_int (n : nat) : 0 < n → n.-1%:Z = n - 1.
Definition Mixin := ZmodMixin addzA addzC add0z addNz.
End intZmod.
End intZmod.
Canonical int_ZmodType := ZmodType int intZmod.Mixin.
Local Open Scope ring_scope.
Section intZmoduleTheory.
Lemma PoszD : {morph Posz : n m / (n + m)%N >-> n + m}.
Lemma NegzE (n : nat) : Negz n = -(n.+1)%:Z.
Lemma int_rect (P : int → Type) :
P 0 → (∀ n : nat, P n → P (n.+1)%N)
→ (∀ n : nat, P (- (n%:Z)) → P (- (n.+1%N%:Z)))
→ ∀ n : int, P n.
Definition int_rec := int_rect.
Definition int_ind := int_rect.
Variant int_spec (x : int) : int → Type :=
| ZintNull : int_spec x 0
| ZintPos n : int_spec x n.+1
| ZintNeg n : int_spec x (- (n.+1)%:Z).
Lemma intP x : int_spec x x.
Definition oppz_add := (@opprD [zmodType of int]).
Lemma subzn (m n : nat) : (n ≤ m)%N → m%:Z - n%:Z = (m - n)%N.
Lemma subzSS (m n : nat) : m.+1%:Z - n.+1%:Z = m%:Z - n%:Z.
End intZmoduleTheory.
Module intRing.
Section intRing.
Definition mulz (m n : int) :=
match m, n with
| Posz m', Posz n' ⇒ (m' × n')%N%:Z
| Negz m', Negz n' ⇒ (m'.+1%N × n'.+1%N)%N%:Z
| Posz m', Negz n' ⇒ - (m' × (n'.+1%N))%N%:Z
| Negz n', Posz m' ⇒ - (m' × (n'.+1%N))%N%:Z
end.
Lemma mul0z : left_zero 0 *%Z.
Lemma mulzC : commutative mulz.
Lemma mulz0 : right_zero 0 *%Z.
Lemma mulzN (m n : int) : (m × (- n))%Z = - (m × n)%Z.
Lemma mulNz (m n : int) : ((- m) × n)%Z = - (m × n)%Z.
Lemma mulzA : associative mulz.
Lemma mul1z : left_id 1%Z mulz.
Lemma mulzS (x : int) (n : nat) : (x × n.+1%:Z)%Z = x + (x × n)%Z.
Lemma mulz_addl : left_distributive mulz (+%R).
Lemma nonzero1z : 1%Z != 0.
Definition comMixin := ComRingMixin mulzA mulzC mul1z mulz_addl nonzero1z.
End intRing.
End intRing.
Canonical int_Ring := Eval hnf in RingType int intRing.comMixin.
Canonical int_comRing := Eval hnf in ComRingType int intRing.mulzC.
Section intRingTheory.
Implicit Types m n : int.
Lemma PoszM : {morph Posz : n m / (n × m)%N >-> n × m}.
Lemma intS (n : nat) : n.+1%:Z = 1 + n%:Z.
Lemma predn_int (n : nat) : (0 < n)%N → n.-1%:Z = n%:Z - 1.
End intRingTheory.
Module intUnitRing.
Section intUnitRing.
Implicit Types m n : int.
Definition unitz := [qualify a n : int | (n == 1) || (n == -1)].
Definition invz n : int := n.
Lemma mulVz : {in unitz, left_inverse 1%R invz *%R}.
Lemma mulzn_eq1 m (n : nat) : (m × n == 1) = (m == 1) && (n == 1%N).
Lemma unitzPl m n : n × m = 1 → m \is a unitz.
Lemma invz_out : {in [predC unitz], invz =1 id}.
Lemma idomain_axiomz m n : m × n = 0 → (m == 0) || (n == 0).
Definition comMixin := ComUnitRingMixin mulVz unitzPl invz_out.
End intUnitRing.
End intUnitRing.
Canonical int_unitRingType :=
Eval hnf in UnitRingType int intUnitRing.comMixin.
Canonical int_comUnitRing := Eval hnf in [comUnitRingType of int].
Canonical int_idomainType :=
Eval hnf in IdomainType int intUnitRing.idomain_axiomz.
Canonical int_countZmodType := [countZmodType of int].
Canonical int_countRingType := [countRingType of int].
Canonical int_countComRingType := [countComRingType of int].
Canonical int_countUnitRingType := [countUnitRingType of int].
Canonical int_countComUnitRingType := [countComUnitRingType of int].
Canonical int_countIdomainType := [countIdomainType of int].
Definition absz m := match m with Posz p ⇒ p | Negz n ⇒ n.+1 end.
Notation "m - n" :=
(@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope.
Arguments absz m%distn_scope.
Module intOrdered.
Section intOrdered.
Implicit Types m n p : int.
Definition lez m n :=
match m, n with
| Posz m', Posz n' ⇒ (m' ≤ n')%N
| Posz m', Negz n' ⇒ false
| Negz m', Posz n' ⇒ true
| Negz m', Negz n' ⇒ (n' ≤ m')%N
end.
Definition ltz m n :=
match m, n with
| Posz m', Posz n' ⇒ (m' < n')%N
| Posz m', Negz n' ⇒ false
| Negz m', Posz n' ⇒ true
| Negz m', Negz n' ⇒ (n' < m')%N
end.
Fact lez_add m n : lez 0 m → lez 0 n → lez 0 (m + n).
Fact lez_mul m n : lez 0 m → lez 0 n → lez 0 (m × n).
Fact lez_anti m : lez 0 m → lez m 0 → m = 0.
Lemma subz_ge0 m n : lez 0 (n - m) = lez m n.
Fact lez_total m n : lez m n || lez n m.
Fact normzN m : normz (- m) = normz m.
Fact gez0_norm m : lez 0 m → normz m = m.
Fact ltz_def m n : (ltz m n) = (n != m) && (lez m n).
Definition Mixin : realLeMixin int_idomainType :=
RealLeMixin
lez_add lez_mul lez_anti subz_ge0 (lez_total 0) normzN gez0_norm ltz_def.
End intOrdered.
End intOrdered.
Canonical int_porderType := POrderType ring_display int intOrdered.Mixin.
Canonical int_latticeType := LatticeType int intOrdered.Mixin.
Canonical int_distrLatticeType := DistrLatticeType int intOrdered.Mixin.
Canonical int_orderType := OrderType int intOrdered.lez_total.
Canonical int_numDomainType := NumDomainType int intOrdered.Mixin.
Canonical int_normedZmodType := NormedZmodType int int intOrdered.Mixin.
Canonical int_realDomainType := [realDomainType of int].
Section intOrderedTheory.
Implicit Types m n p : nat.
Implicit Types x y z : int.
Lemma lez_nat m n : (m ≤ n :> int) = (m ≤ n)%N.
Lemma ltz_nat m n : (m < n :> int) = (m < n)%N.
Definition ltez_nat := (lez_nat, ltz_nat).
Lemma leNz_nat m n : (- m%:Z ≤ n).
Lemma ltNz_nat m n : (- m%:Z < n) = (m != 0%N) || (n != 0%N).
Definition lteNz_nat := (leNz_nat, ltNz_nat).
Lemma lezN_nat m n : (m%:Z ≤ - n%:Z) = (m == 0%N) && (n == 0%N).
Lemma ltzN_nat m n : (m%:Z < - n%:Z) = false.
Lemma le0z_nat n : 0 ≤ n :> int.
Lemma lez0_nat n : n ≤ 0 :> int = (n == 0%N :> nat).
Definition ltezN_nat := (lezN_nat, ltzN_nat).
Definition ltez_natE := (ltez_nat, lteNz_nat, ltezN_nat, le0z_nat, lez0_nat).
Lemma gtz0_ge1 x : (0 < x) = (1 ≤ x).
Lemma lez_add1r x y : (1 + x ≤ y) = (x < y).
Lemma lez_addr1 x y : (x + 1 ≤ y) = (x < y).
Lemma ltz_add1r x y : (x < 1 + y) = (x ≤ y).
Lemma ltz_addr1 x y : (x < y + 1) = (x ≤ y).
End intOrderedTheory.
Bind Scope ring_scope with int.
definition of intmul
Definition intmul (R : zmodType) (x : R) (n : int) := nosimpl
match n with
| Posz n ⇒ (x *+ n)%R
| Negz n ⇒ (x *- (n.+1))%R
end.
Notation "*~%R" := (@intmul _) (at level 0, format " *~%R") : fun_scope.
Notation "x *~ n" := (intmul x n)
(at level 40, left associativity, format "x *~ n") : ring_scope.
Notation intr := ( *~%R 1).
Notation "n %:~R" := (1 *~ n)%R
(at level 2, left associativity, format "n %:~R") : ring_scope.
Lemma pmulrn (R : zmodType) (x : R) (n : nat) : x *+ n = x *~ n%:Z.
Lemma nmulrn (R : zmodType) (x : R) (n : nat) : x *- n = x *~ - n%:Z.
Section ZintLmod.
Definition zmodule (M : Type) : Type := M.
Variable M : zmodType.
Implicit Types m n : int.
Implicit Types x y z : M.
Fact mulrzA_C m n x : (x *~ n) *~ m = x *~ (m × n).
Fact mulrzAC m n x : (x *~ n) *~ m = (x *~ m) *~ n.
Fact mulr1z (x : M) : x *~ 1 = x.
Fact mulrzDr m : {morph ( *~%R^~ m : M → M) : x y / x + y}.
Lemma mulrzBl_nat (m n : nat) x : x *~ (m%:Z - n%:Z) = x *~ m - x *~ n.
Fact mulrzDl x : {morph *~%R x : m n / m + n}.
Definition Mint_LmodMixin :=
@LmodMixin _ [zmodType of M] (fun n x ⇒ x *~ n)
mulrzA_C mulr1z mulrzDr mulrzDl.
Canonical Mint_LmodType := LmodType int M^z Mint_LmodMixin.
Lemma scalezrE n x : n *: (x : M^z) = x *~ n.
Lemma mulrzA x m n : x *~ (m × n) = x *~ m *~ n.
Lemma mulr0z x : x *~ 0 = 0.
Lemma mul0rz n : 0 *~ n = 0 :> M.
Lemma mulrNz x n : x *~ (- n) = - (x *~ n).
Lemma mulrN1z x : x *~ (- 1) = - x.
Lemma mulNrz x n : (- x) *~ n = - (x *~ n).
Lemma mulrzBr x m n : x *~ (m - n) = x *~ m - x *~ n.
Lemma mulrzBl x y n : (x - y) *~ n = x *~ n - y *~ n.
Lemma mulrz_nat (n : nat) x : x *~ n%:R = x *+ n.
Lemma mulrz_sumr : ∀ x I r (P : pred I) F,
x *~ (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) x *~ F i.
Lemma mulrz_suml : ∀ n I r (P : pred I) (F : I → M),
(\sum_(i <- r | P i) F i) *~ n= \sum_(i <- r | P i) F i *~ n.
Canonical intmul_additive x := Additive (@mulrzBr x).
End ZintLmod.
Lemma ffunMzE (I : finType) (M : zmodType) (f : {ffun I → M}) z x :
(f *~ z) x = f x *~ z.
Lemma intz (n : int) : n%:~R = n.
Lemma natz (n : nat) : n%:R = n%:Z :> int.
Section RintMod.
Variable R : ringType.
Implicit Types m n : int.
Implicit Types x y z : R.
Lemma mulrzAl n x y : (x *~ n) × y = (x × y) *~ n.
Lemma mulrzAr n x y : x × (y *~ n) = (x × y) *~ n.
Lemma mulrzl x n : n%:~R × x = x *~ n.
Lemma mulrzr x n : x × n%:~R = x *~ n.
Lemma mulNrNz n x : (-x) *~ (-n) = x *~ n.
Lemma mulrbz x (b : bool) : x *~ b = (if b then x else 0).
Lemma intrD m n : (m + n)%:~R = m%:~R + n%:~R :> R.
Lemma intrM m n : (m × n)%:~R = m%:~R × n%:~R :> R.
Lemma intmul1_is_rmorphism : rmorphism ( *~%R (1 : R)).
Canonical intmul1_rmorphism := RMorphism intmul1_is_rmorphism.
Lemma mulr2z n : n *~ 2 = n + n.
End RintMod.
Lemma mulrzz m n : m *~ n = m × n.
Lemma mulz2 n : n × 2%:Z = n + n.
Lemma mul2z n : 2%:Z × n = n + n.
Section LMod.
Variable R : ringType.
Variable V : (lmodType R).
Implicit Types m n : int.
Implicit Types x y z : R.
Implicit Types u v w : V.
Lemma scaler_int n v : n%:~R *: v = v *~ n.
Lemma scalerMzl a v n : (a *: v) *~ n = (a *~ n) *: v.
Lemma scalerMzr a v n : (a *: v) *~ n = a *: (v *~ n).
End LMod.
Lemma mulrz_int (M : zmodType) (n : int) (x : M) : x *~ n%:~R = x *~ n.
Section MorphTheory.
Section Additive.
Variables (U V : zmodType) (f : {additive U → V}).
Lemma raddfMz n : {morph f : x / x *~ n}.
End Additive.
Section Multiplicative.
Variables (R S : ringType) (f : {rmorphism R → S}).
Lemma rmorphMz : ∀ n, {morph f : x / x *~ n}.
Lemma rmorph_int : ∀ n, f n%:~R = n%:~R.
End Multiplicative.
Section Linear.
Variable R : ringType.
Variables (U V : lmodType R) (f : {linear U → V}).
Lemma linearMn : ∀ n, {morph f : x / x *~ n}.
End Linear.
Lemma raddf_int_scalable (aV rV : lmodType int) (f : {additive aV → rV}) :
scalable f.
Section Zintmul1rMorph.
Variable R : ringType.
Lemma commrMz (x y : R) n : GRing.comm x y → GRing.comm x (y *~ n).
Lemma commr_int (x : R) n : GRing.comm x n%:~R.
End Zintmul1rMorph.
Section ZintBigMorphism.
Variable R : ringType.
Lemma sumMz : ∀ I r (P : pred I) F,
(\sum_(i <- r | P i) F i)%N%:~R = \sum_(i <- r | P i) ((F i)%:~R) :> R.
Lemma prodMz : ∀ I r (P : pred I) F,
(\prod_(i <- r | P i) F i)%N%:~R = \prod_(i <- r | P i) ((F i)%:~R) :> R.
End ZintBigMorphism.
Section Frobenius.
Variable R : ringType.
Implicit Types x y : R.
Variable p : nat.
Hypothesis charFp : p \in [char R].
Lemma Frobenius_autMz x n : (x *~ n)^f = x^f *~ n.
Lemma Frobenius_aut_int n : (n%:~R)^f = n%:~R.
End Frobenius.
Section NumMorphism.
Section PO.
Variables (R : numDomainType).
Implicit Types n m : int.
Implicit Types x y : R.
Lemma rmorphzP (f : {rmorphism int → R}) : f =1 ( *~%R 1).
match n with
| Posz n ⇒ (x *+ n)%R
| Negz n ⇒ (x *- (n.+1))%R
end.
Notation "*~%R" := (@intmul _) (at level 0, format " *~%R") : fun_scope.
Notation "x *~ n" := (intmul x n)
(at level 40, left associativity, format "x *~ n") : ring_scope.
Notation intr := ( *~%R 1).
Notation "n %:~R" := (1 *~ n)%R
(at level 2, left associativity, format "n %:~R") : ring_scope.
Lemma pmulrn (R : zmodType) (x : R) (n : nat) : x *+ n = x *~ n%:Z.
Lemma nmulrn (R : zmodType) (x : R) (n : nat) : x *- n = x *~ - n%:Z.
Section ZintLmod.
Definition zmodule (M : Type) : Type := M.
Variable M : zmodType.
Implicit Types m n : int.
Implicit Types x y z : M.
Fact mulrzA_C m n x : (x *~ n) *~ m = x *~ (m × n).
Fact mulrzAC m n x : (x *~ n) *~ m = (x *~ m) *~ n.
Fact mulr1z (x : M) : x *~ 1 = x.
Fact mulrzDr m : {morph ( *~%R^~ m : M → M) : x y / x + y}.
Lemma mulrzBl_nat (m n : nat) x : x *~ (m%:Z - n%:Z) = x *~ m - x *~ n.
Fact mulrzDl x : {morph *~%R x : m n / m + n}.
Definition Mint_LmodMixin :=
@LmodMixin _ [zmodType of M] (fun n x ⇒ x *~ n)
mulrzA_C mulr1z mulrzDr mulrzDl.
Canonical Mint_LmodType := LmodType int M^z Mint_LmodMixin.
Lemma scalezrE n x : n *: (x : M^z) = x *~ n.
Lemma mulrzA x m n : x *~ (m × n) = x *~ m *~ n.
Lemma mulr0z x : x *~ 0 = 0.
Lemma mul0rz n : 0 *~ n = 0 :> M.
Lemma mulrNz x n : x *~ (- n) = - (x *~ n).
Lemma mulrN1z x : x *~ (- 1) = - x.
Lemma mulNrz x n : (- x) *~ n = - (x *~ n).
Lemma mulrzBr x m n : x *~ (m - n) = x *~ m - x *~ n.
Lemma mulrzBl x y n : (x - y) *~ n = x *~ n - y *~ n.
Lemma mulrz_nat (n : nat) x : x *~ n%:R = x *+ n.
Lemma mulrz_sumr : ∀ x I r (P : pred I) F,
x *~ (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) x *~ F i.
Lemma mulrz_suml : ∀ n I r (P : pred I) (F : I → M),
(\sum_(i <- r | P i) F i) *~ n= \sum_(i <- r | P i) F i *~ n.
Canonical intmul_additive x := Additive (@mulrzBr x).
End ZintLmod.
Lemma ffunMzE (I : finType) (M : zmodType) (f : {ffun I → M}) z x :
(f *~ z) x = f x *~ z.
Lemma intz (n : int) : n%:~R = n.
Lemma natz (n : nat) : n%:R = n%:Z :> int.
Section RintMod.
Variable R : ringType.
Implicit Types m n : int.
Implicit Types x y z : R.
Lemma mulrzAl n x y : (x *~ n) × y = (x × y) *~ n.
Lemma mulrzAr n x y : x × (y *~ n) = (x × y) *~ n.
Lemma mulrzl x n : n%:~R × x = x *~ n.
Lemma mulrzr x n : x × n%:~R = x *~ n.
Lemma mulNrNz n x : (-x) *~ (-n) = x *~ n.
Lemma mulrbz x (b : bool) : x *~ b = (if b then x else 0).
Lemma intrD m n : (m + n)%:~R = m%:~R + n%:~R :> R.
Lemma intrM m n : (m × n)%:~R = m%:~R × n%:~R :> R.
Lemma intmul1_is_rmorphism : rmorphism ( *~%R (1 : R)).
Canonical intmul1_rmorphism := RMorphism intmul1_is_rmorphism.
Lemma mulr2z n : n *~ 2 = n + n.
End RintMod.
Lemma mulrzz m n : m *~ n = m × n.
Lemma mulz2 n : n × 2%:Z = n + n.
Lemma mul2z n : 2%:Z × n = n + n.
Section LMod.
Variable R : ringType.
Variable V : (lmodType R).
Implicit Types m n : int.
Implicit Types x y z : R.
Implicit Types u v w : V.
Lemma scaler_int n v : n%:~R *: v = v *~ n.
Lemma scalerMzl a v n : (a *: v) *~ n = (a *~ n) *: v.
Lemma scalerMzr a v n : (a *: v) *~ n = a *: (v *~ n).
End LMod.
Lemma mulrz_int (M : zmodType) (n : int) (x : M) : x *~ n%:~R = x *~ n.
Section MorphTheory.
Section Additive.
Variables (U V : zmodType) (f : {additive U → V}).
Lemma raddfMz n : {morph f : x / x *~ n}.
End Additive.
Section Multiplicative.
Variables (R S : ringType) (f : {rmorphism R → S}).
Lemma rmorphMz : ∀ n, {morph f : x / x *~ n}.
Lemma rmorph_int : ∀ n, f n%:~R = n%:~R.
End Multiplicative.
Section Linear.
Variable R : ringType.
Variables (U V : lmodType R) (f : {linear U → V}).
Lemma linearMn : ∀ n, {morph f : x / x *~ n}.
End Linear.
Lemma raddf_int_scalable (aV rV : lmodType int) (f : {additive aV → rV}) :
scalable f.
Section Zintmul1rMorph.
Variable R : ringType.
Lemma commrMz (x y : R) n : GRing.comm x y → GRing.comm x (y *~ n).
Lemma commr_int (x : R) n : GRing.comm x n%:~R.
End Zintmul1rMorph.
Section ZintBigMorphism.
Variable R : ringType.
Lemma sumMz : ∀ I r (P : pred I) F,
(\sum_(i <- r | P i) F i)%N%:~R = \sum_(i <- r | P i) ((F i)%:~R) :> R.
Lemma prodMz : ∀ I r (P : pred I) F,
(\prod_(i <- r | P i) F i)%N%:~R = \prod_(i <- r | P i) ((F i)%:~R) :> R.
End ZintBigMorphism.
Section Frobenius.
Variable R : ringType.
Implicit Types x y : R.
Variable p : nat.
Hypothesis charFp : p \in [char R].
Lemma Frobenius_autMz x n : (x *~ n)^f = x^f *~ n.
Lemma Frobenius_aut_int n : (n%:~R)^f = n%:~R.
End Frobenius.
Section NumMorphism.
Section PO.
Variables (R : numDomainType).
Implicit Types n m : int.
Implicit Types x y : R.
Lemma rmorphzP (f : {rmorphism int → R}) : f =1 ( *~%R 1).
intmul and ler/ltr
Lemma ler_pmulz2r n (hn : 0 < n) : {mono *~%R^~ n :x y / x ≤ y :> R}.
Lemma ltr_pmulz2r n (hn : 0 < n) : {mono *~%R^~ n : x y / x < y :> R}.
Lemma ler_nmulz2r n (hn : n < 0) : {mono *~%R^~ n : x y /~ x ≤ y :> R}.
Lemma ltr_nmulz2r n (hn : n < 0) : {mono *~%R^~ n : x y /~ x < y :> R}.
Lemma ler_wpmulz2r n (hn : 0 ≤ n) : {homo *~%R^~ n : x y / x ≤ y :> R}.
Lemma ler_wnmulz2r n (hn : n ≤ 0) : {homo *~%R^~ n : x y /~ x ≤ y :> R}.
Lemma mulrz_ge0 x n (x0 : 0 ≤ x) (n0 : 0 ≤ n) : 0 ≤ x *~ n.
Lemma mulrz_le0 x n (x0 : x ≤ 0) (n0 : n ≤ 0) : 0 ≤ x *~ n.
Lemma mulrz_ge0_le0 x n (x0 : 0 ≤ x) (n0 : n ≤ 0) : x *~ n ≤ 0.
Lemma mulrz_le0_ge0 x n (x0 : x ≤ 0) (n0 : 0 ≤ n) : x *~ n ≤ 0.
Lemma pmulrz_lgt0 x n (n0 : 0 < n) : 0 < x *~ n = (0 < x).
Lemma nmulrz_lgt0 x n (n0 : n < 0) : 0 < x *~ n = (x < 0).
Lemma pmulrz_llt0 x n (n0 : 0 < n) : x *~ n < 0 = (x < 0).
Lemma nmulrz_llt0 x n (n0 : n < 0) : x *~ n < 0 = (0 < x).
Lemma pmulrz_lge0 x n (n0 : 0 < n) : 0 ≤ x *~ n = (0 ≤ x).
Lemma nmulrz_lge0 x n (n0 : n < 0) : 0 ≤ x *~ n = (x ≤ 0).
Lemma pmulrz_lle0 x n (n0 : 0 < n) : x *~ n ≤ 0 = (x ≤ 0).
Lemma nmulrz_lle0 x n (n0 : n < 0) : x *~ n ≤ 0 = (0 ≤ x).
Lemma ler_wpmulz2l x (hx : 0 ≤ x) : {homo *~%R x : x y / x ≤ y}.
Lemma ler_wnmulz2l x (hx : x ≤ 0) : {homo *~%R x : x y /~ x ≤ y}.
Lemma ler_pmulz2l x (hx : 0 < x) : {mono *~%R x : x y / x ≤ y}.
Lemma ler_nmulz2l x (hx : x < 0) : {mono *~%R x : x y /~ x ≤ y}.
Lemma ltr_pmulz2l x (hx : 0 < x) : {mono *~%R x : x y / x < y}.
Lemma ltr_nmulz2l x (hx : x < 0) : {mono *~%R x : x y /~ x < y}.
Lemma pmulrz_rgt0 x n (x0 : 0 < x) : 0 < x *~ n = (0 < n).
Lemma nmulrz_rgt0 x n (x0 : x < 0) : 0 < x *~ n = (n < 0).
Lemma pmulrz_rlt0 x n (x0 : 0 < x) : x *~ n < 0 = (n < 0).
Lemma nmulrz_rlt0 x n (x0 : x < 0) : x *~ n < 0 = (0 < n).
Lemma pmulrz_rge0 x n (x0 : 0 < x) : 0 ≤ x *~ n = (0 ≤ n).
Lemma nmulrz_rge0 x n (x0 : x < 0) : 0 ≤ x *~ n = (n ≤ 0).
Lemma pmulrz_rle0 x n (x0 : 0 < x) : x *~ n ≤ 0 = (n ≤ 0).
Lemma nmulrz_rle0 x n (x0 : x < 0) : x *~ n ≤ 0 = (0 ≤ n).
Lemma mulrIz x (hx : x != 0) : injective ( *~%R x).
Lemma ler_int m n : (m%:~R ≤ n%:~R :> R) = (m ≤ n).
Lemma ltr_int m n : (m%:~R < n%:~R :> R) = (m < n).
Lemma eqr_int m n : (m%:~R == n%:~R :> R) = (m == n).
Lemma ler0z n : (0 ≤ n%:~R :> R) = (0 ≤ n).
Lemma ltr0z n : (0 < n%:~R :> R) = (0 < n).
Lemma lerz0 n : (n%:~R ≤ 0 :> R) = (n ≤ 0).
Lemma ltrz0 n : (n%:~R < 0 :> R) = (n < 0).
Lemma ler1z (n : int) : (1 ≤ n%:~R :> R) = (1 ≤ n).
Lemma ltr1z (n : int) : (1 < n%:~R :> R) = (1 < n).
Lemma lerz1 n : (n%:~R ≤ 1 :> R) = (n ≤ 1).
Lemma ltrz1 n : (n%:~R < 1 :> R) = (n < 1).
Lemma intr_eq0 n : (n%:~R == 0 :> R) = (n == 0).
Lemma mulrz_eq0 x n : (x *~ n == 0) = ((n == 0) || (x == 0)).
Lemma mulrz_neq0 x n : x *~ n != 0 = ((n != 0) && (x != 0)).
Lemma realz n : (n%:~R : R) \in Num.real.
Hint Resolve realz : core.
Definition intr_inj := @mulrIz 1 (oner_neq0 R).
End PO.
End NumMorphism.
End MorphTheory.
Arguments intr_inj {R} [x1 x2].
Definition exprz (R : unitRingType) (x : R) (n : int) := nosimpl
match n with
| Posz n ⇒ x ^+ n
| Negz n ⇒ x ^- (n.+1)
end.
Notation "x ^ n" := (exprz x n) : ring_scope.
Section ExprzUnitRing.
Variable R : unitRingType.
Implicit Types x y : R.
Implicit Types m n : int.
Lemma exprnP x (n : nat) : x ^+ n = x ^ n.
Lemma exprnN x (n : nat) : x ^- n = x ^ -n%:Z.
Lemma expr0z x : x ^ 0 = 1.
Lemma expr1z x : x ^ 1 = x.
Lemma exprN1 x : x ^ (-1) = x^-1.
Lemma invr_expz x n : (x ^ n)^-1 = x ^ (- n).
Lemma exprz_inv x n : (x^-1) ^ n = x ^ (- n).
Lemma exp1rz n : 1 ^ n = 1 :> R.
Lemma exprSz x (n : nat) : x ^ n.+1 = x × x ^ n.
Lemma exprSzr x (n : nat) : x ^ n.+1 = x ^ n × x.
Fact exprzD_nat x (m n : nat) : x ^ (m%:Z + n) = x ^ m × x ^ n.
Fact exprzD_Nnat x (m n : nat) : x ^ (-m%:Z + -n%:Z) = x ^ (-m%:Z) × x ^ (-n%:Z).
Lemma exprzD_ss x m n : (0 ≤ m) && (0 ≤ n) || (m ≤ 0) && (n ≤ 0)
→ x ^ (m + n) = x ^ m × x ^ n.
Lemma exp0rz n : 0 ^ n = (n == 0)%:~R :> R.
Lemma commrXz x y n : GRing.comm x y → GRing.comm x (y ^ n).
Lemma exprMz_comm x y n : x \is a GRing.unit → y \is a GRing.unit →
GRing.comm x y → (x × y) ^ n = x ^ n × y ^ n.
Lemma commrXz_wmulls x y n :
0 ≤ n → GRing.comm x y → (x × y) ^ n = x ^ n × y ^ n.
Lemma unitrXz x n (ux : x \is a GRing.unit) : x ^ n \is a GRing.unit.
Lemma exprzDr x (ux : x \is a GRing.unit) m n : x ^ (m + n) = x ^ m × x ^ n.
Lemma exprz_exp x m n : (x ^ m) ^ n = (x ^ (m × n)).
Lemma exprzAC x m n : (x ^ m) ^ n = (x ^ n) ^ m.
Lemma exprz_out x n (nux : x \isn't a GRing.unit) (hn : 0 ≤ n) :
x ^ (- n) = x ^ n.
End ExprzUnitRing.
Section Exprz_Zint_UnitRing.
Variable R : unitRingType.
Implicit Types x y : R.
Implicit Types m n : int.
Lemma exprz_pmulzl x m n : 0 ≤ n → (x *~ m) ^ n = x ^ n *~ (m ^ n).
Lemma exprz_pintl m n (hn : 0 ≤ n) : m%:~R ^ n = (m ^ n)%:~R :> R.
Lemma exprzMzl x m n (ux : x \is a GRing.unit) (um : m%:~R \is a @GRing.unit R):
(x *~ m) ^ n = (m%:~R ^ n) × x ^ n :> R.
Lemma expNrz x n : (- x) ^ n = (-1) ^ n × x ^ n :> R.
Lemma unitr_n0expz x n :
n != 0 → (x ^ n \is a GRing.unit) = (x \is a GRing.unit).
Lemma intrV (n : int) :
n \in [:: 0; 1; -1] → n%:~R ^-1 = n%:~R :> R.
Lemma rmorphXz (R' : unitRingType) (f : {rmorphism R → R'}) n :
{in GRing.unit, {morph f : x / x ^ n}}.
End Exprz_Zint_UnitRing.
Section ExprzIdomain.
Variable R : idomainType.
Implicit Types x y : R.
Implicit Types m n : int.
Lemma expfz_eq0 x n : (x ^ n == 0) = (n != 0) && (x == 0).
Lemma expfz_neq0 x n : x != 0 → x ^ n != 0.
Lemma exprzMl x y n (ux : x \is a GRing.unit) (uy : y \is a GRing.unit) :
(x × y) ^ n = x ^ n × y ^ n.
Lemma expfV (x : R) (i : int) : (x ^ i) ^-1 = (x ^-1) ^ i.
End ExprzIdomain.
Section ExprzField.
Variable F : fieldType.
Implicit Types x y : F.
Implicit Types m n : int.
Lemma expfzDr x m n : x != 0 → x ^ (m + n) = x ^ m × x ^ n.
Lemma expfz_n0addr x m n : m + n != 0 → x ^ (m + n) = x ^ m × x ^ n.
Lemma expfzMl x y n : (x × y) ^ n = x ^ n × y ^ n.
Lemma fmorphXz (R : unitRingType) (f : {rmorphism F → R}) n :
{morph f : x / x ^ n}.
End ExprzField.
Section ExprzOrder.
Variable R : realFieldType.
Implicit Types x y : R.
Implicit Types m n : int.
Lemma ltr_pmulz2r n (hn : 0 < n) : {mono *~%R^~ n : x y / x < y :> R}.
Lemma ler_nmulz2r n (hn : n < 0) : {mono *~%R^~ n : x y /~ x ≤ y :> R}.
Lemma ltr_nmulz2r n (hn : n < 0) : {mono *~%R^~ n : x y /~ x < y :> R}.
Lemma ler_wpmulz2r n (hn : 0 ≤ n) : {homo *~%R^~ n : x y / x ≤ y :> R}.
Lemma ler_wnmulz2r n (hn : n ≤ 0) : {homo *~%R^~ n : x y /~ x ≤ y :> R}.
Lemma mulrz_ge0 x n (x0 : 0 ≤ x) (n0 : 0 ≤ n) : 0 ≤ x *~ n.
Lemma mulrz_le0 x n (x0 : x ≤ 0) (n0 : n ≤ 0) : 0 ≤ x *~ n.
Lemma mulrz_ge0_le0 x n (x0 : 0 ≤ x) (n0 : n ≤ 0) : x *~ n ≤ 0.
Lemma mulrz_le0_ge0 x n (x0 : x ≤ 0) (n0 : 0 ≤ n) : x *~ n ≤ 0.
Lemma pmulrz_lgt0 x n (n0 : 0 < n) : 0 < x *~ n = (0 < x).
Lemma nmulrz_lgt0 x n (n0 : n < 0) : 0 < x *~ n = (x < 0).
Lemma pmulrz_llt0 x n (n0 : 0 < n) : x *~ n < 0 = (x < 0).
Lemma nmulrz_llt0 x n (n0 : n < 0) : x *~ n < 0 = (0 < x).
Lemma pmulrz_lge0 x n (n0 : 0 < n) : 0 ≤ x *~ n = (0 ≤ x).
Lemma nmulrz_lge0 x n (n0 : n < 0) : 0 ≤ x *~ n = (x ≤ 0).
Lemma pmulrz_lle0 x n (n0 : 0 < n) : x *~ n ≤ 0 = (x ≤ 0).
Lemma nmulrz_lle0 x n (n0 : n < 0) : x *~ n ≤ 0 = (0 ≤ x).
Lemma ler_wpmulz2l x (hx : 0 ≤ x) : {homo *~%R x : x y / x ≤ y}.
Lemma ler_wnmulz2l x (hx : x ≤ 0) : {homo *~%R x : x y /~ x ≤ y}.
Lemma ler_pmulz2l x (hx : 0 < x) : {mono *~%R x : x y / x ≤ y}.
Lemma ler_nmulz2l x (hx : x < 0) : {mono *~%R x : x y /~ x ≤ y}.
Lemma ltr_pmulz2l x (hx : 0 < x) : {mono *~%R x : x y / x < y}.
Lemma ltr_nmulz2l x (hx : x < 0) : {mono *~%R x : x y /~ x < y}.
Lemma pmulrz_rgt0 x n (x0 : 0 < x) : 0 < x *~ n = (0 < n).
Lemma nmulrz_rgt0 x n (x0 : x < 0) : 0 < x *~ n = (n < 0).
Lemma pmulrz_rlt0 x n (x0 : 0 < x) : x *~ n < 0 = (n < 0).
Lemma nmulrz_rlt0 x n (x0 : x < 0) : x *~ n < 0 = (0 < n).
Lemma pmulrz_rge0 x n (x0 : 0 < x) : 0 ≤ x *~ n = (0 ≤ n).
Lemma nmulrz_rge0 x n (x0 : x < 0) : 0 ≤ x *~ n = (n ≤ 0).
Lemma pmulrz_rle0 x n (x0 : 0 < x) : x *~ n ≤ 0 = (n ≤ 0).
Lemma nmulrz_rle0 x n (x0 : x < 0) : x *~ n ≤ 0 = (0 ≤ n).
Lemma mulrIz x (hx : x != 0) : injective ( *~%R x).
Lemma ler_int m n : (m%:~R ≤ n%:~R :> R) = (m ≤ n).
Lemma ltr_int m n : (m%:~R < n%:~R :> R) = (m < n).
Lemma eqr_int m n : (m%:~R == n%:~R :> R) = (m == n).
Lemma ler0z n : (0 ≤ n%:~R :> R) = (0 ≤ n).
Lemma ltr0z n : (0 < n%:~R :> R) = (0 < n).
Lemma lerz0 n : (n%:~R ≤ 0 :> R) = (n ≤ 0).
Lemma ltrz0 n : (n%:~R < 0 :> R) = (n < 0).
Lemma ler1z (n : int) : (1 ≤ n%:~R :> R) = (1 ≤ n).
Lemma ltr1z (n : int) : (1 < n%:~R :> R) = (1 < n).
Lemma lerz1 n : (n%:~R ≤ 1 :> R) = (n ≤ 1).
Lemma ltrz1 n : (n%:~R < 1 :> R) = (n < 1).
Lemma intr_eq0 n : (n%:~R == 0 :> R) = (n == 0).
Lemma mulrz_eq0 x n : (x *~ n == 0) = ((n == 0) || (x == 0)).
Lemma mulrz_neq0 x n : x *~ n != 0 = ((n != 0) && (x != 0)).
Lemma realz n : (n%:~R : R) \in Num.real.
Hint Resolve realz : core.
Definition intr_inj := @mulrIz 1 (oner_neq0 R).
End PO.
End NumMorphism.
End MorphTheory.
Arguments intr_inj {R} [x1 x2].
Definition exprz (R : unitRingType) (x : R) (n : int) := nosimpl
match n with
| Posz n ⇒ x ^+ n
| Negz n ⇒ x ^- (n.+1)
end.
Notation "x ^ n" := (exprz x n) : ring_scope.
Section ExprzUnitRing.
Variable R : unitRingType.
Implicit Types x y : R.
Implicit Types m n : int.
Lemma exprnP x (n : nat) : x ^+ n = x ^ n.
Lemma exprnN x (n : nat) : x ^- n = x ^ -n%:Z.
Lemma expr0z x : x ^ 0 = 1.
Lemma expr1z x : x ^ 1 = x.
Lemma exprN1 x : x ^ (-1) = x^-1.
Lemma invr_expz x n : (x ^ n)^-1 = x ^ (- n).
Lemma exprz_inv x n : (x^-1) ^ n = x ^ (- n).
Lemma exp1rz n : 1 ^ n = 1 :> R.
Lemma exprSz x (n : nat) : x ^ n.+1 = x × x ^ n.
Lemma exprSzr x (n : nat) : x ^ n.+1 = x ^ n × x.
Fact exprzD_nat x (m n : nat) : x ^ (m%:Z + n) = x ^ m × x ^ n.
Fact exprzD_Nnat x (m n : nat) : x ^ (-m%:Z + -n%:Z) = x ^ (-m%:Z) × x ^ (-n%:Z).
Lemma exprzD_ss x m n : (0 ≤ m) && (0 ≤ n) || (m ≤ 0) && (n ≤ 0)
→ x ^ (m + n) = x ^ m × x ^ n.
Lemma exp0rz n : 0 ^ n = (n == 0)%:~R :> R.
Lemma commrXz x y n : GRing.comm x y → GRing.comm x (y ^ n).
Lemma exprMz_comm x y n : x \is a GRing.unit → y \is a GRing.unit →
GRing.comm x y → (x × y) ^ n = x ^ n × y ^ n.
Lemma commrXz_wmulls x y n :
0 ≤ n → GRing.comm x y → (x × y) ^ n = x ^ n × y ^ n.
Lemma unitrXz x n (ux : x \is a GRing.unit) : x ^ n \is a GRing.unit.
Lemma exprzDr x (ux : x \is a GRing.unit) m n : x ^ (m + n) = x ^ m × x ^ n.
Lemma exprz_exp x m n : (x ^ m) ^ n = (x ^ (m × n)).
Lemma exprzAC x m n : (x ^ m) ^ n = (x ^ n) ^ m.
Lemma exprz_out x n (nux : x \isn't a GRing.unit) (hn : 0 ≤ n) :
x ^ (- n) = x ^ n.
End ExprzUnitRing.
Section Exprz_Zint_UnitRing.
Variable R : unitRingType.
Implicit Types x y : R.
Implicit Types m n : int.
Lemma exprz_pmulzl x m n : 0 ≤ n → (x *~ m) ^ n = x ^ n *~ (m ^ n).
Lemma exprz_pintl m n (hn : 0 ≤ n) : m%:~R ^ n = (m ^ n)%:~R :> R.
Lemma exprzMzl x m n (ux : x \is a GRing.unit) (um : m%:~R \is a @GRing.unit R):
(x *~ m) ^ n = (m%:~R ^ n) × x ^ n :> R.
Lemma expNrz x n : (- x) ^ n = (-1) ^ n × x ^ n :> R.
Lemma unitr_n0expz x n :
n != 0 → (x ^ n \is a GRing.unit) = (x \is a GRing.unit).
Lemma intrV (n : int) :
n \in [:: 0; 1; -1] → n%:~R ^-1 = n%:~R :> R.
Lemma rmorphXz (R' : unitRingType) (f : {rmorphism R → R'}) n :
{in GRing.unit, {morph f : x / x ^ n}}.
End Exprz_Zint_UnitRing.
Section ExprzIdomain.
Variable R : idomainType.
Implicit Types x y : R.
Implicit Types m n : int.
Lemma expfz_eq0 x n : (x ^ n == 0) = (n != 0) && (x == 0).
Lemma expfz_neq0 x n : x != 0 → x ^ n != 0.
Lemma exprzMl x y n (ux : x \is a GRing.unit) (uy : y \is a GRing.unit) :
(x × y) ^ n = x ^ n × y ^ n.
Lemma expfV (x : R) (i : int) : (x ^ i) ^-1 = (x ^-1) ^ i.
End ExprzIdomain.
Section ExprzField.
Variable F : fieldType.
Implicit Types x y : F.
Implicit Types m n : int.
Lemma expfzDr x m n : x != 0 → x ^ (m + n) = x ^ m × x ^ n.
Lemma expfz_n0addr x m n : m + n != 0 → x ^ (m + n) = x ^ m × x ^ n.
Lemma expfzMl x y n : (x × y) ^ n = x ^ n × y ^ n.
Lemma fmorphXz (R : unitRingType) (f : {rmorphism F → R}) n :
{morph f : x / x ^ n}.
End ExprzField.
Section ExprzOrder.
Variable R : realFieldType.
Implicit Types x y : R.
Implicit Types m n : int.
ler and exprz
Lemma exprz_ge0 n x (hx : 0 ≤ x) : (0 ≤ x ^ n).
Lemma exprz_gt0 n x (hx : 0 < x) : (0 < x ^ n).
Definition exprz_gte0 := (exprz_ge0, exprz_gt0).
Lemma ler_wpiexpz2l x (x0 : 0 ≤ x) (x1 : x ≤ 1) :
{in ≥ 0 &, {homo (exprz x) : x y /~ x ≤ y}}.
Lemma ler_wniexpz2l x (x0 : 0 ≤ x) (x1 : x ≤ 1) :
{in < 0 &, {homo (exprz x) : x y /~ x ≤ y}}.
Fact ler_wpeexpz2l x (x1 : 1 ≤ x) :
{in ≥ 0 &, {homo (exprz x) : x y / x ≤ y}}.
Fact ler_wneexpz2l x (x1 : 1 ≤ x) :
{in ≤ 0 &, {homo (exprz x) : x y / x ≤ y}}.
Lemma ler_weexpz2l x (x1 : 1 ≤ x) : {homo (exprz x) : x y / x ≤ y}.
Lemma pexprz_eq1 x n (x0 : 0 ≤ x) : (x ^ n == 1) = ((n == 0) || (x == 1)).
Lemma ieexprIz x (x0 : 0 < x) (nx1 : x != 1) : injective (exprz x).
Lemma ler_piexpz2l x (x0 : 0 < x) (x1 : x < 1) :
{in ≥ 0 &, {mono (exprz x) : x y /~ x ≤ y}}.
Lemma ltr_piexpz2l x (x0 : 0 < x) (x1 : x < 1) :
{in ≥ 0 &, {mono (exprz x) : x y /~ x < y}}.
Lemma ler_niexpz2l x (x0 : 0 < x) (x1 : x < 1) :
{in < 0 &, {mono (exprz x) : x y /~ x ≤ y}}.
Lemma ltr_niexpz2l x (x0 : 0 < x) (x1 : x < 1) :
{in < 0 &, {mono (exprz x) : x y /~ x < y}}.
Lemma ler_eexpz2l x (x1 : 1 < x) : {mono (exprz x) : x y / x ≤ y}.
Lemma ltr_eexpz2l x (x1 : 1 < x) : {mono (exprz x) : x y / x < y}.
Lemma ler_wpexpz2r n (hn : 0 ≤ n) :
{in ≥ 0 & , {homo ((@exprz R)^~ n) : x y / x ≤ y}}.
Lemma ler_wnexpz2r n (hn : n ≤ 0) :
{in > 0 & , {homo ((@exprz R)^~ n) : x y /~ x ≤ y}}.
Lemma pexpIrz n (n0 : n != 0) : {in ≥ 0 &, injective ((@exprz R)^~ n)}.
Lemma nexpIrz n (n0 : n != 0) : {in ≤ 0 &, injective ((@exprz R)^~ n)}.
Lemma ler_pexpz2r n (hn : 0 < n) :
{in ≥ 0 & , {mono ((@exprz R)^~ n) : x y / x ≤ y}}.
Lemma ltr_pexpz2r n (hn : 0 < n) :
{in ≥ 0 & , {mono ((@exprz R)^~ n) : x y / x < y}}.
Lemma ler_nexpz2r n (hn : n < 0) :
{in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x ≤ y}}.
Lemma ltr_nexpz2r n (hn : n < 0) :
{in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x < y}}.
Lemma eqr_expz2 n x y : n != 0 → 0 ≤ x → 0 ≤ y →
(x ^ n == y ^ n) = (x == y).
End ExprzOrder.
Section Sgz.
Variable R : numDomainType.
Implicit Types x y z : R.
Implicit Types m n p : int.
Definition sgz x : int := if x == 0 then 0 else if x < 0 then -1 else 1.
Lemma sgz_def x : sgz x = (-1) ^+ (x < 0)%R *+ (x != 0).
Lemma sgrEz x : sgr x = (sgz x)%:~R.
Lemma gtr0_sgz x : 0 < x → sgz x = 1.
Lemma ltr0_sgz x : x < 0 → sgz x = -1.
Lemma sgz0 : sgz (0 : R) = 0.
Lemma sgz1 : sgz (1 : R) = 1.
Lemma sgzN1 : sgz (-1 : R) = -1.
Definition sgzE := (sgz0, sgz1, sgzN1).
Lemma sgz_sgr x : sgz (sgr x) = sgz x.
Lemma normr_sgz x : `|sgz x| = (x != 0).
Lemma normr_sg x : `|sgr x| = (x != 0)%:~R.
End Sgz.
Section MoreSgz.
Variable R : numDomainType.
Lemma sgz_int m : sgz (m%:~R : R) = sgz m.
Lemma sgrz (n : int) : sgr n = sgz n.
Lemma intr_sg m : (sgr m)%:~R = sgr (m%:~R) :> R.
Lemma sgz_id (x : R) : sgz (sgz x) = sgz x.
End MoreSgz.
Section SgzReal.
Variable R : realDomainType.
Implicit Types x y z : R.
Implicit Types m n p : int.
Lemma sgz_cp0 x :
((sgz x == 1) = (0 < x)) ×
((sgz x == -1) = (x < 0)) ×
((sgz x == 0) = (x == 0)).
Variant sgz_val x : bool → bool → bool → bool → bool → bool
→ bool → bool → bool → bool → bool → bool
→ bool → bool → bool → bool → bool → bool
→ R → R → int → Set :=
| SgzNull of x = 0 : sgz_val x true true true true false false
true false false true false false true false false true false false 0 0 0
| SgzPos of x > 0 : sgz_val x false false true false false true
false false true false false true false false true false false true x 1 1
| SgzNeg of x < 0 : sgz_val x false true false false true false
false true false false true false false true false false true false (-x) (-1) (-1).
Lemma sgzP x :
sgz_val x (0 == x) (x ≤ 0) (0 ≤ x) (x == 0) (x < 0) (0 < x)
(0 == sgr x) (-1 == sgr x) (1 == sgr x)
(sgr x == 0) (sgr x == -1) (sgr x == 1)
(0 == sgz x) (-1 == sgz x) (1 == sgz x)
(sgz x == 0) (sgz x == -1) (sgz x == 1) `|x| (sgr x) (sgz x).
Lemma sgzN x : sgz (- x) = - sgz x.
Lemma mulz_sg x : sgz x × sgz x = (x != 0)%:~R.
Lemma mulz_sg_eq1 x y : (sgz x × sgz y == 1) = (x != 0) && (sgz x == sgz y).
Lemma mulz_sg_eqN1 x y : (sgz x × sgz y == -1) = (x != 0) && (sgz x == - sgz y).
Lemma exprz_gt0 n x (hx : 0 < x) : (0 < x ^ n).
Definition exprz_gte0 := (exprz_ge0, exprz_gt0).
Lemma ler_wpiexpz2l x (x0 : 0 ≤ x) (x1 : x ≤ 1) :
{in ≥ 0 &, {homo (exprz x) : x y /~ x ≤ y}}.
Lemma ler_wniexpz2l x (x0 : 0 ≤ x) (x1 : x ≤ 1) :
{in < 0 &, {homo (exprz x) : x y /~ x ≤ y}}.
Fact ler_wpeexpz2l x (x1 : 1 ≤ x) :
{in ≥ 0 &, {homo (exprz x) : x y / x ≤ y}}.
Fact ler_wneexpz2l x (x1 : 1 ≤ x) :
{in ≤ 0 &, {homo (exprz x) : x y / x ≤ y}}.
Lemma ler_weexpz2l x (x1 : 1 ≤ x) : {homo (exprz x) : x y / x ≤ y}.
Lemma pexprz_eq1 x n (x0 : 0 ≤ x) : (x ^ n == 1) = ((n == 0) || (x == 1)).
Lemma ieexprIz x (x0 : 0 < x) (nx1 : x != 1) : injective (exprz x).
Lemma ler_piexpz2l x (x0 : 0 < x) (x1 : x < 1) :
{in ≥ 0 &, {mono (exprz x) : x y /~ x ≤ y}}.
Lemma ltr_piexpz2l x (x0 : 0 < x) (x1 : x < 1) :
{in ≥ 0 &, {mono (exprz x) : x y /~ x < y}}.
Lemma ler_niexpz2l x (x0 : 0 < x) (x1 : x < 1) :
{in < 0 &, {mono (exprz x) : x y /~ x ≤ y}}.
Lemma ltr_niexpz2l x (x0 : 0 < x) (x1 : x < 1) :
{in < 0 &, {mono (exprz x) : x y /~ x < y}}.
Lemma ler_eexpz2l x (x1 : 1 < x) : {mono (exprz x) : x y / x ≤ y}.
Lemma ltr_eexpz2l x (x1 : 1 < x) : {mono (exprz x) : x y / x < y}.
Lemma ler_wpexpz2r n (hn : 0 ≤ n) :
{in ≥ 0 & , {homo ((@exprz R)^~ n) : x y / x ≤ y}}.
Lemma ler_wnexpz2r n (hn : n ≤ 0) :
{in > 0 & , {homo ((@exprz R)^~ n) : x y /~ x ≤ y}}.
Lemma pexpIrz n (n0 : n != 0) : {in ≥ 0 &, injective ((@exprz R)^~ n)}.
Lemma nexpIrz n (n0 : n != 0) : {in ≤ 0 &, injective ((@exprz R)^~ n)}.
Lemma ler_pexpz2r n (hn : 0 < n) :
{in ≥ 0 & , {mono ((@exprz R)^~ n) : x y / x ≤ y}}.
Lemma ltr_pexpz2r n (hn : 0 < n) :
{in ≥ 0 & , {mono ((@exprz R)^~ n) : x y / x < y}}.
Lemma ler_nexpz2r n (hn : n < 0) :
{in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x ≤ y}}.
Lemma ltr_nexpz2r n (hn : n < 0) :
{in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x < y}}.
Lemma eqr_expz2 n x y : n != 0 → 0 ≤ x → 0 ≤ y →
(x ^ n == y ^ n) = (x == y).
End ExprzOrder.
Section Sgz.
Variable R : numDomainType.
Implicit Types x y z : R.
Implicit Types m n p : int.
Definition sgz x : int := if x == 0 then 0 else if x < 0 then -1 else 1.
Lemma sgz_def x : sgz x = (-1) ^+ (x < 0)%R *+ (x != 0).
Lemma sgrEz x : sgr x = (sgz x)%:~R.
Lemma gtr0_sgz x : 0 < x → sgz x = 1.
Lemma ltr0_sgz x : x < 0 → sgz x = -1.
Lemma sgz0 : sgz (0 : R) = 0.
Lemma sgz1 : sgz (1 : R) = 1.
Lemma sgzN1 : sgz (-1 : R) = -1.
Definition sgzE := (sgz0, sgz1, sgzN1).
Lemma sgz_sgr x : sgz (sgr x) = sgz x.
Lemma normr_sgz x : `|sgz x| = (x != 0).
Lemma normr_sg x : `|sgr x| = (x != 0)%:~R.
End Sgz.
Section MoreSgz.
Variable R : numDomainType.
Lemma sgz_int m : sgz (m%:~R : R) = sgz m.
Lemma sgrz (n : int) : sgr n = sgz n.
Lemma intr_sg m : (sgr m)%:~R = sgr (m%:~R) :> R.
Lemma sgz_id (x : R) : sgz (sgz x) = sgz x.
End MoreSgz.
Section SgzReal.
Variable R : realDomainType.
Implicit Types x y z : R.
Implicit Types m n p : int.
Lemma sgz_cp0 x :
((sgz x == 1) = (0 < x)) ×
((sgz x == -1) = (x < 0)) ×
((sgz x == 0) = (x == 0)).
Variant sgz_val x : bool → bool → bool → bool → bool → bool
→ bool → bool → bool → bool → bool → bool
→ bool → bool → bool → bool → bool → bool
→ R → R → int → Set :=
| SgzNull of x = 0 : sgz_val x true true true true false false
true false false true false false true false false true false false 0 0 0
| SgzPos of x > 0 : sgz_val x false false true false false true
false false true false false true false false true false false true x 1 1
| SgzNeg of x < 0 : sgz_val x false true false false true false
false true false false true false false true false false true false (-x) (-1) (-1).
Lemma sgzP x :
sgz_val x (0 == x) (x ≤ 0) (0 ≤ x) (x == 0) (x < 0) (0 < x)
(0 == sgr x) (-1 == sgr x) (1 == sgr x)
(sgr x == 0) (sgr x == -1) (sgr x == 1)
(0 == sgz x) (-1 == sgz x) (1 == sgz x)
(sgz x == 0) (sgz x == -1) (sgz x == 1) `|x| (sgr x) (sgz x).
Lemma sgzN x : sgz (- x) = - sgz x.
Lemma mulz_sg x : sgz x × sgz x = (x != 0)%:~R.
Lemma mulz_sg_eq1 x y : (sgz x × sgz y == 1) = (x != 0) && (sgz x == sgz y).
Lemma mulz_sg_eqN1 x y : (sgz x × sgz y == -1) = (x != 0) && (sgz x == - sgz y).
Lemma muls_eqA x y z : sgr x != 0 ->
(sgr y * sgr z == sgr x) = ((sgr y * sgr x == sgr z) && (sgr z != 0)).
Proof. by do 3!case: sgrP=> _. Qed.
Lemma sgzM x y : sgz (x × y) = sgz x × sgz y.
Lemma sgzX (n : nat) x : sgz (x ^+ n) = (sgz x) ^+ n.
Lemma sgz_eq0 x : (sgz x == 0) = (x == 0).
Lemma sgz_odd (n : nat) x : x != 0 → (sgz x) ^+ n = (sgz x) ^+ (odd n).
Lemma sgz_gt0 x : (sgz x > 0) = (x > 0).
Lemma sgz_lt0 x : (sgz x < 0) = (x < 0).
Lemma sgz_ge0 x : (sgz x ≥ 0) = (x ≥ 0).
Lemma sgz_le0 x : (sgz x ≤ 0) = (x ≤ 0).
Lemma sgz_smul x y : sgz (y *~ (sgz x)) = (sgz x) × (sgz y).
Lemma sgrMz m x : sgr (x *~ m) = sgr x *~ sgr m.
End SgzReal.
Lemma sgz_eq (R R' : realDomainType) (x : R) (y : R') :
(sgz x == sgz y) = ((x == 0) == (y == 0)) && ((0 < x) == (0 < y)).
Lemma intr_sign (R : ringType) s : ((-1) ^+ s)%:~R = (-1) ^+ s :> R.
Section Absz.
Implicit Types m n p : int.
Open Scope nat_scope.
Lemma absz_nat (n : nat) : `|n| = n.
Lemma abszE (m : int) : `|m| = `|m|%R :> int.
Lemma absz0 : `|0%R| = 0.
Lemma abszN m : `|- m| = `|m|.
Lemma absz_eq0 m : (`|m| == 0) = (m == 0%R).
Lemma absz_gt0 m : (`|m| > 0) = (m != 0%R).
Lemma absz1 : `|1%R| = 1.
Lemma abszN1 : `|-1%R| = 1.
Lemma absz_id m : `|(`|m|)| = `|m|.
Lemma abszM m1 m2 : `|(m1 × m2)%R| = `|m1| × `|m2|.
Lemma abszX (n : nat) m : `|m ^+ n| = `|m| ^ n.
Lemma absz_sg m : `|sgr m| = (m != 0%R).
Lemma gez0_abs m : (0 ≤ m)%R → `|m| = m :> int.
Lemma gtz0_abs m : (0 < m)%R → `|m| = m :> int.
Lemma lez0_abs m : (m ≤ 0)%R → `|m| = - m :> int.
Lemma ltz0_abs m : (m < 0)%R → `|m| = - m :> int.
Lemma lez_abs m : m ≤ `|m|%N :> int.
Lemma absz_sign s : `|(-1) ^+ s| = 1.
Lemma abszMsign s m : `|((-1) ^+ s × m)%R| = `|m|.
Lemma mulz_sign_abs m : ((-1) ^+ (m < 0)%R × `|m|%:Z)%R = m.
Lemma mulz_Nsign_abs m : ((-1) ^+ (0 < m)%R × `|m|%:Z)%R = - m.
Lemma intEsign m : m = ((-1) ^+ (m < 0)%R × `|m|%:Z)%R.
Lemma abszEsign m : `|m|%:Z = ((-1) ^+ (m < 0)%R × m)%R.
Lemma intEsg m : m = (sgz m × `|m|%:Z)%R.
Lemma abszEsg m : (`|m|%:Z = sgz m × m)%R.
End Absz.
Section MoreAbsz.
Variable R : numDomainType.
Implicit Type i : int.
Lemma mulr_absz (x : R) i : x *+ `|i| = x *~ `|i|.
Lemma natr_absz i : `|i|%:R = `|i|%:~R :> R.
End MoreAbsz.
Module Export IntDist.
Notation "m - n" :=
(@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope.
Arguments absz m%distn_scope.
Notation "`| m |" := (absz m) : nat_scope.
Coercion Posz : nat >-> int.
Section Distn.
Open Scope nat_scope.
Implicit Type m : int.
Implicit Types n d : nat.
Lemma distnC m1 m2 : `|m1 - m2| = `|m2 - m1|.
Lemma distnDl d n1 n2 : `|d + n1 - (d + n2)| = `|n1 - n2|.
Lemma distnDr d n1 n2 : `|n1 + d - (n2 + d)| = `|n1 - n2|.
Lemma distnEr n1 n2 : n1 ≤ n2 → `|n1 - n2| = n2 - n1.
Lemma distnEl n1 n2 : n2 ≤ n1 → `|n1 - n2| = n1 - n2.
Lemma distn0 n : `|n - 0| = n.
Lemma dist0n n : `|0 - n| = n.
Lemma distnn m : `|m - m| = 0.
Lemma distn_eq0 n1 n2 : (`|n1 - n2| == 0) = (n1 == n2).
Lemma distnS n : `|n - n.+1| = 1.
Lemma distSn n : `|n.+1 - n| = 1.
Lemma distn_eq1 n1 n2 :
(`|n1 - n2| == 1) = (if n1 < n2 then n1.+1 == n2 else n1 == n2.+1).
Lemma leq_add_dist m1 m2 m3 : `|m1 - m3| ≤ `|m1 - m2| + `|m2 - m3|.
Most of this proof generalizes to all real-ordered rings.
Lemma leqif_add_distz m1 m2 m3 :
`|m1 - m3| ≤ `|m1 - m2| + `|m2 - m3|
?= iff (m1 ≤ m2 ≤ m3)%R || (m3 ≤ m2 ≤ m1)%R.
Lemma leqif_add_dist n1 n2 n3 :
`|n1 - n3| ≤ `|n1 - n2| + `|n2 - n3|
?= iff (n1 ≤ n2 ≤ n3) || (n3 ≤ n2 ≤ n1).
Lemma sqrn_dist n1 n2 : `|n1 - n2| ^ 2 + 2 × (n1 × n2) = n1 ^ 2 + n2 ^ 2.
End Distn.
End IntDist.
Section NormInt.
Variable R : numDomainType.
Lemma intr_norm m : `|m|%:~R = `|m%:~R : R|.
Lemma normrMz m (x : R) : `|x *~ m| = `|x| *~ `|m|.
Lemma expN1r (i : int) : (-1 : R) ^ i = (-1) ^+ `|i|.
End NormInt.
Section PolyZintRing.
Variable R : ringType.
Implicit Types x y z: R.
Implicit Types m n : int.
Implicit Types i j k : nat.
Implicit Types p q r : {poly R}.
Lemma coefMrz p n i : (p *~ n)`_i = (p`_i *~ n).
Lemma polyCMz n : {morph (@polyC R) : c / c *~ n}.
Lemma hornerMz n p x : (p *~ n).[x] = p.[x] *~ n.
Lemma horner_int n x : (n%:~R : {poly R}).[x] = n%:~R.
Lemma derivMz n p : (p *~ n)^` = p^` *~ n.
Lemma mulpz p n : p *~ n = n%:~R *: p.
End PolyZintRing.
Section ZnatPred.
Definition Znat := [qualify a n : int | 0 ≤ n].
Fact Znat_key : pred_key Znat.
Canonical Znat_keyd := KeyedQualifier Znat_key.
Lemma Znat_def n : (n \is a Znat) = (0 ≤ n).
Lemma Znat_semiring_closed : semiring_closed Znat.
Canonical Znat_addrPred := AddrPred Znat_semiring_closed.
Canonical Znat_mulrPred := MulrPred Znat_semiring_closed.
Canonical Znat_semiringPred := SemiringPred Znat_semiring_closed.
Lemma ZnatP (m : int) : reflect (∃ n : nat, m = n) (m \is a Znat).
End ZnatPred.
Section rpred.
Lemma rpredMz M S (addS : @zmodPred M S) (kS : keyed_pred addS) m :
{in kS, ∀ u, u *~ m \in kS}.
Lemma rpred_int R S (ringS : @subringPred R S) (kS : keyed_pred ringS) m :
m%:~R \in kS.
Lemma rpredZint (R : ringType) (M : lmodType R) S
(addS : @zmodPred M S) (kS : keyed_pred addS) m :
{in kS, ∀ u, m%:~R *: u \in kS}.
Lemma rpredXz R S (divS : @divrPred R S) (kS : keyed_pred divS) m :
{in kS, ∀ x, x ^ m \in kS}.
Lemma rpredXsign R S (divS : @divrPred R S) (kS : keyed_pred divS) n x :
(x ^ ((-1) ^+ n) \in kS) = (x \in kS).
End rpred.
#[deprecated(since="mathcomp 1.12.0", note="Use polyCMz instead.")]
Notation polyC_mulrz := polyCMz (only parsing).
`|m1 - m3| ≤ `|m1 - m2| + `|m2 - m3|
?= iff (m1 ≤ m2 ≤ m3)%R || (m3 ≤ m2 ≤ m1)%R.
Lemma leqif_add_dist n1 n2 n3 :
`|n1 - n3| ≤ `|n1 - n2| + `|n2 - n3|
?= iff (n1 ≤ n2 ≤ n3) || (n3 ≤ n2 ≤ n1).
Lemma sqrn_dist n1 n2 : `|n1 - n2| ^ 2 + 2 × (n1 × n2) = n1 ^ 2 + n2 ^ 2.
End Distn.
End IntDist.
Section NormInt.
Variable R : numDomainType.
Lemma intr_norm m : `|m|%:~R = `|m%:~R : R|.
Lemma normrMz m (x : R) : `|x *~ m| = `|x| *~ `|m|.
Lemma expN1r (i : int) : (-1 : R) ^ i = (-1) ^+ `|i|.
End NormInt.
Section PolyZintRing.
Variable R : ringType.
Implicit Types x y z: R.
Implicit Types m n : int.
Implicit Types i j k : nat.
Implicit Types p q r : {poly R}.
Lemma coefMrz p n i : (p *~ n)`_i = (p`_i *~ n).
Lemma polyCMz n : {morph (@polyC R) : c / c *~ n}.
Lemma hornerMz n p x : (p *~ n).[x] = p.[x] *~ n.
Lemma horner_int n x : (n%:~R : {poly R}).[x] = n%:~R.
Lemma derivMz n p : (p *~ n)^` = p^` *~ n.
Lemma mulpz p n : p *~ n = n%:~R *: p.
End PolyZintRing.
Section ZnatPred.
Definition Znat := [qualify a n : int | 0 ≤ n].
Fact Znat_key : pred_key Znat.
Canonical Znat_keyd := KeyedQualifier Znat_key.
Lemma Znat_def n : (n \is a Znat) = (0 ≤ n).
Lemma Znat_semiring_closed : semiring_closed Znat.
Canonical Znat_addrPred := AddrPred Znat_semiring_closed.
Canonical Znat_mulrPred := MulrPred Znat_semiring_closed.
Canonical Znat_semiringPred := SemiringPred Znat_semiring_closed.
Lemma ZnatP (m : int) : reflect (∃ n : nat, m = n) (m \is a Znat).
End ZnatPred.
Section rpred.
Lemma rpredMz M S (addS : @zmodPred M S) (kS : keyed_pred addS) m :
{in kS, ∀ u, u *~ m \in kS}.
Lemma rpred_int R S (ringS : @subringPred R S) (kS : keyed_pred ringS) m :
m%:~R \in kS.
Lemma rpredZint (R : ringType) (M : lmodType R) S
(addS : @zmodPred M S) (kS : keyed_pred addS) m :
{in kS, ∀ u, m%:~R *: u \in kS}.
Lemma rpredXz R S (divS : @divrPred R S) (kS : keyed_pred divS) m :
{in kS, ∀ x, x ^ m \in kS}.
Lemma rpredXsign R S (divS : @divrPred R S) (kS : keyed_pred divS) n x :
(x ^ ((-1) ^+ n) \in kS) = (x \in kS).
End rpred.
#[deprecated(since="mathcomp 1.12.0", note="Use polyCMz instead.")]
Notation polyC_mulrz := polyCMz (only parsing).