CFLemmasForTactics.v 6.43 KB
Newer Older
charguer's avatar
charguer committed
1
Set Implicit Arguments.
charguer's avatar
charguer committed
2
Require Export LibInt CFApp CFPrint.
charguer's avatar
charguer committed
3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186


(********************************************************************)
(********************************************************************)
(********************************************************************)
(********************************************************************)

(* 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&lt&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. 



*)