CFTactics.v 109 KB
Newer Older
charguer's avatar
init  
charguer committed
1
Set Implicit Arguments.
charguer's avatar
charguer committed
2
Require Import LibCore Shared CFHeaps.
charguer's avatar
charguer committed
3
Require Export (* LibInt *) CFPrint.
charguer's avatar
init  
charguer committed
4

charguer's avatar
demo  
charguer committed
5

charguer's avatar
cp  
charguer committed
6

charguer's avatar
charguer committed
7 8 9 10


(********************************************************************)
(* ** Shared auxiliary functions *)
charguer's avatar
init  
charguer committed
11 12


charguer's avatar
xgc  
charguer committed
13 14 15 16 17 18 19 20 21 22 23 24
(*--------------------------------------------------------*)
(* ** Tools for manipulating pre-conditions *)

(** [cfml_find_hprop_at X] returns the hprop [X ~> T] that
    appears in the pre-condition. *)

Ltac cfml_find_hprop_at X :=
  match goal with |- ?R ?H ?Q =>
  match H with context [ X ~> ?T ] =>
     constr:(X ~> T) end end.


charguer's avatar
init  
charguer committed
25
(*--------------------------------------------------------*)
charguer's avatar
charguer committed
26
(* ** Tools for manipulating post-conditions *)
charguer's avatar
init  
charguer committed
27

charguer's avatar
charguer committed
28 29 30
(** Auxiliary tactic for obtaining a boolean answer
    to the question "is E an evar?". TODO: move to TLC *)

charguer's avatar
demo  
charguer committed
31
Ltac is_evar_as_bool E :=
charguer's avatar
charguer committed
32
  constr:(ltac:(first 
charguer's avatar
demo  
charguer committed
33
    [ is_evar E; exact true 
charguer's avatar
charguer committed
34
    | exact false ])).
charguer's avatar
demo  
charguer committed
35

charguer's avatar
polylet  
charguer committed
36 37 38 39 40 41 42 43 44
(* [cfml_get_precondition tt] returns the current 
   pre-condition. *)

Ltac cfml_get_precondition tt :=
  match goal with |- ?R ?H ?Q => constr:(H) end.

(* [cfml_get_postcondition tt] returns the current 
   pose-condition. *)

charguer's avatar
charguer committed
45
Ltac cfml_get_postcondition tt :=
charguer's avatar
init  
charguer committed
46
  match goal with |- ?E => 
charguer's avatar
demo  
charguer committed
47 48
  match get_fun_arg E with (_,?Q) => constr:(Q) 
  end end.
charguer's avatar
polylet  
charguer committed
49 50
  (* TODO: is this equivalent to: 
     match goal with |- ?J ?Q => constr:(Q) end. *)
charguer's avatar
demo  
charguer committed
51

charguer's avatar
cp  
charguer committed
52
(** [cfml_postcondition_is_evar tt] returns a boolean indicating
charguer's avatar
charguer committed
53
    whether the post-condition of the current goal is an evar. *)
charguer's avatar
init  
charguer committed
54

charguer's avatar
cp  
charguer committed
55
Ltac cfml_postcondition_is_evar tt := 
charguer's avatar
charguer committed
56 57
  let Q := cfml_get_postcondition tt in
  is_evar_as_bool Q.
charguer's avatar
init  
charguer committed
58 59 60


(*--------------------------------------------------------*)
charguer's avatar
PRE  
charguer committed
61
(* ** Auxiliary functions for reasoning on applications/specs *)
charguer's avatar
init  
charguer committed
62

charguer's avatar
charguer committed
63 64
(* [cfml_get_goal_fun] returns the function associated with the 
   [app] or [spec] at the head of the goal. *)
charguer's avatar
init  
charguer committed
65

charguer's avatar
charguer committed
66
Ltac cfml_get_goal_fun tt :=
charguer's avatar
charguer committed
67
  match goal with 
charguer's avatar
charguer committed
68
  | |- spec ?f ?n ?P => constr:(f)
charguer's avatar
charguer committed
69
  | |- app ?f ?xs ?H ?Q => constr:(f)
charguer's avatar
charguer committed
70
  | |- tag tag_apply (app ?f ?xs) ?H ?Q => constr:(f)
charguer's avatar
charguer committed
71
  end.
charguer's avatar
init  
charguer committed
72

charguer's avatar
charguer committed
73 74
(* [cfml_get_goal_arity] returns the arity associated with the 
   [app] or [spec] at the head of the goal. *)
charguer's avatar
init  
charguer committed
75

charguer's avatar
charguer committed
76 77 78 79 80 81 82 83
Ltac cfml_get_goal_arity tt :=
  let aux xs :=
    let n := eval compute in (List.length xs) in constr:(n) in
  match goal with 
  | |- spec ?f ?n ?P => constr:(n)
  | |- app ?f ?xs ?H ?Q => aux xs
  | |- tag tag_apply (app ?f ?xs ?H ?Q) => aux xs
  end .
charguer's avatar
init  
charguer committed
84

charguer's avatar
cp  
charguer committed
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
(* [cfml_show_types_dyn_list L] displays the types of the 
   arguments in the list [L] *)

Ltac cfml_show_types_dyn_list L :=
  match L with
  | nil => idtac
  | (@dyn ?T ?x) :: ?R => idtac T "->"; cfml_show_types_dyn_list R
  end.

(* [cfml_get_app_args E] returns the arguments associated with the 
   [app] in the term [E] provided *)

Ltac cfml_get_app_args E :=
  match E with 
  | app ?f ?xs ?H ?Q => constr:(xs)
  | tag tag_apply (app ?f ?xs) ?H ?Q => constr:(xs)
  end.

(* [cfml_get_goal_app_args tt] returns the arguments associated with the 
   [app] at the head of the goal. *)

Ltac cfml_get_goal_app_args tt :=
  match goal with |- ?G => cfml_get_app_args G end.

(* [cfml_get_goal_app_ret E] returns the arguments associated with the 
   [app] in the term [E] provided. *)

Ltac cfml_get_app_ret E :=
  match E with 
  | @app_def ?f ?xs ?B ?H ?Q => constr:(B)
  | tag tag_apply (@app_def ?f ?xs ?B) ?H ?Q => constr:(B)
  end.

(* [cfml_get_goal_app_ret tt] returns the arguments associated with the 
   [app] at the head of the goal. *)

Ltac cfml_get_goal_app_ret tt :=
  match goal with |- ?G => cfml_get_app_ret G end.

(* [cfml_show_app_type E] displays the type of the
   function application in [E] *)

Ltac cfml_show_app_type E :=
  let L := cfml_get_app_args E in
  cfml_show_types_dyn_list L;
  let B := cfml_get_app_ret E in
  idtac B.

