Library ssrnat

(c) Copyright Microsoft Corporation and Inria. All rights reserved. 
Require Import ssreflect ssrfun ssrbool eqtype.
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                                                  
    the definitions use the nosimpl tag to prevent undesirable           
    computation during simplification, but remain compatible  with those 
    in Peano.                                                            
    For computation, a module NatRec rebinds all arithmetic  notations   
    to less convenient, but also less inefficient tail-recursive         
    definitions.                                                         
    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                                  
                                                                         
  doubling, halving, and parity                                          
     n.*2, n./2, odd n                                                   
     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) or x0 if n = 0             
                                                                         
  exponentiation, factorial                                              
       m ^ n, fact 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.             
    comparison are BOOLEAN operators, e.g. 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                                       
     m <= n ?= iff c == m <= n &  (m == n) = condition                   
    The transitivity lemma for leqif aggregates the conditions,          
    making 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) (truncating subtraction)             
                                                                         
  countable choice                                                       
    ex_minn : forall P : pred nat, (exists n, P n) -> nat                
   returns the smallest n such that P n holds.                           
                                                                         
  positive interger                                                      
    pos_nat                                                              
    a subType for positive integers, with Canonical projections for most 
    arithmetic operations.                                               

Import Prenex Implicits.

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 (only parsing).

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.

We provide a structurally decreasing predecessor function. 

Definition predn n := if n is n'.+1 then n' else n.

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 predE : Peano.pred =1 predn. Qed.

Lemma succnK : cancel succn predn. Qed.

Lemma succn_inj : injective succn. Qed.

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

Patch for ssreflect match pattern bug -- see ssrbool.v. 

Definition ifn_expr T n x y : T := if n is n'.+1 then x n' else y.

Lemma ifnE : forall T x y n,
  (if n is n'.+1 then x n' else y) = ifn_expr n x y :> T.

Canonical comparison and eqType for nat.                                

Fixpoint eqn (m n : nat) {struct m} : bool :=
  match m, n with
  | 0, 0 => true
  | m'.+1, n'.+1 => eqn m' n'
  | _, _ => false
  end.

Lemma eqnP : Equality.axiom eqn.

Canonical Structure nat_eqMixin := EqMixin eqnP.
Canonical Structure nat_eqType := Eval hnf in EqType nat_eqMixin.

Implicit Arguments eqnP [x y].

Lemma eqnE : eqn = eq_op. Qed.

Lemma eqSS : forall m n, (m.+1 == n.+1) = (m == n). Qed.

