Library Coq.Numbers.NatInt.NZDomain


Require Export NumPrelude NZAxioms.
Require Import NZBase NZOrder NZAddOrder PeanoNat.

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.

Local Notation "f ^ n" := (fun x => nat_rect _ x (fun _ => f) n).

#[global]
Instance nat_rect_wd n {A} (R:relation A) :
 Proper (R==>(R==>R)==>R) (fun x f => nat_rect (fun _ => _) x (fun _ => f) n).

Module NZDomainProp (Import NZ:NZDomainSig').
Include NZBaseProp NZ.

Relationship between points thanks to succ and pred.

For any two points, one is an iterated successor of the other.

Lemma itersucc_or_itersucc 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.

Declare Scope ofnat.
Local Open Scope ofnat.
Notation "[ n ]" := (ofnat n) (at level 7) : 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 NZBaseProp NZ <+ NZOrderProp 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 correspondence 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.

Require Import Plus Minus.