LambdaCFLifted.v 25.8 KB
Newer Older
charguer's avatar
charguer committed
1 2
(**

charguer's avatar
charguer committed
3 4
This file extends [LambdaCF.v] by "lifting" heap predicates like in
[LambdaSepLifted.v], so as to express specifications using logical values,
charguer's avatar
charguer committed
5
as opposed to deeply-embedded values. CF are lifted like triples.
charguer's avatar
charguer committed
6 7 8 9 10 11

Author: Arthur Charguéraud.
License: MIT.

*)

charguer's avatar
charguer committed
12

charguer's avatar
charguer committed
13
Set Implicit Arguments.
charguer's avatar
charguer committed
14
Require Export LibCore LambdaCF LambdaSepLifted.
charguer's avatar
charguer committed
15
Generalizable Variables A B.
charguer's avatar
charguer committed
16

charguer's avatar
charguer committed
17
Open Scope charac.
charguer's avatar
charguer committed
18

charguer's avatar
charguer committed
19
Ltac auto_star ::= jauto.
charguer's avatar
charguer committed
20

charguer's avatar
charguer committed
21

charguer's avatar
compact  
charguer committed
22 23 24
(* ********************************************************************** *)
(* * Auxiliary definitions *)

charguer's avatar
charguer committed
25

charguer's avatar
charguer committed
26
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
27 28 29 30 31
(* ** Type of a formula *)

(** A formula is a binary relation relating a pre-condition
    and a post-condition. *)

charguer's avatar
rename  
charguer committed
32
Definition Formula := forall `{Enc A}, hprop -> (A -> hprop) -> Prop.
charguer's avatar
charguer committed
33

charguer's avatar
rename  
charguer committed
34
Global Instance Inhab_Formula : Inhab Formula.
charguer's avatar
charguer committed
35
Proof using. apply (Inhab_of_val (fun _ _ _ _ => True)). Qed.
charguer's avatar
charguer committed
36

charguer's avatar
rename  
charguer committed
37
Notation "' F H Q" := ((F:Formula) _ _ H Q)
charguer's avatar
charguer committed
38 39
  (at level 65, F at level 0, H at level 0, Q at level 0,
   format "' F  H  Q") : charac.
charguer's avatar
charguer committed
40

charguer's avatar
rename  
charguer committed
41 42
(** Constructor to force the return type of a Formula *)
Definition Formula_typed `{Enc A1} (F : hprop->(A1->hprop)->Prop) : Formula :=
charguer's avatar
charguer committed
43 44 45
  fun `{Enc A2} H (Q:A2->hprop) =>
    exists (Q':A1->hprop), F H Q' /\ PostChange Q' Q.

charguer's avatar
charguer committed
46

charguer's avatar
charguer committed
47 48
(* ---------------------------------------------------------------------- *)
(* ** Lifting of [local] *)
charguer's avatar
charguer committed
49

charguer's avatar
rename  
charguer committed
50
Definition Local (F:Formula) := fun A `{EA:Enc A} H Q =>
charguer's avatar
charguer committed
51
   local (F A EA) H Q.
charguer's avatar
charguer committed
52

charguer's avatar
rename  
charguer committed
53
Lemma local_Local_eq : forall A `{EA:Enc A} (F:Formula),
charguer's avatar
charguer committed
54 55
  local (@Local F A EA) = (@Local F A EA).
Proof using.
charguer's avatar
charguer committed
56
  intros. apply pred_ext_2. intros H Q.
charguer's avatar
charguer committed
57 58 59
  unfold Local. rewrite local_local. split~.
Qed.
  
charguer's avatar
rename  
charguer committed
60
Lemma is_local_Local : forall A `{EA:Enc A} (F:Formula),
charguer's avatar
charguer committed
61
  is_local (@Local F A EA).
charguer's avatar
charguer committed
62
Proof using. intros. unfolds. rewrite~ local_Local_eq. Qed.
charguer's avatar
charguer committed
63

charguer's avatar
charguer committed
64
Hint Resolve is_local_Local.
charguer's avatar
charguer committed
65

charguer's avatar
xapps  
charguer committed
66

charguer's avatar
charguer committed
67 68
(* ********************************************************************** *)
(* * Lifted CF *)
charguer's avatar
charguer committed
69

charguer's avatar
charguer committed
70
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
71 72
(* ** Definition of CF blocks *)

charguer's avatar
rename  
charguer committed
73
(** These auxiliary definitions give the characteristic Formula
charguer's avatar
charguer committed
74 75
    associated with each term construct. *)

charguer's avatar
rename  
charguer committed
76
Definition Cf_fail : Formula := fun `{Enc A} H (Q:A->hprop) =>
charguer's avatar
charguer committed
77 78
  False.

charguer's avatar
rename  
charguer committed
79
Definition Cf_val (v:val) : Formula := 
charguer's avatar
charguer committed
80 81
  fun `{Enc A} H (Q:A->hprop) =>
    exists V, v = enc V /\ H ==> Q V.
charguer's avatar
charguer committed
82

charguer's avatar
rename  
charguer committed
83
Definition Cf_if_val (v:val) (F1 F2 : Formula) : Formula := 
charguer's avatar
charguer committed
84
  fun `{Enc A} H (Q:A->hprop) =>
charguer's avatar
ok  
charguer committed
85 86
    exists (b:bool), v = enc b /\
     (b = true -> 'F1 H Q) /\ (b = false -> 'F2 H Q).
charguer's avatar
charguer committed
87

charguer's avatar
rename  
charguer committed
88
Definition Cf_seq (F1 : Formula) (F2 : Formula) : Formula := 
charguer's avatar
charguer committed
89
  fun `{Enc A} H (Q:A->hprop) =>
charguer's avatar
charguer committed
90
    exists (Q1:unit->hprop), 'F1 H Q1 /\ 'F2 (Q1 tt) Q.
charguer's avatar
charguer committed
91

