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.
First, some complements about
nat_iter
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 correspondance with
their counterpart in nat.