- -

Library mathcomp.ssreflect.ssrnat

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
-Require Import BinNat.
-Require BinPos Ndec.
-Require Export Ring.
- -
-

- -

- 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 support for the ring tactic, and congruence tactics. - 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 the nosimpl tag to prevent undesirable computation - 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, 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. - -

- - 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 + (m - n), 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 ths 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.
- -
-

- -

- Disable Coq prelude hints to improve proof script robustness. -

- -
- -
-

- -

- Declare legacy Arith operators in new scope. -

- -
-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.
- -
-

- -

- Rebind scope delimiters, reserving a scope for the "recursive", - i.e., unprotected version of operators. -

- -
-Delimit Scope N_scope with num.
-Delimit Scope nat_scope with N.
-Delimit Scope nat_rec_scope with Nrec.
- -
-

- -

- Postfix notation for the successor and predecessor functions. - SSreflect uses "pred" for the generic predicate type, and S as - a local bound variable. -

- -
-Notation succn := Datatypes.S.
-Notation predn := Peano.pred.
- -
-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,
-  format "n .+2") : nat_scope.
-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,
-  format "n .+4") : nat_scope.
- -
-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,
-  format "n .-2") : nat_scope.
- -
-Lemma succnK : cancel succn predn.
-Lemma succn_inj : injective succn.
- -
-

- -

- Predeclare postfix doubling/halving operators. -

- -
-Reserved Notation "n .*2" (at level 2, format "n .*2").
-Reserved Notation "n ./2" (at level 2, format "n ./2").
- -
-

- -

- Canonical comparison and eqType for nat. -

