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.