Library Coq.Numbers.Natural.Binary.NBinDefs
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.