Library Stdlib.Arith.PeanoNat

From Stdlib Require Import NAxioms NProperties OrdersFacts DecidableClass.

Module Nat
  <: NAxiomsSig
  <: UsualDecidableTypeFull
  <: OrderedTypeFull
  <: TotalOrder.

Include Corelib.Init.Nat.

Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence.
Local Obligation Tactic := simpl_relation.
#[global] Program Instance succ_wd : Proper (eq==>eq) S.
#[global] Program Instance pred_wd : Proper (eq==>eq) pred.
#[global] Program Instance add_wd : Proper (eq==>eq==>eq) plus.
#[global] Program Instance sub_wd : Proper (eq==>eq==>eq) minus.
#[global] Program Instance mul_wd : Proper (eq==>eq==>eq) mult.
#[global] Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
#[global] Program Instance div_wd : Proper (eq==>eq==>eq) div.
#[global] Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
#[global] Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
#[global] Program Instance testbit_wd : Proper (eq==>eq==>eq) testbit.

Theorem bi_induction :
  forall A : nat -> Prop, Proper (eq==>iff) A ->
    A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n.

Definition recursion {A} : A -> (nat -> A -> A) -> nat -> A :=
  nat_rect (fun _ => A).

#[global] Instance recursion_wd {A} (Aeq : relation A) :
  Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion.

Theorem recursion_0 :
  forall {A} (a : A) (f : nat -> A -> A), recursion a f 0 = a.

Theorem recursion_succ :
  forall {A} (Aeq : relation A) (a : A) (f : nat -> A -> A),
    Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
      forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).

Definition eq := @Logic.eq nat.
Definition le := Peano.le.
Definition lt := Peano.lt.

Lemma pred_succ n : pred (S n) = n.

Lemma pred_0 : pred 0 = 0.

Lemma one_succ : 1 = S 0.

Lemma two_succ : 2 = S 1.

Lemma add_0_l n : 0 + n = n.

Lemma add_succ_l n m : (S n) + m = S (n + m).

Lemma sub_0_r n : n - 0 = n.

Lemma sub_succ_r n m : n - (S m) = pred (n - m).

Lemma mul_0_l n : 0 * n = 0.

Lemma mul_succ_l n m : S n * m = n * m + m.

Lemma lt_succ_r n m : n < S m <-> n <= m.

Lemma eqb_eq n m : eqb n m = true <-> n = m.

#[global]
Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := {
  Decidable_spec := Nat.eqb_eq x y
}.

Lemma leb_le n m : (n <=? m) = true <-> n <= m.

#[global]
Instance Decidable_le_nat : forall (x y : nat), Decidable (x <= y) := {
  Decidable_spec := Nat.leb_le x y
}.

Lemma ltb_lt n m : (n <? m) = true <-> n < m.

Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}.

Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m.

Lemma compare_lt_iff n m : (n ?= m) = Lt <-> n < m.

Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.

Lemma compare_antisym n m : (m ?= n) = CompOpp (n ?= m).

Lemma compare_succ n m : (S n ?= S m) = (n ?= m).

Lemma max_l : forall n m, m <= n -> max n m = n.

Lemma max_r : forall n m, n <= m -> max n m = m.

Lemma min_l : forall n m, n <= m -> min n m = n.

Lemma min_r : forall n m, m <= n -> min n m = m.

Include BoolOrderFacts.

Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

Lemma strong_induction_le (A : nat -> Prop) :
  A 0 -> (forall n, (forall m, m <= n -> A m) -> A (S n)) -> forall n, A n.

Lemma pow_neg_r a b : b<0 -> a^b = 0.

Lemma pow_0_r a : a^0 = 1.

Lemma pow_succ_r a b : 0<=b -> a^(S b) = a * a^b.

Lemma square_spec n : square n = n * n.

Definition Even n := exists m, n = 2*m.
Definition Odd n := exists m, n = 2*m+1.

Module Private_Parity.

Lemma Even_0 : Even 0.

Lemma Even_1 : ~ Even 1.

Lemma Even_2 n : Even n <-> Even (S (S n)).

Lemma Odd_0 : ~ Odd 0.

Lemma Odd_1 : Odd 1.

Lemma Odd_2 n : Odd n <-> Odd (S (S n)).

End Private_Parity.
Import Private_Parity.

Lemma even_spec : forall n, even n = true <-> Even n.