- -
-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.
- -
-Canonical nat_eqMixin := EqMixin eqnP.
-Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin.
- -
- -
-Lemma eqnE : eqn = eq_op.
- -
-Lemma eqSS m n : (m .+1 == n .+1 ) = (m == n ).
- -
-Lemma nat_irrelevance (x y : nat) (E E' : x = y) : E = E'.
- -
-

- -

- Protected addition, with a more systematic set of lemmas. -

- -
-Definition addn_rec := plus.
-Notation "m + n" := (addn_rec m n) : nat_rec_scope.
- -
-Definition addn := nosimpl addn_rec.
-Notation "m + n" := (addn m n) : nat_scope.
- -
-Lemma addnE : addn = addn_rec.
- -
-Lemma plusE : plus = addn.
- -
-Lemma add0n : left_id 0 addn.
-Lemma addSn m n : m .+1 + n = (m + n ).+1.
-Lemma add1n n : 1 + n = n .+1.
- -
-Lemma addn0 : right_id 0 addn.
- -
-Lemma addnS m n : m + n .+1 = (m + n ).+1.
- -
-Lemma addSnnS m n : m .+1 + n = m + n .+1.
- -
-Lemma addnCA : left_commutative addn.
- -
-Lemma addnC : commutative addn.
- -
-Lemma addn1 n : n + 1 = n .+1.
- -
-Lemma addnA : associative addn.
- -
-Lemma addnAC : right_commutative addn.
- -
-Lemma addnACA : interchange addn addn.
- -
-Lemma addn_eq0 m n : (m + n == 0) = (m == 0) && (n == 0).
- -
-Lemma eqn_add2l p m n : (p + m == p + n ) = (m == n ).
- -
-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.
-Lemma add2n m : 2 + m = m .+2.
-Lemma addn3 m : m + 3 = m .+3.
-Lemma add3n m : 3 + m = m .+3.
-Lemma addn4 m : m + 4 = m .+4.
-Lemma add4n m : 4 + m = m .+4.
- -
-

- -

- Protected, structurally decreasing subtraction, and basic lemmas. - Further properties depend on ordering conditions. -

- -
-Definition subn_rec := minus.
-Notation "m - n" := (subn_rec m n) : nat_rec_scope.
- -
-Definition subn := nosimpl subn_rec.
-Notation "m - n" := (subn m n) : nat_scope.
- -
-Lemma subnE : subn = subn_rec.
-Lemma minusE : minus = subn.
- -
-Lemma sub0n : left_zero 0 subn.
-Lemma subn0 : right_id 0 subn.
-Lemma subnn : self_inverse 0 subn.
- -
-Lemma subSS n m : m .+1 - n .+1 = m - n.
-Lemma subn1 n : n - 1 = n .-1.
-Lemma subn2 n : (n - 2)%N = n .-2.
- -
-Lemma subnDl p m n : (p + m ) - (p + n ) = m - n.
- -
-Lemma subnDr p m n : (m + p ) - (n + p ) = m - n.
- -
-Lemma addKn n : cancel (addn n) (subn ^~ n).
- -
-Lemma addnK n : cancel (addn ^~ n) (subn ^~ n).
- -
-Lemma subSnn n : n .+1 - n = 1.
- -
-Lemma subnDA m n p : n - (m + p ) = (n - m ) - p.
- -
-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.
- -
-

- -

- Integer ordering, and its interaction with the other operations. -

- -
-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.
- -
-

- -

- For sorting, etc. -

-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 ).
-Lemma leq0n n : 0 ≤ n.
-Lemma ltn0Sn n : 0 < n .+1.
-Lemma ltn0 n : n < 0 = false.
-Lemma leqnn n : n ≤ n.
-Hint Resolve leqnn : core.
-Lemma ltnSn n : n < n .+1.
-Lemma eq_leq m n : m = n → m ≤ n.
-Lemma leqnSn n : n ≤ n .+1.
-Hint Resolve leqnSn : core.
-Lemma leq_pred n : n .-1 ≤ n.
-Lemma leqSpred n : n ≤ n .-1 .+1.
- -
-Lemma ltn_predK m n : m < n → n .-1 .+1 = n.
- -
-Lemma prednK n : 0 < n → n .-1 .+1 = n.
- -
-Lemma leqNgt m n : (m ≤ n ) = ~~ (n < m ).
- -
-Lemma ltnNge m n : (m < n ) = ~~ (n ≤ m ).
- -
-Lemma ltnn n : n < n = false.
- -
-Lemma leqn0 n : (n ≤ 0) = (n == 0).
-Lemma lt0n n : (0 < n ) = (n != 0).
-Lemma lt0n_neq0 n : 0 < n → n != 0.
-Lemma eqn0Ngt n : (n == 0) = ~~ (n > 0).
-Lemma neq0_lt0n n : (n == 0) = false → 0 < n.
-Hint Resolve lt0n_neq0 neq0_lt0n : core.
- -
-Lemma eqn_leq m n : (m == n ) = (m ≤ n ≤ m ).
- -
-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.
- -
-Lemma leq_gtF m n : m ≤ n → m > n = false.
- -
-Lemma leq_eqVlt m n : (m ≤ n ) = (m == n ) || (m < n ).
- -
-Lemma ltn_neqAle m n : (m < n ) = (m != n ) && (m ≤ n ).
- -
-Lemma leq_trans n m p : m ≤ n → n ≤ p → m ≤ p.
- -
-Lemma leq_ltn_trans n m p : m ≤ n → n < p → m < p.
- -
-Lemma ltnW m n : m < n → m ≤ n.
- Hint Resolve ltnW : core.
- -
-Lemma leqW m n : m ≤ n → m ≤ n .+1.
- -
-Lemma ltn_trans n m p : m < n → n < p → m < p.
- -
-Lemma leq_total m n : (m ≤ n ) || (m ≥ n ).
- -
-

- -

- Link to the legacy comparison predicates. -

- -
-Lemma leP m n : reflect (m ≤ n)%coq_nat (m ≤ n).
- -
-Lemma le_irrelevance m n le_mn1 le_mn2 : le_mn1 = le_mn2 :> (m ≤ n)%coq_nat.
- -
-Lemma ltP m n : reflect (m < n)%coq_nat (m < n).
- -
-Lemma lt_irrelevance m n lt_mn1 lt_mn2 : lt_mn1 = lt_mn2 :> (m < n)%coq_nat.
- -
-

- -

- Comparison predicates. -