(* [cfml_show_app_type_goal tt] displays the type of 
   the function application in the goal.
   (calls [intros] if needed. *)

Ltac cfml_show_app_type_goal tt :=
  match goal with |- ?G => cfml_show_app_type G end.

(* [cfml_show_app_type_concl S] displays the type of 
   the function application in the conclusion of [S] *)

Ltac cfml_show_app_type_concl S :=
  forwards_nounfold_then S ltac:(fun K =>
    cfml_show_app_type K).


charguer's avatar
charguer committed
148
(********************************************************************)
charguer's avatar
charguer committed
149 150
(* ** Simplification, Automation, and Cleaning  *)

charguer's avatar
charguer committed
151 152 153 154 155 156 157 158 159 160 161 162
(*--------------------------------------------------------*)
(* ** [xcur] *)

(** [xcur] is a convenient way to obtain the current precondition.
    Syntax is: [let H := xcur in ...].

    Example: [let H := xcur in xif (\[= 3] \*+ H) ].
*)

Ltac xcur :=
  cfml_get_precondition tt.

charguer's avatar
charguer committed
163 164 165 166 167 168 169 170 171 172 173

(*--------------------------------------------------------*)
(* ** [xclean] *)

(** [xclean] is a tactic that performs some clean up throughout
    the goal by taking care of:
    - rewriting facts such as [true = isTrue P] into [P]
    - simplifying partially applied equality, e.g. [(= 3) n] to [n = 3].

    See [reflect_clean tt] from the Shared.v file.

charguer's avatar
toutbon  
charguer committed
174
    Remark: this tactic is automatically called by [xpull]. 
charguer's avatar
charguer committed
175 176 177 178 179 180 181 182 183 184 185 186
*)

Ltac xclean_core :=
  reflect_clean tt.

Tactic Notation "xclean" :=
  reflect_clean tt.

(* If [xclean] is too long to type, then use:
  Tactic Notation "x" := xclean.
*)

charguer's avatar
init  
charguer committed
187

charguer's avatar
charguer committed
188

charguer's avatar
init  
charguer committed
189 190 191
(*--------------------------------------------------------*)
(* ** [xauto] *)

charguer's avatar
xwhile  
charguer committed
192
(** [xauto] is a specialized version of [auto] that works
charguer's avatar
charguer committed
193 194 195 196 197 198 199 200 201 202
   well in program verification. 
   
   - it will not attempt any work if the head of the goal
     has a tag (i.e. if it is a characteristif formula),
   - it is able to conclude a goal using [xok]
   - it calls [substs] to substitute all equalities before trying
     to call automation. 
     
   Tactics [xauto], [xauto~] and [xauto*] can be configured 
   independently. 
charguer's avatar
init  
charguer committed
203

charguer's avatar
charguer committed
204 205 206
   [xsimpl~] is equivalent to [xsimpl; xauto~].
   [xsimpl*] is equivalent to [xsimpl; xauto*].
*)
charguer's avatar
init  
charguer committed
207

charguer's avatar
charguer committed
208
Ltac xok_core cont :=  (* see [xok] spec further *)
charguer's avatar
charguer committed
209
  solve [ hnf; apply rel_le_refl
charguer's avatar
charguer committed
210 211 212 213
        | apply pred_le_refl
        | apply hsimpl_to_qunit; reflexivity
        | hsimpl; cont tt ].

charguer's avatar
charguer committed
214
Ltac math_0 ::= xclean. (* TODO: why needed? *)
charguer's avatar
init  
charguer committed
215 216

Ltac xauto_common cont :=
charguer's avatar
array  
charguer committed
217 218 219 220 221 222 223
  first [ 
    cfml_check_not_tagged tt;  
    try solve [ cont tt 
              | solve [ apply refl_equal ]
              | xok_core ltac:(fun _ => solve [ cont tt | substs; cont tt ] ) 
              | substs; if_eq; solve [ cont tt | apply refl_equal ]  ]
  | idtac ].
charguer's avatar
init  
charguer committed
224 225 226 227 228 229 230 231 232 233 234

Ltac xauto_tilde_default cont := xauto_common cont.
Ltac xauto_star_default cont := xauto_common cont.

Ltac xauto_tilde := xauto_tilde_default ltac:(fun _ => auto_tilde).
Ltac xauto_star := xauto_star_default ltac:(fun _ => auto_star). 

Tactic Notation "xauto" "~" := xauto_tilde.
Tactic Notation "xauto" "*" := xauto_star.
Tactic Notation "xauto" := xauto~.

charguer's avatar
charguer committed
235

charguer's avatar
charguer committed
236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254
(*--------------------------------------------------------*)
(* ** [xok] *)

(** [xok] proves a goal of the form [H ==> ?H'] or [Q ===> ?Q']
    by unifying the right-hand-side with the left-hand-side. 

    It also tries to call [hsimpl] to see if it solves the goal. 
    TODO: is this last feature of [xok] useful? *)

Tactic Notation "xok" := 
  xok_core ltac:(idcont).
(* [xok~] and [xok*] defined further *)
Tactic Notation "xok" "~" := 
  xok_core ltac:(fun _ => xauto~).
Tactic Notation "xok" "*" := 
  xok_core ltac:(fun _ => xauto*).



charguer's avatar
charguer committed
255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274
(*--------------------------------------------------------*)
(* ** [xsimpl] *)

(** [xsimpl] performs a heap entailement simplification using 
    [hsimpl], then calls the tactic [xclean] for clean up. *)

Ltac xsimpl_core := hsimpl; xclean.

Tactic Notation "xsimpl" := xsimpl_core. 
Tactic Notation "xsimpl" "~" := xsimpl; xauto~.
Tactic Notation "xsimpl" "*" := xsimpl; xauto*.

(* TODO: factorize below with above *)

Ltac xsimpl_core_with E := hsimpl E; xclean.
Tactic Notation "xsimpl" constr(E) := xsimpl_core_with E. 
Tactic Notation "xsimpl" "~" constr(E) := xsimpl E; xauto~.
Tactic Notation "xsimpl" "*" constr(E) := xsimpl E; xauto*.


charguer's avatar
init  
charguer committed
275 276 277 278 279 280 281 282
Tactic Notation "hsimpl" "~" constr(L) :=
  hsimpl L; xauto~.
Tactic Notation "hsimpl" "~" constr(X1) constr(X2) :=
  hsimpl X1 X2; xauto~.
Tactic Notation "hsimpl" "~" constr(X1) constr(X2) constr(X3) :=
  hsimpl X1 X2 X3; xauto~.


charguer's avatar
charguer committed
283 284 285 286 287 288 289 290 291 292 293 294 295

(*--------------------------------------------------------*)
(* ** [xlocal] *)

(** [xlocal] proves a goal of the form [is_local F]
    or [is_local_pred F], by exploiting the fact that
    - [F] may be of the form [local F']
    - [is_local F] may be an assumption
    - [is_local_pred S] may be an assumption, with [F = S x]
*)

Ltac xlocal_core tt ::=
  first [ assumption
charguer's avatar
charguer committed
296 297
        | apply app_local; (* then prove [xs <> nil] *)
          let E := fresh in intro E; discriminate E
charguer's avatar
charguer committed
298 299
        | apply local_is_local 
        (*| apply app_local_pred  --TODO fix *)
charguer's avatar
charguer committed
300 301 302 303
        | match goal with H: is_local_pred ?S |- is_local (?S _) => apply H end ].



charguer's avatar
charguer committed
304

charguer's avatar
charguer committed
305 306 307 308 309 310 311 312 313
(********************************************************************)
(* ** Tactics for Structural Rules *)


(*--------------------------------------------------------*)
(* ** [xpre] *)

(** [xpre] applies to a goal of the form [F H Q] and 
    allows to strengthen the pre-condition [H].
charguer's avatar
cp  
charguer committed
314
    It produces [F ?H' Q] and [H ==> ?H' \* \GC],
charguer's avatar
charguer committed
315 316 317 318
    where [Hexists HG, HG] can be instantiated with garbage
    to collect. *)

Tactic Notation "xpre" constr(H) :=
charguer's avatar
charguer committed
319
  eapply (@local_gc_pre H); [ try xlocal | xtag_pre_post | ].
charguer's avatar
charguer committed
320 321 322 323 324 325 326


(*--------------------------------------------------------*)
(* ** [xpost] *)

(** [xpost] applies to a goal of the form [F H Q] and 
    allows to weaken the pre-condition [Q].
charguer's avatar
cp  
charguer committed
327 328 329 330 331 332 333 334
    It produces [F H ?Q'] and [?Q' ==> ?Q \* \GC].
    
    [xpost Q'] applies to a goal of the form [F H Q]
    and leaves the goals [F H Q'] and [Q' ===> Q]. 
    
    [xpost H'] is a shorthand for [xpost (#H')].

*)
charguer's avatar
charguer committed
335 336 337 338 339 340 341 342 343 344 345 346


(* Lemma used by [xpost] *)

Lemma xpost_lemma : forall B Q' Q (F:~~B) H,
  is_local F -> 
  F H Q' -> 
  Q' ===> Q ->
  F H Q.
Proof using. intros. applys* local_weaken. Qed.

Tactic Notation "xpost" :=
charguer's avatar
charguer committed
347
  eapply xpost_lemma; [ try xlocal | xtag_pre_post | ].
charguer's avatar
charguer committed
348 349 350 351 352 353 354 355

Lemma fix_post : forall (B:Type) (Q':B->hprop) (F:~~B) (H:hprop) Q,
  is_local F ->
  F H Q' -> 
  Q' ===> Q ->
  F H Q.
Proof. intros. apply* local_weaken. Qed.

charguer's avatar
cp  
charguer committed
356 357 358 359 360 361
Ltac xpost_core Q :=
  let Q' := match type of Q with
    | hprop => constr:(fun (_:unit) => Q)
    | _ => constr:(Q)
    end in
  match cfml_postcondition_is_evar tt with
charguer's avatar
charguer committed
362 363
  | true => apply (@fix_post _ Q'); [ try xlocal | xtag_pre_post | apply rel_le_refl ]
  | false => apply (@fix_post _ Q'); [ try xlocal | xtag_pre_post | ]
charguer's avatar
cp  
charguer committed
364 365
  end.

charguer's avatar
charguer committed
366
Tactic Notation "xpost" constr(Q) := 
charguer's avatar
cp  
charguer committed
367
  xpost_core Q.
charguer's avatar
charguer committed
368 369


charguer's avatar
init  
charguer committed
370
(*--------------------------------------------------------*)
charguer's avatar
toutbon  
charguer committed
371
(* ** [xpull] *)
charguer's avatar
charguer committed
372

charguer's avatar
toutbon  
charguer committed
373
(** [xpull_check_not_needed tt] applies to a goal of the form [F H Q]
charguer's avatar
charguer committed
374
    and raises an error if [H] contains existentials or pure propositions
charguer's avatar
toutbon  
charguer committed
375
    that could have been extracted using [xpull] *)
charguer's avatar
charguer committed
376

charguer's avatar
toutbon  
charguer committed
377
Ltac xpull_check_not_needed tt :=
charguer's avatar
polylet  
charguer committed
378
  let H := cfml_get_precondition tt in
charguer's avatar
toutbon  
charguer committed
379
  hpullable_rec H.
charguer's avatar
charguer committed
380

charguer's avatar
toutbon  
charguer committed
381
(** Auxiliary definitions for [xpull]. *)
charguer's avatar
charguer committed
382

charguer's avatar
toutbon  
charguer committed
383
Ltac xpull_core tt :=
charguer's avatar
charguer committed
384
  match goal with
charguer's avatar
toutbon  
charguer committed
385 386
  | |- _ ==> _ => hpull; xclean
  | |- _ ===> _ => let r := fresh "r" in intros r; hpull; xclean
charguer's avatar
PRE  
charguer committed
387
  | |- _ => simpl; hclean; instantiate
charguer's avatar
charguer committed
388
  end.
charguer's avatar
init  
charguer committed
389

charguer's avatar
toutbon  
charguer committed
390
(** [xpull] extracts existentials and pure propositions from
charguer's avatar
charguer committed
391 392 393 394 395
    the precondition [H] of a goal of the form [F H Q],
    or from the left-hand-side [H] of a goal of the form [H ==> H']
    or [H ===> H']. 
    
    It calls [xclean] which is useful for cleaning up *)
charguer's avatar
init  
charguer committed
396

charguer's avatar
toutbon  
charguer committed
397
Tactic Notation "xpull" := 
charguer's avatar
charguer committed
398
  xpull_core tt; xtag_pre_post.
charguer's avatar
init  
charguer committed
399

charguer's avatar
toutbon  
charguer committed
400
(** [xpulls] calls [xpull], assumes that this call produces
charguer's avatar
charguer committed
401 402 403
   an equality at the head of the goal, and it then substitutes 
   this equality away. *)

charguer's avatar
toutbon  
charguer committed
404 405
Tactic Notation "xpulls" :=
  let E := fresh "TEMP" in xpull; intros E; subst_hyp E.
charguer's avatar
charguer committed
406 407

(** DEPRECATED
charguer's avatar
toutbon  
charguer committed
408
   [xpull as I1 .. IN] should now be written [xpull. => I1 .. IN]
charguer's avatar
charguer committed
409

charguer's avatar
toutbon  
charguer committed
410 411 412 413 414
Tactic Notation "xpull" "as" simple_intropattern(I1) := 
  xpull; intros I1; xclean.
Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) := 
  xpull; intros I1 I2; xclean. 
Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) 
charguer's avatar
charguer committed
415
 simple_intropattern(I3) := 
charguer's avatar
toutbon  
charguer committed
416 417
  xpull; intros I1 I2 I3; xclean.
Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) 
charguer's avatar
charguer committed
418
 simple_intropattern(I3) simple_intropattern(I4) := 
charguer's avatar
toutbon  
charguer committed
419 420
  xpull; intros I1 I2 I3 I4; xclean.
Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) 
charguer's avatar
charguer committed
421
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) := 
charguer's avatar
toutbon  
charguer committed
422 423
  xpull; intros I1 I2 I3 I4 I5; xclean.
Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) 
charguer's avatar
charguer committed
424 425
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) := 
charguer's avatar
toutbon  
charguer committed
426 427
  xpull; intros I1 I2 I3 I4 I5 I6; xclean.
Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) 
charguer's avatar
charguer committed
428 429
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) := 
charguer's avatar
toutbon  
charguer committed
430 431
  xpull; intros I1 I2 I3 I4 I5 I6 I7; xclean.
Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) 
charguer's avatar
charguer committed
432 433
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) := 
charguer's avatar
toutbon  
charguer committed
434 435
  xpull; intros I1 I2 I3 I4 I5 I6 I7 I8; xclean.
Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) 
charguer's avatar
charguer committed
436 437 438
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) 
 simple_intropattern(I9) := 
