From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 21 May 2012 16:26:30 +0000 Subject: Merge of the newmem branch: - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Iteration.v | 176 ++++++++++++++++++++++++++++++++------------------------ 1 file changed, 102 insertions(+), 74 deletions(-) (limited to 'lib/Iteration.v') diff --git a/lib/Iteration.v b/lib/Iteration.v index 3625845e..235b6502 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -10,65 +10,88 @@ (* *) (* *********************************************************************) -(* Bounded and unbounded iterators *) +(** Bounded and unbounded iterators *) Require Import Axioms. Require Import Coqlib. -Require Import Classical. -Require Import Max. +Require Import Wfsimpl. -Module Type ITER. -Variable iterate - : forall A B : Type, (A -> B + A) -> A -> option B. -Hypothesis iterate_prop - : forall (A B : Type) (step : A -> B + A) (P : A -> Prop) (Q : B -> Prop), - (forall a : A, P a -> - match step a with inl b => Q b | inr a' => P a' end) -> - forall (a : A) (b : B), iterate A B step a = Some b -> P a -> Q b. -End ITER. +(** This modules defines several Coq encodings of a general "while" loop. + The loop is presented in functional style as the iteration + of a [step] function of type [A -> B + A]: +<< + let rec iterate step a = + match step a with + | inl b -> b + | inr a' -> iterate step a' +>> + This iteration cannot be defined directly in Coq using [Fixpoint], + because Coq is a logic of total functions, and therefore we must + guarantee termination of the loop. +*) -Axiom - dependent_description' : - forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop), - (forall x:A, - exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) -> - sigT (fun f : forall x:A, B x => (forall x:A, R x (f x))). +(** * Terminating iteration *) -(* A constructive implementation using bounded iteration. *) +(** We first implement the case where termination is guaranteed because + the current state [a] decreases at each iteration. *) -Module PrimIter: ITER. +Module WfIter. Section ITERATION. Variables A B: Type. Variable step: A -> B + A. +Variable ord: A -> A -> Prop. +Hypothesis ord_wf: well_founded ord. +Hypothesis step_decr: forall a a', step a = inr _ a' -> ord a' a. -(** The [step] parameter represents one step of the iteration. From a - current iteration state [a: A], it either returns a value of type [B], - meaning that iteration is over and that this [B] value is the final - result of the iteration, or a value [a' : A] which is the next state - of the iteration. +Definition step_info (a: A) : {b | step a = inl _ b} + {a' | step a = inr _ a' & ord a' a}. +Proof. + caseEq (step a); intros. left; exists b; auto. right; exists a0; auto. +Qed. - The naive way to define the iteration is: -<< -Fixpoint iterate (a: A) : B := - match step a with - | inl b => b - | inr a' => iterate a' +Definition iterate_F (a: A) (rec: forall a', ord a' a -> B) : B := + match step_info a with + | inl (exist b P) => b + | inr (exist2 a' P Q) => rec a' Q end. ->> - However, this is a general recursion, not guaranteed to terminate, - and therefore not expressible in Coq. The standard way to work around - this difficulty is to use Noetherian recursion (Coq module [Wf]). - This requires that we equip the type [A] with a well-founded ordering [<] - (no infinite ascending chains) and we demand that [step] satisfies - [step a = inr a' -> a < a']. For the types [A] that are of interest to us - in this development, it is however very painful to define adequate - well-founded orderings, even though we know our iterations always - terminate. - - Instead, we choose to bound the number of iterations by an arbitrary - constant. [iterate] then becomes a function that can fail, + +Definition iterate (a: A) : B := Fix ord_wf iterate_F a. + +(** We now prove an invariance property [iterate_prop], similar to the Hoare + logic rule for "while" loops. *) + +Variable P: A -> Prop. +Variable Q: B -> Prop. + +Hypothesis step_prop: + forall a : A, P a -> + match step a with inl b => Q b | inr a' => P a' end. + +Lemma iterate_prop: + forall a, P a -> Q (iterate a). +Proof. + intros a0. pattern a0. apply well_founded_ind with (R := ord). auto. + intros. unfold iterate; rewrite unroll_Fix. unfold iterate_F. + destruct (step_info x) as [[b U] | [a' U V]]. + exploit step_prop; eauto. rewrite U; auto. + apply H. auto. exploit step_prop; eauto. rewrite U; auto. +Qed. + +End ITERATION. + +End WfIter. + +(** * Bounded iteration *) + +(** The presentation of iteration shown above is predicated on the existence + of a well-founded ordering that decreases at each step of the iteration. + In several parts of the CompCert development, it is very painful to define + such a well-founded ordering and to prove decrease, even though we know our + iterations always terminate. + + In the presentation below, we choose instead to bound the number of iterations + by an arbitrary constant. [iterate] then becomes a function that can fail, of type [A -> option B]. The [None] result denotes failure to reach a result in the number of iterations prescribed, or, in other terms, failure to find a solution to the dataflow problem. The compiler @@ -82,6 +105,13 @@ Fixpoint iterate (a: A) : B := course our proofs also cover the failure case and show that nothing bad happens in this hypothetical case either. *) +Module PrimIter. + +Section ITERATION. + +Variables A B: Type. +Variable step: A -> B + A. + Definition num_iterations := 1000000000000%positive. (** The simple definition of bounded iteration is: @@ -117,19 +147,7 @@ Definition iter_step (x: positive) 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. - 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. +Definition iter: positive -> A -> option B := Fix Plt_wf iter_step. (** The [iterate] function is defined as [iter] up to [num_iterations] through the loop. *) @@ -150,11 +168,12 @@ Lemma iter_prop: Proof. 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. + intros. unfold iter in H1. rewrite unroll_Fix in H1. unfold iter_step in H1. + destruct (peq x 1). discriminate. + specialize (step_prop a H0). + destruct (step a) as [b'|a']_eqn. + inv H1. auto. + apply H with (Ppred x) a'. apply Ppred_Plt; auto. auto. auto. Qed. Lemma iterate_prop: @@ -167,11 +186,21 @@ End ITERATION. End PrimIter. +(** * General iteration *) + (* An implementation using classical logic and unbounded iteration, in the style of Yves Bertot's paper, "Extending the Calculus - of Constructions with Tarski's fix-point theorem". *) + of Constructions with Tarski's fix-point theorem". -Module GenIter: ITER. + As in the bounded case, the [iterate] function returns an option type. + [None] means that iteration does not terminate. + [Some b] means that iteration terminates with the result [b]. *) + +Require Import Classical. +Require Import ClassicalDescription. +Require Import Max. + +Module GenIter. Section ITERATION. @@ -249,30 +278,29 @@ Proof. Qed. Lemma converges_to_exists_uniquely: - forall a, exists b, converges_to a b /\ forall b', converges_to a b' -> b = b'. + forall a, exists! b, converges_to a b . Proof. intro. destruct (converges_to_exists a) as [b CT]. exists b. split. assumption. exact (converges_to_unique _ _ CT). Qed. -Definition exists_iterate := - dependent_description' A (fun _ => option B) - converges_to converges_to_exists_uniquely. - -Definition iterate : A -> option B := - match exists_iterate with existT f P => f end. +Definition iterate (a: A) : option B := + proj1_sig (constructive_definite_description (converges_to a) (converges_to_exists_uniquely a)). Lemma converges_to_iterate: forall a b, converges_to a b -> iterate a = b. Proof. - intros. unfold iterate. destruct exists_iterate as [f P]. - apply converges_to_unique with a. apply P. auto. + intros. unfold iterate. + destruct (constructive_definite_description (converges_to a) (converges_to_exists_uniquely a)) as [b' P]. + simpl. apply converges_to_unique with a; auto. Qed. Lemma iterate_converges_to: forall a, converges_to a (iterate a). Proof. - intros. unfold iterate. destruct exists_iterate as [f P]. apply P. + intros. unfold iterate. + destruct (constructive_definite_description (converges_to a) (converges_to_exists_uniquely a)) as [b' P]. + simpl; auto. Qed. (** Invariance property. *) -- cgit