Lemma nat_irrelevance : forall (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. Qed.

Lemma plusE : plus = addn. Qed.

Lemma add0n : left_id 0 addn. Qed.

Lemma addSn : forall m n, m.+1 + n = (m + n).+1. Qed.

Lemma add1n : forall n, 1 + n = n.+1. Qed.

Lemma addn0 : right_id 0 addn. Qed.

Lemma addnS : forall m n, m + n.+1 = (m + n).+1.

Lemma addSnnS : forall m n, m.+1 + n = m + n.+1.

Lemma addnCA : left_commutative addn.

Lemma addnC : commutative addn.

Lemma addn1 : forall n, n + 1 = n.+1.

Lemma addnA : associative addn.

Lemma addnAC : right_commutative addn.

Lemma addn_eq0 : forall m n, (m + n == 0) = (m == 0) && (n == 0).

Lemma eqn_addl : forall p m n, (p + m == p + n) = (m == n).

Lemma eqn_addr : forall p m n, (m + p == n + p) = (m == n).

Lemma addnI : forall p, injective (addn p).

Lemma addIn : forall p, injective (addn^~ p).

Lemma addn2 : forall m, m + 2 = m.+2. Qed.

Lemma add2n : forall m, 2 + m = m.+2. Qed.

Lemma addn3 : forall m, m + 3 = m.+3. Qed.

Lemma add3n : forall m, 3 + m = m.+3. Qed.

Lemma addn4 : forall m, m + 4 = m.+4. Qed.

Lemma add4n : forall m, 4 + m = m.+4. Qed.

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

Fixpoint subn_rec (m n : nat) {struct m} :=
  match m, n with
  | m'.+1, n'.+1 => (m' - n')%Nrec
  | _, _ => m
  end
where "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. Qed.

Lemma minusE : minus =2 subn.

Lemma sub0n : left_zero 0 subn. Qed.

Lemma subn0 : right_id 0 subn. Qed.

Lemma subnn : self_inverse 0 subn. Qed.

Lemma subSS : forall n m, m.+1 - n.+1 = m - n. Qed.

Lemma subn1 : forall n, n - 1 = n.-1. Qed.

Lemma subn_add2l : forall p m n, (p + m) - (p + n) = m - n.

Lemma subn_add2r : forall p m n, (m + p) - (n + p) = m - n.

Lemma addKn : forall n, cancel (addn n) (subn^~ n).

Lemma addnK : forall n, cancel (addn^~ n) (subn^~ n).

Lemma subSnn : forall n, n.+1 - n = 1.

Lemma subn_sub : forall m n p, (n - m) - p = n - (m + p).

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 ltn := [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 : forall m n, (m < n.+1) = (m <= n).

Lemma leq0n : forall n, 0 <= n.

Lemma ltn0Sn : forall n, 0 < n.+1.

Lemma ltn0 : forall n, n < 0 = false.

Lemma leqnn : forall n, n <= n.
Hint Resolve leqnn.

Lemma ltnSn : forall n, n < n.+1.

Lemma eq_leq : forall m n, m = n -> m <= n.

Lemma leqnSn : forall n, n <= n.+1.
Hint Resolve leqnSn.

Lemma leq_pred : forall n, n.-1 <= n.

Lemma leqSpred : forall n, n <= n.-1.+1.

Lemma ltn_predK : forall m n, m < n -> n.-1.+1 = n.

Lemma prednK : forall n, 0 < n -> n.-1.+1 = n.

Lemma leqNgt : forall m n, (m <= n) = ~~ (n < m).

Lemma ltnNge : forall m n, (m < n) = ~~ (n <= m).

Lemma ltnn : forall n, n < n = false.

Lemma leqn0 : forall n, (n <= 0) = (n == 0).

Lemma lt0n : forall n, (0 < n) = (n != 0).

Lemma lt0n_neq0 : forall n, 0 < n -> n != 0.

Lemma eqn0Ngt : forall n, (n == 0) = ~~ (n > 0).

Lemma neq0_lt0n : forall n, (n == 0) = false -> 0 < n.
Hint Resolve lt0n_neq0 neq0_lt0n.

Lemma eqn_leq : forall m n, (m == n) = (m <= n <= m).

Lemma anti_leq : antisymmetric leq.

Lemma neq_ltn : forall m n, (m != n) = (m < n) || (n < m).

Lemma leq_eqVlt : forall m n, (m <= n) = (m == n) || (m < n).

Lemma ltn_neqAle : forall m n, (m < n) = (m != n) && (m <= n).

Lemma leq_trans : forall n m p, m <= n -> n <= p -> m <= p.

Lemma leq_ltn_trans : forall n m p, m <= n -> n < p -> m < p.

Lemma ltnW : forall m n, m < n -> m <= n.
Hint Resolve ltnW.

Lemma leqW : forall m n, m <= n -> m <= n.+1.

Lemma ltn_trans : forall n m p, m < n -> n < p -> m < p.

Lemma leq_total : forall m n, (m <= n) || (m >= n).

Link to the legacy comparison predicates. 

Lemma leP : forall m n, reflect (m <= n)%coq_nat (m <= n).

Implicit Arguments leP [m n].

Lemma le_irrelevance : forall m n lemn1 lemn2,
  lemn1 = lemn2 :> (m <= n)%coq_nat.

Lemma ltP : forall m n, reflect (m < n)%coq_nat (m < n).

Implicit Arguments ltP [m n].

Lemma lt_irrelevance : forall m n ltmn1 ltmn2,
  ltmn1 = ltmn2 :> (m < n)%coq_nat.

Comparison predicates. 

CoInductive leq_xor_gtn (m n : nat) : 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 : forall m n, leq_xor_gtn m n (m <= n) (n < m).

CoInductive ltn_xor_geq (m n : nat) : 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 : forall m n, ltn_xor_geq m n (n <= m) (m < n).

CoInductive eqn0_xor_gt0 (n : nat) : 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 : forall n, eqn0_xor_gt0 n (n == 0) (0 < n).

CoInductive compare_nat (m n : nat) : bool -> bool -> bool -> Set :=
  | CompareNatLt of m < n : compare_nat m n true false false
  | CompareNatGt of m > n : compare_nat m n false true false
  | CompareNatEq of m = n : compare_nat m n false false true.

Lemma ltngtP : forall m n, compare_nat m n (m < n) (n < m) (m == n).

Monotonicity lemmas 

Definition monotone f := forall m n, (f m <= f n) = (m <= n).

Lemma leq_add2l : forall p m n, (p + m <= p + n) = (m <= n).

Lemma ltn_add2l : forall p m n, (p + m < p + n) = (m < n).

Lemma leq_add2r : forall p m n, (m + p <= n + p) = (m <= n).

Lemma ltn_add2r : forall p m n, (m + p < n + p) = (m < n).

Lemma leq_add : forall m1 m2 n1 n2,
  m1 <= n1 -> m2 <= n2 -> m1 + m2 <= n1 + n2.

Lemma leq_addr : forall m n, n <= n + m.

Lemma leq_addl : forall m n, n <= m + n.

Lemma ltn_addr : forall m n p, m < n -> m < n + p.

Lemma ltn_addl : forall m n p, m < n -> m < p + n.

Lemma addn_gt0 : forall m n, (0 < m + n) = (0 < m) || (0 < n).

Lemma subn_gt0 : forall m n, (0 < n - m) = (m < n).

Lemma subn_eq0 : forall m n, (m - n == 0) = (m <= n).

Lemma leq_sub_add : forall m n p, (m - n <= p) = (m <= n + p).

Lemma leq_subr : forall m n, n - m <= n.

Lemma subnKC : forall m n, m <= n -> m + (n - m) = n.

Lemma subnK : forall m n, m <= n -> (n - m) + m = n.

Lemma addn_subA : forall m n p, p <= n -> m + (n - p) = m + n - p.

Lemma subn_subA : forall m n p, p <= n -> m - (n - p) = m + p - n.

Lemma subKn : forall m n, m <= n -> n - (n - m) = m.

Lemma leq_subS : forall m n, m <= n -> n.+1 - m = (n - m).+1.

Lemma ltn_subS : forall m n, m < n -> n - m = (n - m.+1).+1.

Lemma leq_sub2r : forall p m n, m <= n -> m - p <= n - p.

Lemma leq_sub2l : forall p m n, m <= n -> p - n <= p - m.

Lemma leq_sub2 : forall m1 m2 n1 n2,
  m1 <= m2 -> n2 <= n1 -> m1 - n1 <= m2 - n2.

Lemma ltn_sub2r : forall p m n, p < n -> m < n -> m - p < n - p.

Lemma ltn_sub2l : forall p m n, m < p -> m < n -> p - n < p - m.

Lemma ltn_add_sub : forall m n p, (m + n < p) = (n < p - m).

Eliminating the idiom for structurally decreasing compare and subtract. 
Lemma subn_if_gt : forall 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. Qed.

Lemma maxn0 : right_id 0 maxn. Qed.

Lemma maxnC : commutative maxn.

Lemma maxnl : forall m n, m >= n -> maxn m n = m.

Lemma maxnr : forall m n, m <= n -> maxn m n = n.

Lemma add_sub_maxn : forall m n, m + (n - m) = maxn m n.

Lemma maxnAC : right_commutative maxn.

Lemma maxnA : associative maxn.

Lemma maxnCA : left_commutative maxn.

Lemma eqn_maxr : forall m n, (maxn m n == n) = (m <= n).

Lemma eqn_maxl : forall m n, (maxn m n == m) = (m >= n).

Lemma maxnn : idempotent maxn.

Lemma leq_maxr : forall m n1 n2, (m <= maxn n1 n2) = (m <= n1) || (m <= n2).

Lemma leq_maxl : forall m n1 n2, (maxn n1 n2 <= m) = (n1 <= m) && (n2 <= m).

Lemma addn_maxl : left_distributive addn maxn.

Lemma addn_maxr : right_distributive addn maxn.

Lemma min0n : left_zero 0 minn. Qed.

Lemma minn0 : right_zero 0 minn. Qed.

Lemma minnC : commutative minn.

Lemma minnr : forall m n, m >= n -> minn m n = n.

Lemma minnl : forall m n, m <= n -> minn m n = m.

Lemma addn_min_max : forall m n, minn m n + maxn m n = m + n.

Remark minn_to_maxn : forall m n, minn m n = m + n - maxn m n.

Lemma sub_sub_minn : forall m n, m - (m - n) = minn m n.

Lemma minnCA : left_commutative minn.

Lemma minnA : associative minn.

Lemma minnAC : right_commutative minn.

Lemma eqn_minr : forall m n, (minn m n == n) = (n <= m).

Lemma eqn_minl : forall m n, (minn m n == m) = (m <= n).

Lemma minnn : forall n, minn n n = n.

Lemma leq_minr : forall m n1 n2, (m <= minn n1 n2) = (m <= n1) && (m <= n2).

Lemma leq_minl : forall m n1 n2, (minn n1 n2 <= m) = (n1 <= m) || (n2 <= m).

Lemma addn_minl : left_distributive addn minn.

Lemma addn_minr : right_distributive addn minn.

Quasi-cancellation (really, absorption) lemmas 
Lemma maxnK : forall m n, minn (maxn m n) m = m.

Lemma maxKn : forall m n, minn n (maxn m n) = n.

Lemma minnK : forall m n, maxn (minn m n) m = m.

Lemma minKn : forall m n, maxn n (minn m n) = n.

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

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

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.

End ExMinn.

Lemma eq_ex_minn : forall P Q exP exQ,
  P =1 Q -> @ex_minn P exP = @ex_minn Q exQ.

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 : forall n f x, iter n.+1 f x = iter n f (f x).

Lemma iterS : forall n f x, iter n.+1 f x = f (iter n f x). Qed.

Lemma iter_add : forall n m f x, iter (n + m) f x = iter n f (iter m f x).

Lemma iteriS : forall n f x, iteri n.+1 f x = f n (iteri n f x).

Lemma iteropS : forall idx n op x, iterop n.+1 op x idx = iter n (op x) x.

Lemma eq_iter : forall f f', f =1 f' -> forall n, iter n f =1 iter n f'.

Lemma eq_iteri : forall f f', f =2 f' -> forall n, iteri n f =1 iteri n f'.

Lemma eq_iterop : forall n op op', op =2 op' -> iterop n op =2 iterop n op'.

End Iteration.

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

Lemma mulnE : muln = muln_rec. Qed.

Lemma mul0n : left_zero 0 muln. Qed.

Lemma muln0 : right_zero 0 muln. Qed.

Lemma mul1n : left_id 1 muln. Qed.

Lemma mulSn : forall m n, m.+1 * n = n + m * n. Qed.

Lemma mulSnr : forall m n, m.+1 * n = m * n + n.
Lemma mulnS : forall m n, m * n.+1 = m + m * n.
Lemma mulnSr : forall m n, m * n.+1 = m * n + m.

Lemma muln1 : right_id 1 muln.

Lemma mulnC : commutative muln.

Lemma muln_addl : left_distributive muln addn.

Lemma muln_addr : right_distributive muln addn.

Lemma muln_subl : left_distributive muln subn.

Lemma muln_subr : right_distributive muln subn.

Lemma mulnA : associative muln.

Lemma mulnCA : left_commutative muln.

Lemma mulnAC : right_commutative muln.

Lemma muln_eq0 : forall m n, (m * n == 0) = (m == 0) || (n == 0).

Lemma eqn_mul1 : forall m n, (m * n == 1) = (m == 1) && (n == 1).

Lemma muln_gt0 : forall m n, (0 < m * n) = (0 < m) && (0 < n).

Lemma leq_pmull : forall m n, n > 0 -> m <= n * m.

Lemma leq_pmulr : forall m n, n > 0 -> m <= m * n.

Lemma leq_mul2l : forall m n1 n2, (m * n1 <= m * n2) = (m == 0) || (n1 <= n2).

Lemma leq_mul2r : forall m n1 n2, (n1 * m <= n2 * m) = (m == 0) || (n1 <= n2).

Lemma leq_mul : forall m1 m2 n1 n2, m1 <= n1 -> m2 <= n2 -> m1 * m2 <= n1 * n2.

Lemma eqn_mul2l : forall m n1 n2, (m * n1 == m * n2) = (m == 0) || (n1 == n2).

Lemma eqn_mul2r : forall m n1 n2, (n1 * m == n2 * m) = (m == 0) || (n1 == n2).

Lemma leq_pmul2l : forall m n1 n2, 0 < m -> (m * n1 <= m * n2) = (n1 <= n2).
Implicit Arguments leq_pmul2l [m n1 n2].

Lemma leq_pmul2r : forall m n1 n2, 0 < m -> (n1 * m <= n2 * m) = (n1 <= n2).
Implicit Arguments leq_pmul2r [m n1 n2].

Lemma eqn_pmul2l : forall m n1 n2, 0 < m -> (m * n1 == m * n2) = (n1 == n2).
Implicit Arguments eqn_pmul2l [m n1 n2].

Lemma eqn_pmul2r : forall m n1 n2, 0 < m -> (n1 * m == n2 * m) = (n1 == n2).
Implicit Arguments eqn_pmul2r [m n1 n2].

Lemma ltn_mul2l : forall m n1 n2, (m * n1 < m * n2) = (0 < m) && (n1 < n2).

Lemma ltn_mul2r : forall m n1 n2, (n1 * m < n2 * m) = (0 < m) && (n1 < n2).

Lemma ltn_pmul2l : forall m n1 n2, 0 < m -> (m * n1 < m * n2) = (n1 < n2).
Implicit Arguments ltn_pmul2l [m n1 n2].

Lemma ltn_pmul2r : forall m n1 n2, 0 < m -> (n1 * m < n2 * m) = (n1 < n2).
Implicit Arguments ltn_pmul2r [m n1 n2].

Lemma ltn_Pmull : forall m n, 1 < n -> 0 < m -> m < n * m.

Lemma ltn_Pmulr : forall m n, 1 < n -> 0 < m -> m < m * n.

Lemma ltn_mul : forall 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. Qed.

Lemma expn0 : forall m, m ^ 0 = 1. Qed.

Lemma expn1 : forall m, m ^ 1 = m. Qed.

Lemma expnS : forall m n, m ^ n.+1 = m * m ^ n.

Lemma expnSr : forall m n, m ^ n.+1 = m ^ n * m.

Lemma exp0n : forall n, 0 < n -> 0 ^ n = 0. Qed.

Lemma exp1n : forall n, 1 ^ n = 1.

Lemma expn_add : forall m n1 n2, m ^ (n1 + n2) = m ^ n1 * m ^ n2.

Lemma expn_mull : forall m1 m2 n, (m1 * m2) ^ n = m1 ^ n * m2 ^ n.

Lemma expn_mulr : forall m n1 n2, m ^ (n1 * n2) = (m ^ n1) ^ n2.

Lemma expn_gt0 : forall m n, (0 < m ^ n) = (0 < m) || (n == 0).

Lemma expn_eq0 : forall m e, (m ^ e == 0) = (m == 0) && (e > 0).

Lemma ltn_expl : forall m n, 1 < m -> n < m ^ n.

Lemma leq_exp2l : forall m n1 n2, 1 < m -> (m ^ n1 <= m ^ n2) = (n1 <= n2).

Lemma ltn_exp2l : forall m n1 n2, 1 < m -> (m ^ n1 < m ^ n2) = (n1 < n2).

Lemma eqn_exp2l : forall m n1 n2, 1 < m -> (m ^ n1 == m ^ n2) = (n1 == n2).

Lemma expnI : forall m, 1 < m -> injective (expn m).

Lemma leq_pexp2l : forall m n1 n2, 0 < m -> n1 <= n2 -> m ^ n1 <= m ^ n2.

Lemma ltn_pexp2l : forall m n1 n2, 0 < m -> m ^ n1 < m ^ n2 -> n1 < n2.

Lemma ltn_exp2r : forall m n e, e > 0 -> (m ^ e < n ^ e) = (m < n).

Lemma leq_exp2r : forall m n e, e > 0 -> (m ^ e <= n ^ e) = (m <= n).

Lemma eqn_exp2r : forall m n e, e > 0 -> (m ^ e == n ^ e) = (m == n).

Lemma expIn : forall e, e > 0 -> injective (expn^~ e).

Factorial. 

Fixpoint fact n := if n is n'.+1 then n * fact n' else 1.

A (canonical) structure for positive integers.             
Several types parametrized by integer posses an algebraic  
structure only for non-zero values of the parameter, e.g., 
integers mod n, or square matrices of order n. The pos_nat 
structure allows the type inference to automatically       
discharge this positivity condition. Note that pos_nat     
should not be used for normal arithmetic side condition:   
as Coq does not allow to declare new instances of a        
structure in the midst of a proof, it would be difficult   
to satisfy the conditions for arbitrary expressions.       

Record pos_nat : Type := PosNat { pos_nat_val :> nat; _ : pos_nat_val > 0 }.

Lemma pos_natP : forall n : pos_nat, n > 0. Qed.

Hint Resolve pos_natP.

Canonical Structure pos_nat_subType :=
  Eval hnf in [subType for pos_nat_val by pos_nat_rect].
Definition pos_nat_eqMixin := Eval hnf in [eqMixin of pos_nat by <:].
Canonical Structure pos_nat_eqType := Eval hnf in EqType pos_nat_eqMixin.

Canonical Structure S_pos_nat n := PosNat (ltn0Sn n).

Lemma addr_pos_natP : forall m (n : pos_nat), m + n > 0.
Canonical Structure addr_pos_nat m n := PosNat (addr_pos_natP m n).

Lemma mul_pos_natP : forall (m n : pos_nat), m * n > 0.
Canonical Structure mul_pos_nat m n := PosNat (mul_pos_natP m n).

Lemma exp_pos_natP : forall (n : pos_nat) m, n ^ m > 0.
Canonical Structure exp_pos_nat m n := PosNat (exp_pos_natP m n).

Lemma maxr_pos_natP : forall m (n : pos_nat), maxn m n > 0.
Canonical Structure maxr_pos_nat m n := PosNat (maxr_pos_natP m n).

Lemma min_pos_natP : forall (m n : pos_nat), minn m n > 0.
Canonical Structure min_pos_nat m n := PosNat (min_pos_natP m n).

Lemma fact_gt0 : forall n, fact n > 0.
Canonical Structure fact_pos_nat n := PosNat (fact_gt0 n).

Definition repack_pos_nat n :=
  let: PosNat _ nP := n return (0 < n -> pos_nat) -> pos_nat in fun k => k nP.

Notation "[ 'pos_nat' 'of' n ]" := (repack_pos_nat (fun nP => @PosNat n nP))
  (at level 0, format "[ 'pos_nat' 'of' n ]") : form_scope.

Parity and bits. 

Coercion nat_of_bool (b : bool) := if b then 1 else 0.

Lemma leq_b1 : forall b : bool, b <= 1.

Lemma addn_negb : forall b : bool, ~~ b + b = 1.

Fixpoint odd n := if n is n'.+1 then ~~ odd n' else false.

Lemma oddb : forall b : bool, odd b = b. Qed.

Lemma odd_add : forall m n, odd (m + n) = odd m (+) odd n.

Lemma odd_sub : forall m n, n <= m -> odd (m - n) = odd m (+) odd n.

Lemma odd_opp : forall i m, odd m = false -> i < m -> odd (m - i) = odd i.

Lemma odd_mul : forall m n, odd (m * n) = odd m && odd n.

Lemma odd_exp : forall 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. Qed.

Lemma double0 : 0.*2 = 0. Qed.

Lemma doubleS : forall n, n.+1.*2 = n.*2.+2. Qed.

Lemma addnn : forall n, n + n = n.*2.

Lemma mul2n : forall m, 2 * m = m.*2.

Lemma muln2 : forall m, m * 2 = m.*2.

Lemma double_add : forall m n, (m + n).*2 = m.*2 + n.*2.

Lemma double_sub : forall m n, (m - n).*2 = m.*2 - n.*2.

Lemma leq_double : forall m n, (m.*2 <= n.*2) = (m <= n).

Lemma ltn_double : forall m n, (m.*2 < n.*2) = (m < n).

Lemma ltn_Sdouble : forall m n, (m.*2.+1 < n.*2) = (m < n).

Lemma leq_Sdouble : forall m n, (m.*2 <= n.*2.+1) = (m <= n).

Lemma odd_double : forall n, odd n.*2 = false.

Lemma double_gt0 : forall n, (0 < n.*2) = (0 < n).

Lemma double_eq0 : forall n, (n.*2 == 0) = (n == 0).

Lemma double_mull : forall m n, (m * n).*2 = m.*2 * n.

Lemma double_mulr : forall 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 : forall n, uphalf n.*2 = n.

Lemma uphalf_half : forall n, uphalf n = odd n + n./2.

Lemma odd_double_half : forall n, odd n + n./2.*2 = n.

Lemma half_bit_double : forall n (b : bool), (b + n.*2)./2 = n.

Lemma half_add : forall m n, (m + n)./2 = (odd m && odd n) + (m./2 + n./2).

Lemma half_leq : forall m n, m <= n -> m./2 <= n./2.

Lemma half_gt0 : forall n, (0 < n./2) = (1 < n).

Squares and square identities. 

Lemma mulnn : forall m, m * m = m ^ 2.

Lemma sqrn_add : forall m n, (m + n) ^ 2 = m ^ 2 + n ^ 2 + 2 * (m * n).

Lemma sqrn_sub : forall m n, n <= m ->
  (m - n) ^ 2 = m ^ 2 + n ^ 2 - 2 * (m * n).

Lemma sqrn_add_sub : forall m n, n <= m ->
  (m + n) ^ 2 - 4 * (m * n) = (m - n) ^ 2.

Lemma subn_sqr : forall m n, m ^ 2 - n ^ 2 = (m - n) * (m + n).

Lemma ltn_sqr : forall m n, (m ^ 2 < n ^ 2) = (m < n).

Lemma leq_sqr : forall m n, (m ^ 2 <= n ^ 2) = (m <= n).

Lemma sqrn_gt0 : forall n, (0 < n ^ 2) = (0 < n).

Lemma eqn_sqr : forall 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)
    (at level 70, n at next level,
  format "m '[hv' <= n '/' ?= 'iff' c ']'") : nat_scope.

Coercion leq_of_leqif m n c (H : m <= n ?= iff c) := H.1 : m <= n.

Lemma leqifP : forall m n c,
   reflect (m <= n ?= iff c) (if c then m == n else m < n).

Lemma leqif_refl : forall m c, reflect (m <= m ?= iff c) c.

Lemma leqif_trans : forall m1 m2 m3 c1 c2,
  m1 <= m2 ?= iff c1 -> m2 <= m3 ?= iff c2 -> m1 <= m3 ?= iff c1 && c2.

Lemma monotone_leqif : forall f, monotone f ->
  forall m n c, (f m <= f n ?= iff c) <-> (m <= n ?= iff c).

Lemma leqif_geq : forall m n, m <= n -> m <= n ?= iff (m >= n).

Lemma leqif_eq : forall m n, m <= n -> m <= n ?= iff (m == n).

Lemma leqif_add : forall m1 n1 c1 m2 n2 c2,
    m1 <= n1 ?= iff c1 -> m2 <= n2 ?= iff c2 ->
  m1 + m2 <= n1 + n2 ?= iff c1 && c2.

Lemma leqif_mul : forall 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 : forall m n, 2 * (m * n) <= m ^ 2 + n ^ 2 ?= iff (m == n).

Lemma nat_AGM2 : forall m n, 4 * (m * n) <= (m + n) ^ 2 ?= iff (m == n).

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 : nat) {struct m} :=
  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 : nat) {struct m} :=
  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 : nat) {struct n} :=
  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.