charguer's avatar
toutbon  
charguer committed
439 440
  xpull; intros I1 I2 I3 I4 I5 I6 I7 I8 I9; xclean.
Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) 
charguer's avatar
charguer committed
441 442 443
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) 
 simple_intropattern(I9) simple_intropattern(I10) := 
charguer's avatar
toutbon  
charguer committed
444
  xpull; intros I1 I2 I3 I4 I5 I6 I7 I8 I9 I10; xclean.
charguer's avatar
charguer committed
445
*)
charguer's avatar
charguer committed
446 447 448


(*--------------------------------------------------------*)
charguer's avatar
cp  
charguer committed
449
(* ** [xgc], [xgc_but], [xgc_all], [xgc_post] *)
charguer's avatar
charguer committed
450

charguer's avatar
charguer committed
451 452 453 454 455 456
(** [xgc H'] applies to a goal of the form [F H Q]
    and substracts [H'] from [H]. 
    
    [xgc_but H'] substracts everything but [H'] from [H].  
    
    [xgc_all] substracts everything from [H], leaving [F \[] Q].
charguer's avatar
cp  
charguer committed
457
    It is equivalent to [xgc_but \[]].
charguer's avatar
charguer committed
458

charguer's avatar
cp  
charguer committed
459 460 461
    [xgc_post] applied to the goal [F H Q] replaces the goal 
    with [F H ?Q'] and [Q' ===> Q \*+ \GC], which allows to 
    perform garbage collection.
charguer's avatar
xgc  
charguer committed
462 463 464 465

    [xgc x] is same as [xgc (x ~> T)] where [T] is read in the pre-condition.

    TODO: [xgc] with several arguments, or a list of arguments.
charguer's avatar
cp  
charguer committed
466
*)
charguer's avatar
charguer committed
467

charguer's avatar
xgc  
charguer committed
468
Ltac xgc_remove_hprop H :=
charguer's avatar
cp  
charguer committed
469
  eapply (@local_gc_pre_on H);
charguer's avatar
charguer committed
470 471
    [ try xlocal
    | hsimpl
charguer's avatar
charguer committed
472
    | xtag_pre_post ].
charguer's avatar
init  
charguer committed
473

charguer's avatar
xgc  
charguer committed
474
Ltac xgc_remove_core X :=
charguer's avatar
toutbon  
charguer committed
475
  xpull_check_not_needed tt;
charguer's avatar
xgc  
charguer committed
476 477 478 479 480 481 482
  match type of X with
  | hprop => xgc_remove_hprop X 
  | _ => let E := cfml_find_hprop_at X in
         xgc_remove_hprop E 
  end.

Ltac xgc_keep_hprop H :=
charguer's avatar
cp  
charguer committed
483
  eapply (@local_gc_pre H);
charguer's avatar
charguer committed
484 485
    [ try xlocal
    | hsimpl
charguer's avatar
charguer committed
486
    | xtag_pre_post ].
charguer's avatar
init  
charguer committed
487

charguer's avatar
xgc  
charguer committed
488
Ltac xgc_keep_core X :=
charguer's avatar
toutbon  
charguer committed
489
  xpull_check_not_needed tt;
charguer's avatar
xgc  
charguer committed
490 491 492 493 494 495
  match type of X with
  | hprop => xgc_keep_hprop X 
  | _ => let E := cfml_find_hprop_at X in
         xgc_keep_hprop E 
  end.

charguer's avatar
cp  
charguer committed
496
Ltac xgc_post_core :=
charguer's avatar
toutbon  
charguer committed
497
  xpull_check_not_needed tt;
charguer's avatar
cp  
charguer committed
498
  eapply local_gc_post; 
charguer's avatar
charguer committed
499
  [ try xlocal | | xtag_pre_post ].
charguer's avatar
cp  
charguer committed
500

charguer's avatar
charguer committed
501 502
Tactic Notation "xgc" constr(H) := 
  xgc_remove_core H.
charguer's avatar
charguer committed
503

charguer's avatar
charguer committed
504 505
Tactic Notation "xgc_but" constr(H) := 
  xgc_keep_core H.
charguer's avatar
charguer committed
506

charguer's avatar
cp  
charguer committed
507 508 509
Tactic Notation "xgc_post" := 
  xgc_post_core.

charguer's avatar
lists  
charguer committed
510 511
(* DEPRECATED
Ltac xgc_post_if_not_evar_then cont :=
charguer's avatar
cp  
charguer committed
512
  match cfml_postcondition_is_evar tt with
charguer's avatar
lists  
charguer committed
513 514
  | true => cont tt
  | false => xgc_post; [ cont tt | ]
charguer's avatar
cp  
charguer committed
515
  end.
charguer's avatar
lists  
charguer committed
516
*)
charguer's avatar
cp  
charguer committed
517 518 519 520 521 522 523 524

(* Lemma used by [xgc_all], to remove everything from the 
   pre-condition *)

Lemma local_gc_pre_all : forall B Q (F:~~B) H,
  is_local F -> 
  F \[] Q ->
  F H Q.
charguer's avatar
charguer committed
525
Proof using. intros. apply* (@local_gc_pre_on H). hsimpl. Qed.
charguer's avatar
charguer committed
526

charguer's avatar
charguer committed
527
Tactic Notation "xgc_all" := 
charguer's avatar
charguer committed
528
  eapply local_gc_pre_all; [ try xlocal | xtag_pre_post ].
charguer's avatar
charguer committed
529 530


charguer's avatar
cp  
charguer committed
531

charguer's avatar
init  
charguer committed
532
(*--------------------------------------------------------*)
charguer's avatar
charguer committed
533
(* ** [xframe] and [xframe_but] and [xframe_on] *)
charguer's avatar
init  
charguer committed
534

charguer's avatar
charguer committed
535 536
(** [xframe H'] applies to a goal of the form [F H Q]
    and substracts [H'] from both [H] and [Q].
charguer's avatar
charguer committed
537

charguer's avatar
charguer committed
538
    [xframe_but H'] substracts everything but [H']. *)
charguer's avatar
init  
charguer committed
539

charguer's avatar
charguer committed
540
(* Lemma used by [xframe] *)
charguer's avatar
init  
charguer committed
541

charguer's avatar
charguer committed
542 543 544 545 546 547
Lemma xframe_lemma : forall H1 H2 B Q1 (F:~~B) H Q,
  is_local F -> 
  H ==> H1 \* H2 -> 
  F H1 Q1 -> 
  Q1 \*+ H2 ===> Q ->
  F H Q.
charguer's avatar
cp  
charguer committed
548
Proof using. intros. apply* local_frame. Qed.
charguer's avatar
init  
charguer committed
549

charguer's avatar
charguer committed
550
Ltac xframe_remove_core H :=
charguer's avatar
toutbon  
charguer committed
551
  xpull_check_not_needed tt;
charguer's avatar
charguer committed
552 553 554
  eapply xframe_lemma with (H2 := H);
    [ try xlocal
    | hsimpl
charguer's avatar
charguer committed
555
    | xtag_pre_post
charguer's avatar
charguer committed
556
    | ].
charguer's avatar
init  
charguer committed
557

charguer's avatar
charguer committed
558 559
Tactic Notation "xframe" constr(H) := 
  xframe_remove_core H.
charguer's avatar
init  
charguer committed
560

charguer's avatar
charguer committed
561
Ltac xframe_keep_core H :=
charguer's avatar
toutbon  
charguer committed
562
  xpull_check_not_needed tt;
charguer's avatar
charguer committed
563 564 565
  eapply xframe_lemma with (H1 := H);
    [ try xlocal
    | hsimpl
charguer's avatar
charguer committed
566
    | xtag_pre_post
charguer's avatar
charguer committed
567
    | ].
charguer's avatar
init  
charguer committed
568

charguer's avatar
charguer committed
569 570
Tactic Notation "xframe_but" constr(H) := 
  xframe_keep_core H.
charguer's avatar
init  
charguer committed
571 572


charguer's avatar
charguer committed
573 574 575 576
(** [xframe_on p] applies to a goal of the form [F H Q]
    and calls [xframe (p ~> M)], where [M] is guessed 
    from the occurence of [p ~> M] that can be found in
    the pre-condition [H].
charguer's avatar
charguer committed
577

charguer's avatar
charguer committed
578
    Variants: [xframe_on p1 p2] and [xframe_on p1 p2 p3]. *)
charguer's avatar
init  
charguer committed
579

charguer's avatar
charguer committed
580 581 582 583
Ltac xframes_core_1 s := 
  match goal with |- ?R ?H ?Q =>
    match H with context [ s ~> ?M ] =>
      xframe (s ~> M) end end.
charguer's avatar
init  
charguer committed
584

charguer's avatar
charguer committed
585 586
Tactic Notation "xframes" constr(s1) := 
  xframes_core_1 s1.
charguer's avatar
init  
charguer committed
587

charguer's avatar
charguer committed
588 589 590 591 592
Ltac xframes_core_2 s1 s2 := 
  match goal with |- ?R ?H ?Q =>
    match H with context [ s1 ~> ?M1 ] =>
      match H with context [ s2 ~> ?M2 ] =>
        xframe (s1 ~> M1 \* s2 ~> M2) end end end.
charguer's avatar
init  
charguer committed
593

charguer's avatar
charguer committed
594 595
Tactic Notation "xframes" constr(s1) constr(s2) := 
  xframes_core_2 s1 s2.
charguer's avatar
init  
charguer committed
596

charguer's avatar
charguer committed
597 598 599 600 601 602 603
Ltac xframes_core_3 s1 s2 s3 := 
  match goal with |- ?R ?H ?Q =>
    match H with context [ s1 ~> ?M1 ] =>
      match H with context [ s2 ~> ?M2 ] =>
        match H with context [ s3 ~> ?M3 ] =>
          xframe (s1 ~> M1 \* s2 ~> M2 \* s3 ~> M3) 
  end end end end.
charguer's avatar
charguer committed
604

charguer's avatar
charguer committed
605 606
Tactic Notation "xframes" constr(s1) constr(s2) constr(s3) := 
  xframes_core_3 s1 s2 s3.
charguer's avatar
charguer committed
607

charguer's avatar
init  
charguer committed
608 609

(*--------------------------------------------------------*)
charguer's avatar
charguer committed
610
(* ** [xapply] and [xapplys] *)
charguer's avatar
init  
charguer committed
611

charguer's avatar
charguer committed
612 613 614
(** [xapply E] applies a lemma [E] modulo frame/weakening. 
    It applies to a goal of the form [F H Q], and replaces it
    with [F ?H' ?Q'], applies [E] to the goal, then produces
charguer's avatar
cp  
charguer committed
615 616 617
    the side condition [H ==> ?H'] and,
    - if [Q] is instantiated, then leaves [?Q' ===> Q \* \GC]
    - otherwise instantiates [Q] with [Q'].
charguer's avatar
init  
charguer committed
618

charguer's avatar
charguer committed
619 620
    [xapplys E] is like [xapply E] but also attemps to simplify
    the subgoals.
charguer's avatar
xapp  
charguer committed
621
*)
charguer's avatar
init  
charguer committed
622

charguer's avatar
demo3  
charguer committed
623

charguer's avatar
charguer committed
624
Ltac xapply_core H cont1 cont2 :=
charguer's avatar
cp  
charguer committed
625
  forwards_nounfold_then H ltac:(fun K =>
charguer's avatar
demo3  
charguer committed
626 627 628 629
    match cfml_postcondition_is_evar tt with
    | true => eapply local_frame; [ xlocal | sapply K | cont1 tt | try xok ]
    | false => eapply local_frame_gc; [ xlocal | sapply K | cont1 tt | cont2 tt ]
    end).
charguer's avatar
init  
charguer committed
630

charguer's avatar
charguer committed
631
Ltac xapply_base H :=
charguer's avatar
toutbon  
charguer committed
632
  xpull_check_not_needed tt;
charguer's avatar
charguer committed
633
  xapply_core H ltac:(fun tt => idtac) ltac:(fun tt => idtac). 
charguer's avatar
init  
charguer committed
634

charguer's avatar
charguer committed
635
Ltac xapplys_base H :=
charguer's avatar
toutbon  
charguer committed
636
  xpull_check_not_needed tt;
charguer's avatar
charguer committed
637
  xapply_core H ltac:(fun tt => hcancel) ltac:(fun tt => hsimpl). 
charguer's avatar
init  
charguer committed
638

charguer's avatar
charguer committed
639 640 641 642 643 644
Tactic Notation "xapply" constr(H) :=
  xapply_base H.
Tactic Notation "xapply" "~" constr(H) :=
  xapply H; xauto~.
Tactic Notation "xapply" "*" constr(H) :=
  xapply H; xauto*.
charguer's avatar
init  
charguer committed
645

charguer's avatar
charguer committed
646 647 648 649 650 651
Tactic Notation "xapplys" constr(H) :=
  xapplys_base H.
Tactic Notation "xapplys" "~" constr(H) :=
  xapplys H; xauto~.
Tactic Notation "xapplys" "*" constr(H) :=
  xapplys H; xauto*.
charguer's avatar
init  
charguer committed
652

charguer's avatar
xapp  
charguer committed
653 654 655 656 657 658 659 660 661 662 663
(* -- commented out for faster compilation
Lemma xapply_demo_1 : forall B R H H' (Q:B->hprop),
  is_local R ->
  R H Q ->
  R (H \* H') (Q \*+ H').
Proof using.
  introv HR M. dup 2.
  { xapply M. xsimpl. xsimpl. }
  { xapplys M. }
Qed.
*)
charguer's avatar
init  
charguer committed
664

charguer's avatar
charguer committed
665 666
(*--------------------------------------------------------*)
(* ** [xchange] *)
charguer's avatar
init  
charguer committed
667

charguer's avatar
charguer committed
668 669 670 671 672 673 674 675
(** [xchange E] applies to a goal of the form [F H Q]
    and to a lemma [E] of type [H1 ==> H2] or [H1 = H2]. 
    It replaces the goal with [F H' Q], where [H']
    is computed by replacing [H1] with [H2] in [H].
    
    The substraction is computed by solving [H ==> H1 \* ?H']
    with [hsimpl]. If you need to solve this implication by hand,
    use [xchange_no_simpl E] instead.
charguer's avatar
init  
charguer committed
676

charguer's avatar
charguer committed
677 678
    [xchange <- E] is useful when [E] has type [H2 = H1]
      instead of [H1 = H2].
charguer's avatar
init  
charguer committed
679

charguer's avatar
charguer committed
680 681 682
    [xchange_show E] is useful to visualize the instantiation
    of the lemma used to implement [xchange].
    *)
charguer's avatar
charguer committed
683

charguer's avatar
charguer committed
684
(* Lemma used by [xchange] *)
charguer's avatar
charguer committed
685

charguer's avatar
charguer committed
686 687 688 689 690 691 692
Lemma xchange_lemma : forall H1 H1' H2 B H Q (F:~~B),
  is_local F -> 
  (H1 ==> H1') -> 
  (H ==> H1 \* H2) -> 
  F (H1' \* H2) Q -> 
  F H Q.
Proof using.
charguer's avatar
cp  
charguer committed
693
  introv W1 L W2 M. applys local_frame __ \[]; eauto.
charguer's avatar
charguer committed
694 695
  hsimpl. hchange~ W2. hsimpl~. rew_heap~. 
Qed.
charguer's avatar
charguer committed
696

charguer's avatar
charguer committed
697 698
Ltac xchange_apply L cont :=
   eapply xchange_lemma; 
charguer's avatar
charguer committed
699
     [ try xlocal | applys L | cont tt | xtag_pre_post ].
charguer's avatar
init  
charguer committed
700

charguer's avatar
charguer committed
701 702 703 704 705 706 707 708 709 710 711 712
  (* note: modif should be himpl_proj1 or himpl_proj2 
     ---what does this mean? *)
Ltac xchange_forwards L modif cont :=
  forwards_nounfold_then L ltac:(fun K =>
  match modif with
  | __ => 
     match type of K with
     | _ = _ => xchange_apply (@pred_le_proj1 _ _ _ K) cont
     | _ => xchange_apply K cont
     end
  | _ => xchange_apply (@modif _ _ _ K) cont
  end).
charguer's avatar
init  
charguer committed
713

charguer's avatar
charguer committed
714 715
Ltac xchange_with_core cont H H' :=
  eapply xchange_lemma with (H1:=H) (H1':=H'); 
charguer's avatar
charguer committed
716
    [ try xlocal | | cont tt | xtag_pre_post ].
charguer's avatar
init  
charguer committed
717

charguer's avatar
charguer committed
718 719 720 721 722
Ltac xchange_core cont E modif :=
  match E with
  | ?H ==> ?H' => xchange_with_core cont H H'
  | _ => xchange_forwards E modif ltac:(fun _ => instantiate; cont tt)
  end.
charguer's avatar
init  
charguer committed
723

charguer's avatar
charguer committed
724
Ltac xchange_base cont E modif :=
charguer's avatar
toutbon  
charguer committed
725
  xpull_check_not_needed tt;
charguer's avatar
charguer committed
726 727 728 729 730
  match goal with
  | |- _ ==> _ => hchange_base E modif
  | |- _ ===> _ => hchange_base E modif
  | _ => xchange_core cont E modif
  end.
charguer's avatar
init  
charguer committed
731

charguer's avatar
charguer committed
732 733 734 735 736 737
Tactic Notation "xchange" constr(E) :=
  xchange_base ltac:(fun tt => hsimpl) E __.
Tactic Notation "xchange" "~" constr(E) :=
  xchange E; xauto~.
Tactic Notation "xchange" "*" constr(E) :=
  xchange E; xauto*.
charguer's avatar
init  
charguer committed
738

charguer's avatar
charguer committed
739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754
Tactic Notation "xchange" "<-" constr(E) :=
  xchange_base ltac:(fun tt => hsimpl) E pred_le_proj2.
Tactic Notation "xchange" "~" "<-" constr(E) :=
  xchange <- E; xauto~.
Tactic Notation "xchange" "*" "<-" constr(E) :=
  xchange <- E; xauto*.

Tactic Notation "xchange_no_simpl" constr(E) :=
  xchange_base ltac:(fun tt => idtac) E __.
Tactic Notation "xchange_no_simpl" "<-" constr(E) :=
  xchange_base ltac:(fun tt => idtac) E pred_le_proj2.

Tactic Notation "xchange_show" constr(E) :=
  xchange_forwards E __ ltac:(idcont).
Tactic Notation "xchange_show" "<-" constr(E) :=
  xchange_forwards pred_le_proj2 ltac:(idcont).
charguer's avatar
init  
charguer committed
755 756


charguer's avatar
charguer committed
757
(* DEPRECATED: 
charguer's avatar
init  
charguer committed
758

charguer's avatar
charguer committed
759 760
Tactic Notation "xchange" "->" constr(E) :=
  xchange_base ltac:(fun tt => hsimpl) E pred_le_proj1.
charguer's avatar
init  
charguer committed
761

charguer's avatar
charguer committed
762
Tactic Notation "xchange" constr(E) "as" := 
charguer's avatar
toutbon  
charguer committed
763
  xchange E; try xpull.
charguer's avatar
charguer committed
764
Tactic Notation "xchange" constr(E) "as" simple_intropattern(I1) := 
charguer's avatar
toutbon  
charguer committed
765
  xchange E; try xpull as I1.
charguer's avatar
charguer committed
766 767
Tactic Notation "xchange" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2) 
  := 
charguer's avatar
toutbon  
charguer committed
768
  xchange E; try xpull as I1 I2.
charguer's avatar
charguer committed
769 770
Tactic Notation "xchange" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) := 
charguer's avatar
toutbon  
charguer committed
771
  xchange E; try xpull as I1 I2 I3.
charguer's avatar
charguer committed
772 773
Tactic Notation "xchange" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) := 
charguer's avatar
toutbon  
charguer committed
774
  xchange E; try xpull as I1 I2 I3 I4. 
charguer's avatar
charguer committed
775 776
Tactic Notation "xchange" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) := 
charguer's avatar
toutbon  
charguer committed
777
  xchange E; try xpull as I1 I2 I3 I4 I5. 
charguer's avatar
init  
charguer committed
778

charguer's avatar
charguer committed
779
Tactic Notation "xchange" "~" constr(E) "as" := 
charguer's avatar
toutbon  
charguer committed
780
  xchange~ E; try xpull.
charguer's avatar
charguer committed
781
Tactic Notation "xchange" "~" constr(E) "as" simple_intropattern(I1) := 
charguer's avatar
toutbon  
charguer committed
782
  xchange~ E; try xpull as I1.
charguer's avatar
charguer committed
783
Tactic Notation "xchange" "~" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2) := 
charguer's avatar
toutbon  
charguer committed
784
  xchange~ E; try xpull as I1 I2.
charguer's avatar
charguer committed
785 786
Tactic Notation "xchange" "~" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) := 
charguer's avatar
toutbon  
charguer committed
787
  xchange~ E; try xpull as I1 I2 I3.
charguer's avatar
charguer committed
788 789
Tactic Notation "xchange" "~" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) := 
charguer's avatar
toutbon  
charguer committed
790
  xchange~ E; try xpull as I1 I2 I3 I4. 
charguer's avatar
charguer committed
791 792
Tactic Notation "xchange" "~" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) := 
charguer's avatar
toutbon  
charguer committed
793
  xchange~ E; try xpull as I1 I2 I3 I4 I5. 
charguer's avatar
ready  
charguer committed
794

charguer's avatar
charguer committed
795
Tactic Notation "xchange" "*" constr(E) "as" := 
charguer's avatar
toutbon  
charguer committed
796
  xchange* E; try xpull.
charguer's avatar
charguer committed
797
Tactic Notation "xchange" "*" constr(E) "as" simple_intropattern(I1) := 
charguer's avatar
toutbon  
charguer committed
798
  xchange* E; try xpull as I1.
charguer's avatar
charguer committed
799
Tactic Notation "xchange" "*" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2) := 
charguer's avatar
toutbon  
charguer committed
800
  xchange* E; try xpull as I1 I2.
charguer's avatar
charguer committed
801 802
Tactic Notation "xchange" "*" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) := 
charguer's avatar
toutbon  
charguer committed
803
  xchange* E; try xpull as I1 I2 I3.
charguer's avatar
charguer committed
804 805
Tactic Notation "xchange" "*" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) := 
charguer's avatar
toutbon  
charguer committed
806
  xchange* E; try xpull as I1 I2 I3 I4. 