Lemma odd_spec : forall n, odd n = true <-> Odd n.

Lemma divmod_spec : forall x y q u, u <= y ->
  let (q',u') := divmod x y q u in
  x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y.

Lemma div_mod_eq x y : x = y*(x/y) + x mod y.

Lemma div_mod x y : y <> 0 -> x = y*(x/y) + x mod y.

Lemma mod_bound_pos x y : 0<=x -> 0<y -> 0 <= x mod y < y.

Lemma sqrt_iter_spec : forall k p q r,
  q = p+p -> r<=q ->
  let s := sqrt_iter k p q r in
  s*s <= k + p*p + (q - r) < (S s)*(S s).

Lemma sqrt_specif n : (sqrt n)*(sqrt n) <= n < S (sqrt n) * S (sqrt n).

Definition sqrt_spec a (Ha:0<=a) := sqrt_specif a.

Lemma sqrt_neg a : a<0 -> sqrt a = 0.

Lemma log2_iter_spec : forall k p q r,
  2^(S p) = q + S r -> r < 2^p ->
  let s := log2_iter k p q r in
  2^s <= k + q < 2^(S s).

Lemma log2_spec n : 0<n ->
  2^(log2 n) <= n < 2^(S (log2 n)).

Lemma log2_nonpos n : n<=0 -> log2 n = 0.

Lemma iter_swap_gen A B (f:A -> B) (g:A -> A) (h:B -> B) :
 (forall a, f (g a) = h (f a)) -> forall n a,
 f (iter n g a) = iter n h (f a).

Lemma iter_swap :
  forall n (A:Type) (f:A -> A) (x:A),
    iter n f (f x) = f (iter n f x).

Lemma iter_succ :
  forall n (A:Type) (f:A -> A) (x:A),
    iter (S n) f x = f (iter n f x).

Lemma iter_succ_r :
  forall n (A:Type) (f:A -> A) (x:A),
    iter (S n) f x = iter n f (f x).

Lemma iter_add :
  forall p q (A:Type) (f:A -> A) (x:A),
    iter (p+q) f x = iter p f (iter q f x).

Lemma iter_ind (A:Type) (f:A -> A) (a:A) (P:nat -> A -> Prop) :
    P 0 a ->
    (forall n a', P n a' -> P (S n) (f a')) ->
    forall n, P n (iter n f a).

Lemma iter_rect (A:Type) (f:A -> A) (a:A) (P:nat -> A -> Type) :
    P 0 a ->
    (forall n a', P n a' -> P (S n) (f a')) ->
    forall n, P n (iter n f a).

Lemma iter_invariant :
  forall (n:nat) (A:Type) (f:A -> A) (Inv:A -> Prop),
    (forall x:A, Inv x -> Inv (f x)) ->
    forall x:A, Inv x -> Inv (iter n f x).

Definition divide x y := exists z, y=z*x.
Notation "( x | y )" := (divide x y) (at level 0) : nat_scope.

Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b).

Lemma gcd_divide_l : forall a b, (gcd a b | a).

Lemma gcd_divide_r : forall a b, (gcd a b | b).

Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b).

Lemma gcd_nonneg a b : 0<=gcd a b.

Definition double_S : forall n, double (S n) = S (S (double n))
                    := fun n => add_succ_r (S n) n.

Definition double_add : forall n m, double (n + m) = double n + double m
                      := fun n m => add_shuffle1 n m n m.

Lemma double_twice : forall n, double n = 2*n.

Module Type PrivateBitwiseSpec.
  Parameter testbit_odd_0 : forall a : nat, testbit (add (mul 2 a) 1) 0 = true.
  Parameter testbit_even_0 : forall a : nat, testbit (mul 2 a) 0 = false.
  Parameter testbit_odd_succ : forall a n : nat, le 0 n ->
    testbit (add (mul 2 a) 1) (succ n) = testbit a n.
  Parameter testbit_even_succ : forall a n : nat, le 0 n ->
    testbit (mul 2 a) (succ n) = testbit a n.
  Parameter testbit_neg_r : forall a n : nat, lt n 0 -> testbit a n = false.
  Parameter shiftr_spec : forall a n m : nat, le 0 m ->
    testbit (shiftr a n) m = testbit a (add m n).
  Parameter shiftl_spec_high :
    forall a n m : nat, le 0 m ->
    le n m -> testbit (shiftl a n) m = testbit a (sub m n).
  Parameter shiftl_spec_low :
    forall a n m : nat, lt m n -> testbit (shiftl a n) m = false.
  Parameter land_spec :
    forall a b n : nat, testbit (land a b) n = testbit a n && testbit b n.
  Parameter lor_spec :
    forall a b n : nat, testbit (lor a b) n = testbit a n || testbit b n.
  Parameter ldiff_spec :
    forall a b n : nat,
    testbit (ldiff a b) n = testbit a n && negb (testbit b n).
  Parameter lxor_spec :
    forall a b n : nat, testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
  Parameter div2_spec :
    forall a : nat, eq (div2 a) (shiftr a 1).
  Parameter div2_double : forall n, div2 (2*n) = n.
  Parameter div2_succ_double : forall n, div2 (S (2*n)) = n.
  Parameter div2_bitwise : forall op n a b,
    div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b).
  Parameter odd_bitwise : forall op n a b,
    odd (bitwise op (S n) a b) = op (odd a) (odd b).
  Parameter testbit_bitwise_1 : forall op, (forall b, op false b = false) ->
    forall n m a b, a<=n ->
    testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).
  Parameter testbit_bitwise_2 : forall op, op false false = false ->
    forall n m a b, a<=n -> b<=n ->
    testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).
