Library Coq.Numbers.NatInt.NZDomain
In this file, we investigate the shape of domains satisfying
the NZDomainSig interface. In particular, we define a
translation from Peano numbers nat into NZ.
Relationship between points thanks to succ and pred.
For any two points, one is an iterated successor of the other.
Generalized version of pred_succ when iterating
From a given point, all others are iterated successors
or iterated predecessors.
In particular, all points are either iterated successors of 0
or iterated predecessors of 0 (or both).
Study of initial point w.r.t. succ (if any).
First case: let's assume such an initial point exists
(i.e. S isn't surjective)...
... then we have unicity of this initial point.
... then all other points are descendant of it.
NB : We would like to have
pred n == n for the initial element,
but nothing forces that. For instance we can have -3 as initial point,
and P(-3) = 2. A bit odd indeed, but legal according to
NZDomainSig.
We can hence have
n == (P^k) m without
exists k', m == (S^k') n.
We need decidability of
eq (or classical reasoning) for this:
Second case : let's suppose now S surjective, i.e. no initial point.
To summarize:
S is always injective, P is always surjective (thanks to
pred_succ).
I) If S is not surjective, we have an initial point, which is unique.
This bottom is below zero: we have N shifted (or not) to the left.
P cannot be injective: P init = P (S (P init)).
(P init) can be arbitrary.
II) If S is surjective, we have
forall n, S (P n) = n, S and P are
bijective and reciprocal.
IIa) if
exists k<>O, 0 == S^k 0, then we have a cyclic structure Z/nZ
IIb) otherwise, we have Z
An alternative induction principle using S and P.
It is weaker than
bi_induction. For instance it cannot prove that
we can go from one point by many
S or many
P, but only by many
S mixed with many
P. Think of a model with two copies of N:
0, 1=S 0, 2=S 1, ...
0', 1'=S 0', 2'=S 1', ...
and P 0 = 0' and P 0' = 0.
We now focus on the translation from nat into NZ.
First, relationship with 0, succ, pred.
Since P 0 can be anything in NZ (either -1, 0, or even other
numbers, we cannot state previous lemma for n=O.
If we require in addition a strict order on NZ, we can prove that
ofnat is injective, and hence that NZ is infinite
(i.e. we ban Z/nZ models)
For basic operations, we can prove correspondence with
their counterpart in nat.