charguer's avatar
charguer committed
807 808
Tactic Notation "xchange" "*" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) := 
charguer's avatar
toutbon  
charguer committed
809
  xchange* E; try xpull as I1 I2 I3 I4 I5.
charguer's avatar
init  
charguer committed
810

charguer's avatar
charguer committed
811
*)
charguer's avatar
init  
charguer committed
812

charguer's avatar
charguer committed
813 814 815 816 817 818
(* DEPRECATED: chaining xchange operations.
Tactic Notation "xchange" constr(E1) constr(E2) :=
  xchange E1; xchange E2.
Tactic Notation "xchange" constr(E1) constr(E2) constr(E3) :=
  xchange E1; xchange E2 E3.
*)
charguer's avatar
init  
charguer committed
819

charguer's avatar
charguer committed
820

charguer's avatar
charguer committed
821
(************************************************************)
charguer's avatar
xwhile  
charguer committed
822
(* ** [xopen] *)
charguer's avatar
init  
charguer committed
823

charguer's avatar
xwhile  
charguer committed
824
(** [xopen] is a tactic for applying [xchange] without having
charguer's avatar
charguer committed
825
    to explicitly specify the name of a focusing lemma.
charguer's avatar
charguer committed
826

charguer's avatar
xwhile  
charguer committed
827
    [xopen p] applies to a goal of the form 
charguer's avatar
charguer committed
828 829 830 831
    [F H Q] or [H ==> H'] or [Q ===> Q'].
    It first searches for the pattern [p ~> T] in the pre-condition,
    then looks up in a database for the focus lemma [E] associated with
    the form [T], and then calls [xchange E].
charguer's avatar
charguer committed
832

charguer's avatar
xwhile  
charguer committed
833
    [xopen_show p] shows the lemma found, it is useful for debugging.
charguer's avatar
charguer committed
834 835
   
    Example for registering a focusing lemma:
charguer's avatar
charguer committed
836 837
      Hint Extern 1 (RegisterOpen (Tree _)) => Provide tree_open.
    See [Demo_proof.v] for examples.
charguer's avatar
ready  
charguer committed
838

charguer's avatar
xwhile  
charguer committed
839
    Then, use: [xopen p].
charguer's avatar
xfocus  
charguer committed
840 841
    
    Variants:
charguer's avatar
toutbon  
charguer committed
842
    - [xopenx t]  is short for [xopen t; xpull] 
charguer's avatar
array  
charguer committed
843

charguer's avatar
toutbon  
charguer committed
844
    - [xopenxs t]  is short for [xopen t; xpulls]  // EXPERIMENTAL
charguer's avatar
array  
charguer committed
845

charguer's avatar
xwhile  
charguer committed
846 847
    - [xopen2 p] to perform [xopen p] twice. Only applies when there
      is no existentials to be extracted after the first [xopen].
charguer's avatar
array  
charguer committed
848 849

*)
charguer's avatar
ready  
charguer committed
850

