summaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic/Abstract
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract')
-rw-r--r--theories/Numbers/Cyclic/Abstract/CyclicAxioms.v12
-rw-r--r--theories/Numbers/Cyclic/Abstract/DoubleType.v71
-rw-r--r--theories/Numbers/Cyclic/Abstract/NZCyclic.v33
3 files changed, 106 insertions, 10 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 3312161a..951a4ef2 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * 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 *)
+(* // * 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) *)
(************************************************************************)
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
@@ -17,7 +19,7 @@ Set Implicit Arguments.
Require Import ZArith.
Require Import Znumtheory.
-Require Import BigNumPrelude.
+Require Import Zpow_facts.
Require Import DoubleType.
Local Open Scope Z_scope.
diff --git a/theories/Numbers/Cyclic/Abstract/DoubleType.v b/theories/Numbers/Cyclic/Abstract/DoubleType.v
new file mode 100644
index 00000000..fe0476e4
--- /dev/null
+++ b/theories/Numbers/Cyclic/Abstract/DoubleType.v
@@ -0,0 +1,71 @@
+(************************************************************************)
+(* * 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) *)
+(************************************************************************)
+(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
+(************************************************************************)
+
+Set Implicit Arguments.
+
+Require Import ZArith.
+Local Open Scope Z_scope.
+
+Definition base digits := Z.pow 2 (Zpos digits).
+Arguments base digits: simpl never.
+
+Section Carry.
+
+ Variable A : Type.
+
+ Inductive carry :=
+ | C0 : A -> carry
+ | C1 : A -> carry.
+
+ Definition interp_carry (sign:Z)(B:Z)(interp:A -> Z) c :=
+ match c with
+ | C0 x => interp x
+ | C1 x => sign*B + interp x
+ end.
+
+End Carry.
+
+Section Zn2Z.
+
+ Variable znz : Type.
+
+ (** From a type [znz] representing a cyclic structure Z/nZ,
+ we produce a representation of Z/2nZ by pairs of elements of [znz]
+ (plus a special case for zero). High half of the new number comes
+ first.
+ *)
+
+ Inductive zn2z :=
+ | W0 : zn2z
+ | WW : znz -> znz -> zn2z.
+
+ Definition zn2z_to_Z (wB:Z) (w_to_Z:znz->Z) (x:zn2z) :=
+ match x with
+ | W0 => 0
+ | WW xh xl => w_to_Z xh * wB + w_to_Z xl
+ end.
+
+End Zn2Z.
+
+Arguments W0 {znz}.
+
+(** From a cyclic representation [w], we iterate the [zn2z] construct
+ [n] times, gaining the type of binary trees of depth at most [n],
+ whose leafs are either W0 (if depth < n) or elements of w
+ (if depth = n).
+*)
+
+Fixpoint word (w:Type) (n:nat) : Type :=
+ match n with
+ | O => w
+ | S n => zn2z (word w n)
+ end.
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index df9b8339..64935ffe 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -1,15 +1,18 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * 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 *)
+(* // * 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 BigNumPrelude.
+Require Import ZArith.
+Require Import Zpow_facts.
Require Import DoubleType.
Require Import CyclicAxioms.
@@ -139,6 +142,26 @@ rewrite 2 ZnZ.of_Z_correct; auto with zarith.
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.
+Proof.
+intros Q b Q0 QS.
+set (Q' := fun n => (n < b /\ Q n) \/ (b <= n)).
+assert (H : forall n, 0 <= n -> Q' n).
+apply natlike_rec2; unfold Q'.
+destruct (Z.le_gt_cases b 0) as [H | H]. now right. left; now split.
+intros n H IH. destruct IH as [[IH1 IH2] | IH].
+destruct (Z.le_gt_cases (b - 1) n) as [H1 | H1].
+right; auto with zarith.
+left. split; [auto with zarith | now apply (QS n)].
+right; auto with zarith.
+unfold Q' in *; intros n H1 H2. destruct (H n H1) as [[H3 H4] | H3].
+assumption. now apply Z.le_ngt in H3.
+Qed.
+
Lemma B_holds : forall n : Z, 0 <= n < wB -> B n.
Proof.
intros n [H1 H2].
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 11:29:38 +0000