Library Coq.Numbers.Natural.Binary.NBinary
Require Import BinPos.
Require Export BinNat.
Require Import NAxioms NProperties.
Local Open Scope N_scope.
Bi-directional induction.
Theorem bi_induction :
forall A : N -> Prop, Proper (eq==>iff) A ->
A N0 -> (forall n, A n <-> A (Nsucc n)) -> forall n : N, A n.
Basic operations.
Definition eq_equiv : Equivalence (@eq N) := eq_equivalence.
Local Obligation Tactic := simpl_relation.
Program Instance succ_wd : Proper (eq==>eq) Nsucc.
Program Instance pred_wd : Proper (eq==>eq) Npred.
Program Instance add_wd : Proper (eq==>eq==>eq) Nplus.
Program Instance sub_wd : Proper (eq==>eq==>eq) Nminus.
Program Instance mul_wd : Proper (eq==>eq==>eq) Nmult.
Definition pred_succ := Npred_succ.
Definition add_0_l := Nplus_0_l.
Definition add_succ_l := Nplus_succ.
Definition sub_0_r := Nminus_0_r.
Definition sub_succ_r := Nminus_succ_r.
Definition mul_0_l := Nmult_0_l.
Definition mul_succ_l n m := eq_trans (Nmult_Sn_m n m) (Nplus_comm _ _).
Order
Program Instance lt_wd : Proper (eq==>eq==>iff) Nlt.
Definition lt_eq_cases := Nle_lteq.
Definition lt_irrefl := Nlt_irrefl.
Theorem lt_succ_r : forall n m, n < (Nsucc m) <-> n <= m.
Theorem min_l : forall n m, n <= m -> Nmin n m = n.
Theorem min_r : forall n m, m <= n -> Nmin n m = m.
Theorem max_l : forall n m, m <= n -> Nmax n m = n.
Theorem max_r : forall n m : N, n <= m -> Nmax n m = m.
Part specific to natural numbers, not integers.
Theorem pred_0 : Npred 0 = 0.
Definition recursion (A : Type) : A -> (N -> A -> A) -> N -> A :=
Nrect (fun _ => A).
Implicit Arguments recursion [A].
Instance recursion_wd A (Aeq : relation A) :
Proper (Aeq==>(eq==>Aeq==>Aeq)==>eq==>Aeq) (@recursion A).
Theorem recursion_0 :
forall (A : Type) (a : A) (f : N -> A -> A), recursion a f N0 = a.
Theorem recursion_succ :
forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A),
Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
forall n : N, Aeq (recursion a f (Nsucc 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 := N.
Definition eq := @eq N.
Definition zero := N0.
Definition succ := Nsucc.
Definition pred := Npred.
Definition add := Nplus.
Definition sub := Nminus.
Definition mul := Nmult.
Definition lt := Nlt.
Definition le := Nle.
Definition min := Nmin.
Definition max := Nmax.
End NBinaryAxiomsMod.
Module Export NBinaryPropMod := NPropFunct NBinaryAxiomsMod.