charguer's avatar
charguer committed
851 852 853 854 855 856 857
Ltac get_refocus_args tt :=
  match goal with 
  | |- ?Q1 ===> ?Q2 => constr:(Q1,Q2)
  | |- ?H1 ==> ?H2 => constr:(H1,H2)
  | |- ?R ?H1 ?Q2 => constr:(H1,Q2)
  (* TODO: gérer le cas de fonctions appliquées à R *)
  end.
charguer's avatar
charguer committed
858

charguer's avatar
charguer committed
859 860
Ltac get_refocus_constr_in H t :=
  match H with context [ t ~> ?T ] => constr:(T) end.
charguer's avatar
init  
charguer committed
861

charguer's avatar
xwhile  
charguer committed
862
Ltac xopen_constr t :=
charguer's avatar
charguer committed
863 864
  match get_refocus_args tt with (?H1,?H2) =>
  get_refocus_constr_in H1 t end.
charguer's avatar
charguer committed
865

charguer's avatar
xwhile  
charguer committed
866 867
Ltac xopen_core t :=
  let C1 := xopen_constr t in
charguer's avatar
charguer committed
868
  ltac_database_get database_xopen C1;
charguer's avatar
charguer committed
869 870
  let K := fresh "TEMP" in
  intros K; xchange (K t); clear K.