- -
-Variant leq_xor_gtn m n : bool → bool → Set :=
-  | LeqNotGtn of m ≤ n : leq_xor_gtn m n true false
-  | GtnNotLeq of n < m : leq_xor_gtn m n false true.
- -
-Lemma leqP m n : leq_xor_gtn m n (m ≤ n) (n < m).
- -
-Variant ltn_xor_geq m n : bool → bool → Set :=
-  | LtnNotGeq of m < n : ltn_xor_geq m n false true
-  | GeqNotLtn of n ≤ m : ltn_xor_geq m n true false.
- -
-Lemma ltnP m n : ltn_xor_geq m n (n ≤ m) (m < n).
- -
-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).
- -
-Variant compare_nat m n :
-   bool → bool → bool → bool → bool → bool → Set :=
-  | CompareNatLt of m < n : compare_nat m n true false true false false false
-  | CompareNatGt of m > n : compare_nat m n false true false true false false
-  | CompareNatEq of m = n : compare_nat m n true true false false true true.
- -
-Lemma ltngtP m n : compare_nat m n (m ≤ n) (n ≤ m) (m < n)
-                                   (n < m) (n == m) (m == n).
- -
-

- -

- Monotonicity lemmas -

- -
-Lemma leq_add2l p m n : (p + m ≤ p + n ) = (m ≤ n ).
- -
-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_addr m n : n ≤ n + m.
- -
-Lemma leq_addl m n : n ≤ m + n.
- -
-Lemma ltn_addr m n p : m < n → m < n + p.
- -
-Lemma ltn_addl m n p : m < n → m < p + n.
- -
-Lemma addn_gt0 m n : (0 < m + n ) = (0 < m ) || (0 < n ).
- -
-Lemma subn_gt0 m n : (0 < n - m ) = (m < n ).
- -
-Lemma subn_eq0 m n : (m - n == 0) = (m ≤ n ).
- -
-Lemma leq_subLR m n p : (m - n ≤ p ) = (m ≤ n + p ).
- -
-Lemma leq_subr m n : n - m ≤ n.
- -
-Lemma subnKC m n : m ≤ n → m + (n - m ) = 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 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.
- -
-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 ).
- -
-

- -

- Eliminating the idiom for structurally decreasing compare and subtract. -

-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 ).
- -
-

- -

- Max and min. -

- -
-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.
-Lemma maxn0 : right_id 0 maxn.
- -
-Lemma maxnC : commutative maxn.
- -
-Lemma maxnE m n : maxn m n = m + (n - m ).
- -
-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 maxn.
- -
-Lemma leq_max m n1 n2 : (m ≤ maxn n1 n2 ) = (m ≤ n1 ) || (m ≤ n2 ).
-Lemma leq_maxl m n : m ≤ maxn m n.
-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.
- -
-Lemma addn_maxl : left_distributive addn maxn.
- -
-Lemma addn_maxr : right_distributive addn maxn.
- -
-Lemma min0n : left_zero 0 minn.
-Lemma minn0 : right_zero 0 minn.
- -
-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 ).
- -
-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).
- -
-Lemma minn_idPr {m n} : reflect (minn m n = n) (m ≥ n).
- -
-Lemma minnn : idempotent minn.
- -
-Lemma leq_min m n1 n2 : (m ≤ minn n1 n2 ) = (m ≤ n1 ) && (m ≤ n2 ).
- -
-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 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 minnSS m n : minn m .+1 n .+1 = (minn m n ).+1.
- -
-

- -

- Quasi-cancellation (really, absorption) lemmas -

-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.
- -
-

- -

- Distributivity. -

-Lemma maxn_minl : left_distributive maxn minn.
- -
-Lemma maxn_minr : right_distributive maxn minn.
- -
-Lemma minn_maxl : left_distributive minn maxn.
- -
-Lemma minn_maxr : right_distributive minn maxn.
- -
-

- -

- Getting a concrete value from an abstract existence proof. -

