Library Coq.Numbers.Natural.Peano.NPeano
Bi-directional induction.
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.
Basic operations.
Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence.
Local Obligation Tactic := simpl_relation.
Program Instance succ_wd : Proper (eq==>eq) S.
Program Instance pred_wd : Proper (eq==>eq) pred.
Program Instance add_wd : Proper (eq==>eq==>eq) plus.
Program Instance sub_wd : Proper (eq==>eq==>eq) minus.
Program Instance mul_wd : Proper (eq==>eq==>eq) mult.
Theorem pred_succ : forall n : nat, pred (S n) = n.
Theorem add_0_l : forall n : nat, 0 + n = n.
Theorem add_succ_l : forall n m : nat, (S n) + m = S (n + m).
Theorem sub_0_r : forall n : nat, n - 0 = n.
Theorem sub_succ_r : forall n m : nat, n - (S m) = pred (n - m).
Theorem mul_0_l : forall n : nat, 0 * n = 0.
Theorem mul_succ_l : forall n m : nat, S n * m = n * m + m.
Order on natural numbers
Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
Theorem lt_eq_cases : forall n m : nat, n <= m <-> n < m \/ n = m.
Theorem lt_irrefl : forall n : nat, ~ (n < n).
Theorem lt_succ_r : forall n m : nat, n < S m <-> n <= m.
Theorem min_l : forall n m : nat, n <= m -> min n m = n.
Theorem min_r : forall n m : nat, m <= n -> min n m = m.
Theorem max_l : forall n m : nat, m <= n -> max n m = n.
Theorem max_r : forall n m : nat, n <= m -> max n m = m.
Facts specific to natural numbers, not integers.
Theorem pred_0 : pred 0 = 0.
Definition recursion (A : Type) : A -> (nat -> A -> A) -> nat -> A :=
nat_rect (fun _ => A).
Implicit Arguments recursion [A].
Instance recursion_wd (A : Type) (Aeq : relation A) :
Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
Theorem recursion_0 :
forall (A : Type) (a : A) (f : nat -> A -> A), recursion a f 0 = a.
Theorem recursion_succ :
forall (A : Type) (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)).
The instantiation of operations.
Placing them at the very end avoids having indirections in above lemmas.
Definition t := nat.
Definition eq := @eq nat.
Definition zero := 0.
Definition succ := S.
Definition pred := pred.
Definition add := plus.
Definition sub := minus.
Definition mul := mult.
Definition lt := lt.
Definition le := le.
Definition min := min.
Definition max := max.
End NPeanoAxiomsMod.
Now we apply the largest property functor
Euclidean Division
Definition divF div x y := if leb y x then S (div (x-y) y) else 0.
Definition modF mod x y := if leb y x then mod (x-y) y else x.
Definition initF (_ _ : nat) := 0.
Fixpoint loop {A} (F:A->A)(i:A) (n:nat) : A :=
match n with
| 0 => i
| S n => F (loop F i n)
end.
Definition div x y := loop divF initF x x y.
Definition modulo x y := loop modF initF x x y.
Infix "/" := div : nat_scope.
Infix "mod" := modulo (at level 40, no associativity) : nat_scope.
Lemma div_mod : forall x y, y<>0 -> x = y*(x/y) + x mod y.
Lemma mod_upper_bound : forall x y, y<>0 -> x mod y < y.
Require Import NDiv.
Module NDivMod <: NDivSig.
Include NPeanoAxiomsMod.
Definition div := div.
Definition modulo := modulo.
Definition div_mod := div_mod.
Definition mod_upper_bound := mod_upper_bound.
Local Obligation Tactic := simpl_relation.
Program Instance div_wd : Proper (eq==>eq==>eq) div.
Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
End NDivMod.
Module Export NDivPropMod := NDivPropFunct NDivMod NPeanoPropMod.