charguer's avatar
charguer committed
871

charguer's avatar
xwhile  
charguer committed
872 873 874
Ltac xopen_show_core t := 
  let C1 := xopen_constr t in
  pose C1; 
charguer's avatar
charguer committed
875
  try ltac_database_get database_xopen C1; 
charguer's avatar
xwhile  
charguer committed
876 877 878 879
  intros.

Tactic Notation "xopen_show" constr(t) :=
  xopen_show_core t.
charguer's avatar
charguer committed
880

charguer's avatar
xwhile  
charguer committed
881 882 883 884 885 886
Tactic Notation "xopen" constr(t) :=
  xopen_core t.
Tactic Notation "xopen" "~" constr(t) :=
  xopen t; xauto~.
Tactic Notation "xopen" "*" constr(t) :=
  xopen t; xauto*.
charguer's avatar
charguer committed
887

charguer's avatar
xwhile  
charguer committed
888 889 890 891 892 893
Tactic Notation "xopen2" constr(x) :=
  xopen x; xopen x.
Tactic Notation "xopen2" "~" constr(x) :=
  xopen2 x; xauto_tilde.
Tactic Notation "xopen2" "*" constr(x) :=
  xopen2 x; xauto_star.
charguer's avatar
xfocus  
charguer committed
894

charguer's avatar
xwhile  
charguer committed
895
Tactic Notation "xopenx" constr(t) :=
charguer's avatar
toutbon  
charguer committed
896
  xopen t; xpull.
