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.
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).
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)...
... 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:
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
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.
An alternative induction principle using S and P.
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.
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.