Notation Local oddn := odd.
Fixpoint odd (n : nat) := if n is n'.+2 then odd n' else eqn n 1.

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

Lemma doubleE : double =1 doublen.

Lemma add_mulE : forall n m s, add_mul n m s = addn (muln n m) s.

Lemma mulE : mul =2 muln.

Lemma mul_expE : forall 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 Ndec.Neqb.

Canonical Structure bin_nat_eqMixin := EqMixin eq_binP.
Canonical Structure bin_nat_eqType := Eval hnf in EqType 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 Local 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 : nat) {struct n0} :=
  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_gt0 : forall p, Psucc p = p.+1 :> nat.

Lemma nat_of_addn_gt0 : forall p1 p2, (p1 + p2)%positive = p1 + p2 :> nat.

Lemma nat_of_add_bin : forall b1 b2, (b1 + b2)%num = b1 + b2 :> nat.

Lemma nat_of_mul_bin : forall b1 b2, (b1 * b2)%num = b1 * b2 :> nat.

Lemma nat_of_exp_bin : forall n (b : N), n ^ (b : nat) = 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 Structure number_subType :=
  [newType for bin_of_number by number_rect].
Definition number_eqMixin := Eval hnf in [eqMixin of number by <:].
Canonical Structure number_eqType := Eval hnf in EqType 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 
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 ].