- -
-Section ExMinn.
- -
-Variable P : pred nat.
-Hypothesis exP : ∃ 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 & ∀ 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.
- -
-Lemma ex_minnP : ex_minn_spec ex_minn.
- -
-End ExMinn.
- -
-Section ExMaxn.
- -
-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).
- -
-Definition ex_maxn := m - ex_minn ex_maxn_subproof.
- -
-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.
- -
-End ExMaxn.
- -
-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.
- -
-Section Iteration.
- -
-Variable T : Type.
-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.
- -
-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).
- -
-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 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 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_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_0 n : iter n succn 0 = n.
- -
-Lemma iter_predn m n : iter n predn m = m - n.
- -
-

- -

- Multiplication. -

- -
-Definition muln_rec := mult.
-Notation "m * n" := (muln_rec m n) : nat_rec_scope.
- -
-Definition muln := nosimpl muln_rec.
-Notation "m * n" := (muln m n) : nat_scope.
- -
-Lemma multE : mult = muln.
-Lemma mulnE : muln = muln_rec.
- -
-Lemma mul0n : left_zero 0 muln.
-Lemma muln0 : right_zero 0 muln.
-Lemma mul1n : left_id 1 muln.
-Lemma mulSn m n : m .+1 × n = n + m × n.
-Lemma mulSnr m n : m .+1 × n = m × n + n.
- -
-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.
- -
-Lemma mulnDr : right_distributive muln addn.
- -
-Lemma mulnBl : left_distributive muln subn.
- -
-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).
- -
-Lemma muln_eq1 m n : (m × n == 1) = (m == 1) && (n == 1).
- -
-Lemma muln_gt0 m n : (0 < m × n ) = (0 < m ) && (0 < n ).
- -
-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.
- -
-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 ).
- -
-Lemma leq_pmul2r m n1 n2 : 0 < m → (n1 × m ≤ n2 × m ) = (n1 ≤ n2 ).
- -
-Lemma eqn_pmul2l m n1 n2 : 0 < m → (m × n1 == m × n2 ) = (n1 == n2 ).
- -
-Lemma eqn_pmul2r m n1 n2 : 0 < m → (n1 × m == n2 × 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 ).
- -
-Lemma ltn_pmul2r m n1 n2 : 0 < m → (n1 × m < n2 × m ) = (n1 < n2 ).
- -
-Lemma ltn_Pmull m n : 1 < n → 0 < m → m < n × m.
- -
-Lemma ltn_Pmulr m n : 1 < n → 0 < m → m < m × n.
- -
-Lemma ltn_mul m1 m2 n1 n2 : m1 < n1 → m2 < n2 → m1 × m2 < n1 × n2.
- -
-Lemma maxn_mulr : right_distributive muln maxn.
- -
-Lemma maxn_mull : left_distributive muln maxn.
- -
-Lemma minn_mulr : right_distributive muln minn.
- -
-Lemma minn_mull : left_distributive muln minn.
- -
-

- -

- Exponentiation. -

- -
-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.
- -
-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 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.
- -
-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.
- -
-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 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 ).
- -
-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).
- -
-

- -

- Factorial. -

- -
-Fixpoint fact_rec n := if n is n'.+1 then n × fact_rec n' else 1.
- -
-Definition factorial := nosimpl fact_rec.
- -
-Notation "n `!" := (factorial n) (at level 2, format "n `!") : nat_scope.
- -
-Lemma factE : factorial = fact_rec.
- -
-Lemma fact0 : 0`! = 1.
- -
-Lemma factS n : (n .+1 )`! = n .+1 × n `!.
- -
-Lemma fact_gt0 n : n `! > 0.
- -
-

- -

- Parity and bits. -

