Require Export NZAxioms.
Require Import ZArith.
Require Import Zpow_facts.
Require Import DoubleType.
Require Import CyclicAxioms.
Require Import Lia.

Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig.

Local Open Scope Z_scope.

Local Notation wB := (base ZnZ.digits).

Local Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99).

Definition eq (n m : t) := [| n |] = [| m |].
Definition zero := ZnZ.zero.
Definition one := ZnZ.one.
Definition two := ZnZ.succ ZnZ.one.
Definition succ := ZnZ.succ.
Definition pred := ZnZ.pred.
Definition add := ZnZ.add.
Definition sub := ZnZ.sub.
Definition mul := ZnZ.mul.

Local Infix "==" := eq (at level 70).
Local Notation "0" := zero.
Local Notation S := succ.
Local Notation P := pred.
Local Infix "+" := add.
Local Infix "-" := sub.
Local Infix "*" := mul.

Global Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred
 ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic.
Ltac zify :=
 unfold eq, zero, one, two, succ, pred, add, sub, mul in *;
 autorewrite with cyclic.
Ltac zcongruence := repeat red; intros; zify; congruence.

#[global]
Instance eq_equiv : Equivalence eq.

Local Obligation Tactic := zcongruence.

#[global]
Program Instance succ_wd : Proper (eq ==> eq) succ.
#[global]
Program Instance pred_wd : Proper (eq ==> eq) pred.
#[global]
Program Instance add_wd : Proper (eq ==> eq ==> eq) add.
#[global]
Program Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
#[global]
Program Instance mul_wd : Proper (eq ==> eq ==> eq) mul.

Theorem gt_wB_1 : 1 < wB.

Theorem gt_wB_0 : 0 < wB.

Lemma one_mod_wB : 1 mod wB = 1.

Lemma succ_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB.

Lemma pred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB.

Lemma NZ_to_Z_mod : forall n, [| n |] mod wB = [| n |].

Theorem pred_succ : forall n, P (S n) == n.

Theorem one_succ : one == succ zero.

Theorem two_succ : two == succ one.

Section Induction.

Variable A : t -> Prop.
Hypothesis A_wd : Proper (eq ==> iff) A.
Hypothesis A0 : A 0.
Hypothesis AS : forall n, A n <-> A (S n).

Let B (n : Z) := A (ZnZ.of_Z n).

Lemma B0 : B 0.

Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).

Theorem Zbounded_induction :
  (forall Q : Z -> Prop, forall b : Z,
    Q 0 ->
    (forall n, 0 <= n -> n < b - 1 -> Q n -> Q (n + 1)) ->
      forall n, 0 <= n -> n < b -> Q n)%Z.

Lemma B_holds : forall n : Z, 0 <= n < wB -> B n.

Theorem bi_induction : forall n, A n.

End Induction.

Theorem add_0_l : forall n, 0 + n == n.

Theorem add_succ_l : forall n m, (S n) + m == S (n + m).

Theorem sub_0_r : forall n, n - 0 == n.

Theorem sub_succ_r : forall n m, n - (S m) == P (n - m).

Theorem mul_0_l : forall n, 0 * n == 0.

Theorem mul_succ_l : forall n m, (S n) * m == n * m + m.

Definition t := t.

End NZCyclicAxiomsMod.