Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

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

From CyclicType to NZAxiomsSig

A Z/nZ representation given by a module type CyclicType implements NZAxiomsSig, e.g. the common properties between N and Z with no ordering. Notice that the n in Z/nZ is a power of 2.

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

Local Open Scope Z_scope.

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.
Notation S := succ.
Notation P := pred.
Local Infix "+" := add.
Local Infix "-" := sub.
Local Infix "*" := mul.

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.

Instance eq_equiv : Equivalence eq.Equivalence eq
Proof.Equivalence eq
unfold eq.Equivalence (fun n m : t => [|n|] = [|m|]) firstorder.
Qed.

Local Obligation Tactic := zcongruence.

Instance succ_wd : Proper (eq ==> eq) succ.
Instance pred_wd : Proper (eq ==> eq) pred.
Instance add_wd : Proper (eq ==> eq ==> eq) add.
Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
Instance mul_wd : Proper (eq ==> eq ==> eq) mul.

Theorem gt_wB_1 : 1 < wB.1 < wB
Proof.1 < wB
unfold base.1 < 2 ^ Z.pos ZnZ.digits apply Zpower_gt_1; unfold Z.lt; auto with zarith.
Qed.

Theorem gt_wB_0 : 0 < wB.0 < wB
Proof.0 < wB
pose proof gt_wB_1; auto with zarith.
Qed.

Lemma one_mod_wB : 1 mod wB = 1.1 mod wB = 1
Proof.1 mod wB = 1
rewrite Zmod_small.1 = 1
0 <= 1 < wB reflexivity.0 <= 1 < wB split.0 <= 1
1 < wB auto with zarith.1 < wB apply gt_wB_1.
Qed.

Lemma succ_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB.forall n : Z, (n + 1) mod wB = (n mod wB + 1) mod wB
Proof.forall n : Z, (n + 1) mod wB = (n mod wB + 1) mod wB
intro n.n:Z
(n + 1) mod wB = (n mod wB + 1) mod wB rewrite <- one_mod_wB at 2.n:Z
(n + 1) mod wB = (n mod wB + 1 mod wB) mod wB now rewrite <- Zplus_mod.
Qed.

Lemma pred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB.forall n : Z, (n - 1) mod wB = (n mod wB - 1) mod wB
Proof.forall n : Z, (n - 1) mod wB = (n mod wB - 1) mod wB
intro n.n:Z
(n - 1) mod wB = (n mod wB - 1) mod wB rewrite <- one_mod_wB at 2.n:Z
(n - 1) mod wB = (n mod wB - 1 mod wB) mod wB now rewrite Zminus_mod.
Qed.

Lemma NZ_to_Z_mod : forall n, [| n |] mod wB = [| n |].forall n : t, [|n|] mod wB = [|n|]
Proof.forall n : t, [|n|] mod wB = [|n|]
intro n; rewrite Zmod_small.n:t
[|n|] = [|n|]
n:t
0 <= [|n|] < wB reflexivity.n:t
0 <= [|n|] < wB apply ZnZ.spec_to_Z.
Qed.

Theorem pred_succ : forall n, P (S n) == n.forall n : t, P (S n) == n
Proof.forall n : t, P (S n) == n
intro n.n:t
P (S n) == n zify.n:t
(([|n|] + 1) mod wB - 1) mod wB = [|n|]
rewrite <- pred_mod_wB.n:t
([|n|] + 1 - 1) mod wB = [|n|]
replace ([| n |] + 1 - 1)%Z with [| n |] by ring.n:t
[|n|] mod wB = [|n|] apply NZ_to_Z_mod.
Qed.

Theorem one_succ : one == succ zero.one == S 0
Proof.one == S 0
zify; simpl Z.add.1 = 1 mod wB now rewrite one_mod_wB.
Qed.

Theorem two_succ : two == succ one.two == S one
Proof.two == S one
reflexivity.
Qed.

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).
 (* Below, we use only -> direction *)

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

Lemma B0 : B 0.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
B 0
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
B 0
unfold B.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
A (ZnZ.of_Z 0) apply A0.
Qed.

Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1)
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1)
intros n H1 H2 H3.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB - 1
H3:B n
B (n + 1)
unfold B in *.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB - 1
H3:A (ZnZ.of_Z n)
A (ZnZ.of_Z (n + 1)) apply AS in H3.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB - 1
H3:A (S (ZnZ.of_Z n))
A (ZnZ.of_Z (n + 1))
setoid_replace (ZnZ.of_Z (n + 1)) with (S (ZnZ.of_Z n)).A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB - 1
H3:A (S (ZnZ.of_Z n))
A (S (ZnZ.of_Z n))
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB - 1
H3:A (S (ZnZ.of_Z n))
ZnZ.of_Z (n + 1) == S (ZnZ.of_Z n) assumption.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB - 1
H3:A (S (ZnZ.of_Z n))
ZnZ.of_Z (n + 1) == S (ZnZ.of_Z n)
zify.A:t -> Prop
A_wd:Proper
  ((fun n0 m : t => [|n0|] = [|m|]) ==> iff) A
