Set Implicit Arguments. Require Export LibInt CFApp CFPrint. (********************************************************************) (********************************************************************) (********************************************************************) (********************************************************************) (* DEPRECATED (*-- version very old *) Notation "'While' Q1 'Do' Q2 '_Done'" := (!While (fun H Q => forall R:~~unit, is_local R -> (forall H Q, (If_ Q1 Then (Q2 ;; R) Else (Ret tt)) H Q -> R H Q) -> R H Q)) (at level 69, Q2 at level 68, only parsing) : charac. Lemma while_loop_cf_to_inv' : forall (A:Type) (I:A->hprop) (J:A->bool->hprop) (lt:binary A), forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop), wf lt -> (exists X0, H ==> (I X0)) -> (forall X, F1 (I X) (J X) /\ F2 (J X true) (# Hexists Y, (I Y) \* \[lt Y X]) /\ J X false ==> Q tt) -> (While F1 Do F2 _Done) H Q. Proof. introv W (X0&I0) M. apply local_erase. introv LR HR. applys* local_weaken (rm I0). gen X0. intros X. induction_wf IH: W X. destruct (M X) as (M1&M2&M3). applys HR. xlet*. xif. xseq*. xextract as Y L. xapply* IH; hsimpl. xret_no_gc~. Qed. Lemma while_loop_cf_to_inv : forall (A:Type) (I:A->hprop) (B:A->bool->Prop) (lt:binary A) (W:wf lt), forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop), (exists X0, H ==> (I X0)) -> (forall X, F1 (I X) (fun b => \[B X b] \* I X) /\ F2 (\[B X true] \* I X) (# Hexists Y, (I Y) \* \[lt Y X]) /\ \[B X false] \* I X ==> Q tt) -> (While F1 Do F2 _Done) H Q. Proof. intros. eapply while_loop_cf_to_inv' with (J:= fun X b => \[B X b] \* I X); eauto. Qed. Ltac xwhile_inv_core W I B := match type of W with | wf _ => eapply (@while_loop_cf_to_inv _ I B _ W) | _ -> nat => eapply (@while_loop_cf_to_inv _ I B (measure W)); [ try prove_wf | | ] | _ => eapply (@while_loop_cf_to_inv _ I B W); [ try prove_wf | | ] end. Tactic Notation "xwhile_inv" constr(W) constr(I) constr(B) := xwhile_pre ltac:(fun _ => xwhile_inv_core W I B). Tactic Notation "xwhile_inv_body" := apply local_erase; esplit; splits (3%nat). (*-- version old *) (** [xwhile_inv I] proves a while loop using an invariant of the form [fun b m => H], where [b] is a boolean value that describes whether the loop condition returns true, and where [m] is an integer whose value should decrease towards zero at every iteration. *) Lemma while_loop_cf_inv_measure : forall (I:bool->int->hprop), forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop), (exists b m, H ==> I b m) -> (forall b m, F1 (I b m) (fun b' => Hexists m', I b' m')) -> (forall m, F2 (I true m) (# Hexists b m', \[0 <= m' < m] \* I b m')) -> (forall m, I false m ==> Q tt \* Hexists H', H') -> (While F1 Do F2 _Done) H Q. (* TODO: see cf spec *) Ltac xwhile_inv_measure_core I := apply (@while_loop_cf_inv_measure I). Tactic Notation "xwhile_inv" constr(I) := xwhile_pre ltac:(fun _ => xwhile_inv_measure_core I). (*--version was in this file *) Definition while_loop_cf (F1:~~bool) (F2:~~unit) := local (fun (H:hprop) (Q:unit->hprop) => forall R:~~unit, is_local R -> (forall H Q, (exists Q', F1 H Q' /\ (local (fun H Q => exists Q', F2 H Q' /\ R (Q' tt) Q) (Q' true) Q) /\ Q' false ==> Q tt) -> R H Q) -> R H Q). Definition while_loop_inv (F1:~~bool) (F2:~~unit) := local (fun (H:hprop) (Q:unit->hprop) => exists (A:Type) (I:A->hprop) (J:A->bool->hprop) (lt:binary A), wf lt /\ (exists X0, H ==> (I X0)) /\ (forall X, F1 (I X) (J X) /\ F2 (J X true) (# Hexists Y, (I Y) \* \[lt Y X]) /\ J X false ==> Q tt)). Lemma while_loop_cf_to_inv : forall (F1:~~bool) (F2:~~unit), while_loop_inv F1 F2 ===> while_loop_cf F1 F2. Proof using. intros. apply local_weaken_body. intros H Q (A&I&J<&W&(X0&I0)&M). introv LR HR. applys* local_weaken I0. clear I0. gen X0. intros X. induction_wf IH: W X. destruct (M X) as (M1&M2&M3). applys HR. exists (J X). splits~. apply local_erase. esplit. split. apply M2. applys local_extract_exists; autos~. intros x. rewrite star_comm. apply~ local_intro_prop. Qed. Lemma while_loop_cf_inv_measure : forall (I:bool->int->hprop), forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop), (exists b m, H ==> I b m) -> (forall b m, F1 (I b m) (fun b' => I b' m)) -> (forall m, F2 (I true m) (# Hexists b m', \[0 <= m' < m] \* I b m')) -> (forall m, I false m ==> Q tt \* Hexists H', H') -> while_loop_cf F1 F2 H Q. Proof using. introv (bi&mi&Hi) Hc Hs He. applys~ local_weaken_gc (I bi mi). xlocal. clear Hi. apply local_erase. introv LR HR. gen bi. induction_wf IH: (int_downto_wf 0) mi. intros. applys (rm HR). esplit. splits. applys Hc. simpl. apply local_erase. esplit. split. applys Hs. simpl. eapply local_extract_exists. xlocal. intros b. eapply local_extract_exists. xlocal. intros m'. eapply local_intro_prop with (F:=R). auto. intros E. applys IH. applys E. simpl. applys He. Qed. Definition for_loop_cf (a:int) (b:int) (F:~~unit) := local (fun (H:hprop) (Q:unit->hprop) => forall S:int->~~unit, is_local_pred S -> (forall i H Q, ((i <= (b)%Z -> (local (fun H Q => exists Q', F H Q' /\ S (i+1) (Q' tt) Q) H Q)) /\ (i > b%Z -> H ==> Q tt)) -> S i H Q) -> S a H Q). Definition for_loop_inv (a:int) (b:int) (F:~~unit) := local (fun (H:hprop) (Q:unit->hprop) => (a > (b)%Z -> H ==> (Q tt)) /\ (a <= (b)%Z -> exists H', exists I, (H ==> I a \* H') /\ (forall i, a <= i /\ i <= (b)%Z -> F (I i) (# I(i+1))) /\ (I ((b)%Z+1) \* H' ==> Q tt))). Lemma for_loop_cf_to_inv : forall (a:int) (b:int) (F:~~unit), for_loop_inv a b F ===> for_loop_cf a b F. Proof using. intros. apply local_weaken_body. intros H Q (Mgt&Mle). introv LS HS. tests C: (a > b). apply HS. split. math. auto. clear Mgt. specializes Mle. math. destruct Mle as (H'&I&M1&M2&M3). applys~ (@local_wframe unit) (# I (b+1)); [| intros u; destruct~ u ]. clear M1. asserts L: (a <= a <= b+1). math. generalize L. set (a' := a) at 1. generalize a as i. unfold a'. intros i. induction_wf IH: (int_upto_wf (b+1)) i. intros Bnd. applys HS. split; intros C'. apply local_erase. esplit. split. apply M2; auto with maths. forwards: IH (i+1); auto with maths. math_rewrite~ (i = b +1). Qed. *)