- -
-Coercion nat_of_bool (b : bool) := if b then 1 else 0.
- -
-Lemma leq_b1 (b : bool) : b ≤ 1.
- -
-Lemma addn_negb (b : bool) : ~~ b + b = 1.
- -
-Lemma eqb0 (b : bool) : (b == 0 :> nat ) = ~~ b.
- -
-Lemma eqb1 (b : bool) : (b == 1 :> nat ) = b.
- -
-Lemma lt0b (b : bool) : (b > 0) = b.
- -
-Lemma sub1b (b : bool) : 1 - b = ~~ b.
- -
-Lemma mulnb (b1 b2 : bool) : b1 × b2 = b1 && b2.
- -
-Lemma mulnbl (b : bool) n : b × n = (if b then n else 0).
- -
-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 oddb (b : bool) : odd b = b.
- -
-Lemma odd_add m n : odd (m + n) = odd m (+) odd n.
- -
-Lemma odd_sub m n : n ≤ m → odd (m - n) = odd m (+) odd n.
- -
-Lemma odd_opp i m : odd m = false → i ≤ m → odd (m - i) = odd i.
- -
-Lemma odd_mul m n : odd (m × n) = odd m && odd n.
- -
-Lemma odd_exp m n : odd (m ^ n) = (n == 0) || odd m.
- -
-

- -

- Doubling. -

- -
-Fixpoint double_rec n := if n is n'.+1 then n'.*2%Nrec.+2 else 0
-where "n .*2" := (double_rec n) : nat_rec_scope.
- -
-Definition double := nosimpl double_rec.
-Notation "n .*2" := (double n) : nat_scope.
- -
-Lemma doubleE : double = double_rec.
- -
-Lemma double0 : 0.*2 = 0.
- -
-Lemma doubleS n : n .+1 .*2 = n .*2 .+2.
- -
-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.
- -
-Lemma leq_double m n : (m .*2 ≤ n .*2 ) = (m ≤ n ).
- -
-Lemma ltn_double m n : (m .*2 < n .*2 ) = (m < n ).
- -
-Lemma ltn_Sdouble m n : (m .*2 .+1 < n .*2 ) = (m < n ).
- -
-Lemma leq_Sdouble m n : (m .*2 ≤ n .*2 .+1 ) = (m ≤ n ).
- -
-Lemma odd_double n : odd n .*2 = false.
- -
-Lemma double_gt0 n : (0 < n .*2 ) = (0 < n ).
- -
-Lemma double_eq0 n : (n .*2 == 0) = (n == 0).
- -
-Lemma doubleMl m n : (m × n ).*2 = m .*2 × n.
- -
-Lemma doubleMr m n : (m × n ).*2 = m × n .*2.
- -
-

- -

- Halving. -

- -
-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 doubleK : cancel double half.
- -
-Definition half_double := doubleK.
-Definition double_inj := can_inj doubleK.
- -
-Lemma uphalf_double n : uphalf n .*2 = n.
- -
-Lemma uphalf_half n : uphalf n = odd n + n ./2.
- -
-Lemma odd_double_half n : odd n + n ./2 .*2 = n.
- -
-Lemma half_bit_double n (b : bool) : (b + n .*2 )./2 = n.
- -
-Lemma halfD m n : (m + n )./2 = (odd m && odd n ) + (m ./2 + n ./2 ).
- -
-Lemma half_leq m n : m ≤ n → m ./2 ≤ n ./2.
- -
-Lemma half_gt0 n : (0 < n ./2 ) = (1 < n ).
- -
-Lemma odd_geq m n : odd n → (m ≤ n ) = (m ./2 .*2 ≤ n ).
- -
-Lemma odd_ltn m n : odd n → (n < m ) = (n < m ./2 .*2 ).
- -
-Lemma odd_gt0 n : odd n → n > 0.
- -
-Lemma odd_gt2 n : odd n → n > 1 → n > 2.
- -
-

- -

- Squares and square identities. -