A0:A ZnZ.zero
AS:forall n0 : t, A n0 <-> A (ZnZ.succ n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB - 1
H3:A (ZnZ.succ (ZnZ.of_Z n))
[|ZnZ.of_Z (n + 1)|] = ([|ZnZ.of_Z n|] + 1) mod wB
rewrite 2 ZnZ.of_Z_correct; auto with zarith.A:t -> Prop
A_wd:Proper
  ((fun n0 m : t => [|n0|] = [|m|]) ==> iff) A
A0:A ZnZ.zero
AS:forall n0 : t, A n0 <-> A (ZnZ.succ n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB - 1
H3:A (ZnZ.succ (ZnZ.of_Z n))
n + 1 = (n + 1) mod wB
symmetry; apply Zmod_small; auto with zarith.
Qed.

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.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
forall (Q : Z -> Prop) (b : Z),
Q 0 ->
(forall n : Z, 0 <= n -> n < b - 1 -> Q n -> Q (n + 1)) ->
forall n : Z, 0 <= n -> n < b -> Q n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
forall (Q : Z -> Prop) (b : Z),
Q 0 ->
(forall n : Z, 0 <= n -> n < b - 1 -> Q n -> Q (n + 1)) ->
forall n : Z, 0 <= n -> n < b -> Q n
intros Q b Q0 QS.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
forall n : Z, 0 <= n -> n < b -> Q n
set (Q' := fun n => (n < b /\ Q n) \/ (b <= n)).A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
forall n : Z, 0 <= n -> n < b -> Q n
assert (H : forall n, 0 <= n -> Q' n).A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
forall n : Z, 0 <= n -> Q' n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:forall n : Z, 0 <= n -> Q' n
forall n : Z, 0 <= n -> n < b -> Q n
apply natlike_rec2; unfold Q'.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
0 < b /\ Q 0 \/ b <= 0
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
forall z : Z,
0 <= z ->
z < b /\ Q z \/ b <= z ->
Z.succ z < b /\ Q (Z.succ z) \/ b <= Z.succ z
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:forall n : Z, 0 <= n -> Q' n
forall n : Z, 0 <= n -> n < b -> Q n
destruct (Z.le_gt_cases b 0) as [H | H].A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:b <= 0
0 < b /\ Q 0 \/ b <= 0
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:0 < b
0 < b /\ Q 0 \/ b <= 0
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
forall z : Z,
0 <= z ->
z < b /\ Q z \/ b <= z ->
Z.succ z < b /\ Q (Z.succ z) \/ b <= Z.succ z
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:forall n : Z, 0 <= n -> Q' n
forall n : Z, 0 <= n -> n < b -> Q n now right.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:0 < b
0 < b /\ Q 0 \/ b <= 0
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
forall z : Z,
0 <= z ->
z < b /\ Q z \/ b <= z ->
Z.succ z < b /\ Q (Z.succ z) \/ b <= Z.succ z
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:forall n : Z, 0 <= n -> Q' n
forall n : Z, 0 <= n -> n < b -> Q n left; now split.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
forall z : Z,
0 <= z ->
z < b /\ Q z \/ b <= z ->
Z.succ z < b /\ Q (Z.succ z) \/ b <= Z.succ z
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:forall n : Z, 0 <= n -> Q' n
forall n : Z, 0 <= n -> n < b -> Q n
intros n H IH.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
n:Z
H:0 <= n
IH:n < b /\ Q n \/ b <= n
Z.succ n < b /\ Q (Z.succ n) \/ b <= Z.succ n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:forall n : Z, 0 <= n -> Q' n
forall n : Z, 0 <= n -> n < b -> Q n destruct IH as [[IH1 IH2] | IH].A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
n:Z
H:0 <= n
IH1:n < b
IH2:Q n
Z.succ n < b /\ Q (Z.succ n) \/ b <= Z.succ n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
n:Z
H:0 <= n
IH:b <= n
Z.succ n < b /\ Q (Z.succ n) \/ b <= Z.succ n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:forall n : Z, 0 <= n -> Q' n
forall n : Z, 0 <= n -> n < b -> Q n
destruct (Z.le_gt_cases (b - 1) n) as [H1 | H1].A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
n:Z
H:0 <= n
IH1:n < b
IH2:Q n
H1:b - 1 <= n
Z.succ n < b /\ Q (Z.succ n) \/ b <= Z.succ n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
n:Z
H:0 <= n
IH1:n < b
IH2:Q n
H1:n < b - 1
Z.succ n < b /\ Q (Z.succ n) \/ b <= Z.succ n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
n:Z
H:0 <= n
IH:b <= n
Z.succ n < b /\ Q (Z.succ n) \/ b <= Z.succ n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:forall n : Z, 0 <= n -> Q' n
forall n : Z, 0 <= n -> n < b -> Q n
right; auto with zarith.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
n:Z
H:0 <= n
IH1:n < b
IH2:Q n
H1:n < b - 1
Z.succ n < b /\ Q (Z.succ n) \/ b <= Z.succ n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
n:Z
H:0 <= n
IH:b <= n
Z.succ n < b /\ Q (Z.succ n) \/ b <= Z.succ n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:forall n : Z, 0 <= n -> Q' n
forall n : Z, 0 <= n -> n < b -> Q n
left.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
n:Z
H:0 <= n
IH1:n < b
IH2:Q n
H1:n < b - 1
Z.succ n < b /\ Q (Z.succ n)
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
n:Z
H:0 <= n
IH:b <= n
Z.succ n < b /\ Q (Z.succ n) \/ b <= Z.succ n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:forall n : Z, 0 <= n -> Q' n
forall n : Z, 0 <= n -> n < b -> Q n split; [auto with zarith | now apply (QS n)].A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
n:Z
H:0 <= n
IH:b <= n
Z.succ n < b /\ Q (Z.succ n) \/ b <= Z.succ n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:forall n : Z, 0 <= n -> Q' n
forall n : Z, 0 <= n -> n < b -> Q n
right; auto with zarith.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n : Z,
0 <= n -> n < b - 1 -> Q n -> Q (n + 1)
Q':=fun n : Z => n < b /\ Q n \/ b <= n:Z -> Prop
H:forall n : Z, 0 <= n -> Q' n
forall n : Z, 0 <= n -> n < b -> Q n
unfold Q' in *; intros n H1 H2.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
H:forall n0 : Z,
0 <= n0 -> n0 < b /\ Q n0 \/ b <= n0
n:Z
H1:0 <= n
H2:n < b
Q n destruct (H n H1) as [[H3 H4] | H3].A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
H:forall n0 : Z,
0 <= n0 -> n0 < b /\ Q n0 \/ b <= n0
n:Z
H1:0 <= n
H2, H3:n < b
H4:Q n
Q n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
H:forall n0 : Z,
0 <= n0 -> n0 < b /\ Q n0 \/ b <= n0
n:Z
H1:0 <= n
H2:n < b
H3:b <= n
Q n
assumption.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
Q:Z -> Prop
b:Z
Q0:Q 0
QS:forall n0 : Z,
0 <= n0 -> n0 < b - 1 -> Q n0 -> Q (n0 + 1)
Q':=fun n0 : Z => n0 < b /\ Q n0 \/ b <= n0:Z -> Prop
H:forall n0 : Z,
0 <= n0 -> n0 < b /\ Q n0 \/ b <= n0
n:Z
H1:0 <= n
H2:n < b
H3:b <= n
Q n now apply Z.le_ngt in H3.
Qed.

Lemma B_holds : forall n : Z, 0 <= n < wB -> B n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
forall n : Z, 0 <= n < wB -> B n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
forall n : Z, 0 <= n < wB -> B n
intros n [H1 H2].A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB
B n
apply Zbounded_induction with wB.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB
B 0
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB
forall n0 : Z,
0 <= n0 -> n0 < wB - 1 -> B n0 -> B (n0 + 1)
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB
0 <= n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB
n < wB
apply B0.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB
forall n0 : Z,
0 <= n0 -> n0 < wB - 1 -> B n0 -> B (n0 + 1)
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB
0 <= n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB
n < wB apply BS.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB
0 <= n
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB
n < wB assumption.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:Z
H1:0 <= n
H2:n < wB
n < wB assumption.
Qed.

Theorem bi_induction : forall n, A n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
forall n : t, A n
Proof.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n : t, A n <-> A (S n)
B:=fun n : Z => A (ZnZ.of_Z n):Z -> Prop
forall n : t, A n
intro n.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:t
A n setoid_replace n with (ZnZ.of_Z (ZnZ.to_Z n)).A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:t
A (ZnZ.of_Z [|n|])
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:t
n == ZnZ.of_Z [|n|]
apply B_holds.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:t
0 <= [|n|] < wB
A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:t
n == ZnZ.of_Z [|n|] apply ZnZ.spec_to_Z.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:t
n == ZnZ.of_Z [|n|]
red.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:t
[|n|] = [|ZnZ.of_Z [|n|]|] symmetry.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:t
[|ZnZ.of_Z [|n|]|] = [|n|] apply ZnZ.of_Z_correct.A:t -> Prop
A_wd:Proper (eq ==> iff) A
A0:A 0
AS:forall n0 : t, A n0 <-> A (S n0)
B:=fun n0 : Z => A (ZnZ.of_Z n0):Z -> Prop
n:t
0 <= [|n|] < wB
apply ZnZ.spec_to_Z.
Qed.

End Induction.

Theorem add_0_l : forall n, 0 + n == n.forall n : t, 0 + n == n
Proof.forall n : t, 0 + n == n
intro n.n:t
0 + n == n zify.n:t
(0 + [|n|]) mod wB = [|n|]
rewrite Z.add_0_l.n:t
[|n|] mod wB = [|n|] apply Zmod_small.n:t
0 <= [|n|] < wB apply ZnZ.spec_to_Z.
Qed.

Theorem add_succ_l : forall n m, (S n) + m == S (n + m).forall n m : t, S n + m == S (n + m)
Proof.forall n m : t, S n + m == S (n + m)
intros n m.n, m:t
S n + m == S (n + m) zify.n, m:t
(([|n|] + 1) mod wB + [|m|]) mod wB =
(([|n|] + [|m|]) mod wB + 1) mod wB
rewrite succ_mod_wB.n, m:t
(([|n|] mod wB + 1) mod wB + [|m|]) mod wB =
(([|n|] + [|m|]) mod wB + 1) mod wB repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0.n, m:t
([|n|] mod wB + 1 + [|m|]) mod wB =
([|n|] + [|m|] + 1) mod wB
rewrite <- (Z.add_assoc ([| n |] mod wB) 1 [| m |]).n, m:t
([|n|] mod wB + (1 + [|m|])) mod wB =
([|n|] + [|m|] + 1) mod wB rewrite Zplus_mod_idemp_l.n, m:t
([|n|] + (1 + [|m|])) mod wB =
([|n|] + [|m|] + 1) mod wB
rewrite (Z.add_comm 1 [| m |]); now rewrite Z.add_assoc.
Qed.

Theorem sub_0_r : forall n, n - 0 == n.forall n : t, n - 0 == n
Proof.forall n : t, n - 0 == n
intro n.n:t
n - 0 == n zify.n:t
([|n|] - 0) mod wB = [|n|] rewrite Z.sub_0_r.n:t
[|n|] mod wB = [|n|] apply NZ_to_Z_mod.
Qed.

Theorem sub_succ_r : forall n m, n - (S m) == P (n - m).forall n m : t, n - S m == P (n - m)
Proof.forall n m : t, n - S m == P (n - m)
intros n m.n, m:t
n - S m == P (n - m) zify.n, m:t
([|n|] - ([|m|] + 1) mod wB) mod wB =
(([|n|] - [|m|]) mod wB - 1) mod wB rewrite Zminus_mod_idemp_r, Zminus_mod_idemp_l.n, m:t
([|n|] - ([|m|] + 1)) mod wB =
([|n|] - [|m|] - 1) mod wB
now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z
     by ring.
Qed.

Theorem mul_0_l : forall n, 0 * n == 0.forall n : t, 0 * n == 0
Proof.forall n : t, 0 * n == 0
intro n.n:t
0 * n == 0 now zify.
Qed.

Theorem mul_succ_l : forall n m, (S n) * m == n * m + m.forall n m : t, S n * m == n * m + m
Proof.forall n m : t, S n * m == n * m + m
intros n m.n, m:t
S n * m == n * m + m zify.n, m:t
(([|n|] + 1) mod wB * [|m|]) mod wB =
(([|n|] * [|m|]) mod wB + [|m|]) mod wB rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l.n, m:t
(([|n|] + 1) * [|m|]) mod wB =
([|n|] * [|m|] + [|m|]) mod wB
now rewrite Z.mul_add_distr_r, Z.mul_1_l.
Qed.

Definition t := t.

End NZCyclicAxiomsMod.