End PrivateBitwiseSpec.


Module PrivateImplementsBitwiseSpec : PrivateBitwiseSpec.

Lemma div2_double n : div2 (2*n) = n.

Lemma div2_succ_double n : div2 (S (2*n)) = n.

Lemma le_div2 n : div2 (S n) <= n.

Lemma lt_div2 n : 0 < n -> div2 n < n.

Lemma div2_decr a n : a <= S n -> div2 a <= n.

Lemma testbit_0_l : forall n, testbit 0 n = false.

Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.

Lemma testbit_even_0 a : testbit (2*a) 0 = false.

Lemma testbit_odd_succ' a n : testbit (2*a+1) (S n) = testbit a n.

Lemma testbit_even_succ' a n : testbit (2*a) (S n) = testbit a n.

Lemma shiftr_specif : forall a n m,
  testbit (shiftr a n) m = testbit a (m+n).

Lemma shiftl_specif_high : forall a n m, n<=m ->
  testbit (shiftl a n) m = testbit a (m-n).

Lemma shiftl_spec_low : forall a n m, m<n ->
  testbit (shiftl a n) m = false.

Lemma div2_bitwise : forall op n a b,
  div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b).

Lemma odd_bitwise : forall op n a b,
  odd (bitwise op (S n) a b) = op (odd a) (odd b).

Lemma testbit_bitwise_1 : forall op, (forall b, op false b = false) ->
  forall n m a b, a<=n ->
  testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).

Lemma testbit_bitwise_2 : forall op, op false false = false ->
  forall n m a b, a<=n -> b<=n ->
  testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).

Lemma land_spec a b n :
  testbit (land a b) n = testbit a n && testbit b n.

Lemma ldiff_spec a b n :
  testbit (ldiff a b) n = testbit a n && negb (testbit b n).

Lemma lor_spec a b n :
  testbit (lor a b) n = testbit a n || testbit b n.

Lemma lxor_spec a b n :
  testbit (lxor a b) n = xorb (testbit a n) (testbit b n).

Lemma div2_spec a : div2 a = shiftr a 1.

Definition testbit_odd_succ a n (_:0<=n) := testbit_odd_succ' a n.

Definition testbit_even_succ a n (_:0<=n) := testbit_even_succ' a n.

Lemma testbit_neg_r a n (H:n<0) : testbit a n = false.

Definition shiftl_spec_high a n m (_:0<=m) := shiftl_specif_high a n m.

Definition shiftr_spec a n m (_:0<=m) := shiftr_specif a n m.
End PrivateImplementsBitwiseSpec.
Include PrivateImplementsBitwiseSpec.

Lemma div_0_r a : a / 0 = 0.

Lemma mod_0_r a : a mod 0 = a.

Include NExtraPreProp <+ NExtraProp0.

Lemma binary_induction (A : nat -> Prop) :
  A 0 -> (forall n, A n -> A (2 * n)) -> (forall n, A n -> A (2 * n + 1))
  -> forall n, A n.

