Module mathcomp.boot.ssrnat
From Corelib Require Import PosDef.From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
A version of arithmetic on nat (natural numbers) that is better suited to
small scale reflection than the Coq Arith library. It contains an
extensive equational theory (including, e.g., the AGM inequality), as well
as a congruence tactic.
The following operations and notations are provided:
successor and predecessor
n.+1, n.+2, n.+3, n.+4 and n.-1, n.-2
this frees the names "S" and "pred"
basic arithmetic
m + n, m - n, m * n
Important: m - n denotes TRUNCATED subtraction: m - n = 0 if m <= n.
The definitions use simpl never to prevent undesirable computation
during simplification, but remain compatible with the ones provided in
the Coq.Init.Peano prelude.
For computation, a module NatTrec rebinds all arithmetic notations
to less convenient but also less inefficient tail-recursive functions;
the auxiliary functions used by these versions are flagged with %Nrec.
Also, there is support for input and output of large nat values.
Num 3 082 241 inputs the number 3082241
[Num of n] outputs the value n
There are coercions num >-> BinNat.N >-> nat; ssrnat rebinds the scope
delimiter for BinNat.N to %num (to be used with notations from
`From Stdlib Require Import BinNatDef`), as it uses the shorter %N for
its own notations (Peano notations are flagged with %coq_nat).
doubling, halving, and parity
n.*2, n./2, odd n, uphalf n, with uphalf n = n.+1./2
bool coerces to nat so we can write, e.g., n = odd n + n./2.*2.
iteration
iter n f x0 == f ( .. (f x0))
iteri n g x0 == g n.-1 (g ... (g 0 x0))
iterop n op x x0 == op x (... op x x) (n x's) or x0 if n = 0
exponentiation, factorial
m ^ n, n`!
m ^ 1 is convertible to m, and m ^ 2 to m * m
comparison
m <= n, m < n, m >= n, m > n, m == n, m <= n <= p, etc.,
comparisons are BOOLEAN operators, and m == n is the generic eqType
operation.
Most compatibility lemmas are stated as boolean equalities; this keeps
the size of the library down. All the inequalities refer to the same
constant "leq"; in particular m < n is identical to m.+1 <= n.
-> patterns for contextual rewriting:
leqLHS := (X in (X <= _)%N)%pattern
leqRHS := (X in (_ <= X)%N)%pattern
ltnLHS := (X in (X < _)%N)%pattern
ltnRHS := (X in (_ < X)%N)%pattern
conditionally strict inequality `leqif'
m <= n ?= iff condition == (m <= n) and ((m == n) = condition)
This is actually a pair of boolean equalities, so rewriting with an
`leqif' lemma can affect several kinds of comparison. The transitivity
lemma for leqif aggregates the conditions, allowing for arguments of
the form ``m <= n <= p <= m, so equality holds throughout''.
maximum and minimum
maxn m n, minn m n
Note that maxn m n = m + (n - m), due to the truncating subtraction.
Absolute difference (linear distance) between nats is defined in the int
library (in the int.IntDist sublibrary), with the syntax `|m - n|. The
'-' in this notation is the signed integer difference.
countable choice
ex_minn : forall P : pred nat, (exists n, P n) -> nat
This returns the smallest n such that P n holds.
ex_maxn : forall (P : pred nat) m,
(exists n, P n) -> (forall n, P n -> n <= m) -> nat
This returns the largest n such that P n holds (given an explicit upper
bound).
This file adds the following suffix conventions to those documented in
ssrbool.v and eqtype.v:
A (infix) -- conjunction, as in
ltn_neqAle : (m < n) = (m != n) && (m <= n).
B -- subtraction, as in subBn : (m - n) - p = m - (n + p).
D -- addition, as in mulnDl : (m + n) * p = m * p + n * p.
M -- multiplication, as in expnMn : (m * n) ^ p = m ^ p * n ^ p.
p (prefix) -- positive, as in
eqn_pmul2l : m > 0 -> (m * n1 == m * n2) = (n1 == n2).
P -- greater than 1, as in
ltn_Pmull : 1 < n -> 0 < m -> m < n * m.
S -- successor, as in addSn : n.+1 + m = (n + m).+1.
V (infix) -- disjunction, as in
leq_eqVlt : (m <= n) = (m == n) || (m < n).
X - exponentiation, as in lognX : logn p (m ^ n) = logn p m * n in
file prime.v (the suffix is not used in this file).
Suffixes that abbreviate operations (D, B, M and X) are used to abbreviate
second-rank operations in equational lemma names that describe left-hand
sides (e.g., mulnDl); they are not used to abbreviate the main operation
of relational lemmas (e.g., leq_add2l).
For the asymmetrical exponentiation operator expn (m ^ n) a right suffix
indicates an operation on the exponent, e.g., expnM : m ^ (n1 * n2) = ...;
a trailing "n" is used to indicate the left operand, e.g.,
expnMn : (m1 * m2) ^ n = ... The operands of other operators are selected
using the l/r suffixes.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Declare Scope coq_nat_scope.
#[global] Remove Hints plus_n_O plus_n_Sm mult_n_O mult_n_Sm : core.
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.
Delimit Scope N_scope with num.
#[warning="-hiding-delimiting-key"]
Delimit Scope nat_scope with N.
Notation succn := Datatypes.S.
Notation predn := Peano.pred.
Notation "n .+1" := (succn n) (left associativity, format "n .+1") : nat_scope.
Notation "n .+2" := n.+1.+1 (left associativity, format "n .+2") : nat_scope.
Notation "n .+3" := n.+2.+1 (left associativity, format "n .+3") : nat_scope.
Notation "n .+4" := n.+2.+2 (left associativity, format "n .+4") : nat_scope.
Notation "n .-1" := (predn n) (left associativity, format "n .-1") : nat_scope.
Notation "n .-2" := n.-1.-1 (left associativity, format "n .-2") : nat_scope.
Lemma succnK : cancel succn predn
Proof.
by []. Qed.
Proof.
by move=> n m []. Qed.
Reserved Notation "n .*2" (left associativity, format "n .*2").
Reserved Notation "n ./2" (left associativity, format "n ./2").
Fixpoint eqn m n {struct m} :=
match m, n with
| 0, 0 => true
| m'.+1, n'.+1 => eqn m' n'
| _, _ => false
end.
Lemma eqnP : Equality.axiom eqn.
Proof.
HB.instance Definition _ := hasDecEq.Build nat eqnP.
Arguments eqn !m !n.
Arguments eqnP {x y}.
Lemma eqnE : eqn = eq_op
Proof.
by []. Qed.
Lemma eqSS m n : (m.+1 == n.+1) = (m == n)
Proof.
by []. Qed.
Lemma nat_irrelevance (x y : nat) (E E' : x = y) : E = E'.
Proof.
Definition addn := plus.
Arguments addn : simpl never.
#[deprecated(since="mathcomp 2.3.0", use=addn)]
Definition addn_rec := addn.
Notation "m + n" := (addn m n) : nat_scope.
Lemma addnE : addn = plus
Proof.
by []. Qed.
Lemma plusE : plus = addn
Proof.
by []. Qed.
Lemma add0n : left_id 0 addn
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
by []. Qed.
Lemma addn0 : right_id 0 addn
Proof.
Lemma addnS m n : m + n.+1 = (m + n).+1
Proof.
Lemma addSnnS m n : m.+1 + n = m + n.+1
Proof.
Lemma addnCA : left_commutative addn.
Proof.
Lemma addnC : commutative addn.
Lemma addn1 n : n + 1 = n.+1
Proof.
Lemma addnA : associative addn.
Lemma addnAC : right_commutative addn.
Lemma addnCAC m n p : m + n + p = p + n + m.
Lemma addnACl m n p: m + n + p = n + (p + m).
Lemma addnACA : interchange addn addn.
Lemma addn_eq0 m n : (m + n == 0) = (m == 0) && (n == 0).
Proof.
by case: m; case: n. Qed.
Lemma addn_eq1 m n :
(m + n == 1) = ((m == 1) && (n == 0)) || ((m == 0) && (n == 1)).
Proof.
by case: m n => [|[|m]] [|[|n]]. Qed.
Lemma eqn_add2l p m n : (p + m == p + n) = (m == n).
Proof.
by elim: p. Qed.
Lemma eqn_add2r p m n : (m + p == n + p) = (m == n).
Lemma addnI : right_injective addn.
Lemma addIn : left_injective addn.
Lemma addn2 m : m + 2 = m.+2
Proof.
Proof.
by []. Qed.
Proof.
Proof.
by []. Qed.
Proof.
Proof.
by []. Qed.
Definition subn := minus.
Arguments subn : simpl never.
#[deprecated(since="mathcomp 2.3.0", use=subn)]
Definition subn_rec := subn.
Notation "m - n" := (subn m n) : nat_scope.
Lemma subnE : subn = minus
Proof.
by []. Qed.
Proof.
by []. Qed.
Lemma sub0n : left_zero 0 subn
Proof.
by []. Qed.
Proof.
by case. Qed.
Proof.
by elim. Qed.
Lemma subSS n m : m.+1 - n.+1 = m - n
Proof.
by []. Qed.
Proof.
by case: n => [|[]]. Qed.
Proof.
by case: n => [|[|[]]]. Qed.
Lemma subnDl p m n : (p + m) - (p + n) = m - n.
Proof.
by elim: p. Qed.
Lemma subnDr p m n : (m + p) - (n + p) = m - n.
Lemma addnK n : cancel (addn^~ n) (subn^~ n).
Lemma addKn n : cancel (addn n) (subn^~ n).
Lemma subSnn n : n.+1 - n = 1.
Proof.
Lemma subnDA m n p : n - (m + p) = (n - m) - p.
Proof.
by elim: m n => [|m IHm] []. Qed.
Lemma subnAC : right_commutative subn.
Lemma subnS m n : m - n.+1 = (m - n).-1.
Lemma subSKn m n : (m.+1 - n).-1 = m - n.
Proof.
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.
Definition geq := [rel m n | m >= n].
Definition ltn := [rel m n | m < n].
Definition gtn := [rel m n | m > n].
Notation "m <= n <= p" := ((m <= n) && (n <= p)) : nat_scope.
Notation "m < n <= p" := ((m < n) && (n <= p)) : nat_scope.
Notation "m <= n < p" := ((m <= n) && (n < p)) : nat_scope.
Notation "m < n < p" := ((m < n) && (n < p)) : nat_scope.
Lemma ltnS m n : (m < n.+1) = (m <= n)
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
by elim: n. Qed.
Lemma ltnSn n : n < n.+1
Proof.
by []. Qed.
Proof.
by move->. Qed.
Proof.
by elim: n. Qed.
Lemma leq_pred n : n.-1 <= n
Proof.
by case: n => /=. Qed.
Proof.
by case: n => /=. Qed.
Lemma ltn_predL n : (n.-1 < n) = (0 < n).
Proof.
Lemma ltn_predRL m n : (m < n.-1) = (m.+1 < n).
Proof.
Lemma ltn_predK m n : m < n -> n.-1.+1 = n.
Proof.
by case: n. Qed.
Lemma prednK n : 0 < n -> n.-1.+1 = n.
Proof.
Lemma leqNgt m n : (m <= n) = ~~ (n < m).
Proof.
by elim: m n => [|m IHm] []. Qed.
Lemma leqVgt m n : (m <= n) || (n < m)
Lemma ltnNge m n : (m < n) = ~~ (n <= m).
Proof.
Lemma ltnn n : (n < n) = false.
Lemma leqn0 n : (n <= 0) = (n == 0)
Proof.
by case: n. Qed.
Proof.
by case: n. Qed.
Proof.
by case: n. Qed.
Proof.
by case: n. Qed.
Proof.
by case: n. Qed.
Lemma eqn_leq m n : (m == n) = (m <= n <= m).
Proof.
by elim: m n => [|m IHm] []. Qed.
Lemma anti_leq : antisymmetric leq.
Lemma neq_ltn m n : (m != n) = (m < n) || (n < m).
Lemma gtn_eqF m n : m < n -> (n == m) = false.
Lemma ltn_eqF m n : m < n -> (m == n) = false.
Lemma ltn_geF m n : m < n -> (m >= n) = false.
Proof.
Lemma leq_gtF m n : m <= n -> (m > n) = false.
Proof.
Lemma leq_eqVlt m n : (m <= n) = (m == n) || (m < n).
Proof.
by elim: m n => [|m IHm] []. Qed.
Lemma ltn_neqAle m n : (m < n) = (m != n) && (m <= n).
Lemma leq_trans n m p : m <= n -> n <= p -> m <= p.
Proof.
by elim: n m p => [|i IHn] [|m] [|p] //; apply: IHn m p. Qed.
Lemma leq_ltn_trans n m p : m <= n -> n < p -> m < p.
Proof.
Lemma ltn_leq_trans n m p : m < n -> n <= p -> m < p.
Proof.
Lemma ltnW m n : m < n -> m <= n.
Proof.
Lemma leqW m n : m <= n -> m <= n.+1.
Proof.
Lemma ltn_trans n m p : m < n -> n < p -> m < p.
Lemma leq_total m n : (m <= n) || (m >= n).
Lemma leq_leP {m n} : reflect (forall k, n <= k -> m <= k) (m <= n).
Lemma ltn_gtP {m n} : reflect (forall k, k <= m -> k < n) (m < n).
Proof.
Lemma leq_geP {m n} : reflect (forall k, k <= m -> k <= n) (m <= n).
Lemma leq_ltP {m n} : reflect (forall k, n < k -> m < k) (m <= n).
Lemma leq_gtP {m n} : reflect (forall k, k < m -> k < n) (m <= n).
Lemma ltn_ltP {m n} : reflect (forall k, n <= k -> m < k) (m < n).
Proof.
Lemma eqn_geP {m n} : reflect (forall k, (k <= m) = (k <= n)) (m == n).
Lemma eqn_leP {m n} : reflect (forall k, (m <= k) = (n <= k)) (m == n).
Lemma eqn_gtP {m n} : reflect (forall k, (k < m) = (k < n)) (m == n).
Proof.
Lemma eqn_ltP {m n} : reflect (forall k, (m < k) = (n < k)) (m == n).
Proof.
Lemma ubnP m : {n | m < n}
Proof.
Proof.
by []. Qed.
Variant ubn_geq_spec m : nat -> Type := UbnGeq n of m >= n : ubn_geq_spec m n.
Variant ubn_eq_spec m : nat -> Type := UbnEq n of m == n : ubn_eq_spec m n.
Lemma ubnPleq m : ubn_leq_spec m m
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
Lemma leP m n : reflect (m <= n)%coq_nat (m <= n).
Proof.
Lemma le_irrelevance m n le_mn1 le_mn2 : le_mn1 = le_mn2 :> (m <= n)%coq_nat.
Proof.
elim/ltn_ind: n => n IHn in le_mn1 le_mn2 *; set n1 := n in le_mn1 *.
pose def_n : n = n1 := erefl n; transitivity (eq_ind _ _ le_mn2 _ def_n) => //.
case: n1 / le_mn1 le_mn2 => [|n1 le_mn1] {n}[|n le_mn2] in (def_n) IHn *.
- by rewrite [def_n]eq_axiomK.
- by case/leP/idPn: (le_mn2); rewrite -def_n ltnn.
- by case/leP/idPn: (le_mn1); rewrite def_n ltnn.
case: def_n (def_n) => <-{n1} def_n in le_mn1 *.
by rewrite [def_n]eq_axiomK /=; congr le_S; apply: IHn.
Qed.
pose def_n : n = n1 := erefl n; transitivity (eq_ind _ _ le_mn2 _ def_n) => //.
case: n1 / le_mn1 le_mn2 => [|n1 le_mn1] {n}[|n le_mn2] in (def_n) IHn *.
- by rewrite [def_n]eq_axiomK.
- by case/leP/idPn: (le_mn2); rewrite -def_n ltnn.
- by case/leP/idPn: (le_mn1); rewrite def_n ltnn.
case: def_n (def_n) => <-{n1} def_n in le_mn1 *.
by rewrite [def_n]eq_axiomK /=; congr le_S; apply: IHn.
Qed.
Lemma ltP m n : reflect (m < n)%coq_nat (m < n).
Proof.
Lemma lt_irrelevance m n lt_mn1 lt_mn2 : lt_mn1 = lt_mn2 :> (m < n)%coq_nat.
Proof.
Lemma leq_add2l p m n : (p + m <= p + n) = (m <= n).
Proof.
by elim: p. Qed.
Lemma ltn_add2l p m n : (p + m < p + n) = (m < n).
Lemma leq_add2r p m n : (m + p <= n + p) = (m <= n).
Lemma ltn_add2r p m n : (m + p < n + p) = (m < n).
Lemma leq_add m1 m2 n1 n2 : m1 <= n1 -> m2 <= n2 -> m1 + m2 <= n1 + n2.
Lemma leq_addl m n : n <= m + n
Proof.
Lemma leq_addr m n : n <= n + m
Lemma ltn_addl m n p : m < n -> m < p + n.
Lemma ltn_addr m n p : m < n -> m < n + p.
Lemma addn_gt0 m n : (0 < m + n) = (0 < m) || (0 < n).
Lemma subn_gt0 m n : (0 < n - m) = (m < n).
Proof.
by elim: m n => [|m IHm] [|n] //; apply: IHm n. Qed.
Lemma subn_eq0 m n : (m - n == 0) = (m <= n).
Proof.
by []. Qed.
Lemma leq_subLR m n p : (m - n <= p) = (m <= n + p).
Lemma leq_subr m n : n - m <= n.
Lemma ltn_subrR m n : (n < n - m) = false.
Lemma leq_subrR m n : (n <= n - m) = (m == 0) || (n == 0).
Lemma ltn_subrL m n : (n - m < n) = (0 < m) && (0 < n).
Lemma subnKC m n : m <= n -> m + (n - m) = n.
Proof.
by elim: m n => [|m IHm] [|n] // /(IHm n) {2}<-. Qed.
Lemma addnBn m n : m + (n - m) = m - n + n.
Lemma subnK m n : m <= n -> (n - m) + m = n.
Lemma addnBA m n p : p <= n -> m + (n - p) = m + n - p.
Lemma addnBAC m n p : n <= m -> m - n + p = m + p - n.
Lemma addnBCA m n p : p <= m -> p <= n -> m + (n - p) = n + (m - p).
Lemma addnABC m n p : p <= m -> p <= n -> m + (n - p) = m - p + n.
Lemma subnBA m n p : p <= n -> m - (n - p) = m + p - n.
Lemma subnA m n p : p <= n -> n <= m -> m - (n - p) = m - n + p.
Lemma subKn m n : m <= n -> n - (n - m) = m.
Lemma subSn m n : m <= n -> n.+1 - m = (n - m).+1.
Lemma subnSK m n : m < n -> (n - m.+1).+1 = n - m
Proof.
Lemma addnCBA m n p : p <= n -> m + (n - p) = n + m - p.
Lemma addnBr_leq n p m : n <= p -> m + (n - p) = m.
Lemma addnBl_leq m n p : m <= n -> m - n + p = p.
Lemma subnDAC m n p : m - (n + p) = m - p - n.
Lemma subnCBA m n p : p <= n -> m - (n - p) = p + m - n.
Lemma subnBr_leq n p m : n <= p -> m - (n - p) = m.
Lemma subnBl_leq m n p : m <= n -> (m - n) - p = 0.
Lemma subnBAC m n p : p <= n -> n <= m -> m - (n - p) = p + (m - n).
Lemma subDnAC m n p : p <= n -> m + n - p = n - p + m.
Lemma subDnCA m n p : p <= m -> m + n - p = n + (m - p).
Lemma subDnCAC m n p : m <= p -> m + n - p = n - (p - m).
Lemma addnBC m n : m - n + n = n - m + m.
Lemma addnCB m n : m - n + n = m + (n - m).
Lemma addBnAC m n p : n <= m -> m - n + p = p + m - n.
Lemma addBnCAC m n p : n <= m -> n <= p -> m - n + p = p - n + m.
Lemma addBnA m n p : n <= m -> p <= n -> m - n + p = m - (n - p).
Lemma subBnAC m n p : m - n - p = m - (p + n).
Lemma predn_sub m n : (m - n).-1 = (m.-1 - n).
Proof.
Lemma leq_sub2r p m n : m <= n -> m - p <= n - p.
Lemma leq_sub2l p m n : m <= n -> p - n <= p - m.
Lemma leq_sub m1 m2 n1 n2 : m1 <= m2 -> n2 <= n1 -> m1 - n1 <= m2 - n2.
Lemma ltn_sub2r p m n : p < n -> m < n -> m - p < n - p.
Lemma ltn_sub2l p m n : m < p -> m < n -> p - n < p - m.
Lemma ltn_subRL m n p : (n < p - m) = (m + n < p).
Lemma leq_psubRL m n p : 0 < n -> (n <= p - m) = (m + n <= p).
Lemma ltn_psubLR m n p : 0 < p -> (m - n < p) = (m < n + p).
Lemma leq_subRL m n p : m <= p -> (n <= p - m) = (m + n <= p).
Lemma ltn_subLR m n p : n <= m -> (m - n < p) = (m < n + p).
Lemma leq_subCl m n p : (m - n <= p) = (m - p <= n).
Lemma ltn_subCr m n p : (p < m - n) = (n < m - p).
Lemma leq_psubCr m n p : 0 < p -> 0 < n -> (p <= m - n) = (n <= m - p).
Proof.
Lemma ltn_psubCl m n p : 0 < p -> 0 < n -> (m - n < p) = (m - p < n).
Proof.
Lemma leq_subCr m n p : n <= m -> p <= m -> (p <= m - n) = (n <= m - p).
Lemma ltn_subCl m n p : n <= m -> p <= m -> (m - n < p) = (m - p < n).
Lemma leq_sub2rE p m n : p <= n -> (m - p <= n - p) = (m <= n).
Lemma leq_sub2lE m n p : n <= m -> (m - p <= m - n) = (n <= p).
Lemma ltn_sub2rE p m n : p <= m -> (m - p < n - p) = (m < n).
Lemma ltn_sub2lE m n p : p <= m -> (m - p < m - n) = (n < p).
Lemma eqn_sub2rE p m n : p <= m -> p <= n -> (m - p == n - p) = (m == n).
Proof.
Lemma eqn_sub2lE m n p : p <= m -> n <= m -> (m - p == m - n) = (p == n).
Proof.
Definition maxn m n := if m < n then n else m.
Definition minn m n := if m < n then m else n.
Lemma max0n : left_id 0 maxn
Proof.
by case. Qed.
Proof.
by []. Qed.
Lemma maxnC : commutative maxn.
Lemma maxnE m n : maxn m n = m + (n - m).
Proof.
Lemma maxnAC : right_commutative maxn.
Lemma maxnA : associative maxn.
Lemma maxnCA : left_commutative maxn.
Lemma maxnACA : interchange maxn maxn.
Lemma maxn_idPl {m n} : reflect (maxn m n = m) (m >= n).
Lemma maxn_idPr {m n} : reflect (maxn m n = n) (m <= n).
Lemma maxnn : idempotent_op maxn.
Proof.
Lemma leq_max m n1 n2 : (m <= maxn n1 n2) = (m <= n1) || (m <= n2).
Proof.
Lemma leq_maxr m n : n <= maxn m n
Lemma gtn_max m n1 n2 : (m > maxn n1 n2) = (m > n1) && (m > n2).
Lemma geq_max m n1 n2 : (m >= maxn n1 n2) = (m >= n1) && (m >= n2).
Lemma maxnSS m n : maxn m.+1 n.+1 = (maxn m n).+1.
Proof.
Lemma addn_maxl : left_distributive addn maxn.
Lemma addn_maxr : right_distributive addn maxn.
Lemma subn_maxl : left_distributive subn maxn.
Proof.
Lemma min0n : left_zero 0 minn
Proof.
by case. Qed.
Proof.
by []. Qed.
Lemma minnC : commutative minn.
Lemma addn_min_max m n : minn m n + maxn m n = m + n.
Lemma minnE m n : minn m n = m - (m - n).
Proof.
Lemma minnAC : right_commutative minn.
Lemma minnA : associative minn.
Lemma minnCA : left_commutative minn.
Lemma minnACA : interchange minn minn.
Lemma minn_idPl {m n} : reflect (minn m n = m) (m <= n).
Proof.
Lemma minn_idPr {m n} : reflect (minn m n = n) (m >= n).
Lemma minnn : idempotent_op minn.
Proof.
Lemma leq_min m n1 n2 : (m <= minn n1 n2) = (m <= n1) && (m <= n2).
Proof.
Lemma gtn_min m n1 n2 : (m > minn n1 n2) = (m > n1) || (m > n2).
Lemma geq_min m n1 n2 : (m >= minn n1 n2) = (m >= n1) || (m >= n2).
Lemma ltn_min m n1 n2 : (m < minn n1 n2) = (m < n1) && (m < n2).
Proof.
Lemma geq_minl m n : minn m n <= m
Lemma geq_minr m n : minn m n <= n
Lemma addn_minr : right_distributive addn minn.
Lemma addn_minl : left_distributive addn minn.
Lemma subn_minl : left_distributive subn minn.
Proof.
Lemma minnSS m n : minn m.+1 n.+1 = (minn m n).+1.
Proof.
Lemma maxnK m n : minn (maxn m n) m = m.
Lemma maxKn m n : minn n (maxn m n) = n.
Lemma minnK m n : maxn (minn m n) m = m.
Lemma minKn m n : maxn n (minn m n) = n.
Lemma maxn_minl : left_distributive maxn minn.
Proof.
Lemma maxn_minr : right_distributive maxn minn.
Lemma minn_maxl : left_distributive minn maxn.
Lemma minn_maxr : right_distributive minn maxn.
Variant leq_xor_gtn m n : nat -> nat -> nat -> nat -> bool -> bool -> Set :=
| LeqNotGtn of m <= n : leq_xor_gtn m n m m n n true false
| GtnNotLeq of n < m : leq_xor_gtn m n n n m m false true.
Lemma leqP m n : leq_xor_gtn m n (minn n m) (minn m n) (maxn n m) (maxn m n)
(m <= n) (n < m).
Proof.
Variant ltn_xor_geq m n : nat -> nat -> nat -> nat -> bool -> bool -> Set :=
| LtnNotGeq of m < n : ltn_xor_geq m n m m n n false true
| GeqNotLtn of n <= m : ltn_xor_geq m n n n m m true false.
Lemma ltnP m n : ltn_xor_geq m n (minn n m) (minn m n) (maxn n m) (maxn m n)
(n <= m) (m < n).
Proof.
Variant eqn0_xor_gt0 n : bool -> bool -> Set :=
| Eq0NotPos of n = 0 : eqn0_xor_gt0 n true false
| PosNotEq0 of n > 0 : eqn0_xor_gt0 n false true.
Lemma posnP n : eqn0_xor_gt0 n (n == 0) (0 < n).
Proof.
by case: n; constructor. Qed.
Variant compare_nat m n : nat -> nat -> nat -> nat ->
bool -> bool -> bool -> bool -> bool -> bool -> Set :=
| CompareNatLt of m < n :
compare_nat m n m m n n false false false true false true
| CompareNatGt of m > n :
compare_nat m n n n m m false false true false true false
| CompareNatEq of m = n :
compare_nat m n m m m m true true true true false false.
Lemma ltngtP m n :
compare_nat m n (minn n m) (minn m n) (maxn n m) (maxn m n)
(n == m) (m == n) (n <= m) (m <= n) (n < m) (m < n).
Proof.
Lemma subn_if_gt T m n F (E : T) :
(if m.+1 - n is m'.+1 then F m' else E) = (if n <= m then F (m - n) else E).
Notation leqLHS := (X in (X <= _)%N)%pattern.
Notation leqRHS := (X in (_ <= X)%N)%pattern.
Notation ltnLHS := (X in (X < _)%N)%pattern.
Notation ltnRHS := (X in (_ < X)%N)%pattern.
Section ExMinn.
Variable P : pred nat.
Hypothesis exP : exists n, P n.
Inductive acc_nat i : Prop := AccNat0 of P i | AccNatS of acc_nat i.+1.
Lemma find_ex_minn : {m | P m & forall n, P n -> n >= m}.
Proof.
have: forall n, P n -> n >= 0 by [].
have: acc_nat 0.
case exP => n; rewrite -(addn0 n); elim: n 0 => [|n IHn] j; first by left.
by rewrite addSnnS; right; apply: IHn.
move: 0; fix find_ex_minn 2 => m IHm m_lb; case Pm: (P m); first by exists m.
apply: find_ex_minn m.+1 _ _ => [|n Pn]; first by case: IHm; rewrite ?Pm.
by rewrite ltn_neqAle m_lb //; case: eqP Pm => // -> /idP[].
Qed.
have: acc_nat 0.
case exP => n; rewrite -(addn0 n); elim: n 0 => [|n IHn] j; first by left.
by rewrite addSnnS; right; apply: IHn.
move: 0; fix find_ex_minn 2 => m IHm m_lb; case Pm: (P m); first by exists m.
apply: find_ex_minn m.+1 _ _ => [|n Pn]; first by case: IHm; rewrite ?Pm.
by rewrite ltn_neqAle m_lb //; case: eqP Pm => // -> /idP[].
Qed.
Definition ex_minn := s2val find_ex_minn.
Inductive ex_minn_spec : nat -> Type :=
ExMinnSpec m of P m & (forall n, P n -> n >= m) : ex_minn_spec m.
Lemma ex_minnP : ex_minn_spec ex_minn.
Proof.
End ExMinn.
Section ExMaxn.
Variables (P : pred nat) (m : nat).
Hypotheses (exP : exists i, P i) (ubP : forall i, P i -> i <= m).
Lemma ex_maxn_subproof : exists i, P (m - i).
Definition ex_maxn := m - ex_minn ex_maxn_subproof.
Variant ex_maxn_spec : nat -> Type :=
ExMaxnSpec i of P i & (forall j, P j -> j <= i) : ex_maxn_spec i.
Lemma ex_maxnP : ex_maxn_spec ex_maxn.
Proof.
End ExMaxn.
Lemma eq_ex_minn P Q exP exQ : P =1 Q -> @ex_minn P exP = @ex_minn Q exQ.
Proof.
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.
Proof.
Section Iteration.
Variable T : Type.
Implicit Types m n : nat.
Implicit Types x y : T.
Implicit Types S : {pred T}.
Definition iter n f x :=
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.
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).
Proof.
by elim: n => //= n <-. Qed.
Lemma iterS n f x : iter n.+1 f x = f (iter n f x)
Proof.
by []. Qed.
Lemma iterD n m f x : iter (n + m) f x = iter n f (iter m f x).
Proof.
by elim: n => //= n ->. Qed.
Lemma iteriS n f x : iteri n.+1 f x = f n (iteri n f x).
Proof.
by []. Qed.
Lemma iteropS idx n op x : iterop n.+1 op x idx = iter n (op x) x.
Proof.
by elim: n => //= n ->. Qed.
Lemma eq_iter f f' : f =1 f' -> forall n, iter n f =1 iter n f'.
Proof.
by move=> eq_f n x; elim: n => //= n ->; rewrite eq_f. Qed.
Lemma iter_fix n f x : f x = x -> iter n f x = x.
Proof.
by move=> fixf; elim: n => //= n ->. Qed.
Lemma eq_iteri f f' : f =2 f' -> forall n, iteri n f =1 iteri n f'.
Proof.
by move=> eq_f n x; elim: n => //= n ->; rewrite eq_f. Qed.
Lemma eq_iterop n op op' : op =2 op' -> iterop n op =2 iterop n op'.
Proof.
Lemma iter_in f S i : {homo f : x / x \in S} -> {homo iter i f : x / x \in S}.
Proof.
by move=> f_in x xS; elim: i => [|i /f_in]. Qed.
End Iteration.
Lemma iter_succn m n : iter n succn m = m + n.
Proof.
Lemma iter_succn_0 n : iter n succn 0 = n.
Proof.
Lemma iter_predn m n : iter n predn m = m - n.
Definition muln := mult.
Arguments muln : simpl never.
#[deprecated(since="mathcomp 2.3.0", use=muln)]
Definition muln_rec := muln.
Notation "m * n" := (muln m n) : nat_scope.
Lemma multE : mult = muln
Proof.
by []. Qed.
Proof.
by []. Qed.
Lemma mul0n : left_zero 0 muln
Proof.
by []. Qed.
Proof.
by elim. Qed.
Proof.
Proof.
by []. Qed.
Proof.
Lemma mulnS m n : m * n.+1 = m + m * n.
Lemma mulnSr m n : m * n.+1 = m * n + m.
Lemma iter_addn m n p : iter n (addn m) p = m * n + p.
Lemma iter_addn_0 m n : iter n (addn m) 0 = m * n.
Lemma muln1 : right_id 1 muln.
Lemma mulnC : commutative muln.
Lemma mulnDl : left_distributive muln addn.
Proof.
Lemma mulnDr : right_distributive muln addn.
Lemma mulnBl : left_distributive muln subn.
Proof.
Lemma mulnBr : right_distributive muln subn.
Lemma mulnA : associative muln.
Lemma mulnCA : left_commutative muln.
Lemma mulnAC : right_commutative muln.
Lemma mulnACA : interchange muln muln.
Lemma muln_eq0 m n : (m * n == 0) = (m == 0) || (n == 0).
Proof.
Lemma muln_eq1 m n : (m * n == 1) = (m == 1) && (n == 1).
Proof.
Lemma muln_gt0 m n : (0 < m * n) = (0 < m) && (0 < n).
Proof.
Lemma leq_pmull m n : n > 0 -> m <= n * m.
Lemma leq_pmulr m n : n > 0 -> m <= m * n.
Lemma leq_mul2l m n1 n2 : (m * n1 <= m * n2) = (m == 0) || (n1 <= n2).
Lemma leq_mul2r m n1 n2 : (n1 * m <= n2 * m) = (m == 0) || (n1 <= n2).
Lemma leq_mul m1 m2 n1 n2 : m1 <= n1 -> m2 <= n2 -> m1 * m2 <= n1 * n2.
Proof.
Lemma eqn_mul2l m n1 n2 : (m * n1 == m * n2) = (m == 0) || (n1 == n2).
Lemma eqn_mul2r m n1 n2 : (n1 * m == n2 * m) = (m == 0) || (n1 == n2).
Lemma leq_pmul2l m n1 n2 : 0 < m -> (m * n1 <= m * n2) = (n1 <= n2).
Arguments leq_pmul2l [m n1 n2].
Lemma leq_pmul2r m n1 n2 : 0 < m -> (n1 * m <= n2 * m) = (n1 <= n2).
Arguments leq_pmul2r [m n1 n2].
Lemma eqn_pmul2l m n1 n2 : 0 < m -> (m * n1 == m * n2) = (n1 == n2).
Arguments eqn_pmul2l [m n1 n2].
Lemma eqn_pmul2r m n1 n2 : 0 < m -> (n1 * m == n2 * m) = (n1 == n2).
Arguments eqn_pmul2r [m n1 n2].
Lemma ltn_mul2l m n1 n2 : (m * n1 < m * n2) = (0 < m) && (n1 < n2).
Lemma ltn_mul2r m n1 n2 : (n1 * m < n2 * m) = (0 < m) && (n1 < n2).
Lemma ltn_pmul2l m n1 n2 : 0 < m -> (m * n1 < m * n2) = (n1 < n2).
Arguments ltn_pmul2l [m n1 n2].
Lemma ltn_pmul2r m n1 n2 : 0 < m -> (n1 * m < n2 * m) = (n1 < n2).
Arguments ltn_pmul2r [m n1 n2].
Lemma ltn_Pmull m n : 1 < n -> 0 < m -> m < n * m.
Proof.
Lemma ltn_Pmulr m n : 1 < n -> 0 < m -> m < m * n.
Lemma ltn_mull m1 m2 n1 n2 : 0 < n2 -> m1 < n1 -> m2 <= n2 -> m1 * m2 < n1 * n2.
Proof.
move=> n20 lt_mn1 le_mn2.
rewrite (@leq_ltn_trans (m1 * n2)) ?leq_mul2l ?le_mn2 ?orbT//.
by rewrite ltn_mul2r lt_mn1 n20.
Qed.
rewrite (@leq_ltn_trans (m1 * n2)) ?leq_mul2l ?le_mn2 ?orbT//.
by rewrite ltn_mul2r lt_mn1 n20.
Qed.
Lemma ltn_mulr m1 m2 n1 n2 : 0 < n1 -> m1 <= n1 -> m2 < n2 -> m1 * m2 < n1 * n2.
Lemma ltn_mul m1 m2 n1 n2 : m1 < n1 -> m2 < n2 -> m1 * m2 < n1 * n2.
Proof.
Lemma maxnMr : right_distributive muln maxn.
Proof.
Lemma maxnMl : left_distributive muln maxn.
Lemma minnMr : right_distributive muln minn.
Proof.
Lemma minnMl : left_distributive muln minn.
Lemma iterM (T : Type) (n m : nat) (f : T -> T) :
iter (n * m) f =1 iter n (iter m f).
Definition expn m n := iterop n muln m 1.
Arguments expn : simpl never.
#[deprecated(since="mathcomp 2.3.0", use=expn)]
Definition expn_rec := expn.
Notation "m ^ n" := (expn m n) : nat_scope.
Lemma expnE n m : expn m n = iterop n muln m 1
Proof.
by []. Qed.
Lemma expn0 m : m ^ 0 = 1
Proof.
by []. Qed.
Proof.
by []. Qed.
Proof.
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 exp0n n : 0 < n -> 0 ^ n = 0
Proof.
by case: n => [|[]]. Qed.
Lemma exp1n n : 1 ^ n = 1.
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 expnM m n1 n2 : m ^ (n1 * n2) = (m ^ n1) ^ n2.
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_eq0 m e : (m ^ e == 0) = (m == 0) && (e > 0).
Lemma ltn_expl m n : 1 < m -> n < m ^ n.
Proof.
move=> m_gt1; elim: n => //= n; rewrite -(leq_pmul2l (ltnW m_gt1)) expnS.
by apply: leq_trans; apply: ltn_Pmull.
Qed.
by apply: leq_trans; apply: ltn_Pmull.
Qed.
Lemma leq_exp2l m n1 n2 : 1 < m -> (m ^ n1 <= m ^ n2) = (n1 <= n2).
Proof.
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 expnI m : 1 < m -> injective (expn m).
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_exp2r m n e : e > 0 -> (m ^ e < n ^ e) = (m < n).
Proof.
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 expIn e : e > 0 -> injective (expn^~ e).
Lemma iterX (T : Type) (n m : nat) (f : T -> T) :
iter (n ^ m) f =1 iter m (iter n) f.
Fixpoint factorial n := if n is n'.+1 then n * factorial n' else 1.
Arguments factorial : simpl never.
#[deprecated(since="mathcomp 2.3.0", use=factorial)]
Definition fact_rec := factorial.
Notation "n `!" := (factorial n) (at level 1, format "n `!") : nat_scope.
Lemma factE n : factorial n = if n is n'.+1 then n * factorial n' else 1.
Proof.
by case: n. Qed.
Lemma fact0 : 0`! = 1
Proof.
by []. Qed.
Lemma factS n : (n.+1)`! = n.+1 * n`!
Proof.
by []. Qed.
Lemma fact_gt0 n : n`! > 0.
Proof.
Lemma fact_geq n : n <= n`!.
Lemma ltn_fact m n : 0 < m -> m < n -> m`! < n`!.
Proof.
Coercion nat_of_bool (b : bool) := if b then 1 else 0.
Lemma leq_b1 (b : bool) : b <= 1
Proof.
by case: b. Qed.
Lemma addn_negb (b : bool) : ~~ b + b = 1
Proof.
by case: b. Qed.
Lemma eqb0 (b : bool) : (b == 0 :> nat) = ~~ b
Proof.
by case: b. Qed.
Lemma eqb1 (b : bool) : (b == 1 :> nat) = b
Proof.
by case: b. Qed.
Lemma lt0b (b : bool) : (b > 0) = b
Proof.
by case: b. Qed.
Lemma sub1b (b : bool) : 1 - b = ~~ b
Proof.
by case: b. Qed.
Lemma mulnb (b1 b2 : bool) : b1 * b2 = b1 && b2.
Proof.
by case: b1; case: b2. Qed.
Lemma mulnbl (b : bool) n : b * n = (if b then n else 0).
Proof.
Lemma mulnbr (b : bool) n : n * b = (if b then n else 0).
Fixpoint odd n := if n is n'.+1 then ~~ odd n' else false.
Lemma oddS n : odd n.+1 = ~~ odd n
Proof.
by []. Qed.
Lemma oddb (b : bool) : odd b = b
Proof.
by case: b. Qed.
Lemma oddD m n : odd (m + n) = odd m (+) odd n.
Lemma oddB m n : n <= m -> odd (m - n) = odd m (+) odd n.
Lemma oddN i m : odd m = false -> i <= m -> odd (m - i) = odd i.
Proof.
Lemma oddM m n : odd (m * n) = odd m && odd n.
Lemma oddX m n : odd (m ^ n) = (n == 0) || odd m.
Fixpoint double n := if n is n'.+1 then (double n').+2 else 0.
Arguments double : simpl never.
#[deprecated(since="mathcomp 2.3.0", use=double)]
Definition double_rec := double.
Notation "n .*2" := (double n) : nat_scope.
Lemma doubleE n : double n = if n is n'.+1 then (double n').+2 else 0.
Proof.
by case: n. Qed.
Lemma double0 : 0.*2 = 0
Proof.
by []. Qed.
Lemma doubleS n : n.+1.*2 = n.*2.+2
Proof.
by []. Qed.
Lemma double_pred n : n.-1.*2 = n.*2.-2
Proof.
by case: n. Qed.
Lemma predn_doubleS n : n.+1.*2.-1 = n.*2.+1
Proof.
by []. Qed.
Lemma addnn n : n + n = n.*2.
Lemma mul2n m : 2 * m = m.*2.
Lemma muln2 m : m * 2 = m.*2.
Lemma doubleD m n : (m + n).*2 = m.*2 + n.*2.
Lemma doubleB m n : (m - n).*2 = m.*2 - n.*2.
Proof.
by elim: m n => [|m IHm] []. Qed.
Lemma leq_double m n : (m.*2 <= n.*2) = (m <= n).
Lemma ltn_double m n : (m.*2 < n.*2) = (m < n).
Proof.
Lemma ltn_Sdouble m n : (m.*2.+1 < n.*2) = (m < n).
Proof.
Lemma leq_Sdouble m n : (m.*2 <= n.*2.+1) = (m <= n).
Proof.
Lemma odd_double n : odd n.*2 = false.
Lemma double_gt0 n : (0 < n.*2) = (0 < n).
Proof.
by case: n. Qed.
Lemma double_eq0 n : (n.*2 == 0) = (n == 0).
Proof.
by case: n. Qed.
Lemma doubleMl m n : (m * n).*2 = m.*2 * n.
Lemma doubleMr m n : (m * n).*2 = m * n.*2.
Lemma neq_doubleS_double n m : (n.*2.+1 == m.*2) = false.
Proof.
case: (leqP m n) => mn; apply/negbTE; rewrite neq_ltn ?ltn_Sdouble ?mn//.
by rewrite ltnS leq_double mn orbT.
Qed.
by rewrite ltnS leq_double mn orbT.
Qed.
Fixpoint half (n : nat) : nat := if n is n'.+1 then uphalf n' else n
with uphalf (n : nat) : nat := if n is n'.+1 then n'./2.+1 else n
where "n ./2" := (half n) : nat_scope.
Lemma uphalfE n : uphalf n = n.+1./2.
Proof.
by []. Qed.
Lemma doubleK : cancel double half.
Proof.
by elim=> //= n ->. Qed.
Definition half_double := doubleK.
Definition double_inj := can_inj doubleK.
Lemma uphalf_double n : uphalf n.*2 = n.
Proof.
by elim: n => //= n ->. Qed.
Lemma uphalf_half n : uphalf n = odd n + n./2.
Lemma odd_double_half n : odd n + n./2.*2 = n.
Proof.
Lemma halfK n : n./2.*2 = n - odd n.
Proof.
Lemma uphalfK n : (uphalf n).*2 = odd n + n.
Lemma odd_halfK n : odd n -> n./2.*2 = n.-1.
Lemma even_halfK n : ~~ odd n -> n./2.*2 = n.
Lemma odd_uphalfK n : odd n -> (uphalf n).*2 = n.+1.
Proof.
Lemma even_uphalfK n : ~~ odd n -> (uphalf n).*2 = n.
Lemma half_bit_double n (b : bool) : (b + n.*2)./2 = n.
Proof.
Lemma halfD m n : (m + n)./2 = (odd m && odd n) + (m./2 + n./2).
Proof.
rewrite -[n in LHS]odd_double_half addnCA.
rewrite -[m in LHS]odd_double_half -addnA -doubleD.
by do 2!case: odd; rewrite /= ?add0n ?half_double ?uphalf_double.
Qed.
rewrite -[m in LHS]odd_double_half -addnA -doubleD.
by do 2!case: odd; rewrite /= ?add0n ?half_double ?uphalf_double.
Qed.
Lemma half_leq m n : m <= n -> m./2 <= n./2.
Lemma geq_half_double m n : (m <= n./2) = (m.*2 <= n).
Proof.
rewrite -[X in _.*2 <= X]odd_double_half.
case: odd; last by rewrite leq_double.
by case: m => // m; rewrite doubleS ltnS ltn_double.
Qed.
case: odd; last by rewrite leq_double.
by case: m => // m; rewrite doubleS ltnS ltn_double.
Qed.
Lemma ltn_half_double m n : (m./2 < n) = (m < n.*2).
Proof.
Lemma leq_half_double m n : (m./2 <= n) = (m <= n.*2.+1).
Proof.
Lemma gtn_half_double m n : (n < m./2) = (n.*2.+1 < m).
Proof.
Lemma half_gt0 n : (0 < n./2) = (1 < n).
Proof.
by case: n => [|[]]. Qed.
Lemma uphalf_leq m n : m <= n -> uphalf m <= uphalf n.
Proof.
Lemma leq_uphalf_double m n : (uphalf m <= n) = (m <= n.*2).
Proof.
Lemma geq_uphalf_double m n : (m <= uphalf n) = (m.*2 <= n.+1).
Proof.
Lemma gtn_uphalf_double m n : (n < uphalf m) = (n.*2 < m).
Proof.
Lemma ltn_uphalf_double m n : (uphalf m < n) = (m.+1 < n.*2).
Proof.
Lemma uphalf_gt0 n : (0 < uphalf n) = (0 < n).
Proof.
by case: n. Qed.
Lemma odd_geq m n : odd n -> (m <= n) = (m./2.*2 <= n).
Proof.
move=> odd_n; rewrite -[m in LHS]odd_double_half -[n]odd_double_half odd_n.
by case: (odd m); rewrite // leq_Sdouble ltnS leq_double.
Qed.
by case: (odd m); rewrite // leq_Sdouble ltnS leq_double.
Qed.
Lemma odd_ltn m n : odd n -> (n < m) = (n < m./2.*2).
Lemma odd_gt0 n : odd n -> n > 0
Proof.
by case: n. Qed.
Lemma odd_gt2 n : odd n -> n > 1 -> n > 2.
Proof.
Lemma mulnn m : m * m = m ^ 2.
Lemma sqrnD m n : (m + n) ^ 2 = m ^ 2 + n ^ 2 + 2 * (m * n).
Proof.
Lemma sqrnB m n : n <= m -> (m - n) ^ 2 = m ^ 2 + n ^ 2 - 2 * (m * n).
Proof.
Lemma sqrnD_sub m n : n <= m -> (m + n) ^ 2 - 4 * (m * n) = (m - n) ^ 2.
Proof.
Lemma subn_sqr m n : m ^ 2 - n ^ 2 = (m - n) * (m + n).
Lemma ltn_sqr m n : (m ^ 2 < n ^ 2) = (m < n).
Proof.
Lemma leq_sqr m n : (m ^ 2 <= n ^ 2) = (m <= n).
Proof.
Lemma sqrn_gt0 n : (0 < n ^ 2) = (0 < n).
Proof.
Lemma eqn_sqr m n : (m ^ 2 == n ^ 2) = (m == n).
Proof.
Lemma sqrn_inj : injective (expn ^~ 2).
Proof.
Definition leqif m n C := ((m <= n) * ((m == n) = C))%type.
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.
Lemma leqifP m n C : reflect (m <= n ?= iff C) (if C then m == n else m < n).
Proof.
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.
Proof.
move=> ltm12 ltm23; apply/leqifP; rewrite -ltm12.
have [->|eqm12] := eqVneq; first by rewrite ltn_neqAle !ltm23 andbT; case C23.
by rewrite (@leq_trans m2) ?ltm23 // ltn_neqAle eqm12 ltm12.
Qed.
have [->|eqm12] := eqVneq; first by rewrite ltn_neqAle !ltm23 andbT; case C23.
by rewrite (@leq_trans m2) ?ltm23 // ltn_neqAle eqm12 ltm12.
Qed.
Lemma mono_leqif f : {mono f : m n / m <= n} ->
forall 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).
Proof.
Lemma leqif_eq m n : m <= n -> m <= n ?= iff (m == n).
Proof.
by []. Qed.
Lemma geq_leqif a b C : a <= b ?= iff C -> (b <= a) = C.
Proof.
Lemma ltn_leqif a b C : a <= b ?= iff C -> (a < b) = ~~ C.
Lemma ltnNleqif x y C : x <= y ?= iff ~~ C -> (x < y) = C.
Lemma eq_leqif x y C : x <= y ?= iff C -> (x == y) = C.
Lemma eqTleqif x y C : x <= y ?= iff C -> C -> x = y.
Lemma leqif_add m1 n1 C1 m2 n2 C2 :
m1 <= n1 ?= iff C1 -> m2 <= n2 ?= iff C2 ->
m1 + m2 <= n1 + n2 ?= iff C1 && C2.
Proof.
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).
Proof.
case: n1 => [|n1] le1; first by case: m1 le1 => [|m1] [_ <-] //.
case: n2 m2 => [|n2] [|m2] /=; try by case=> // _ <-; rewrite !muln0 ?andbF.
have /leq_pmul2l-/mono_leqif<-: 0 < n1.+1 by [].
by apply: leqif_trans; have /leq_pmul2r-/mono_leqif->: 0 < m2.+1.
Qed.
case: n2 m2 => [|n2] [|m2] /=; try by case=> // _ <-; rewrite !muln0 ?andbF.
have /leq_pmul2l-/mono_leqif<-: 0 < n1.+1 by [].
by apply: leqif_trans; have /leq_pmul2r-/mono_leqif->: 0 < m2.+1.
Qed.
Lemma nat_Cauchy m n : 2 * (m * n) <= m ^ 2 + n ^ 2 ?= iff (m == n).
Proof.
Lemma nat_AGM2 m n : 4 * (m * n) <= (m + n) ^ 2 ?= iff (m == n).
Proof.
Section ContraLeq.
Implicit Types (b : bool) (m n : nat) (P : Prop).
Lemma contraTleq b m n : (n < m -> ~~ b) -> (b -> m <= n).
Lemma contraTltn b m n : (n <= m -> ~~ b) -> (b -> m < n).
Lemma contraPleq P m n : (n < m -> ~ P) -> (P -> m <= n).
Lemma contraPltn P m n : (n <= m -> ~ P) -> (P -> m < n).
Lemma contraNleq b m n : (n < m -> b) -> (~~ b -> m <= n).
Lemma contraNltn b m n : (n <= m -> b) -> (~~ b -> m < n).
Lemma contra_not_leq P m n : (n < m -> P) -> (~ P -> m <= n).
Proof.
Lemma contra_not_ltn P m n : (n <= m -> P) -> (~ P -> m < n).
Proof.
Lemma contraFleq b m n : (n < m -> b) -> (b = false -> m <= n).
Lemma contraFltn b m n : (n <= m -> b) -> (b = false -> m < n).
Lemma contra_leqT b m n : (~~ b -> m < n) -> (n <= m -> b).
Lemma contra_ltnT b m n : (~~ b -> m <= n) -> (n < m -> b).
Lemma contra_leqN b m n : (b -> m < n) -> (n <= m -> ~~ b).
Lemma contra_ltnN b m n : (b -> m <= n) -> (n < m -> ~~ b).
Lemma contra_leq_not P m n : (P -> m < n) -> (n <= m -> ~ P).
Proof.
Lemma contra_ltn_not P m n : (P -> m <= n) -> (n < m -> ~ P).
Proof.
Lemma contra_leqF b m n : (b -> m < n) -> (n <= m -> b = false).
Lemma contra_ltnF b m n : (b -> m <= n) -> (n < m -> b = false).
Lemma contra_leq m n p q : (q < p -> n < m) -> (m <= n -> p <= q).
Lemma contra_leq_ltn m n p q : (q <= p -> n < m) -> (m <= n -> p < q).
Lemma contra_ltn_leq m n p q : (q < p -> n <= m) -> (m < n -> p <= q).
Lemma contra_ltn m n p q : (q <= p -> n <= m) -> (m < n -> p < q).
End ContraLeq.
Section Monotonicity.
Variable T : Type.
Lemma homo_ltn_in (D : {pred nat}) (f : nat -> T) (r : T -> T -> Prop) :
(forall y x z, r x y -> r y z -> r x z) ->
{in D &, forall i j k, i < k < j -> k \in D} ->
{in D, forall i, i.+1 \in D -> r (f i) (f i.+1)} ->
{in D &, {homo f : i j / i < j >-> r i j}}.
Proof.
move=> r_trans Dcx r_incr i j iD jD lt_ij; move: (lt_ij) (jD) => /subnKC<-.
elim: (_ - _) => [|k ihk]; first by rewrite addn0 => Dsi; apply: r_incr.
move=> DSiSk [: DSik]; apply: (r_trans _ _ _ (ihk _)); rewrite ?addnS.
by abstract: DSik; apply: (Dcx _ _ iD DSiSk); rewrite ltn_addr ?addnS /=.
by apply: r_incr; rewrite -?addnS.
Qed.
elim: (_ - _) => [|k ihk]; first by rewrite addn0 => Dsi; apply: r_incr.
move=> DSiSk [: DSik]; apply: (r_trans _ _ _ (ihk _)); rewrite ?addnS.
by abstract: DSik; apply: (Dcx _ _ iD DSiSk); rewrite ltn_addr ?addnS /=.
by apply: r_incr; rewrite -?addnS.
Qed.
Lemma homo_ltn (f : nat -> T) (r : T -> T -> Prop) :
(forall y x z, r x y -> r y z -> r x z) ->
(forall i, r (f i) (f i.+1)) -> {homo f : i j / i < j >-> r i j}.
Proof.
Lemma homo_leq_in (D : {pred nat}) (f : nat -> T) (r : T -> T -> Prop) :
(forall x, r x x) -> (forall y x z, r x y -> r y z -> r x z) ->
{in D &, forall i j k, i < k < j -> k \in D} ->
{in D, forall i, i.+1 \in D -> r (f i) (f i.+1)} ->
{in D &, {homo f : i j / i <= j >-> r i j}}.
Proof.
move=> r_refl r_trans Dcx /(homo_ltn_in r_trans Dcx) lt_r i j iD jD.
case: ltngtP => [? _||->] //; exact: lt_r.
Qed.
case: ltngtP => [? _||->] //; exact: lt_r.
Qed.
Lemma homo_leq (f : nat -> T) (r : T -> T -> Prop) :
(forall x, r x x) -> (forall y x z, r x y -> r y z -> r x z) ->
(forall i, r (f i) (f i.+1)) -> {homo f : i j / i <= j >-> r i j}.
Proof.
Section NatToNat.
Variable (f : nat -> nat).
This listing of "Let"s factor out the required premises 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).
Proof.
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}.
Proof.
Lemma inj_homo_ltn : injective f -> {homo f : m n / m <= n} ->
{homo f : m n / m < n}.
Proof.
Lemma ltnW_nhomo : {homo f : m n /~ m < n} -> {homo f : m n /~ m <= n}.
Proof.
Lemma inj_nhomo_ltn : injective f -> {homo f : m n /~ m <= n} ->
{homo f : m n /~ m < n}.
Proof.
Lemma incn_inj : {mono f : m n / m <= n} -> injective f.
Proof.
Lemma decn_inj : {mono f : m n /~ m <= n} -> injective f.
Proof.
Lemma leqW_mono : {mono f : m n / m <= n} -> {mono f : m n / m < n}.
Proof.
Lemma leqW_nmono : {mono f : m n /~ m <= n} -> {mono f : m n /~ m < n}.
Proof.
Lemma leq_mono : {homo f : m n / m < n} -> {mono f : m n / m <= n}.
Proof.
Lemma leq_nmono : {homo f : m n /~ m < n} -> {mono f : m n /~ m <= n}.
Proof.
Variables (D D' : {pred nat}).
Lemma ltnW_homo_in : {in D & D', {homo f : m n / m < n}} ->
{in D & D', {homo f : m n / m <= n}}.
Proof.
Lemma ltnW_nhomo_in : {in D & D', {homo f : m n /~ m < n}} ->
{in D & D', {homo f : m n /~ m <= n}}.
Proof.
Lemma inj_homo_ltn_in : {in D & D', injective f} ->
{in D & D', {homo f : m n / m <= n}} ->
{in D & D', {homo f : m n / m < n}}.
Proof.
Lemma inj_nhomo_ltn_in : {in D & D', injective f} ->
{in D & D', {homo f : m n /~ m <= n}} ->
{in D & D', {homo f : m n /~ m < n}}.
Proof.
Lemma incn_inj_in : {in D &, {mono f : m n / m <= n}} ->
{in D &, injective f}.
Proof.
Lemma decn_inj_in : {in D &, {mono f : m n /~ m <= n}} ->
{in D &, injective f}.
Proof.
Lemma leqW_mono_in : {in D &, {mono f : m n / m <= n}} ->
{in D &, {mono f : m n / m < n}}.
Proof.
Lemma leqW_nmono_in : {in D &, {mono f : m n /~ m <= n}} ->
{in D &, {mono f : m n /~ m < n}}.
Proof.
Lemma leq_mono_in : {in D &, {homo f : m n / m < n}} ->
{in D &, {mono f : m n / m <= n}}.
Proof.
Lemma leq_nmono_in : {in D &, {homo f : m n /~ m < n}} ->
{in D &, {mono f : m n /~ m <= n}}.
Proof.
End NatToNat.
End Monotonicity.
Lemma leq_pfact : {in [pred n | 0 < n] &, {mono factorial : m n / m <= n}}.
Proof.
Lemma leq_fact : {homo factorial : m n / m <= n}.
Lemma ltn_pfact : {in [pred n | 0 < n] &, {mono factorial : m n / m < n}}.
Proof.
Module NatTrec.
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.
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.
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.
Notation "n ^ m" := (exp n m) : nat_scope.
Local Notation oddn := odd.
Fixpoint odd n := if n is n'.+2 then odd n' else eqn n 1.
Local Notation doublen := double.
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.
Proof.
Lemma doubleE : double =1 doublen.
Lemma add_mulE n m s : add_mul n m s = addn (muln n m) s.
Lemma mulE : mul =2 muln.
Lemma mul_expE m n p : mul_exp m n p = muln (expn m n) p.
Lemma expE : exp =2 expn.
Lemma oddE : odd =1 oddn.
Proof.
Definition trecE := (addE, (doubleE, oddE), (mulE, add_mulE, (expE, mul_expE))).
End NatTrec.
Notation natTrecE := NatTrec.trecE.
Definition N_eqb n m :=
match n, m with
| N0, N0 => true
| Npos p, Npos q => Pos.eqb p q
| _, _ => false
end.
Lemma eq_binP : Equality.axiom N_eqb.
Proof.
HB.instance Definition _ := hasDecEq.Build N eq_binP.
Arguments N_eqb !n !m.
Section NumberInterpretation.
Section Trec.
Import NatTrec.
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
end.
End Trec.
Local Coercion nat_of_pos : positive >-> nat.
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
end.
Definition bin_of_nat n0 := if n0 is n.+1 then Npos (pos_of_nat n n) else N0.
Lemma bin_of_natK : cancel bin_of_nat nat_of_bin.
Proof.
Lemma nat_of_binK : cancel nat_of_bin bin_of_nat.
Proof.
Lemma nat_of_succ_pos p : Pos.succ p = p.+1 :> nat.
Proof.
Lemma nat_of_add_pos p q : Pos.add p q = p + q :> nat.
Proof.
Lemma nat_of_mul_pos p q : Pos.mul p q = p * q :> nat.
Proof.
elim: p => [p IHp|p IHp|] /=; rewrite ?mul1n //;
by rewrite ?nat_of_add_pos /= !natTrecE IHp doubleMl.
Qed.
by rewrite ?nat_of_add_pos /= !natTrecE IHp doubleMl.
Qed.
End NumberInterpretation.
Record number : Type := Num {bin_of_number :> N}.
Definition number_subType := Eval hnf in [isNew for bin_of_number].
HB.instance Definition _ := number_subType.
HB.instance Definition _ := [Equality of number by <:].
Notation "[ 'Num' 'of' e ]" := (Num (bin_of_nat e))
(format "[ 'Num' 'of' e ]") : nat_scope.
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).
Ltac succn_to_add :=
match goal with
| |- 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'
end; succn_to_add; rewrite {}/x
| _ => idtac
end.
Ltac nat_norm :=
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) =>
symmetry;
rewrite -1?(addnC X1) -?(addnCA X1);
apply: (congr1 (addn X1) _);
symmetry
end ].