- -
-Lemma mulnn m : m × m = m ^ 2.
- -
-Lemma sqrnD m n : (m + n ) ^ 2 = m ^ 2 + n ^ 2 + 2 × (m × n ).
- -
-Lemma sqrn_sub m n : n ≤ m → (m - n ) ^ 2 = m ^ 2 + n ^ 2 - 2 × (m × n ).
- -
-Lemma sqrnD_sub m n : n ≤ m → (m + n ) ^ 2 - 4 × (m × n ) = (m - n ) ^ 2.
- -
-Lemma subn_sqr m n : m ^ 2 - n ^ 2 = (m - n ) × (m + n ).
- -
-Lemma ltn_sqr m n : (m ^ 2 < n ^ 2) = (m < n ).
- -
-Lemma leq_sqr m n : (m ^ 2 ≤ n ^ 2) = (m ≤ n ).
- -
-Lemma sqrn_gt0 n : (0 < n ^ 2) = (0 < n ).
- -
-Lemma eqn_sqr m n : (m ^ 2 == n ^ 2) = (m == n ).
- -
-Lemma sqrn_inj : injective (expn ^~ 2).
- -
-

- -

- Almost strict inequality: an inequality that is strict unless some - specific condition holds, such as the Cauchy-Schwartz or the AGM - inequality (we only prove the order-2 AGM here; the general one - requires sequences). - We formalize the concept as a rewrite multirule, that can be used - both to rewrite the non-strict inequality to true, and the equality - to the specific condition (for strict inequalities use the ltn_neqAle - lemma); in addition, the conditional equality also coerces to a - non-strict one. -

- -
-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).
- -
-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.
- -
-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_eq m n : m ≤ n → m ≤ n ?= iff (m == n ).
- -
-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 leqif_add m1 n1 C1 m2 n2 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 ).
- -
-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 ).
- -
-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 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.
- -
-

- -

- Support for larger integers. The normal definitions of +, - and even - IO are unsuitable for Peano integers larger than 2000 or so because - they are not tail-recursive. We provide a workaround module, along - with a rewrite multirule to change the tailrec operators to the - normal ones. We handle IO via the NatBin module, but provide our - own (more efficient) conversion functions. -

- -
-Module NatTrec.
- -
-

- -

- Usage: - Import NatTrec. - in section definining functions, rebinds all - non-tail recursive operators. - rewrite !trecE. - in the correctness proof, restores operators -

- -
-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.
- -
-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.
- -
-Lemma addE : add =2 addn.
- -
-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.
- -
-Definition trecE := (addE , (doubleE , oddE ), (mulE , add_mulE , (expE , mul_expE ))).
- -
-End NatTrec.
- -
-Notation natTrecE := NatTrec.trecE.
- -
-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.
- -
- -
-Section NumberInterpretation.
- -
-Import BinPos.
- -
-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.
- -
- -
-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 0%num.
- -
-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_succ_pos p : Pos.succ p = p .+1 :> 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_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.
- -
-End NumberInterpretation.
- -
-

- -

- Big(ger) nat IO; usage: - Num 1 072 399 - to create large numbers for test cases - Eval compute in [Num of some expression] - to display the resut of an expression that - returns a larger integer. -

- -
-Record number : Type := Num {bin_of_number :> N}.
- -
-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_eqType := Eval hnf in EqType number number_eqMixin.
- -
-Notation "[ 'Num' 'of' e ]" := (Num (bin_of_nat e))
- (at level 0, format "[ 'Num' 'of' e ]") : nat_scope.
- -
-

- -

- Interface to ring/ring_simplify tactics -

- -
-Lemma nat_semi_ring : semi_ring_theory 0 1 addn muln (@eq _).
- -
-Lemma nat_semi_morph :
- semi_morph 0 1 addn muln (@eq _) 0%num 1%num Nplus Nmult pred1 nat_of_bin.
- -
-Lemma nat_power_theory : power_theory 1 muln (@eq _) nat_of_bin expn.
- -
-

- -

- Interface to the ring tactic machinery. -

- -
-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 nat_litteral e :=
-  match pop_succn e with
-  | ?n.+1 ⇒ constr: (bin_of_nat n)
-  | _ ⇒ NotConstant
-  end.
- -
-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.
- -
-Add Ring nat_ring_ssr : nat_semi_ring (morphism nat_semi_morph,
-   constants [nat_litteral], preprocess [succn_to_add],
-   power_tac nat_power_theory [nat_litteral]).
- -
-

- -

- A congruence tactic, similar to the boolean one, along with an .+1/+ - normalization tactic. -

- -
-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 ].
-