charguer's avatar
array  
charguer committed
897

charguer's avatar
xwhile  
charguer committed
898
Tactic Notation "xopenxs" constr(t) :=
charguer's avatar
toutbon  
charguer committed
899
  xopen t; xpulls.
charguer's avatar
array  
charguer committed
900 901


charguer's avatar
xfocus  
charguer committed
902

charguer's avatar
charguer committed
903
(************************************************************)
charguer's avatar
xwhile  
charguer committed
904
(* ** [xclose] *)
charguer's avatar
charguer committed
905

charguer's avatar
xwhile  
charguer committed
906
(** [xclose] is the symmetrical of [xopen]. It works in the 
charguer's avatar
charguer committed
907
    same way, except that it looks for an unfocusing lemma.
charguer's avatar
charguer committed
908

charguer's avatar
xwhile  
charguer committed
909
    [xclose p] applies to a goal of the form 
charguer's avatar
charguer committed
910 911 912 913 914
    [F H Q] or [H ==> H'] or [Q ===> Q'].
    It first searches for the pattern [p ~> T] in the pre-condition,
    then looks up in a database for the unfocus lemma [E] associated with
    the form [T], and then calls [xchange E].
   
charguer's avatar
xwhile  
charguer committed
915
    [xclose_show p] shows the lemma found, it is useful for debugging.
charguer's avatar
charguer committed
916

charguer's avatar
charguer committed
917
    Example for registering a focusing lemma:
charguer's avatar
init  
charguer committed
918

charguer's avatar
charguer committed
919 920
     Hint Extern 1 (RegisterClose (Ref Id (MNode _ _ _))) => 
        Provide tree_node_close.
charguer's avatar
init  
charguer committed
921

charguer's avatar
xwhile  
charguer committed
922
    Then, use: [xclose p]. 
charguer's avatar
xfocus  
charguer committed
923 924
    
    Variants:
charguer's avatar
xwhile  
charguer committed
925 926 927 928

    - [xclose p1 .. pn] is short for [xclose p1; ..; xclose pn]

    - [xclose2 p] to perform [xclose p] twice.
charguer's avatar
xfocus  
charguer committed
929 930

*)
charguer's avatar
init  
charguer committed
931