Lemma tail_add_spec n m : tail_add n m = n + m.

Lemma tail_addmul_spec r n m : tail_addmul r n m = r + n * m.

Lemma tail_mul_spec n m : tail_mul n m = n * m.

Definition Even_Odd_dec n : {Even n} + {Odd n}.

Lemma Even_add_split n m :
  Even (n + m) -> Even n /\ Even m \/ Odd n /\ Odd m.

Lemma Odd_add_split n m :
  Odd (n + m) -> Odd n /\ Even m \/ Even n /\ Odd m.

Lemma Even_Even_add n m: Even n -> Even m -> Even (n + m).

Lemma Odd_add_l n m : Odd n -> Even m -> Odd (n + m).

Lemma Odd_add_r n m : Even n -> Odd m -> Odd (n + m).

Lemma Odd_Odd_add n m : Odd n -> Odd m -> Even (n + m).

Lemma Even_add_aux n m :
  (Odd (n + m) <-> Odd n /\ Even m \/ Even n /\ Odd m) /\
  (Even (n + m) <-> Even n /\ Even m \/ Odd n /\ Odd m).

Lemma Even_add_Even_inv_r n m : Even (n + m) -> Even n -> Even m.

Lemma Even_add_Even_inv_l n m : Even (n + m) -> Even m -> Even n.

Lemma Even_add_Odd_inv_r n m : Even (n + m) -> Odd n -> Odd m.

Lemma Even_add_Odd_inv_l n m : Even (n + m) -> Odd m -> Odd n.

Lemma Odd_add_Even_inv_l n m : Odd (n + m) -> Odd m -> Even n.

Lemma Odd_add_Even_inv_r n m : Odd (n + m) -> Odd n -> Even m.

Lemma Odd_add_Odd_inv_l n m : Odd (n + m) -> Even m -> Odd n.

Lemma Odd_add_Odd_inv_r n m : Odd (n + m) -> Even n -> Odd m.

Lemma Even_mul_aux n m :
  (Odd (n * m) <-> Odd n /\ Odd m) /\ (Even (n * m) <-> Even n \/ Even m).

Lemma Even_mul_l n m : Even n -> Even (n * m).

Lemma Even_mul_r n m : Even m -> Even (n * m).

Lemma Even_mul_inv_r n m : Even (n * m) -> Odd n -> Even m.

Lemma Even_mul_inv_l n m : Even (n * m) -> Odd m -> Even n.

Lemma Odd_mul n m : Odd n -> Odd m -> Odd (n * m).

Lemma Odd_mul_inv_l n m : Odd (n * m) -> Odd n.

Lemma Odd_mul_inv_r n m : Odd (n * m) -> Odd m.

Lemma Even_div2 n : Even n -> div2 n = div2 (S n).

Lemma Odd_div2 n : Odd n -> S (div2 n) = div2 (S n).

Lemma div2_Even n : div2 n = div2 (S n) -> Even n.

Lemma div2_Odd n : S (div2 n) = div2 (S n) -> Odd n.

Lemma Even_Odd_div2 n :
  (Even n <-> div2 n = div2 (S n)) /\ (Odd n <-> S (div2 n) = div2 (S n)).

Lemma Even_Odd_double n :
  (Even n <-> n = double (div2 n)) /\ (Odd n <-> n = S (double (div2 n))).

Lemma Even_double n : Even n -> n = double (div2 n).

Lemma double_Even n : n = double (div2 n) -> Even n.

Lemma Odd_double n : Odd n -> n = S (double (div2 n)).

Lemma double_Odd n : n = S (double (div2 n)) -> Odd n.

Inductive Even_alt : nat -> Prop :=
| Even_alt_O : Even_alt 0
| Even_alt_S : forall n, Odd_alt n -> Even_alt (S n)
with Odd_alt : nat -> Prop :=
| Odd_alt_S : forall n, Even_alt n -> Odd_alt (S n).

Lemma Even_alt_Even : forall n, Even_alt n <-> Even n.

Lemma Odd_alt_Odd : forall n, Odd_alt n <-> Odd n.

Scheme Odd_alt_Even_alt_ind := Minimality for Odd_alt Sort Prop
with Even_alt_Odd_alt_ind := Minimality for Even_alt Sort Prop.

