# Library Coq.Numbers.NatInt.NZDomain

Require Export NumPrelude NZAxioms.
Require Import NZBase NZOrder NZAddOrder Plus Minus.
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, a section about iterating a function.
Section Iter.
Variable A : Type.
Fixpoint iter (f:A->A)(n:nat) : A -> A := fun a =>
match n with
| O => a
| S n => f (iter f n a)
end.
Infix "^" := iter.
Lemma iter_alt : forall f n m, (f ^( Datatypes.S n )) m = (f ^ n) (f m).
Lemma iter_plus : forall f n n' m, (f ^( n + n' )) m = (f ^ n) ((f ^ n') m).
Lemma iter_plus_bis : forall f n n' m, (f ^( n + n' )) m = (f ^ n') ((f ^ n) m).
Global Instance iter_wd (R:relation A) : Proper (( R ==> R )==> eq ==> R ==> R) iter.
End Iter.
Implicit Arguments iter [A].
Local Infix "^" := iter.
Module NZDomainProp (Import NZ:NZDomainSig').

# Relationship between points thanks to succ and pred.

We prove that any points in NZ have a common descendant by succ
Definition common_descendant n m := exists k , exists l , (S ^ k) n == (S ^ l) m.
Instance common_descendant_wd : Proper (eq ==> eq ==> iff) common_descendant.
Instance common_descendant_equiv : Equivalence common_descendant.
Lemma common_descendant_with_0 : forall n, common_descendant n 0.
Lemma common_descendant_always : forall n m, common_descendant n m.
Thanks to succ being injective, we can then deduce that for any two points, one is an iterated successor of the other.
Lemma itersucc_or_itersucc : forall n m, exists k , n == (S ^ k) m \/ m == (S ^ k) n.
Generalized version of pred_succ when iterating
Lemma succ_swap_pred : forall k n m, n == (S ^ k) m -> m == (P ^ k) n.
From a given point, all others are iterated successors or iterated predecessors.
Lemma itersucc_or_iterpred : forall n m, exists k , n == (S ^ k) m \/ n == (P ^ k) m.
In particular, all points are either iterated successors of 0 or iterated predecessors of 0 (or both).
Lemma itersucc0_or_iterpred0 :
forall n, exists p : nat , n == (S ^ p) 0 \/ n == (P ^ p) 0.

# Study of initial point w.r.t. succ (if any).

Definition initial n := forall m, n ~= S m.
Lemma initial_alt : forall n, initial n <-> S (P n) ~= n.
Lemma initial_alt2 : forall n, initial n <-> ~ exists m , n == S m.
First case: let's assume such an initial point exists (i.e. S isn't surjective)...
Section InitialExists.
Hypothesis init : t.
Hypothesis Initial : initial init.
... then we have unicity of this initial point.
Lemma initial_unique : forall m, initial m -> m == init.
... then all other points are descendant of it.
Lemma initial_ancestor : forall m, exists p , m == (S ^ p) init.
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:
Section SuccPred.
Hypothesis eq_decidable : forall n m, n == m \/ n ~= m.
Lemma succ_pred_approx : forall n, ~ initial n -> S (P n) == n.
End SuccPred.
End InitialExists.
Second case : let's suppose now S surjective, i.e. no initial point.
Section InitialDontExists.
Hypothesis succ_onto : forall n, exists m , n == S m.
Lemma succ_onto_gives_succ_pred : forall n, S (P n) == n.
Lemma succ_onto_pred_injective : forall n m, P n == P m -> n == m.
End InitialDontExists.
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.
Lemma bi_induction_pred :
forall A : t -> Prop, Proper (eq ==> iff) A ->
A 0 -> (forall n, A n -> A (S n)) -> (forall n, A n -> A (P n)) ->
forall n, A n.
Lemma central_induction_pred :
forall A : t -> Prop, Proper (eq ==> iff) A -> forall n0,
A n0 -> (forall n, A n -> A (S n)) -> (forall n, A n -> A (P n)) ->
forall n, A n.
End NZDomainProp.
We now focus on the translation from nat into NZ. First, relationship with 0, succ, pred.
Module NZOfNat (Import NZ:NZDomainSig').
Definition ofnat (n : nat) : t := (S ^ n) 0.
Notation "[ n ]" := (ofnat n) (at level 7) : ofnat.
Local Open Scope ofnat.
Lemma ofnat_zero : [ O ] == 0.
Lemma ofnat_succ : forall n, [ Datatypes.S n ] == succ [ n ].
Lemma ofnat_pred : forall n, n <> O -> [ Peano.pred n ] == P [ n ].
Since P 0 can be anything in NZ (either -1, 0, or even other numbers, we cannot state previous lemma for n=O.
End NZOfNat.
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)
Module NZOfNatOrd (Import NZ:NZOrdSig').
Include NZOfNat NZ.
Include NZOrderPropFunct NZ.
Local Open Scope ofnat.
Theorem ofnat_S_gt_0 :
forall n : nat, 0 < [ Datatypes.S n ].
Theorem ofnat_S_neq_0 :
forall n : nat, 0 ~= [ Datatypes.S n ].
Lemma ofnat_injective : forall n m, [ n ] == [ m ] -> n = m.
Lemma ofnat_eq : forall n m, [ n ] == [ m ] <-> n = m.
Lemma ofnat_lt : forall n m : nat, [ n ] < [ m ] <-> (n < m)%nat.
Lemma ofnat_le : forall n m : nat, [ n ] <= [ m ] <-> (n <= m)%nat.
End NZOfNatOrd.
For basic operations, we can prove correspondance with their counterpart in nat.
Module NZOfNatOps (Import NZ:NZAxiomsSig').
Include NZOfNat NZ.
Local Open Scope ofnat.
Lemma ofnat_add_l : forall n m, [ n ] + m == (S ^ n) m.
Lemma ofnat_add : forall n m, [ n + m ] == [ n ] + [ m ].
Lemma ofnat_mul : forall n m, [ n * m ] == [ n ] * [ m ].
Lemma ofnat_sub_r : forall n m, n - [ m ] == (P ^ m) n.
Lemma ofnat_sub : forall n m, m <= n -> [ n - m ] == [ n ] - [ m ].
End NZOfNatOps.