aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Lists/StreamMemo.v (renamed from theories/Ints/num/MemoFn.v)98
-rw-r--r--theories/Numbers/BigNumPrelude.v (renamed from theories/Ints/Zaux.v)0
-rw-r--r--theories/Numbers/Cyclic/Abstract/ZnZ.v (renamed from theories/Ints/num/ZnZ.v)2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v (renamed from theories/Ints/Basic_type.v)0
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v (renamed from theories/Ints/num/GenAdd.v)2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/GenBase.v (renamed from theories/Ints/num/GenBase.v)4
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v (renamed from theories/Ints/num/GenDiv.v)2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v (renamed from theories/Ints/num/GenDivn1.v)2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/GenLift.v (renamed from theories/Ints/num/GenLift.v)2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/GenMul.v (renamed from theories/Ints/num/GenMul.v)2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v (renamed from theories/Ints/num/GenSqrt.v)2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/GenSub.v (renamed from theories/Ints/num/GenSub.v)2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v (renamed from theories/Ints/num/Zn2Z.v)2
-rw-r--r--theories/Numbers/Cyclic/Int31/Int31.v (renamed from theories/Ints/Int31.v)0
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v (renamed from theories/Ints/BigZ.v)0
-rw-r--r--theories/Numbers/Integer/BigZ/ZMake.v (renamed from theories/Ints/num/ZMake.v)2
-rw-r--r--theories/Numbers/Integer/TreeMod/ZTreeMod.v4
-rw-r--r--theories/Numbers/Natural/BigN/BigN.v (renamed from theories/Ints/BigN.v)0
-rw-r--r--theories/Numbers/Natural/BigN/NMake.v (renamed from theories/Ints/num/NMake.v)4
-rw-r--r--theories/Numbers/Natural/BigN/Nbasic.v (renamed from theories/Ints/num/Nbasic.v)2
-rw-r--r--theories/Numbers/Natural/BigN/genN.ml (renamed from theories/Ints/num/genN.ml)0
-rw-r--r--theories/Numbers/Rational/BigQ/BigQ.v (renamed from theories/Ints/num/BigQ.v)0
-rw-r--r--theories/Numbers/Rational/BigQ/Q0Make.v (renamed from theories/Ints/num/Q0Make.v)2
-rw-r--r--theories/Numbers/Rational/BigQ/QMake_base.v (renamed from theories/Ints/num/QMake_base.v)2
-rw-r--r--theories/Numbers/Rational/BigQ/QbiMake.v (renamed from theories/Ints/num/QbiMake.v)2
-rw-r--r--theories/Numbers/Rational/BigQ/QifMake.v (renamed from theories/Ints/num/QifMake.v)2
-rw-r--r--theories/Numbers/Rational/BigQ/QpMake.v (renamed from theories/Ints/num/QpMake.v)2
-rw-r--r--theories/Numbers/Rational/BigQ/QvMake.v (renamed from theories/Ints/num/QvMake.v)2
28 files changed, 82 insertions, 62 deletions
diff --git a/theories/Ints/num/MemoFn.v b/theories/Lists/StreamMemo.v
index 7d2c7af01..bdbe0eccc 100644
--- a/theories/Ints/num/MemoFn.v
+++ b/theories/Lists/StreamMemo.v
@@ -7,32 +7,27 @@
(************************************************************************)
Require Import Eqdep_dec.
+Require Import Streams.
+
+(** * Memoization *)
+
+(** Successive outputs of a given function [f] are stored in
+ a stream in order to avoid duplicated computations. *)
Section MemoFunction.
Variable A: Type.
Variable f: nat -> A.
-Variable g: A -> A.
-
-Hypothesis Hg_correct: forall n, f (S n) = g (f n).
-
-(* Memo Stream *)
-CoInductive MStream: Type :=
- MSeq : A -> MStream -> MStream.
-(* Hd and Tl function *)
-Definition mhd (x: MStream) :=
- let (a,s) := x in a.
-Definition mtl (x: MStream) :=
- let (a,s) := x in s.
-
-CoFixpoint memo_make (n: nat): MStream:= MSeq (f n) (memo_make (S n)).
+CoFixpoint memo_make (n:nat) : Stream A := Cons (f n) (memo_make (S n)).
Definition memo_list := memo_make 0.
-Fixpoint memo_get (n: nat) (l: MStream) {struct n}: A :=
- match n with O => mhd l | S n1 =>
- memo_get n1 (mtl l) end.
+Fixpoint memo_get (n:nat) (l:Stream A) : A :=
+ match n with
+ | O => hd l
+ | S n1 => memo_get n1 (tl l)
+ end.
Theorem memo_get_correct: forall n, memo_get n memo_list = f n.
Proof.
@@ -44,13 +39,21 @@ intros n; apply trans_equal with (f (n + 0)); try exact (F1 n 0).
rewrite <- plus_n_O; auto.
Qed.
-(* Building with possible sharing using g *)
-CoFixpoint imemo_make (fn: A): MStream :=
+(** Building with possible sharing using a iterator [g] :
+ We now suppose in addition that [f n] is in fact the [n]-th
+ iterate of a function [g].
+*)
+
+Variable g: A -> A.
+
+Hypothesis Hg_correct: forall n, f (S n) = g (f n).
+
+CoFixpoint imemo_make (fn:A) : Stream A :=
let fn1 := g fn in
- MSeq fn1 (imemo_make fn1).
+ Cons fn1 (imemo_make fn1).
Definition imemo_list := let f0 := f 0 in
- MSeq f0 (imemo_make f0).
+ Cons f0 (imemo_make f0).
Theorem imemo_get_correct: forall n, memo_get n imemo_list = f n.
Proof.
@@ -65,13 +68,14 @@ Qed.
End MemoFunction.
+(** For a dependent function, the previous solution is
+ reused thanks to a temporarly hiding of the dependency
+ in a "container" [memo_val]. *)
+
Section DependentMemoFunction.
Variable A: nat -> Type.
Variable f: forall n, A n.
-Variable g: forall n, A n -> A (S n).
-
-Hypothesis Hg_correct: forall n, f (S n) = g n (f n).
Inductive memo_val: Type :=
memo_mval: forall n, A n -> memo_val.
@@ -101,16 +105,11 @@ match v with
end.
Let mf n := memo_mval n (f n).
-Let mg v := match v with
- memo_mval n1 v1 => memo_mval (S n1) (g n1 v1) end.
-
Definition dmemo_list := memo_list _ mf.
Definition dmemo_get n l := memo_get_val n (memo_get _ n l).
-Definition dimemo_list := imemo_list _ mf mg.
-
Theorem dmemo_get_correct: forall n, dmemo_get n dmemo_list = f n.
Proof.
intros n; unfold dmemo_get, dmemo_list.
@@ -129,6 +128,17 @@ assert (e = refl_equal n).
rewrite H; auto.
Qed.
+(** Finally, a version with both dependency and iterator *)
+
+Variable g: forall n, A n -> A (S n).
+
+Hypothesis Hg_correct: forall n, f (S n) = g n (f n).
+
+Let mg v := match v with
+ memo_mval n1 v1 => memo_mval (S n1) (g n1 v1) end.
+
+Definition dimemo_list := imemo_list _ mf mg.
+
Theorem dimemo_get_correct: forall n, dmemo_get n dimemo_list = f n.
Proof.
intros n; unfold dmemo_get, dimemo_list.
@@ -150,17 +160,20 @@ Qed.
End DependentMemoFunction.
-(* An example with the memo function on factorial *)
+(** An example with the memo function on factorial *)
(*
Require Import ZArith.
+Open Scope Z_scope.
-Fixpoint tfact (n: nat) {struct n} :=
- match n with O => 1%Z |
- S n1 => (Z_of_nat n * tfact n1)%Z end.
+Fixpoint tfact (n: nat) :=
+ match n with
+ | O => 1
+ | S n1 => Z_of_nat n * tfact n1
+ end.
Definition lfact_list :=
- dimemo_list _ tfact (fun n z => (Z_of_nat (S n) * z)%Z).
+ dimemo_list _ tfact (fun n z => (Z_of_nat (S n) * z)).
Definition lfact n := dmemo_get _ tfact n lfact_list.
@@ -170,16 +183,23 @@ intros n; unfold lfact, lfact_list.
rewrite dimemo_get_correct; auto.
Qed.
-Fixpoint nop p := match p with
-xH => 0 | xI p1 => nop p1 | xO p1 => nop p1 end.
+Fixpoint nop p :=
+ match p with
+ | xH => 0
+ | xI p1 => nop p1
+ | xO p1 => nop p1
+ end.
-Fixpoint test z := match z with
-Z0 => 0 | Zpos p1 => nop p1 | Zneg p1 => nop p1 end.
+Fixpoint test z :=
+ match z with
+ | Z0 => 0
+ | Zpos p1 => nop p1
+ | Zneg p1 => nop p1
+ end.
Time Eval vm_compute in test (lfact 2000).
Time Eval vm_compute in test (lfact 2000).
Time Eval vm_compute in test (lfact 1500).
Time Eval vm_compute in (lfact 1500).
-
*)
diff --git a/theories/Ints/Zaux.v b/theories/Numbers/BigNumPrelude.v
index 8e4b1d64f..8e4b1d64f 100644
--- a/theories/Ints/Zaux.v
+++ b/theories/Numbers/BigNumPrelude.v
diff --git a/theories/Ints/num/ZnZ.v b/theories/Numbers/Cyclic/Abstract/ZnZ.v
index d5b798a18..dfe091209 100644
--- a/theories/Ints/num/ZnZ.v
+++ b/theories/Numbers/Cyclic/Abstract/ZnZ.v
@@ -8,7 +8,7 @@
(* Benjamin Gregoire, INRIA Laurent Thery, INRIA *)
(************************************************************************)
-(* $Id:$ *)
+(* $Id$ *)
(** * Signature and specification of a bounded integer structure *)
diff --git a/theories/Ints/Basic_type.v b/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v
index 2116aaddd..2116aaddd 100644
--- a/theories/Ints/Basic_type.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v
diff --git a/theories/Ints/num/GenAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v
index fae16aad6..889ccaa4d 100644
--- a/theories/Ints/num/GenAdd.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v
@@ -16,7 +16,7 @@
Set Implicit Arguments.
Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Basic_type.
Require Import GenBase.
diff --git a/theories/Ints/num/GenBase.v b/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v
index e93e3a489..2283e3ca0 100644
--- a/theories/Ints/num/GenBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id:$ *)
+(* $Id$ *)
(** * *)
@@ -20,7 +20,7 @@
Set Implicit Arguments.
Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Basic_type.
Require Import JMeq.
diff --git a/theories/Ints/num/GenDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v
index ea6868a90..0e9993b10 100644
--- a/theories/Ints/num/GenDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v
@@ -9,7 +9,7 @@
Set Implicit Arguments.
Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Basic_type.
Require Import GenBase.
Require Import GenDivn1.
diff --git a/theories/Ints/num/GenDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v
index 3c70adb61..a686f0c27 100644
--- a/theories/Ints/num/GenDivn1.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v
@@ -9,7 +9,7 @@
Set Implicit Arguments.
Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Basic_type.
Require Import GenBase.
diff --git a/theories/Ints/num/GenLift.v b/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v
index f74cdc30b..5f8b00a52 100644
--- a/theories/Ints/num/GenLift.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v
@@ -9,7 +9,7 @@
Set Implicit Arguments.
Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Basic_type.
Require Import GenBase.
diff --git a/theories/Ints/num/GenMul.v b/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v
index 9a56f1ee3..57cdeeb88 100644
--- a/theories/Ints/num/GenMul.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v
@@ -9,7 +9,7 @@
Set Implicit Arguments.
Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Basic_type.
Require Import GenBase.
diff --git a/theories/Ints/num/GenSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v
index 63a0930ed..f8cb16858 100644
--- a/theories/Ints/num/GenSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v
@@ -9,7 +9,7 @@
Set Implicit Arguments.
Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Basic_type.
Require Import GenBase.
diff --git a/theories/Ints/num/GenSub.v b/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v
index 6ffb24575..b96d09562 100644
--- a/theories/Ints/num/GenSub.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v
@@ -9,7 +9,7 @@
Set Implicit Arguments.
Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Basic_type.
Require Import GenBase.
diff --git a/theories/Ints/num/Zn2Z.v b/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v
index 48cf26840..9b77cf039 100644
--- a/theories/Ints/num/Zn2Z.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v
@@ -9,7 +9,7 @@
Set Implicit Arguments.
Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Basic_type.
Require Import GenBase.
Require Import GenAdd.
diff --git a/theories/Ints/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index d7e80d4a2..d7e80d4a2 100644
--- a/theories/Ints/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
diff --git a/theories/Ints/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 8c7c1f809..8c7c1f809 100644
--- a/theories/Ints/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
diff --git a/theories/Ints/num/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 75fc19584..da65d276f 100644
--- a/theories/Ints/num/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -7,7 +7,7 @@
(************************************************************************)
Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
Open Scope Z_scope.
diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
index f81c71d72..2bb9bec4b 100644
--- a/theories/Numbers/Integer/TreeMod/ZTreeMod.v
+++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v
@@ -8,13 +8,13 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id:$ i*)
+(*i $Id$ i*)
Require Export NZAxioms.
Require Import NMake. (* contains W0Type *)
Require Import ZnZ.
Require Import Basic_type. (* contains base *)
-Require Import Zaux.
+Require Import BigNumPrelude.
Module NZBigIntsAxiomsMod (Import BoundedIntsMod : W0Type) <: NZAxiomsSig.
diff --git a/theories/Ints/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index b64a853fd..b64a853fd 100644
--- a/theories/Ints/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
diff --git a/theories/Ints/num/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 8cb779350..6705c1898 100644
--- a/theories/Ints/num/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -17,7 +17,7 @@
- Remark: File automatically generated
*)
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import ZArith.
Require Import Basic_type.
Require Import ZnZ.
@@ -26,7 +26,7 @@ Require Import Nbasic.
Require Import GenMul.
Require Import GenDivn1.
Require Import Wf_nat.
-Require Import MemoFn.
+Require Import StreamMemo.
Module Type W0Type.
Parameter w : Set.
diff --git a/theories/Ints/num/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 1398e8f55..3d20c35ce 100644
--- a/theories/Ints/num/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -7,7 +7,7 @@
(************************************************************************)
Require Import ZArith.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Basic_type.
Require Import Max.
Require Import GenBase.
diff --git a/theories/Ints/num/genN.ml b/theories/Numbers/Natural/BigN/genN.ml
index 8bf583ab6..8bf583ab6 100644
--- a/theories/Ints/num/genN.ml
+++ b/theories/Numbers/Natural/BigN/genN.ml
diff --git a/theories/Ints/num/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 33e5f669c..33e5f669c 100644
--- a/theories/Ints/num/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
diff --git a/theories/Ints/num/Q0Make.v b/theories/Numbers/Rational/BigQ/Q0Make.v
index d5809ea59..e075bdb15 100644
--- a/theories/Ints/num/Q0Make.v
+++ b/theories/Numbers/Rational/BigQ/Q0Make.v
@@ -9,7 +9,7 @@
Require Import Bool.
Require Import ZArith.
Require Import Znumtheory.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Arith.
Require Export BigN.
Require Export BigZ.
diff --git a/theories/Ints/num/QMake_base.v b/theories/Numbers/Rational/BigQ/QMake_base.v
index 0cd2d2122..e12c78581 100644
--- a/theories/Ints/num/QMake_base.v
+++ b/theories/Numbers/Rational/BigQ/QMake_base.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id:$ *)
+(* $Id$ *)
(** * An implementation of rational numbers based on big integers *)
diff --git a/theories/Ints/num/QbiMake.v b/theories/Numbers/Rational/BigQ/QbiMake.v
index a98fda9d7..8420a5360 100644
--- a/theories/Ints/num/QbiMake.v
+++ b/theories/Numbers/Rational/BigQ/QbiMake.v
@@ -9,7 +9,7 @@
Require Import Bool.
Require Import ZArith.
Require Import Znumtheory.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Arith.
Require Export BigN.
Require Export BigZ.
diff --git a/theories/Ints/num/QifMake.v b/theories/Numbers/Rational/BigQ/QifMake.v
index 83c182ee0..6df06bdf2 100644
--- a/theories/Ints/num/QifMake.v
+++ b/theories/Numbers/Rational/BigQ/QifMake.v
@@ -9,7 +9,7 @@
Require Import Bool.
Require Import ZArith.
Require Import Znumtheory.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Arith.
Require Export BigN.
Require Export BigZ.
diff --git a/theories/Ints/num/QpMake.v b/theories/Numbers/Rational/BigQ/QpMake.v
index a28434baf..a194431ec 100644
--- a/theories/Ints/num/QpMake.v
+++ b/theories/Numbers/Rational/BigQ/QpMake.v
@@ -9,7 +9,7 @@
Require Import Bool.
Require Import ZArith.
Require Import Znumtheory.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Arith.
Require Export BigN.
Require Export BigZ.
diff --git a/theories/Ints/num/QvMake.v b/theories/Numbers/Rational/BigQ/QvMake.v
index 85655dafc..1282c8694 100644
--- a/theories/Ints/num/QvMake.v
+++ b/theories/Numbers/Rational/BigQ/QvMake.v
@@ -9,7 +9,7 @@
Require Import Bool.
Require Import ZArith.
Require Import Znumtheory.
-Require Import Zaux.
+Require Import BigNumPrelude.
Require Import Arith.
Require Export BigN.
Require Export BigZ.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 03:29:08 +0000