Library Coq.Numbers.Natural.Binary.NBinDefs



Require Import BinPos.
Require Export BinNat.
Require Import NSub.

Open Local Scope N_scope.

Implementation of NAxiomsSig module type via BinNat.N

Module NBinaryAxiomsMod <: NAxiomsSig.
Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig.
Module Export NZAxiomsMod <: NZAxiomsSig.

Definition NZ := N.
Definition NZeq := @eq N.
Definition NZ0 := N0.
Definition NZsucc := Nsucc.
Definition NZpred := Npred.
Definition NZadd := Nplus.
Definition NZsub := Nminus.
Definition NZmul := Nmult.

Theorem NZeq_equiv : equiv N NZeq.
Add Relation N NZeq
 reflexivity proved by (proj1 NZeq_equiv)
 symmetry proved by (proj2 (proj2 NZeq_equiv))
 transitivity proved by (proj1 (proj2 NZeq_equiv))
as NZeq_rel.

Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.

Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.

Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.

Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.

Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.

Theorem NZinduction :
  forall A : NZ -> Prop, predicate_wd NZeq A ->
    A N0 -> (forall n, A n <-> A (NZsucc n)) -> forall n : NZ, A n.

Theorem NZpred_succ : forall n : NZ, NZpred (NZsucc n) = n.

Theorem NZadd_0_l : forall n : NZ, N0 + n = n.

Theorem NZadd_succ_l : forall n m : NZ, (NZsucc n) + m = NZsucc (n + m).

Theorem NZsub_0_r : forall n : NZ, n - N0 = n.

Theorem NZsub_succ_r : forall n m : NZ, n - (NZsucc m) = NZpred (n - m).

Theorem NZmul_0_l : forall n : NZ, N0 * n = N0.

Theorem NZmul_succ_l : forall n m : NZ, (NZsucc n) * m = n * m + m.

End NZAxiomsMod.

Definition NZlt := Nlt.
Definition NZle := Nle.
Definition NZmin := Nmin.
Definition NZmax := Nmax.

Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd.

Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd.

Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd.

Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd.

Theorem NZlt_eq_cases : forall n m : N, n <= m <-> n < m \/ n = m.

Theorem NZlt_irrefl : forall n : NZ, ~ n < n.

Theorem NZlt_succ_r : forall n m : NZ, n < (NZsucc m) <-> n <= m.

Theorem NZmin_l : forall n m : N, n <= m -> NZmin n m = n.

Theorem NZmin_r : forall n m : N, m <= n -> NZmin n m = m.

Theorem NZmax_l : forall n m : N, m <= n -> NZmax n m = n.

Theorem NZmax_r : forall n m : N, n <= m -> NZmax n m = m.

End NZOrdAxiomsMod.

Definition recursion (A : Type) (a : A) (f : N -> A -> A) (n : N) :=
  Nrect (fun _ => A) a f n.
Implicit Arguments recursion [A].

Theorem pred_0 : Npred N0 = N0.

Theorem recursion_wd :
forall (A : Type) (Aeq : relation A),
  forall a a' : A, Aeq a a' ->
    forall f f' : N -> A -> A, fun2_eq NZeq Aeq Aeq f f' ->
      forall x x' : N, x = x' ->
        Aeq (recursion a f x) (recursion a' f' x').

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 -> fun2_wd NZeq Aeq Aeq f ->
      forall n : N, Aeq (recursion a f (Nsucc n)) (f n (recursion a f n)).

End NBinaryAxiomsMod.

Module Export NBinarySubPropMod := NSubPropFunct NBinaryAxiomsMod.