Library Stdlib.Numbers.NatInt.NZDomain

From Stdlib Require Export NumPrelude NZAxioms.
From Stdlib 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.