Lemma Odd_Even_ind (P Q : nat -> Prop) :
  (forall n, Even n -> Q n -> P (S n)) ->
  Q 0 -> (forall n, Odd n -> P n -> Q (S n)) -> forall n, Odd n -> P n.

Lemma Even_Odd_ind (P Q : nat -> Prop) :
  (forall n, Even n -> Q n -> P (S n)) ->
  Q 0 -> (forall n, Odd n -> P n -> Q (S n)) -> forall n, Even n -> Q n.


Scheme Odd_alt_Even_alt_sind := Minimality for Odd_alt Sort SProp
with Even_alt_Odd_alt_sind := Minimality for Even_alt Sort SProp.

Lemma Odd_Even_sind (P Q : nat -> SProp) :
  (forall n, Even n -> Q n -> P (S n)) ->
  Q 0 -> (forall n, Odd n -> P n -> Q (S n)) -> forall n, Odd n -> P n.

Lemma Even_Odd_sind (P Q : nat -> SProp) :
  (forall n, Even n -> Q n -> P (S n)) ->
  Q 0 -> (forall n, Odd n -> P n -> Q (S n)) -> forall n, Even n -> Q n.

Definition EvenT n := { m | n = 2 * m }.
Definition OddT n := { m | n = 2 * m + 1 }.

Lemma EvenT_0 : EvenT 0.

Lemma EvenT_2 n : EvenT n -> EvenT (S (S n)).

Lemma OddT_1 : OddT 1.

Lemma OddT_2 n : OddT n -> OddT (S (S n)).

Lemma EvenT_S_OddT n : EvenT (S n) -> OddT n.

Lemma OddT_S_EvenT n : OddT (S n) -> EvenT n.

Lemma even_EvenT : forall n, even n = true -> EvenT n.

Lemma odd_OddT : forall n, odd n = true -> OddT n.

Lemma EvenT_Even n : EvenT n -> Even n.

Lemma OddT_Odd n : OddT n -> Odd n.

Lemma Even_EvenT n : Even n -> EvenT n.

Lemma Odd_OddT n : Odd n -> OddT n.

Lemma EvenT_even n : EvenT n -> even n = true.

Lemma OddT_odd n : OddT n -> odd n = true.

Lemma EvenT_OddT_dec n : EvenT n + OddT n.

Lemma OddT_EvenT_rect (P Q : nat -> Type) :
  (forall n, EvenT n -> Q n -> P (S n)) ->
  Q 0 -> (forall n, OddT n -> P n -> Q (S n)) -> forall n, OddT n -> P n.

Lemma EvenT_OddT_rect (P Q : nat -> Type) :
  (forall n, EvenT n -> Q n -> P (S n)) ->
  Q 0 -> (forall n, OddT n -> P n -> Q (S n)) -> forall n, EvenT n -> Q n.

End Nat.

Bind Scope nat_scope with Nat.t nat.

Infix "^" := Nat.pow : nat_scope.
Infix "=?" := Nat.eqb (at level 70) : nat_scope.
Infix "<=?" := Nat.leb (at level 70) : nat_scope.
Infix "<?" := Nat.ltb (at level 70) : nat_scope.
Infix "?=" := Nat.compare (at level 70) : nat_scope.
Infix "/" := Nat.div : nat_scope.
Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope.

#[global] Hint Unfold Nat.le : core.
#[global] Hint Unfold Nat.lt : core.

#[local]
Definition lt_n_Sm_le := (fun n m => (proj1 (Nat.lt_succ_r n m))).
Register lt_n_Sm_le as num.nat.lt_n_Sm_le.
#[local]
Definition le_lt_n_Sm := (fun n m => (proj2 (Nat.lt_succ_r n m))).
Register le_lt_n_Sm as num.nat.le_lt_n_Sm.
#[local]
Definition lt_S_n := (fun n m => (proj2 (Nat.succ_lt_mono n m))).
Register lt_S_n as num.nat.lt_S_n.
Register Nat.le_lt_trans as num.nat.le_lt_trans.
#[local]
Definition pred_of_minus := (fun n => eq_sym (Nat.sub_1_r n)).
Register pred_of_minus as num.nat.pred_of_minus.
Register Nat.le_trans as num.nat.le_trans.
Register Nat.nlt_0_r as num.nat.nlt_0_r.

Section TestOrder.
  Let test : forall x y, x<=y -> y<=x -> x=y.
End TestOrder.