diff options
Diffstat (limited to 'lib/Iteration.v')
-rw-r--r-- | lib/Iteration.v | 64 |
1 files changed, 51 insertions, 13 deletions
diff --git a/lib/Iteration.v b/lib/Iteration.v index 3c4b5998..85c5ded8 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -1,6 +1,5 @@ (* Bounded and unbounded iterators *) -Require Recdef. Require Import Coqlib. Require Import Classical. Require Import Max. @@ -72,15 +71,51 @@ Fixpoint iterate (a: A) : B := Definition num_iterations := 1000000000000%positive. -Function iter (niter: positive) (s: A) {wf Plt niter} : option B := - if peq niter xH then None else - match step s with - | inl res => Some res - | inr s' => iter (Ppred niter) s' - end. +(** The simple definition of bounded iteration is: +<< +Fixpoint iterate (niter: nat) (a: A) {struct niter} : option B := + match niter with + | O => None + | S niter' => + match step a with + | inl b => b + | inr a' => iterate niter' a' + end + end. +>> + This function is structural recursive over the parameter [niter] + (number of iterations), represented here as a Peano integer (type [nat]). + However, we want to use very large values of [niter]. As Peano integers, + these values would be much too large to fit in memory. Therefore, + we must express iteration counts as a binary integer (type [positive]). + However, Peano induction over type [positive] is not structural recursion, + so we cannot define [iterate] as a Coq fixpoint and must use + Noetherian recursion instead. *) + +Definition iter_step (x: positive) + (next: forall y, Plt y x -> A -> option B) + (s: A) : option B := + match peq x xH with + | left EQ => None + | right NOTEQ => + match step s with + | inl res => Some res + | inr s' => next (Ppred x) (Ppred_Plt x NOTEQ) s' + end + end. + +Definition iter: positive -> A -> option B := + Fix Plt_wf (fun _ => A -> option B) iter_step. + +(** We then prove the expected unrolling equations for [iter]. *) + +Remark unroll_iter: + forall x, iter x = iter_step x (fun y _ => iter y). Proof. - intros. apply Ppred_Plt. auto. - apply Plt_wf. + unfold iter; apply (Fix_eq Plt_wf (fun _ => A -> option B) iter_step). + intros. unfold iter_step. apply extensionality. intro s. + case (peq x xH); intro. auto. + rewrite H. auto. Qed. (** The [iterate] function is defined as [iter] up to @@ -100,10 +135,13 @@ Hypothesis step_prop: Lemma iter_prop: forall n a b, P a -> iter n a = Some b -> Q b. Proof. - intros n a. functional induction (iter n a); intros. - discriminate. - inversion H0; subst b. generalize (step_prop s H). rewrite e0. auto. - apply IHo. generalize (step_prop s H). rewrite e0. auto. auto. + apply (well_founded_ind Plt_wf + (fun p => forall a b, P a -> iter p a = Some b -> Q b)). + intros until b. intro. rewrite unroll_iter. + unfold iter_step. case (peq x 1); intro. congruence. + generalize (step_prop a H0). + case (step a); intros. congruence. + apply H with (Ppred x) a0. apply Ppred_Plt; auto. auto. auto. Qed. Lemma iterate_prop: |