Library Coq.Numbers.Natural.SpecViaZ.NSigNAxioms
The interface NSig.NType implies the interface NAxiomsSig
Module NTypeIsNAxioms (
Import N :
NType').
Hint Rewrite
spec_0 spec_succ spec_add spec_mul spec_pred spec_sub
spec_div spec_modulo spec_gcd spec_compare spec_eq_bool
spec_max spec_min spec_power_pos spec_power
:
nsimpl.
Ltac nsimpl :=
autorewrite with nsimpl.
Ltac ncongruence :=
unfold eq;
repeat red;
intros;
nsimpl;
congruence.
Ltac zify :=
unfold eq,
lt,
le in *;
nsimpl.
Local Obligation Tactic :=
ncongruence.
Instance eq_equiv :
Equivalence eq.
Program Instance succ_wd :
Proper (
eq==>eq)
succ.
Program Instance pred_wd :
Proper (
eq==>eq)
pred.
Program Instance add_wd :
Proper (
eq==>eq==>eq)
add.
Program Instance sub_wd :
Proper (
eq==>eq==>eq)
sub.
Program Instance mul_wd :
Proper (
eq==>eq==>eq)
mul.
Theorem pred_succ :
forall n,
pred (
succ n)
== n.
Definition N_of_Z z :=
of_N (
Zabs_N z).
Section Induction.
Variable A :
N.t ->
Prop.
Hypothesis A_wd :
Proper (
eq==>iff)
A.
Hypothesis A0 :
A 0.
Hypothesis AS :
forall n,
A n <-> A (
succ n).
Let B (
z :
Z) :=
A (
N_of_Z z).
Lemma B0 :
B 0.
Lemma BS :
forall z :
Z, (0
<= z)%
Z ->
B z ->
B (
z + 1).
Lemma B_holds :
forall z :
Z, (0
<= z)%
Z ->
B z.
Theorem bi_induction :
forall n,
A n.
End Induction.
Theorem add_0_l :
forall n, 0
+ n == n.
Theorem add_succ_l :
forall n m,
(succ n) + m == succ (
n + m).
Theorem sub_0_r :
forall n,
n - 0
== n.
Theorem sub_succ_r :
forall n m,
n - (succ m) == pred (
n - m).
Theorem mul_0_l :
forall n, 0
* n == 0.
Theorem mul_succ_l :
forall n m,
(succ n) * m == n * m + m.
Order
Properties specific to natural numbers, not integers.