charguer's avatar
rename  
charguer committed
92
Definition Cf_let (F1 : Formula) (F2of : forall `{EA1:Enc A1}, A1 -> Formula) : Formula := 
charguer's avatar
charguer committed
93
  fun `{Enc A} H (Q:A->hprop) =>
charguer's avatar
charguer committed
94 95 96
    exists (A1:Type) (EA1:Enc A1) (Q1:A1->hprop), 
        'F1 H Q1 
     /\ (forall (X:A1), '(F2of X) (Q1 X) Q).
charguer's avatar
charguer committed
97

charguer's avatar
rename  
charguer committed
98
Definition Cf_let_typed `{EA1:Enc A1} (F1 : Formula) (F2of : A1 -> Formula) : Formula := 
charguer's avatar
ok  
charguer committed
99
  fun `{Enc A} H (Q:A->hprop) =>
charguer's avatar
charguer committed
100 101 102 103
    exists (Q1:A1->hprop), 
        'F1 H Q1 
     /\ (forall (X:A1), '(F2of X) (Q1 X) Q).

charguer's avatar
rename  
charguer committed
104
Definition Cf_if (F0 F1 F2 : Formula) : Formula := 
charguer's avatar
charguer committed
105
  Cf_let_typed F0 (fun (X:bool) => Local (Cf_if_val (enc X) F1 F2)).
charguer's avatar
charguer committed
106

charguer's avatar
stable  
charguer committed
107 108 109
Definition Cf_app (t : trm) : Formula :=  
  @Triple t.

charguer's avatar
charguer committed
110 111 112 113 114 115 116 117 118 119
(* TODO simplified version to use:
Definition Cf_while (F1 F2 : Formula) : Formula := 
  fun `{Enc A} H (Q:A->hprop) =>
    forall (F:Formula), is_local (@F unit _) ->
      (forall H' (Q':unit->hprop), 
         '(Local (Cf_if F1 (Local (Cf_seq F2 (F:Formula))) (Local (Cf_val val_unit)))) H' Q' ->
         '(F:Formula) H' Q') ->
      '(F:Formula) H Q.
*)

charguer's avatar
rename  
charguer committed
120 121
Definition Cf_while (F1 F2 : Formula) : Formula := 
  Formula_typed (fun H (Q:unit->hprop) =>
charguer's avatar
cpsapp  
charguer committed
122 123
    forall (F:Formula), is_local (@F unit _) ->
      (forall H' (Q':unit->hprop), 
charguer's avatar
charguer committed
124 125 126
         '(Local (Cf_if F1 (Local (Cf_seq F2 (F:Formula))) (Local (Cf_val val_unit)))) H' Q' ->
         '(F:Formula) H' Q') ->
      '(F:Formula) H Q).
charguer's avatar
charguer committed
127

charguer's avatar
charguer committed
128 129
Definition Cf_for (n1 n2 : int) (F1 : int->Formula) : Formula := 
  (* Formula_typed (fun H (Q:unit->hprop) => *)
charguer's avatar
charguer committed
130
  fun `{Enc A} H (Q:A->hprop) =>
charguer's avatar
charguer committed
131 132 133 134 135
    forall (S:int->Formula), (forall i, is_local (@S i unit _)) ->
    let F i := Local (If (i <= n2) then (Local (Cf_seq (F1 i) (S (i+1))))
                             else (Local (Cf_val val_unit))) in
    (forall i H' Q', '(F i) H' Q' -> '(S i) H' Q') -> 
    '(S n1) H Q.
charguer's avatar
charguer committed
136

charguer's avatar
charguer committed
137

charguer's avatar
charguer committed
138
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
139 140
(* ** Definition of the CF generator *)

charguer's avatar
rename  
charguer committed
141
Definition Cf_def Cf (t:trm) : Formula :=
charguer's avatar
charguer committed
142
  match t with
charguer's avatar
charguer committed
143 144 145 146 147 148
  | trm_val v => Local (Cf_val v)
  | trm_var x => Local (Cf_fail) (* unbound variable *)
  | trm_fun x t1 => Local (Cf_val (val_fun x t1))
  | trm_fix f x t1 => Local (Cf_val (val_fix f x t1))
  | trm_if t0 t1 t2 => Local (Cf_if (Cf t0) (Cf t1) (Cf t2))
  | trm_seq t1 t2 => Local (Cf_seq (Cf t1) (Cf t2))
charguer's avatar
cleanup  
charguer committed
149 150
  | trm_let y t1 t2 => Local (Cf_let (Cf t1) 
                                (fun `{EA:Enc A} (X:A) => Cf (subst y (enc X) t2)))
charguer's avatar
stable  
charguer committed
151
  | trm_app t1 t2 => Local (Cf_app t)
charguer's avatar
charguer committed
152
  | trm_while t1 t2 => Local (Cf_while (Cf t1) (Cf t2))
charguer's avatar
charguer committed
153 154 155 156 157 158
  | trm_for x t1 t2 t3 => Local (
      match t1, t2 with 
      | trm_val (val_int n1), trm_val (val_int n2) => 
            Cf_for n1 n2 (fun X => Cf (subst x X t3))
      | _, _ => Cf_fail (* not supported *)
      end)
charguer's avatar
xapps  
charguer committed
159 160
  end.

charguer's avatar
charguer committed
161
Definition Cf := FixFun Cf_def.
charguer's avatar
charguer committed
162

charguer's avatar
charguer committed
163 164
Lemma Cf_unfold_iter : forall n t,
  Cf t = func_iter n Cf_def Cf t.
charguer's avatar
charguer committed
165
Proof using.
charguer's avatar
charguer committed
166 167
  applys~ (FixFun_fix_iter (measure trm_size)). auto with wf.
  intros f1 f2 t IH. unfold Cf_def.
charguer's avatar
charguer committed
168
  destruct t; fequals.
charguer's avatar
charguer committed
169 170
  { fequals~. }
  { fequals~. }
charguer's avatar
compile  
charguer committed
171
  { fequals~. applys~ fun_ext_3. }
charguer's avatar
charguer committed
172
  { fequals~. }
charguer's avatar
charguer committed
173 174
  { destruct t1; fequals~. destruct v0; fequals~.
    destruct t2; fequals~. destruct v0; fequals~.
charguer's avatar
charguer committed
175
    applys~ fun_ext_1. }
charguer's avatar
charguer committed
176 177
Qed.

charguer's avatar
charguer committed
178 179 180
Lemma Cf_unfold : forall t,
  Cf t = Cf_def Cf t.
Proof using. applys (Cf_unfold_iter 1). Qed.
charguer's avatar
charguer committed
181

charguer's avatar
charguer committed
182

charguer's avatar
charguer committed
183
(* ********************************************************************** *)
charguer's avatar
charguer committed
184 185
(* ** Soundness proof *)

charguer's avatar
charguer committed
186
(* ---------------------------------------------------------------------- *)
charguer's avatar
charguer committed
187 188
(* ** Soundness of the CF generator *)

charguer's avatar
charguer committed
189
Lemma is_local_Cf : forall A `{EA:Enc A} T,
charguer's avatar
charguer committed
190
  is_local ((Cf T) A EA).
charguer's avatar
charguer committed
191
Proof.
charguer's avatar
charguer committed
192
  intros. rewrite Cf_unfold. destruct T; try apply is_local_local.
charguer's avatar
charguer committed
193
Qed.
charguer's avatar
charguer committed
194

charguer's avatar
rename  
charguer committed
195
Definition Sound_for (t:trm) (F:Formula) := 
charguer's avatar
charguer committed
196 197
  forall `{EA:Enc A} H (Q:A->hprop), 'F H Q -> Triple t H Q.

charguer's avatar
rename  
charguer committed
198
Lemma Sound_for_Local : forall t (F:Formula),
charguer's avatar
charguer committed
199 200 201
  Sound_for t F ->
  Sound_for t (Local F).
Proof using.
charguer's avatar
charguer committed
202
  unfold sound_for. introv SF. intros A EA H Q M.
charguer's avatar
charguer committed
203
  rewrite is_local_Triple. applys local_weaken_body M. applys SF.
charguer's avatar
charguer committed
204 205
Qed.

charguer's avatar
charguer committed
206 207 208 209
Lemma Sound_for_Cf : forall (t:trm),
  Sound_for t (Cf t).
Proof using.
  intros t. induction_wf: trm_size t. 
charguer's avatar
charguer committed
210
  rewrite Cf_unfold. destruct t;
charguer's avatar
charguer committed
211 212
   try (applys Sound_for_Local; intros A EA H Q P).  
  { destruct P as (V&E&P). applys* Rule_val. }
charguer's avatar
charguer committed
213
  { false. }
charguer's avatar
charguer committed
214
  { destruct P as (V&E&P). 
charguer's avatar
charguer committed
215
    applys Triple_enc_val_inv (fun r => \[r = enc V] \* H).
charguer's avatar
charguer committed
216 217 218
    { applys Rule_fun. rewrite E. hsimpl~. }
    { intros X. hpull ;=> EX. subst X. hchange P. hsimpl. simple~. } }
  { destruct P as (V&E&P). 
charguer's avatar
charguer committed
219
    applys Triple_enc_val_inv (fun r => \[r = enc V] \* H).
charguer's avatar
charguer committed
220 221
    { applys Rule_fix. rewrite E. hsimpl~. }
    { intros X. hpull ;=> EX. subst X. hchange P. hsimpl. simple~. } }
charguer's avatar
charguer committed
222 223
  { destruct P as (Q1&P1&P2). applys @Rule_if. 
    { applys* IH. }
charguer's avatar
charguer committed
224 225 226 227
    { intros b. specializes P2 b. applys Sound_for_Local (rm P2).
      clears A H Q1. intros A EA H Q (b'&P1'&P2'&P3').
      asserts E: (b = b'). { destruct b; destruct b'; auto. }
      clear P1'. subst b'. case_if; applys* IH. } }
charguer's avatar
charguer committed
228
  { destruct P as (H1&P1&P2). applys Rule_seq H1.
charguer's avatar
charguer committed
229 230
    { applys~ IH. }
    { intros X. applys~ IH. } } 
charguer's avatar
charguer committed
231
  { destruct P as (A1&EA1&Q1&P1&P2). applys Rule_let Q1.
charguer's avatar
charguer committed
232
    { applys~ IH. }
charguer's avatar
charguer committed
233
    { intros X. specializes P2 X.
charguer's avatar
cleanup  
charguer committed
234
      unfold Subst. rewrite enc_dyn_eq. applys~ IH. } }
charguer's avatar
xapps  
charguer committed
235
  { auto. }
charguer's avatar
charguer committed
236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251
  { hnf in P. destruct P as (Q'&P&HC). simpls.
    applys Triple_enc_change HC.
    applys P. { xlocal. } clears H Q. intros H Q P.
    applys Rule_while_raw. applys Sound_for_Local (rm P). 
    clears A H Q Q'. intros A EA H Q (Q1&P1&P2). applys Rule_if.  
    { applys* IH. }
    { intros b. specializes P2 b. applys Sound_for_Local (rm P2).
      clears A H Q1. intros A EA H Q (b'&P1&P2&P3).
      asserts E: (b = b'). { destruct b; destruct b'; auto. }
      clears P1. subst b'. case_if as C.
      { forwards~ P2': (rm P2). applys Sound_for_Local (rm P2'). 
        clears A H b. intros A EA H Q (H1&P1&P2). applys Rule_seq.
         { applys* IH. }
         { applys P2. } }
      { forwards~ P3': (rm P3). applys Sound_for_Local (rm P3'). 
        clears A H b. intros A EA H Q (V&E&P). applys* Rule_val. } } }
charguer's avatar
charguer committed
252 253 254 255 256 257 258 259 260 261 262 263 264 265 266
  { destruct t1; tryfalse. destruct v0; tryfalse. 
    destruct t2; tryfalse. destruct v0; tryfalse.
    renames z to n1, z0 to n2.
    (* hnf in P. destruct P as (Q'&P&HC). simpls.
    applys Triple_enc_change HC. *)
    applys P. { intros; xlocal. } (* todo xlocal *)
    clears A H. intros i H Q P. applys Sound_for_Local (rm P). 
    clears A H. intros A EA H Q P. applys Rule_for_raw.
    case_if as C.
    { applys Sound_for_Local (rm P). clears A H i. 
      intros A EA H Q (H1&P1&P2). applys Rule_seq.
      { applys* IH. }
      { applys P2. } }
    { applys Sound_for_Local (rm P). clears A H i.
      intros A EA H Q (V&E&P). applys* Rule_val. } }
charguer's avatar
xapps  
charguer committed
267
Qed.
charguer's avatar
charguer committed
268

charguer's avatar
charguer committed
269
Theorem Triple_of_Cf : forall (t:trm) A `{EA:Enc A} H (Q:A->hprop), 
charguer's avatar
charguer committed
270 271 272 273 274
  '(Cf t) H Q -> 
  Triple t H Q.
Proof using. intros. applys* Sound_for_Cf. Qed.


charguer's avatar
charguer committed
275
(* ********************************************************************** *)
charguer's avatar
rename  
charguer committed
276
(* * Practical proofs using characteristic Formulae *)
charguer's avatar
charguer committed
277

charguer's avatar
charguer committed
278
(* ---------------------------------------------------------------------- *)
charguer's avatar
rename  
charguer committed
279
(* ** Notation for characteristic Formulae *)
charguer's avatar
charguer committed
280

charguer's avatar
stable  
charguer committed
281 282 283 284 285 286 287 288
(** Notation [F PRE H POST Q] for stating specifications, e.g. 
    [Triple t PRE H POST Q] is the same as [Triple t H Q] *)

Notation "F 'PRE' H 'POST' Q" :=
  (F H Q)
  (at level 69, only parsing) : charac.

(** Notation [PRE H CODE F POST Q] for displaying characteristic formulae *)
charguer's avatar
cpsapp  
charguer committed
289 290 291 292 293 294 295
(*

  Notation "'PRE' H 'CODE' F 'POST' Q" :=
    (@Local F _ _ H Q) (at level 69,
    format "'[v' '[' 'PRE'  H  ']' '/' '[' 'CODE'  F  ']' '/' '[' 'POST'  Q  ']' ']'")
    : charac2.
*)
charguer's avatar
stable  
charguer committed
296

charguer's avatar
cpsapp  
charguer committed
297 298 299
Notation "'`Fail'" :=
  (Local (Cf_fail))
  (at level 69) : charac.
charguer's avatar
charguer committed
300

charguer's avatar
charguer committed
301
Notation "'`Val' v" :=
charguer's avatar
cpsapp  
charguer committed
302
  (Local (Cf_val v))
charguer's avatar
charguer committed
303
  (at level 69) : charac.
charguer's avatar
charguer committed
304

charguer's avatar
charguer committed
305
Notation "'`LetIf' F0 'Then' F1 'Else' F2" :=
charguer's avatar
cpsapp  
charguer committed
306
  (Local (Cf_if F0 F1 F2))
charguer's avatar
charguer committed
307
  (at level 69, F0 at level 0) : charac.
charguer's avatar
charguer committed
308

charguer's avatar
charguer committed
309
Notation "'`If' v 'Then' F1 'Else' F2" :=
charguer's avatar
cpsapp  
charguer committed
310
  (Local (Cf_if_val v F1 F2))
charguer's avatar
xapps  
charguer committed
311 312
  (at level 69) : charac.

charguer's avatar
charguer committed
313
Notation "'`Seq' F1 ;; F2" :=
charguer's avatar
cpsapp  
charguer committed
314
  (Local (Cf_seq F1 F2))
charguer's avatar
charguer committed
315 316
  (at level 68, right associativity,
   format "'[v' '`Seq'  '[' F1 ']'  ;;  '/'  '[' F2 ']' ']'") : charac.
charguer's avatar
charguer committed
317

charguer's avatar
cpsapp  
charguer committed
318 319
Notation "'``Let' x ':=' F1 'in' F2" :=
  (Local (Cf_let_typed F1 (fun x => F2)))
charguer's avatar
charguer committed
320
  (at level 69, x ident, right associativity,
charguer's avatar
cpsapp  
charguer committed
321
  format "'[v' '[' '``Let'  x  ':='  F1  'in' ']'  '/'  '[' F2 ']' ']'") : charac.
charguer's avatar
charguer committed
322

charguer's avatar
charguer committed
323
Notation "'`Let' [ A EA ] x ':=' F1 'in' F2" :=
charguer's avatar
cpsapp  
charguer committed
324
  (Local (Cf_let F1 (fun A EA x => F2)))
charguer's avatar
charguer committed
325 326
  (at level 69, A at level 0, EA at level 0, x ident, right associativity,
  format "'[v' '[' '`Let'  [ A  EA ]  x  ':='  F1  'in' ']'  '/'  '[' F2 ']' ']'") : charac.
charguer's avatar
charguer committed
327

charguer's avatar
xapps  
charguer committed
328
Notation "'`App' t " :=
charguer's avatar
cpsapp  
charguer committed
329
  (Local (Cf_app t))
charguer's avatar
xapps  
charguer committed
330 331
  (at level 68, t at level 0) : charac.

charguer's avatar
cpsapp  
charguer committed
332 333 334 335 336
Notation "'`While' F1 'Do' F2 'Done'" :=
  (Local (Cf_while F1 F2))
  (at level 69, F2 at level 68,
   format "'[v' '`While'  F1  'Do'  '/' '[' F2 ']' '/'  'Done' ']'")
   : charac.
charguer's avatar
charguer committed
337

charguer's avatar
charguer committed
338 339 340 341 342 343
Notation "'`For' x '=' n1 'To' n2 'Do' F3 'Done'" :=
  (Local (Cf_for n1 n2 (fun x => F3)))
  (at level 69, x ident,
   format "'[v' '`For'  x  '='  n1  'To'  n2  'Do'  '/' '[' F3 ']' '/'  'Done' ']'")
  : charac.

charguer's avatar
charguer committed
344
Open Scope charac.
charguer's avatar
charguer committed
345 346


charguer's avatar
charguer committed
347 348
(* ---------------------------------------------------------------------- *)
(* ** Lemmas for tactics *)
charguer's avatar
compact  
charguer committed
349

charguer's avatar
charguer committed
350 351 352
Lemma Triple_trm_of_Cf_iter : forall (n:nat) t A `{EA:Enc A} H (Q:A->hprop), 
  func_iter n Cf_def Cf t A EA H Q ->
  Triple t H Q.
charguer's avatar
compact  
charguer committed
353
Proof using.
charguer's avatar
charguer committed
354
  introv M. rewrite <- Cf_unfold_iter in M. applys* Triple_of_Cf.
charguer's avatar
compact  
charguer committed
355 356
Qed.

charguer's avatar
charguer committed
357 358 359 360 361
Lemma Triple_apps_funs_of_Cf_iter : forall n F (Vs:dyns) (vs:vals) xs t A `{EA:Enc A} H (Q:A->hprop), 
  F = val_funs xs t ->
  vs = encs Vs ->
  var_funs_exec (length Vs) xs ->
  func_iter n Cf_def Cf (Substs xs Vs t) A EA H Q ->
charguer's avatar
ok  
charguer committed
362
  Triple (trm_apps F vs) H Q.
charguer's avatar
charguer committed
363
Proof using.
charguer's avatar
charguer committed
364
  introv EF EV N M. rewrite var_funs_exec_eq in N. rew_istrue in N.
charguer's avatar
ok  
charguer committed
365
  subst. applys* Rule_apps_funs. applys* Triple_trm_of_Cf_iter.
charguer's avatar
charguer committed
366
Qed.
charguer's avatar
compact  
charguer committed
367

charguer's avatar
cleanup  
charguer committed
368
Lemma Triple_apps_fixs_of_Cf_iter : forall n F f (Vs:dyns) (vs:vals) xs t A `{EA:Enc A} H (Q:A->hprop), 
charguer's avatar
ok  
charguer committed
369 370 371 372
  F = val_fixs f xs t ->
  vs = encs Vs ->
  var_fixs_exec f (length Vs) xs ->
  func_iter n Cf_def Cf (subst f F (Substs xs Vs t)) A EA H Q ->
charguer's avatar
cleanup  
charguer committed
373
  Triple (trm_apps (val_fixs f xs t) vs) H Q.
charguer's avatar
ok  
charguer committed
374
Proof using.
charguer's avatar
charguer committed
375
  introv EF EV N M. rewrite var_fixs_exec_eq in N. rew_istrue in N.
charguer's avatar
ok  
charguer committed
376 377
  subst. applys* Rule_apps_fixs. applys* Triple_trm_of_Cf_iter.
Qed.
charguer's avatar
compact  
charguer committed
378

charguer's avatar
cpsapp  
charguer committed
379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400
Definition Cf_while_inv (F1 F2 : Formula) := fun (H:hprop) (Q:unit->hprop) =>
  exists (A:Type) (I:bool->A->hprop) (R:A->A->Prop) H',
     wf R 
  /\ (H ==> Hexists b X, I b X \* H') 
  /\ (forall (F:Formula), is_local (@F unit _) -> forall b X, 
      (forall b' X', R X' X -> 'F (I b' X') (fun (_:unit) => Hexists Y, I false Y)) ->
      '(Local (Cf_if F1 (Local (Cf_seq F2 F)) (Local (Cf_val val_unit)))) 
        (I b X) (fun (_:unit) => Hexists Y, I false Y))
  /\ ((fun (_:unit) => Hexists X, I false X \* H') ===> Q).

Lemma Cf_while_of_Cf_while_inv : forall (F1 F2 : Formula) (H:hprop) (Q:unit->hprop),
  (Cf_while_inv F1 F2) H Q ->
  '(Cf_while F1 F2) H Q.
Proof using.
  introv (A&I&R&H'&MR&MH&MB&MQ). exists Q; split; [|applys @PostChange_refl]. 
  intros F LF HF. xchange MH. xpull ;=> b X.
  applys local_frame (I b X) H' (fun (_:unit) => Hexists Y, I false Y);
   [ xlocal | | hsimpl | hchanges~ MQ ]. (* todo: change goal order in weakenpost*)
  gen b. induction_wf IH: MR X. intros. applys (rm HF).
  applys MB. xlocal. intros b' X' HR'. applys~ IH.
Qed.

charguer's avatar
compact  
charguer committed
401

charguer's avatar
cleanup  
charguer committed
402 403
(* ********************************************************************** *)
(* * CFLifted tactics *)
charguer's avatar
xapps  
charguer committed
404

charguer's avatar
seplift  
charguer committed
405 406 407 408 409 410 411 412 413 414
(* ---------------------------------------------------------------------- *)
(* ** Registering specifications *)

Notation "'Register_Rule' t" := (Register_goal (Triple t _ _))
  (at level 69) : charac.

Notation "'Register_Spec' f" := (Register_Rule (trm_apps (trm_val f) _))
  (at level 69) : charac.


charguer's avatar
charguer committed
415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440
(* ---------------------------------------------------------------------- *)
(* ** [xspec] *)

Ltac xspec_context_for f :=
  match goal with 
  | H: context [ Triple _ _ _ ] |- _ =>  
      match type of H with
      | context [ trm_app (trm_val f) _ ] => generalize H
      | context [ trm_apps (trm_val f) _ ] => generalize H
      end end.

Ltac xspec_context_triple tt :=
  let f := xcf_get_fun_from_goal tt in
  xspec_context_for f.

Ltac xspec_context_formula F :=
  match goal with H: context [ F _ _ _ _ ] |- _ => generalize H end.

Ltac xspec_context G ::=
  match G with 
  | Triple _ _ _ => xspec_context_triple tt
  | ?F _ _ _ _ => xspec_context_formula F
  (* last line only for CF lifted *)
  end.


charguer's avatar
seplift  
charguer committed
441 442 443
(* ---------------------------------------------------------------------- *)
(* ** Specification of primitives *)

charguer's avatar
ok  
charguer committed
444 445 446 447 448 449 450
Hint Extern 1 (Register_Spec (val_prim val_ref)) => Provide Rule_ref.
Hint Extern 1 (Register_Spec (val_prim val_get)) => Provide Rule_get.
Hint Extern 1 (Register_Spec (val_prim val_set)) => Provide Rule_set.
Hint Extern 1 (Register_Spec (val_prim val_alloc)) => Provide Rule_alloc.
Hint Extern 1 (Register_Spec (val_prim val_eq)) => Provide Rule_eq.
Hint Extern 1 (Register_Spec (val_prim val_add)) => Provide Rule_add.
Hint Extern 1 (Register_Spec (val_prim val_ptr_add)) => Provide Rule_ptr_add.
charguer's avatar
seplift  
charguer committed
451 452


charguer's avatar
cleanup  
charguer committed
453
(*--------------------------------------------------------*)
charguer's avatar
charguer committed
454
(* ** [hsimpl] and [xpull] cleanup of boolean reflection *)
charguer's avatar
xapps  
charguer committed
455

charguer's avatar
charguer committed
456
Ltac hsimpl_post_before_generalize tt ::=
charguer's avatar
compile  
charguer committed
457
  autorewrite with rew_bool_eq.
charguer's avatar
charguer committed
458 459

Ltac himpl_post_processing_for_hyp H ::=
charguer's avatar
compile  
charguer committed
460
  autorewrite with rew_bool_eq in H.
charguer's avatar
charguer committed
461 462

Ltac xpull_post_processing_for_hyp H ::=
charguer's avatar
compile  
charguer committed
463
  autorewrite with rew_bool_eq in H.
charguer's avatar
xapps  
charguer committed
464 465


charguer's avatar
cleanup  
charguer committed
466
(*--------------------------------------------------------*)
charguer's avatar
charguer committed
467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489
(* ** [xdecode_args] : used internally *)

Ltac xdecode_arg v :=
  let W := constr:(decode v) in
  let W' := (eval simpl decode in W) in   
  match W' with Dyn ?V' => 
    change (trm_val v) with (trm_val (enc V'))
  end.

Ltac xdecode_args_from_trms ts :=
  match ts with 
  | (trm_val (enc ?V))::?ts' => xdecode_args_from_trms ts'
  | (trm_val ?v)::?ts' => xdecode_arg v; xdecode_args_from_trms ts'
  | nil => idtac
  end.

Ltac xdecode_args tt :=
  match goal with |- Triple (trm_apps ?f ?ts) ?H ?Q =>
    xdecode_args_from_trms ts end.


(*--------------------------------------------------------*)
(* ** [xeq_enc] : used internally *)
charguer's avatar
xapps  
charguer committed
490

charguer's avatar
lifted  
charguer committed
491 492
(** [xeq_enc] solves goal of the form [ v = enc ?V ]. *)

charguer's avatar
cleanup  
charguer committed
493
(* DEPRECATED
charguer's avatar
cleanup  
charguer committed
494 495
Ltac xeq_enc_core tt :=
  match goal with |- ?v = enc ?V => applys (refl_equal (enc (decode v))) end.
charguer's avatar
cleanup  
charguer committed
496 497 498 499 500 501 502 503
*)

Ltac xeq_enc_core tt :=
  match goal with |- ?v = enc ?V => 
    let W := constr:(decode v) in
    let W' := (eval simpl decode in W) in   
    match W' with Dyn ?V' => refine (refl_equal (enc V')) 
  end end.
charguer's avatar
xapps  
charguer committed
504

charguer's avatar
cleanup  
charguer committed
505 506
Tactic Notation "xeq_enc" :=
  xeq_enc_core tt.
charguer's avatar
compact  
charguer committed
507

charguer's avatar
charguer committed
508

charguer's avatar
cleanup  
charguer committed
509
(*--------------------------------------------------------*)
charguer's avatar
charguer committed
510
(* ** [xeq_encs] : used internally *)
charguer's avatar
charguer committed
511

charguer's avatar
lifted  
charguer committed
512 513 514 515 516 517 518 519 520 521 522 523 524 525 526
(** [xeq_encs] solves goal of the form [ [`V1; ..; `VN] = encs ?VS ]. *)

Lemma encs_nil : 
  encs nil = @nil val.
Proof using. auto. Qed.

Lemma encs_cons : forall `{EA:Enc A} (V:A) (VS:dyns),
  encs ((Dyn V)::VS) = (enc V)::(encs VS).
Proof using. auto. Qed.

Hint Rewrite <- @encs_nil @encs_cons : rew_encs.

Tactic Notation "rew_encs" := 
  autorewrite with rew_encs.

charguer's avatar
charguer committed
527
Ltac xeq_encs_core tt :=
charguer's avatar
lifted  
charguer committed
528 529 530 531
  rew_encs; reflexivity.

(* DEPRECATED
match goal with |- ?vs = encs ?Vs => applys (refl_equal (encs (decodes vs))) end.*)
charguer's avatar
charguer committed
532

charguer's avatar
charguer committed
533
Tactic Notation "xeq_encs" :=
charguer's avatar
charguer committed
534
  xeq_encs_core tt.
charguer's avatar
charguer committed
535

charguer's avatar
charguer committed
536

charguer's avatar
ok  
charguer committed
537
(*--------------------------------------------------------*)
charguer's avatar
lifted  
charguer committed
538
(* ** [rew_dyn] *)
charguer's avatar
ok  
charguer committed
539

charguer's avatar
lifted  
charguer committed
540
Hint Rewrite dyn_to_val_dyn_make @enc_decode enc_dyn_eq : rew_dyn.
charguer's avatar
ok  
charguer committed
541 542

Tactic Notation "rew_dyn" := 
charguer's avatar
lifted  
charguer committed
543
  autorewrite with rew_dyn; simpl dyn_value.
charguer's avatar
ok  
charguer committed
544
Tactic Notation "rew_dyn" "in" hyp(H) := 
charguer's avatar
lifted  
charguer committed
545
  autorewrite with rew_dyn in H; simpl dyn_value in H.
charguer's avatar
ok  
charguer committed
546
Tactic Notation "rew_dyn" "in" "*" := 
charguer's avatar
lifted  
charguer committed
547
  autorewrite with rew_dyn in *; simpl dyn_value in *.
charguer's avatar
ok  
charguer committed
548 549


charguer's avatar
charguer committed
550
(*--------------------------------------------------------*)
charguer's avatar
cleanup  
charguer committed
551
(* ** [xcf] *)
charguer's avatar
charguer committed
552

charguer's avatar
charguer committed
553 554 555 556 557 558 559 560 561
Ltac xcf_get_fun_remove_encs f ::=
  match f with
  | @enc func _ ?f => xcf_get_fun_remove_encs f
  | @enc val _ ?f => xcf_get_fun_remove_encs f
  | _ => constr:(f)
  end.

Ltac xcf_get_fun_from_goal tt ::=
  match goal with |- Triple ?t _ _ => xcf_get_fun_from_trm t end.
charguer's avatar
ok  
charguer committed
562

charguer's avatar
cleanup  
charguer committed
563
Ltac xcf_post tt ::= 
charguer's avatar
stable  
charguer committed
564
  simpl; rew_enc_dyn.
charguer's avatar
cleanup  
charguer committed
565 566 567

(** todo: follow similar strategy to avoid the need to fold in LambdaCF *)

charguer's avatar
charguer committed
568 569 570 571 572 573 574 575 576 577 578 579 580 581 582
Ltac xcf_trm n :=
  applys Triple_trm_of_Cf_iter n; [ xcf_post tt ].

Ltac xcf_basic_fun n f' :=
  let f := xcf_get_fun tt in 
  match f with  
  | val_funs _ _ =>
      applys Triple_apps_funs_of_Cf_iter n;  
      [ reflexivity | try xeq_encs | reflexivity | xcf_post tt ]      
  | val_fixs _ _ _ => 
      applys Triple_apps_fixs_of_Cf_iter n f';
      [ reflexivity | try xeq_encs | reflexivity | xcf_post tt ] 
  end.

Ltac xcf_fun n :=
charguer's avatar
cleanup  
charguer committed
583
  rew_nary;
charguer's avatar
charguer committed
584
  try xdecode_args tt;
charguer's avatar
cleanup  
charguer committed
585 586 587 588
  let f' := xcf_get_fun tt in 
  xcf_reveal_fun tt;
  rew_nary; 
  rew_vals_to_trms;
charguer's avatar
charguer committed
589
  xcf_basic_fun n f'.
charguer's avatar
xapps  
charguer committed
590

charguer's avatar
charguer committed
591
Ltac xcf_core n ::=
charguer's avatar
charguer committed
592
  intros; first [ xcf_fun n | xcf_trm n ].
charguer's avatar
cleanup  
charguer committed
593

charguer's avatar
charguer committed
594

charguer's avatar
cleanup  
charguer committed
595 596
(*--------------------------------------------------------*)
(* ** [xval] *)
charguer's avatar
charguer committed
597

charguer's avatar
cleanup  
charguer committed
598 599
Ltac xval_nohtop_core tt ::=
  applys local_erase; unfold Cf_val.
charguer's avatar
charguer committed
600 601 602 603 604 605 606 607 608 609 610

(* todo: xval wouldn't work if the postcondition isn't specified 
   and the result value has been introduced locally, e.g. with nested lets *)

Lemma xval_htop_evar : forall A (V:A) (EA:Enc A) v H,
  v = enc V ->
  Local (Cf_val v) H (fun (x:A) => \[x = V] \* H).
Proof using.
  introv E. applys local_erase. exists V. split~. hsimpl~.
Qed. 

charguer's avatar
charguer committed
611
Arguments xval_htop_evar [A].
charguer's avatar
charguer committed
612 613 614 615 616 617 618 619 620 621 622

Lemma xval_htop_lemma : forall A (V:A) (EA:Enc A) v H Q,
  v = enc V ->
  H ==> Q V \* \Top ->
  Local (Cf_val v) H Q.
Proof using.
  introv E M. unfold Cf_val.
  applys~ local_htop_post (Q \*+ \Top).
  applys local_erase. exists~ V.
Qed. 

charguer's avatar
charguer committed
623
Arguments xval_htop_lemma [A].
charguer's avatar
charguer committed
624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639

(* TODO; simplify proof of original xval_htop_lemma in LambdaCF *)

Lemma xval_htop_as_lemma : forall A (V:A) (EA:Enc A) v H Q,
  v = enc V ->
  (forall (x:A), x = V -> H ==> Q x \* \Top) ->
  Local (Cf_val v) H Q.
Proof using. intros. applys* xval_htop_lemma. Qed. 

Ltac xval_basic tt ::=
  match goal with
  | |- Local ?F ?H ?Q => is_evar Q; applys xval_htop_evar; [ try xeq_enc ]
  | _ => applys xval_htop_lemma; [ try xeq_enc | ]
  end.
(* TODO: should we force the ?F to be a Cf_val ?*)

charguer's avatar
charguer committed
640 641 642

(* warning : all below are modified copy-paste  *)

charguer's avatar
charguer committed
643 644 645
(* TODO: better factorization of the code by using an auxiliary function
   to test whether the head is a Local Cf_val or something else *)

charguer's avatar
charguer committed
646 647 648 649 650 651 652 653 654 655 656
Ltac xval_template xlet_tactic xval_tactic xlet_cont ::=
  match goal with
  | |- Local (Cf_let _ _) _ _ => xlet_tactic tt; [ xval_tactic tt | xlet_cont tt ]
  | |- Local (Cf_if _ _ _) _ _ => xlet_tactic tt; [ xval_tactic tt | xlet_cont tt ]
  | _ => xval_tactic tt
  end.


(*--------------------------------------------------------*)
(* ** [xvals ] *)

charguer's avatar
cleanup  
charguer committed
657 658 659 660 661 662 663 664 665 666
Ltac xvals_core tt ::=
  match goal with
  | |- Local (Cf_val _) _ _ => xval_basic tt; hsimpl
  | _ => xval_template ltac:(fun tt => xlet) ltac:(xval_basic) ltac:(xapps_let_cont)
  end.


(*--------------------------------------------------------*)
(* ** [xval as ] *)

charguer's avatar
charguer committed
667 668
Ltac xval_as_basic X EX ::=
  match goal with
charguer's avatar
charguer committed
669
  | |- Local ?F ?H ?Q => is_evar Q; applys local_erase; applys refl_rel_incl'
charguer's avatar
charguer committed
670 671 672
  | _ => applys xval_htop_as_lemma; intros X EX
  end.

charguer's avatar
charguer committed
673 674 675
Ltac xval_as_core X ::=
  match goal with
  | |- Local (Cf_val _) _ _ => let EX := fresh "E" X in xval_as_basic X EX
charguer's avatar
charguer committed
676
  | _ => xval_template ltac:(fun tt => xlet as X) ltac:(xval_basic) ltac:(xapp_as_let_cont)
charguer's avatar
charguer committed
677 678
  end.

charguer's avatar
charguer committed
679

charguer's avatar
cleanup  
charguer committed
680 681
(*--------------------------------------------------------*)
(* ** [xval V] *)
charguer's avatar
charguer committed
682 683 684 685 686 687 688 689 690 691 692 693 694

Ltac xval_arg V :=
  match goal with
  | |- Local ?F ?H ?Q => is_evar Q; applys xval_htop_evar; [ try reflexivity ]
  | _ => applys (xval_htop_lemma V); [ try reflexivity | ]
  end.

Tactic Notation "xval" constr(V) := 
  xval_arg V.

(*todo: [xvals V] *)


charguer's avatar
cleanup  
charguer committed
695 696
(*--------------------------------------------------------*)
(* ** [xlet] *)
charguer's avatar
xapps  
charguer committed
697

charguer's avatar
cleanup  
charguer committed
698 699 700
(* Playing some tricks with the identity function to prevent undesired eager typeclass resolution *)
(* TODO: should no longer be needed *)

charguer's avatar
rename  
charguer committed
701
Lemma Cf_let_intro' : forall A1 (EA1:id Enc A1) (Q1:A1->hprop) (F1 : Formula) (F2of : forall A1 `{EA1:Enc A1}, A1 -> Formula),
charguer's avatar
cleanup  
charguer committed
702 703 704 705 706
  forall A (EA:id Enc A) H (Q:A->hprop),
  F1 A1 EA1 H Q1 ->
  (forall (X:A1), (@F2of A1 EA1 X) A EA (Q1 X) Q) ->
  (Cf_let F1 (@F2of)) A EA H Q.
Proof using. intros. hnf. exists A1 EA1 Q1. auto. Qed.
charguer's avatar
charguer committed
707

charguer's avatar
rename  
charguer committed
708
Lemma Cf_let_intro : forall A1 (EA1:Enc A1) (Q1:A1->hprop) (F1 : Formula) (F2of : forall A1 `{EA1:Enc A1}, A1 -> Formula),
charguer's avatar
cleanup  
charguer committed
709 710
  forall A (EA:Enc A) H (Q:A->hprop),
  'F1 H Q1 ->
charguer's avatar
ok  
charguer committed
711
  (forall (X:A1), '(F2of A1 X) (Q1 X) Q) ->
charguer's avatar
cleanup  
charguer committed
712 713
  '(Cf_let F1 F2of) H Q.
Proof using. intros. hnf. exists A1 EA1 Q1. auto. Qed.
charguer's avatar
charguer committed
714

charguer's avatar
cleanup  
charguer committed
715
Ltac xlet_untyped_core tt := 
charguer's avatar
stable  
charguer committed
716
  applys local_erase; eapply @Cf_let_intro'.
charguer's avatar
charguer committed
717

charguer's avatar
cleanup  
charguer committed
718
Ltac xlet_typed_core tt := 
charguer's avatar
stable  
charguer committed
719
  applys local_erase; esplit; split.
charguer's avatar
cleanup  
charguer committed
720 721 722 723 724 725 726 727

Ltac xlet_core tt ::=
  match goal with
  | |- Local (Cf_let _ _) _ _ => xlet_untyped_core tt
  | |- Local (Cf_let_typed _ _) _ _ => xlet_typed_core tt
  | |- Local (Cf_if _ _ _) _ _ => xlet_typed_core tt
  end.

charguer's avatar
xapps  
charguer committed
728

charguer's avatar
cleanup  
charguer committed
729 730
(*--------------------------------------------------------*)
(* ** xif *)
charguer's avatar
xapps  
charguer committed
731

charguer's avatar
ok  
charguer committed
732
(*
charguer's avatar
cleanup  
charguer committed
733 734 735
Ltac xif_core tt ::=
  applys local_erase; 
  applys Cf_if_val_bool;
charguer's avatar
charguer committed
736
  rew_istrue.
charguer's avatar
ok  
charguer committed
737
*)
charguer's avatar
cleanup  
charguer committed
738
  (* applys Cf_if_val_isTrue ;=> C. *)
charguer's avatar
charguer committed
739 740


charguer's avatar
cleanup  
charguer committed
741 742
(*--------------------------------------------------------*)
(* ** [xfail] *)
charguer's avatar
charguer committed
743

charguer's avatar
cleanup  
charguer committed
744 745 746 747 748 749
Ltac xfail_core tt ::=
  applys local_erase; unfold Cf_fail.


(*--------------------------------------------------------*)
(* ** xapp *)
charguer's avatar
xapps  
charguer committed
750

charguer's avatar
cleanup  
charguer committed
751 752 753 754
(* Remark:
  Ltac xapply_core H cont1 cont2 :=
    forwards_nounfold_then H ltac:(fun K =>
      match xpostcondition_is_evar tt with
charguer's avatar
charguer committed
755
      | true => eapply local_frame; [ xlocal | sapply K | cont1 tt | try apply refl_rel_incl' ]
charguer's avatar
cleanup  
charguer committed
756 757 758 759
      | false => eapply local_frame_htop; [ xlocal | sapply K | cont1 tt | cont2 tt ]
      end).
*)

charguer's avatar
ok  
charguer committed
760
Ltac xapp_xapply E cont_post ::=
charguer's avatar
charguer committed
761 762
  match goal with
  | |- ?F ?H ?Q => is_evar Q; xapplys E
charguer's avatar
charguer committed
763 764 765 766 767
  | |- ?F ?H (fun (_:unit) => ?H') => is_evar H'; xapplys E (* TODO: is needed? *)
  | _ =>  
     first [ xapply_core E ltac:(fun tt => solve [ hcancel ]) ltac:(cont_post)
           | xapply_core E ltac:(idcont) ltac:(idcont) ]
    (* DEPRECATED xapply_core E ltac:(fun tt => hcancel) ltac:(cont_post)  *)
charguer's avatar
charguer committed
768
  end.
charguer's avatar
charguer committed
769

charguer's avatar
charguer committed
770

charguer's avatar
ok  
charguer committed
771
(* todo: factorize using a "remove local" tactic *)
charguer's avatar
stable  
charguer committed
772 773
Ltac xapp_basic_prepare tt ::=
  unfold Cf_app;
charguer's avatar
ok  
charguer committed
774
  try match goal with |- @Local _ _ _ _ _ => apply local_erase end;
charguer's avatar
charguer committed
775 776
  rew_nary;
  try xdecode_args tt.
charguer's avatar
xapps  
charguer committed
777

charguer's avatar
cleanup  
charguer committed
778 779 780
Ltac xapp_template xlet_tactic xapp_tactic xlet_cont ::=
  match goal with
  | |- Local (Cf_let _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | xlet_cont tt ]
charguer's avatar
cleanup  
charguer committed
781
  | |- Local (Cf_let_typed _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | xlet_cont tt ]
charguer's avatar
cleanup  
charguer committed
782 783 784 785
  | |- Local (Cf_if _ _ _) _ _ => xlet_tactic tt; [ xapp_tactic tt | xlet_cont tt ]
  | |- Local (Cf_seq _ _) _ _ => xseq; [ xapp_tactic tt | ]
  | _ => xapp_tactic tt
  end.
charguer's avatar
xapps  
charguer committed
786

charguer's avatar
cleanup  
charguer committed
787 788 789
(* TODO: find out why sapply is too slow *)
Ltac fast_apply E :=
  first [ eapply E (* | sapply E *) ].
charguer's avatar
charguer committed
790

charguer's avatar
cleanup  
charguer committed
791 792 793
Ltac xapply_core H cont1 cont2 ::=
  forwards_nounfold_then H ltac:(fun K =>
    match xpostcondition_is_evar tt with
charguer's avatar
charguer committed
794
    | true => eapply local_frame; [ xlocal | fast_apply K | cont1 tt | try apply refl_rel_incl' ]
charguer's avatar
cleanup  
charguer committed
795 796
    | false => eapply local_frame_htop; [ xlocal | fast_apply K | cont1 tt | cont2 tt ]
    end).
charguer's avatar
charguer committed
797

charguer's avatar
charguer committed
798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825

(* ---------------------------------------------------------------------- *)
(* ** Tactic [xwhile] *)

Ltac xpostchange_solve tt :=
  first [ apply PostChange_refl
        | fail 100 "Postcondition not of the expected type" ].

Ltac xformula_typed_elim tt :=
  esplit; split; [ | xpostchange_solve tt ].


Ltac xwhile_template xwhile_tactic xseq_cont ::=
  match goal with
  | |- Local (Cf_seq _ _) _ _ => xseq; [ xwhile_tactic tt | xseq_cont tt ]
  | _ => xwhile_tactic tt
  end.

Ltac xwhile_intros_all R LR HR ::=
  intros R LR HR; 
  change (R) with (R:Formula) in *.

Ltac xwhile_basic xwhile_intros_tactic ::=
  applys local_erase;
  xformula_typed_elim tt;
  xwhile_intros_tactic tt.