From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.ssreflect.ssrnat.html | 1125 +++++++++++++++------------
1 file changed, 642 insertions(+), 483 deletions(-)
(limited to 'docs/htmldoc/mathcomp.ssreflect.ssrnat.html')
diff --git a/docs/htmldoc/mathcomp.ssreflect.ssrnat.html b/docs/htmldoc/mathcomp.ssreflect.ssrnat.html
index f1661e2..bcbccb1 100644
--- a/docs/htmldoc/mathcomp.ssreflect.ssrnat.html
+++ b/docs/htmldoc/mathcomp.ssreflect.ssrnat.html
@@ -21,10 +21,9 @@
@@ -153,6 +152,16 @@
+
+ Disable Coq prelude hints to improve proof script robustness.
+
+
+
+
+
+
+
+
Declare legacy Arith operators in new scope.
@@ -162,13 +171,13 @@
Delimit Scope coq_nat_scope with coq_nat.
-Notation "m + n" := (plus m n) : coq_nat_scope.
-Notation "m - n" := (minus m n) : coq_nat_scope.
-Notation "m * n" := (mult m n) : coq_nat_scope.
-Notation "m <= n" := (le m n) : coq_nat_scope.
-Notation "m < n" := (lt m n) : coq_nat_scope.
-Notation "m >= n" := (ge m n) : coq_nat_scope.
-Notation "m > n" := (gt m n) : coq_nat_scope.
+Notation "m + n" := (plus m n) : coq_nat_scope.
+Notation "m - n" := (minus m n) : coq_nat_scope.
+Notation "m * n" := (mult m n) : coq_nat_scope.
+Notation "m <= n" := (le m n) : coq_nat_scope.
+Notation "m < n" := (lt m n) : coq_nat_scope.
+Notation "m >= n" := (ge m n) : coq_nat_scope.
+Notation "m > n" := (gt m n) : coq_nat_scope.
@@ -195,28 +204,28 @@
-
Notation succn :=
Datatypes.S.
-
Notation predn :=
Peano.pred.
+
Notation succn :=
Datatypes.S.
+
Notation predn :=
Peano.pred.
-
Notation "n .+1" := (
succn n) (
at level 2,
left associativity,
+
Notation "n .+1" := (
succn n) (
at level 2,
left associativity,
format "n .+1") :
nat_scope.
-
Notation "n .+2" :=
n.+1.+1 (
at level 2,
left associativity,
+
Notation "n .+2" :=
n.+1.+1 (
at level 2,
left associativity,
format "n .+2") :
nat_scope.
-
Notation "n .+3" :=
n.+2.+1 (
at level 2,
left associativity,
+
Notation "n .+3" :=
n.+2.+1 (
at level 2,
left associativity,
format "n .+3") :
nat_scope.
-
Notation "n .+4" :=
n.+2.+2 (
at level 2,
left associativity,
+
Notation "n .+4" :=
n.+2.+2 (
at level 2,
left associativity,
format "n .+4") :
nat_scope.
-
Notation "n .-1" := (
predn n) (
at level 2,
left associativity,
+
Notation "n .-1" := (
predn n) (
at level 2,
left associativity,
format "n .-1") :
nat_scope.
-
Notation "n .-2" :=
n.-1.-1 (
at level 2,
left associativity,
+
Notation "n .-2" :=
n.-1.-1 (
at level 2,
left associativity,
format "n .-2") :
nat_scope.
-
Lemma succnK :
cancel succn predn.
-
Lemma succn_inj :
injective succn.
+
Lemma succnK :
cancel succn predn.
+
Lemma succn_inj :
injective succn.
@@ -241,9 +250,9 @@
Fixpoint eqn m n {struct m} :=
match m, n with
- | 0, 0 ⇒ true
- | m'.+1, n'.+1 ⇒ eqn m' n'
- | _, _ ⇒ false
+ | 0, 0 ⇒ true
+ | m'.+1, n'.+1 ⇒ eqn m' n'
+ | _, _ ⇒ false
end.
@@ -251,18 +260,18 @@
Canonical nat_eqMixin := EqMixin eqnP.
-Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin.
+Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin.
-Lemma eqnE : eqn = eq_op.
+Lemma eqnE : eqn = eq_op.
-Lemma eqSS m n : (m.+1 == n.+1) = (m == n).
+Lemma eqSS m n : (m.+1 == n.+1) = (m == n).
-Lemma nat_irrelevance (x y : nat) (E E' : x = y) : E = E'.
+Lemma nat_irrelevance (x y : nat) (E E' : x = y) : E = E'.
@@ -273,73 +282,73 @@
@@ -351,53 +360,53 @@
@@ -408,13 +417,13 @@
-
Definition leq m n :=
m - n == 0.
+
Definition leq m n :=
m - n == 0.
-
Notation "m <= n" := (
leq m n) :
nat_scope.
-
Notation "m < n" := (
m.+1 ≤ n) :
nat_scope.
-
Notation "m >= n" := (
n ≤ m) (
only parsing) :
nat_scope.
-
Notation "m > n" := (
n < m) (
only parsing) :
nat_scope.
+
Notation "m <= n" := (
leq m n) :
nat_scope.
+
Notation "m < n" := (
m.+1 ≤ n) :
nat_scope.
+
Notation "m >= n" := (
n ≤ m) (
only parsing) :
nat_scope.
+
Notation "m > n" := (
n < m) (
only parsing) :
nat_scope.
@@ -423,92 +432,98 @@
For sorting, etc.
@@ -519,16 +534,16 @@
@@ -539,39 +554,39 @@
@@ -582,85 +597,94 @@
@@ -670,7 +694,7 @@
@@ -681,117 +705,117 @@
@@ -800,16 +824,16 @@
Quasi-cancellation (really, absorption) lemmas
@@ -818,16 +842,16 @@
Distributivity.
@@ -841,21 +865,21 @@
Section ExMinn.
-Variable P : pred nat.
-Hypothesis exP : ∃ n, P n.
+Variable P : pred nat.
+Hypothesis exP : ∃ n, P n.
-Inductive acc_nat i : Prop := AccNat0 of P i | AccNatS of acc_nat i.+1.
+Inductive acc_nat i : Prop := AccNat0 of P i | AccNatS of acc_nat i.+1.
-Lemma find_ex_minn : {m | P m & ∀ n, P n → n ≥ m}.
+Lemma find_ex_minn : {m | P m & ∀ n, P n → n ≥ m}.
Definition ex_minn := s2val find_ex_minn.
-Inductive ex_minn_spec : nat → Type :=
- ExMinnSpec m of P m & (∀ n, P n → n ≥ m) : ex_minn_spec m.
+Inductive ex_minn_spec : nat → Type :=
+ ExMinnSpec m of P m & (∀ n, P n → n ≥ m) : ex_minn_spec m.
Lemma ex_minnP : ex_minn_spec ex_minn.
@@ -867,18 +891,18 @@
Section ExMaxn.
-Variables (P : pred nat) (m : nat).
-Hypotheses (exP : ∃ i, P i) (ubP : ∀ i, P i → i ≤ m).
+Variables (P : pred nat) (m : nat).
+Hypotheses (exP : ∃ i, P i) (ubP : ∀ i, P i → i ≤ m).
-Lemma ex_maxn_subproof : ∃ i, P (m - i).
+Lemma ex_maxn_subproof : ∃ i, P (m - i).
-Definition ex_maxn := m - ex_minn ex_maxn_subproof.
+Definition ex_maxn := m - ex_minn ex_maxn_subproof.
-CoInductive ex_maxn_spec : nat → Type :=
- ExMaxnSpec i of P i & (∀ j, P j → j ≤ i) : ex_maxn_spec i.
+Variant ex_maxn_spec : nat → Type :=
+ ExMaxnSpec i of P i & (∀ j, P j → j ≤ i) : ex_maxn_spec i.
Lemma ex_maxnP : ex_maxn_spec ex_maxn.
@@ -887,67 +911,67 @@
End ExMaxn.
-Lemma eq_ex_minn P Q exP exQ : P =1 Q → @ex_minn P exP = @ex_minn Q exQ.
+Lemma eq_ex_minn P Q exP exQ : P =1 Q → @ex_minn P exP = @ex_minn Q exQ.
-Lemma eq_ex_maxn (P Q : pred nat) m n exP ubP exQ ubQ :
- P =1 Q → @ex_maxn P m exP ubP = @ex_maxn Q n exQ ubQ.
+Lemma eq_ex_maxn (P Q : pred nat) m n exP ubP exQ ubQ :
+ P =1 Q → @ex_maxn P m exP ubP = @ex_maxn Q n exQ ubQ.
Section Iteration.
Variable T : Type.
-Implicit Types m n : nat.
+Implicit Types m n : nat.
Implicit Types x y : T.
Definition iter n f x :=
- let fix loop m := if m is i.+1 then f (loop i) else x in loop n.
+ let fix loop m := if m is i.+1 then f (loop i) else x in loop n.
Definition iteri n f x :=
- let fix loop m := if m is i.+1 then f i (loop i) else x in loop n.
+ let fix loop m := if m is i.+1 then f i (loop i) else x in loop n.
Definition iterop n op x :=
let f i y := if i is 0 then x else op x y in iteri n f.
-Lemma iterSr n f x : iter n.+1 f x = iter n f (f x).
+Lemma iterSr n f x : iter n.+1 f x = iter n f (f x).
-Lemma iterS n f x : iter n.+1 f x = f (iter n f x).
+Lemma iterS n f x : iter n.+1 f x = f (iter n f x).
-Lemma iter_add n m f x : iter (n + m) f x = iter n f (iter m f x).
+Lemma iter_add n m f x : iter (n + m) f x = iter n f (iter m f x).
-Lemma iteriS n f x : iteri n.+1 f x = f n (iteri n f x).
+Lemma iteriS n f x : iteri n.+1 f x = f n (iteri n f x).
-Lemma iteropS idx n op x : iterop n.+1 op x idx = iter n (op x) x.
+Lemma iteropS idx n op x : iterop n.+1 op x idx = iter n (op x) x.
-Lemma eq_iter f f' : f =1 f' → ∀ n, iter n f =1 iter n f'.
+Lemma eq_iter f f' : f =1 f' → ∀ n, iter n f =1 iter n f'.
-Lemma eq_iteri f f' : f =2 f' → ∀ n, iteri n f =1 iteri n f'.
+Lemma eq_iteri f f' : f =2 f' → ∀ n, iteri n f =1 iteri n f'.
-Lemma eq_iterop n op op' : op =2 op' → iterop n op =2 iterop n op'.
+Lemma eq_iterop n op op' : op =2 op' → iterop n op =2 iterop n op'.
End Iteration.
-Lemma iter_succn m n : iter n succn m = m + n.
+Lemma iter_succn m n : iter n succn m = m + n.
-Lemma iter_succn_0 n : iter n succn 0 = n.
+Lemma iter_succn_0 n : iter n succn 0 = n.
-Lemma iter_predn m n : iter n predn m = m - n.
+Lemma iter_predn m n : iter n predn m = m - n.
@@ -958,138 +982,138 @@
@@ -1101,81 +1125,81 @@
Definition expn_rec m n := iterop n muln m 1.
-Notation "m ^ n" := (expn_rec m n) : nat_rec_scope.
-Definition expn := nosimpl expn_rec.
-Notation "m ^ n" := (expn m n) : nat_scope.
+Notation "m ^ n" := (expn_rec m n) : nat_rec_scope.
+Definition expn := nosimpl expn_rec.
+Notation "m ^ n" := (expn m n) : nat_scope.
-Lemma expnE : expn = expn_rec.
+Lemma expnE : expn = expn_rec.
-Lemma expn0 m : m ^ 0 = 1.
-Lemma expn1 m : m ^ 1 = m.
-Lemma expnS m n : m ^ n.+1 = m × m ^ n.
-Lemma expnSr m n : m ^ n.+1 = m ^ n × m.
+Lemma expn0 m : m ^ 0 = 1.
+Lemma expn1 m : m ^ 1 = m.
+Lemma expnS m n : m ^ n.+1 = m × m ^ n.
+Lemma expnSr m n : m ^ n.+1 = m ^ n × m.
-Lemma iter_muln m n p : iter n (muln m) p = m ^ n × p.
+Lemma iter_muln m n p : iter n (muln m) p = m ^ n × p.
-Lemma iter_muln_1 m n : iter n (muln m) 1 = m ^ n.
+Lemma iter_muln_1 m n : iter n (muln m) 1 = m ^ n.
-Lemma exp0n n : 0 < n → 0 ^ n = 0.
+Lemma exp0n n : 0 < n → 0 ^ n = 0.
-Lemma exp1n n : 1 ^ n = 1.
+Lemma exp1n n : 1 ^ n = 1.
-Lemma expnD m n1 n2 : m ^ (n1 + n2) = m ^ n1 × m ^ n2.
+Lemma expnD m n1 n2 : m ^ (n1 + n2) = m ^ n1 × m ^ n2.
-Lemma expnMn m1 m2 n : (m1 × m2) ^ n = m1 ^ n × m2 ^ n.
+Lemma expnMn m1 m2 n : (m1 × m2) ^ n = m1 ^ n × m2 ^ n.
-Lemma expnM m n1 n2 : m ^ (n1 × n2) = (m ^ n1) ^ n2.
+Lemma expnM m n1 n2 : m ^ (n1 × n2) = (m ^ n1) ^ n2.
-Lemma expnAC m n1 n2 : (m ^ n1) ^ n2 = (m ^ n2) ^ n1.
+Lemma expnAC m n1 n2 : (m ^ n1) ^ n2 = (m ^ n2) ^ n1.
-Lemma expn_gt0 m n : (0 < m ^ n) = (0 < m) || (n == 0).
+Lemma expn_gt0 m n : (0 < m ^ n) = (0 < m) || (n == 0).
-Lemma expn_eq0 m e : (m ^ e == 0) = (m == 0) && (e > 0).
+Lemma expn_eq0 m e : (m ^ e == 0) = (m == 0) && (e > 0).
-Lemma ltn_expl m n : 1 < m → n < m ^ n.
+Lemma ltn_expl m n : 1 < m → n < m ^ n.
-Lemma leq_exp2l m n1 n2 : 1 < m → (m ^ n1 ≤ m ^ n2) = (n1 ≤ n2).
+Lemma leq_exp2l m n1 n2 : 1 < m → (m ^ n1 ≤ m ^ n2) = (n1 ≤ n2).
-Lemma ltn_exp2l m n1 n2 : 1 < m → (m ^ n1 < m ^ n2) = (n1 < n2).
+Lemma ltn_exp2l m n1 n2 : 1 < m → (m ^ n1 < m ^ n2) = (n1 < n2).
-Lemma eqn_exp2l m n1 n2 : 1 < m → (m ^ n1 == m ^ n2) = (n1 == n2).
+Lemma eqn_exp2l m n1 n2 : 1 < m → (m ^ n1 == m ^ n2) = (n1 == n2).
-Lemma expnI m : 1 < m → injective (expn m).
+Lemma expnI m : 1 < m → injective (expn m).
-Lemma leq_pexp2l m n1 n2 : 0 < m → n1 ≤ n2 → m ^ n1 ≤ m ^ n2.
+Lemma leq_pexp2l m n1 n2 : 0 < m → n1 ≤ n2 → m ^ n1 ≤ m ^ n2.
-Lemma ltn_pexp2l m n1 n2 : 0 < m → m ^ n1 < m ^ n2 → n1 < n2.
+Lemma ltn_pexp2l m n1 n2 : 0 < m → m ^ n1 < m ^ n2 → n1 < n2.
-Lemma ltn_exp2r m n e : e > 0 → (m ^ e < n ^ e) = (m < n).
+Lemma ltn_exp2r m n e : e > 0 → (m ^ e < n ^ e) = (m < n).
-Lemma leq_exp2r m n e : e > 0 → (m ^ e ≤ n ^ e) = (m ≤ n).
+Lemma leq_exp2r m n e : e > 0 → (m ^ e ≤ n ^ e) = (m ≤ n).
-Lemma eqn_exp2r m n e : e > 0 → (m ^ e == n ^ e) = (m == n).
+Lemma eqn_exp2r m n e : e > 0 → (m ^ e == n ^ e) = (m == n).
-Lemma expIn e : e > 0 → injective (expn^~ e).
+Lemma expIn e : e > 0 → injective (expn^~ e).
@@ -1186,25 +1210,25 @@
@@ -1215,55 +1239,55 @@
@@ -1274,63 +1298,63 @@
@@ -1341,49 +1365,49 @@
@@ -1394,34 +1418,34 @@
@@ -1440,55 +1464,185 @@
-
Definition leqif m n C := (
(m ≤ n) × ((m == n) = C))%
type.
+
Definition leqif m n C := (
(m ≤ n) × ((m == n) = C))%
type.
-
Notation "m <= n ?= 'iff' C" := (
leqif m n C) :
nat_scope.
+
Notation "m <= n ?= 'iff' C" := (
leqif m n C) :
nat_scope.
-
Coercion leq_of_leqif m n C (
H :
m ≤ n ?= iff C) :=
H.1 : m ≤ n.
+
Coercion leq_of_leqif m n C (
H :
m ≤ n ?= iff C) :=
H.1 : m ≤ n.
-
Lemma leqifP m n C :
reflect (
m ≤ n ?= iff C) (
if C then m == n else m < n).
+
Lemma leqifP m n C :
reflect (
m ≤ n ?= iff C) (
if C then m == n else m < n).
-
Lemma leqif_refl m C :
reflect (
m ≤ m ?= iff C)
C.
+
Lemma leqif_refl m C :
reflect (
m ≤ m ?= iff C)
C.
Lemma leqif_trans m1 m2 m3 C12 C23 :
-
m1 ≤ m2 ?= iff C12 → m2 ≤ m3 ?= iff C23 → m1 ≤ m3 ?= iff C12 && C23.
+
m1 ≤ m2 ?= iff C12 → m2 ≤ m3 ?= iff C23 → m1 ≤ m3 ?= iff C12 && C23.
-
Lemma mono_leqif f :
{mono f : m n / m ≤ n} →
-
∀ m n C,
(f m ≤ f n ?= iff C) = (m ≤ n ?= iff C).
+
Lemma mono_leqif f :
{mono f : m n / m ≤ n} →
+
∀ m n C,
(f m ≤ f n ?= iff C) = (m ≤ n ?= iff C).
-
Lemma leqif_geq m n :
m ≤ n → m ≤ n ?= iff (m ≥ n).
+
Lemma leqif_geq m n :
m ≤ n → m ≤ n ?= iff (m ≥ n).
-
Lemma leqif_eq m n :
m ≤ n → m ≤ n ?= iff (m == n).
+
Lemma leqif_eq m n :
m ≤ n → m ≤ n ?= iff (m == n).
-
Lemma geq_leqif a b C :
a ≤ b ?= iff C → (b ≤ a) = C.
+
Lemma geq_leqif a b C :
a ≤ b ?= iff C → (b ≤ a) = C.
-
Lemma ltn_leqif a b C :
a ≤ b ?= iff C → (a < b) = ~~ C.
+
Lemma ltn_leqif a b C :
a ≤ b ?= iff C → (a < b) = ~~ C.
Lemma leqif_add m1 n1 C1 m2 n2 C2 :
-
m1 ≤ n1 ?= iff C1 → m2 ≤ n2 ?= iff C2 →
-
m1 + m2 ≤ n1 + n2 ?= iff C1 && C2.
+
m1 ≤ n1 ?= iff C1 → m2 ≤ n2 ?= iff C2 →
+
m1 + m2 ≤ n1 + n2 ?= iff C1 && C2.
Lemma leqif_mul m1 n1 C1 m2 n2 C2 :
-
m1 ≤ n1 ?= iff C1 → m2 ≤ n2 ?= iff C2 →
-
m1 × m2 ≤ n1 × n2 ?= iff (n1 × n2 == 0
) || (C1 && C2).
+
m1 ≤ n1 ?= iff C1 → m2 ≤ n2 ?= iff C2 →
+
m1 × m2 ≤ n1 × n2 ?= iff (n1 × n2 == 0
) || (C1 && C2).
+
+
+
Lemma nat_Cauchy m n : 2
× (m × n) ≤ m ^ 2
+ n ^ 2
?= iff (m == n).
+
+
+
Lemma nat_AGM2 m n : 4
× (m × n) ≤ (m + n) ^ 2
?= iff (m == n).
-
Lemma nat_Cauchy m n : 2
× (m × n) ≤ m ^ 2
+ n ^ 2
?= iff (m == n).
+
Section Monotonicity.
+
Variable T :
Type.
+
+
+
Lemma homo_ltn_in (
D :
{pred nat}) (
f :
nat → T) (
r :
T → T → Prop) :
+
(∀ y x z,
r x y → r y z → r x z) →
+
{in D &, ∀ i j k,
i < k < j → k \in D} →
+
{in D, ∀ i,
i.+1 \in D → r (
f i) (
f i.+1)
} →
+
{in D &, {homo f : i j / i < j >-> r i j}}.
+
+
+
Lemma homo_ltn (
f :
nat → T) (
r :
T → T → Prop) :
+
(∀ y x z,
r x y → r y z → r x z) →
+
(∀ i,
r (
f i) (
f i.+1)
) → {homo f : i j / i < j >-> r i j}.
+
+
+
Lemma homo_leq_in (
D :
{pred nat}) (
f :
nat → T) (
r :
T → T → Prop) :
+
(∀ x,
r x x) → (∀ y x z,
r x y → r y z → r x z) →
+
{in D &, ∀ i j k,
i < k < j → k \in D} →
+
{in D, ∀ i,
i.+1 \in D → r (
f i) (
f i.+1)
} →
+
{in D &, {homo f : i j / i ≤ j >-> r i j}}.
+
+
+
Lemma homo_leq (
f :
nat → T) (
r :
T → T → Prop) :
+
(∀ x,
r x x) → (∀ y x z,
r x y → r y z → r x z) →
+
(∀ i,
r (
f i) (
f i.+1)
) → {homo f : i j / i ≤ j >-> r i j}.
+
+
+
Section NatToNat.
+
Variable (
f :
nat → nat).
+
+
+
+
+
+ This listing of "Let"s factor out the required premices for the
+ subsequent lemmas, putting them in the context so that "done" solves the
+ goals quickly
+
+
+
+
+
Let ltn_neqAle :=
ltn_neqAle.
+
Let gtn_neqAge x y :
(y < x) = (x != y) && (y ≤ x).
+
Let anti_leq :=
anti_leq.
+
Let anti_geq :
antisymmetric geq.
+
Let leq_total :=
leq_total.
+
+
+
Lemma ltnW_homo :
{homo f : m n / m < n} → {homo f : m n / m ≤ n}.
+
+
+
Lemma homo_inj_lt :
injective f → {homo f : m n / m ≤ n} →
+
{homo f : m n / m < n}.
+
+
+
Lemma ltnW_nhomo :
{homo f : m n /~ m < n} → {homo f : m n /~ m ≤ n}.
+
+
+
Lemma nhomo_inj_lt :
injective f → {homo f : m n /~ m ≤ n} →
+
{homo f : m n /~ m < n}.
+
+
+
Lemma incrn_inj :
{mono f : m n / m ≤ n} → injective f.
+
+
+
Lemma decrn_inj :
{mono f : m n /~ m ≤ n} → injective f.
+
+
+
Lemma leqW_mono :
{mono f : m n / m ≤ n} → {mono f : m n / m < n}.
+
+
+
Lemma leqW_nmono :
{mono f : m n /~ m ≤ n} → {mono f : m n /~ m < n}.
+
+
+
Lemma leq_mono :
{homo f : m n / m < n} → {mono f : m n / m ≤ n}.
+
+
+
Lemma leq_nmono :
{homo f : m n /~ m < n} → {mono f : m n /~ m ≤ n}.
+
+
+
Variables (
D D' :
{pred nat}).
-
Lemma nat_AGM2 m n : 4
× (m × n) ≤ (m + n) ^ 2
?= iff (m == n).
+
Lemma ltnW_homo_in :
{in D & D', {homo f : m n / m < n}} →
+
{in D & D', {homo f : m n / m ≤ n}}.
+
+
+
Lemma ltnW_nhomo_in :
{in D & D', {homo f : m n /~ m < n}} →
+
{in D & D', {homo f : m n /~ m ≤ n}}.
+
+
+
Lemma homo_inj_lt_in :
{in D & D', injective f} →
+
{in D & D', {homo f : m n / m ≤ n}} →
+
{in D & D', {homo f : m n / m < n}}.
+
+
+
Lemma nhomo_inj_lt_in :
{in D & D', injective f} →
+
{in D & D', {homo f : m n /~ m ≤ n}} →
+
{in D & D', {homo f : m n /~ m < n}}.
+
+
+
Lemma incrn_inj_in :
{in D &, {mono f : m n / m ≤ n}} →
+
{in D &, injective f}.
+
+
+
Lemma decrn_inj_in :
{in D &, {mono f : m n /~ m ≤ n}} →
+
{in D &, injective f}.
+
+
+
Lemma leqW_mono_in :
{in D &, {mono f : m n / m ≤ n}} →
+
{in D &, {mono f : m n / m < n}}.
+
+
+
Lemma leqW_nmono_in :
{in D &, {mono f : m n /~ m ≤ n}} →
+
{in D &, {mono f : m n /~ m < n}}.
+
+
+
Lemma leq_mono_in :
{in D &, {homo f : m n / m < n}} →
+
{in D &, {mono f : m n / m ≤ n}}.
+
+
+
Lemma leq_nmono_in :
{in D &, {homo f : m n /~ m < n}} →
+
{in D &, {mono f : m n /~ m ≤ n}}.
+
+
+
End NatToNat.
+
End Monotonicity.
-
Fixpoint add m n :=
if m is m'.+1 then m' + n.+1 else n
-
where "n + m" := (
add n m) :
nat_scope.
+
Fixpoint add m n :=
if m is m'.+1 then m' + n.+1 else n
+
where "n + m" := (
add n m) :
nat_scope.
-
Fixpoint add_mul m n s :=
if m is m'.+1 then add_mul m' n (
n + s)
else s.
+
Fixpoint add_mul m n s :=
if m is m'.+1 then add_mul m' n (
n + s)
else s.
-
Definition mul m n :=
if m is m'.+1 then add_mul m' n n else 0.
+
Definition mul m n :=
if m is m'.+1 then add_mul m' n n else 0.
-
Notation "n * m" := (
mul n m) :
nat_scope.
+
Notation "n * m" := (
mul n m) :
nat_scope.
-
Fixpoint mul_exp m n p :=
if n is n'.+1 then mul_exp m n' (
m × p)
else p.
+
Fixpoint mul_exp m n p :=
if n is n'.+1 then mul_exp m n' (
m × p)
else p.
-
Definition exp m n :=
if n is n'.+1 then mul_exp m n' m else 1.
+
Definition exp m n :=
if n is n'.+1 then mul_exp m n' m else 1.
-
Notation "n ^ m" := (
exp n m) :
nat_scope.
+
Notation "n ^ m" := (
exp n m) :
nat_scope.
-
Fixpoint odd n :=
if n is n'.+2 then odd n' else eqn n 1.
+
Fixpoint odd n :=
if n is n'.+2 then odd n' else eqn n 1.
-
Definition double n :=
if n is n'.+1 then n' + n.+1 else 0.
-
Notation "n .*2" := (
double n) :
nat_scope.
+
Definition double n :=
if n is n'.+1 then n' + n.+1 else 0.
+
Notation "n .*2" := (
double n) :
nat_scope.
-
Lemma addE :
add =2 addn.
+
Lemma addE :
add =2 addn.
-
Lemma doubleE :
double =1 doublen.
+
Lemma doubleE :
double =1 doublen.
-
Lemma add_mulE n m s :
add_mul n m s = addn (
muln n m)
s.
+
Lemma add_mulE n m s :
add_mul n m s = addn (
muln n m)
s.
-
Lemma mulE :
mul =2 muln.
+
Lemma mulE :
mul =2 muln.
-
Lemma mul_expE m n p :
mul_exp m n p = muln (
expn m n)
p.
+
Lemma mul_expE m n p :
mul_exp m n p = muln (
expn m n)
p.
-
Lemma expE :
exp =2 expn.
+
Lemma expE :
exp =2 expn.
-
Lemma oddE :
odd =1 oddn.
+
Lemma oddE :
odd =1 oddn.
-
Definition trecE :=
(addE, (doubleE, oddE), (mulE, add_mulE, (expE, mul_expE))).
+
Definition trecE :=
(addE, (doubleE, oddE), (mulE, add_mulE, (expE, mul_expE))).
End NatTrec.
@@ -1579,11 +1733,13 @@
Notation natTrecE :=
NatTrec.trecE.
-
Lemma eq_binP :
Equality.axiom Ndec.Neqb.
+
Lemma eq_binP :
Equality.axiom N.eqb.
Canonical bin_nat_eqMixin :=
EqMixin eq_binP.
-
Canonical bin_nat_eqType :=
Eval hnf in EqType N bin_nat_eqMixin.
+
Canonical bin_nat_eqType :=
Eval hnf in EqType N bin_nat_eqMixin.
+
+
Section NumberInterpretation.
@@ -1600,9 +1756,9 @@
Fixpoint nat_of_pos p0 :=
match p0 with
- |
xO p ⇒
(nat_of_pos p).*2
- |
xI p ⇒
(nat_of_pos p).*2.+1
- |
xH ⇒ 1
+ |
xO p ⇒
(nat_of_pos p).*2
+ |
xI p ⇒
(nat_of_pos p).*2.+1
+ |
xH ⇒ 1
end.
@@ -1611,40 +1767,43 @@
-
Coercion nat_of_bin b :=
if b is Npos p then p : nat else 0.
+
Coercion nat_of_bin b :=
if b is Npos p then p : nat else 0.
Fixpoint pos_of_nat n0 m0 :=
match n0,
m0 with
- |
n.+1,
m.+2 ⇒
pos_of_nat n m
- |
n.+1, 1 ⇒
xO (
pos_of_nat n n)
- |
n.+1, 0 ⇒
xI (
pos_of_nat n n)
- | 0,
_ ⇒
xH
+ |
n.+1,
m.+2 ⇒
pos_of_nat n m
+ |
n.+1, 1 ⇒
xO (
pos_of_nat n n)
+ |
n.+1, 0 ⇒
xI (
pos_of_nat n n)
+ | 0,
_ ⇒
xH
end.
-
Definition bin_of_nat n0 :=
if n0 is n.+1 then Npos (
pos_of_nat n n)
else 0%
num.
+
Definition bin_of_nat n0 :=
if n0 is n.+1 then Npos (
pos_of_nat n n)
else 0%
num.
-
Lemma bin_of_natK :
cancel bin_of_nat nat_of_bin.
+
Lemma bin_of_natK :
cancel bin_of_nat nat_of_bin.
-
Lemma nat_of_binK :
cancel nat_of_bin bin_of_nat.
+
Lemma nat_of_binK :
cancel nat_of_bin bin_of_nat.
-
Lemma nat_of_succ_gt0 p :
Psucc p = p.+1 :> nat.
+
Lemma nat_of_succ_pos p :
Pos.succ p = p.+1 :> nat.
-
Lemma nat_of_addn_gt0 p q : (
p + q)%
positive = p + q :> nat.
+
Lemma nat_of_add_pos p q : (
p + q)%
positive = p + q :> nat.
+
+
+
Lemma nat_of_mul_pos p q : (
p × q)%
positive = p × q :> nat.
-
Lemma nat_of_add_bin b1 b2 : (
b1 + b2)%
num = b1 + b2 :> nat.
+
Lemma nat_of_add_bin b1 b2 : (
b1 + b2)%
num = b1 + b2 :> nat.
-
Lemma nat_of_mul_bin b1 b2 : (
b1 × b2)%
num = b1 × b2 :> nat.
-
+
Lemma nat_of_mul_bin b1 b2 : (
b1 × b2)%
num = b1 × b2 :> nat.
+
-
Lemma nat_of_exp_bin n (
b :
N) :
n ^ b = pow_N 1
muln n b.
+
Lemma nat_of_exp_bin n (
b :
N) :
n ^ b = pow_N 1
muln n b.
End NumberInterpretation.
@@ -1663,21 +1822,21 @@
-
Record number :
Type :=
Num {
bin_of_number :>
N}.
+
Record number :
Type :=
Num {
bin_of_number :>
N}.
-
Definition extend_number (
nn :
number)
m :=
Num (
nn × 1000
+ bin_of_nat m).
+
Definition extend_number (
nn :
number)
m :=
Num (
nn × 1000
+ bin_of_nat m).
Coercion extend_number : number >-> Funclass.
-
Canonical number_subType :=
[newType for bin_of_number].
-
Definition number_eqMixin :=
Eval hnf in [eqMixin of number by <:].
+
Canonical number_subType :=
[newType for bin_of_number].
+
Definition number_eqMixin :=
Eval hnf in [eqMixin of number by <:].
Canonical number_eqType :=
Eval hnf in EqType number number_eqMixin.
-
Notation "[ 'Num' 'of' e ]" := (
Num (
bin_of_nat e))
+
Notation "[ 'Num' 'of' e ]" := (
Num (
bin_of_nat e))
(
at level 0,
format "[ 'Num' 'of' e ]") :
nat_scope.
@@ -1689,14 +1848,14 @@
@@ -1707,7 +1866,7 @@
-
Fixpoint pop_succn e :=
if e is e'.+1 then fun n ⇒
pop_succn e' n.+1 else id.
+
Fixpoint pop_succn e :=
if e is e'.+1 then fun n ⇒
pop_succn e' n.+1 else id.
Ltac pop_succn e :=
eval lazy beta iota delta [
pop_succn]
in (
pop_succn e 1).
@@ -1715,18 +1874,18 @@
Ltac nat_litteral e :=
match pop_succn e with
- | ?
n.+1 ⇒
constr: (
bin_of_nat n)
+ | ?
n.+1 ⇒
constr: (
bin_of_nat n)
|
_ ⇒
NotConstant
end.
Ltac succn_to_add :=
match goal with
- | |-
context G [?
e.+1] ⇒
+ | |-
context G [?
e.+1] ⇒
let x :=
fresh "NatLit0"
in
match pop_succn e with
- | ?
n.+1 ⇒
pose x :=
n.+1;
let G' :=
context G [
x]
in change G'
- |
_ ?
e' ?
n ⇒
pose x :=
n;
let G' :=
context G [
x + e']
in change G'
+ | ?
n.+1 ⇒
pose x :=
n.+1;
let G' :=
context G [
x]
in change G'
+ |
_ ?
e' ?
n ⇒
pose x :=
n;
let G' :=
context G [
x + e']
in change G'
end;
succn_to_add;
rewrite {}/
x
|
_ ⇒
idtac
end.
@@ -1747,19 +1906,19 @@
Ltac nat_norm :=
-
succn_to_add;
rewrite ?
add0n ?
addn0 -?
addnA ?
(addSn, addnS, add0n, addn0).
+
succn_to_add;
rewrite ?
add0n ?
addn0 -?
addnA ?
(addSn, addnS, add0n, addn0).
Ltac nat_congr :=
first
- [
apply: (
congr1 succn _)
- |
apply: (
congr1 predn _)
- |
apply: (
congr1 (
addn _)
_)
- |
apply: (
congr1 (
subn _)
_)
- |
apply: (
congr1 (
addn^~ _)
_)
- |
match goal with |- (?
X1 + ?
X2 = ?
X3) ⇒
+ [
apply: (
congr1 succn _)
+ |
apply: (
congr1 predn _)
+ |
apply: (
congr1 (
addn _)
_)
+ |
apply: (
congr1 (
subn _)
_)
+ |
apply: (
congr1 (
addn^~ _)
_)
+ |
match goal with |- (?
X1 + ?
X2 = ?
X3) ⇒
symmetry;
rewrite -1?(
addnC X1) -?(
addnCA X1);
-
apply: (
congr1 (
addn X1)
_);
+
apply: (
congr1 (
addn X1)
_);
symmetry
end ].
--
cgit v1.2.3