charguer's avatar
xwhile  
charguer committed
932
Ltac xclose_constr t :=
charguer's avatar
charguer committed
933 934
  match get_refocus_args tt with (?H1,?H2) =>
  get_refocus_constr_in H1 t end.
charguer's avatar
init  
charguer committed
935

charguer's avatar
xwhile  
charguer committed
936 937
Ltac xclose_core t :=
  let C1 := xclose_constr t in
charguer's avatar
charguer committed
938
  ltac_database_get database_xclose C1;
charguer's avatar
charguer committed
939 940
  let K := fresh "TEMP" in
  intros K; xchange (K t); clear K.
charguer's avatar
init  
charguer committed
941

charguer's avatar
xwhile  
charguer committed
942 943 944
Ltac xclose_show_core t := 
  let C1 := xclose_constr t in
  pose C1; 
charguer's avatar
charguer committed
945
  try ltac_database_get database_xclose C1; 
charguer's avatar
xwhile  
charguer committed
946
  intros.
charguer's avatar
charguer committed
947

charguer's avatar
xwhile  
charguer committed
948 949
Tactic Notation "xclose_show" constr(t) :=
  xclose_show_core t.
charguer's avatar
charguer committed
950

charguer's avatar
xwhile  
charguer committed
951 952 953 954 955 956
Tactic Notation "xclose" constr(t) :=
  xclose_core t.
Tactic Notation "xclose" "~" constr(t) :=
  xclose t; xauto~.
Tactic Notation "xclose" "*" constr(t) :=
  xclose t; xauto*.
charguer's avatar
xfocus  
charguer committed