Library Coq.Numbers.Natural.Binary.NBinary



Require Import BinPos.
Require Export BinNat.
Require Import NAxioms NProperties.

Local Open Scope N_scope.

Implementation of NAxiomsSig module type via BinNat.N


Module NBinaryAxiomsMod <: NAxiomsSig.

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.