CFTactics.v 98.1 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 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24

(*--------------------------------------------------------*)
(* ** TODO: move to LibTactics.v *)

Inductive ltac_goal_to_discard := ltac_goal_to_discard_intro.

Ltac forwards_nounfold_skip_sides_then S cont :=
  let MARK := fresh in 
  generalize ltac_goal_to_discard_intro; 
  intro MARK;
  forwards_nounfold_then S ltac:(fun K =>
    clear MARK;
    cont K);
  match goal with
  | MARK: ltac_goal_to_discard |- _ => skip 
  | _ => idtac
  end.


charguer's avatar
stdlib  
charguer committed
25 26 27 28 29 30 31
(* [xinduction IH: E X] now accepts for [E] either
   - a proof of [wf R] for [R] of type [A->A->Prop]
   - a binary relation of type [A->A->Prop]
   - a measure of type [A->nat]
 *)
 
Ltac induction_wf_core_then IH E X cont :=
charguer's avatar
cp  
charguer committed
32 33
  let T := type of E in
  let T := eval hnf in T in
charguer's avatar
stdlib  
charguer committed
34 35
  let clearX tt := 
    first [ clear X | fail 3 "the variable on which the induction is done appears in the hypotheses" ] in
charguer's avatar
cp  
charguer committed
36
  match T with
charguer's avatar
stdlib  
charguer committed
37 38 39
  | ?A -> nat =>
     induction_wf_core_then IH (measure_wf E) X cont
     (* TODO: error message might not show up in this case *)
charguer's avatar
cp  
charguer committed
40
  | ?A -> ?A -> Prop =>
charguer's avatar
stdlib  
charguer committed
41
     pattern X; 
charguer's avatar
cp  
charguer committed
42
     first [
charguer's avatar
stdlib  
charguer committed
43 44
       applys well_founded_ind E; 
       clearX tt;
charguer's avatar
cp  
charguer committed
45
       [ change well_founded with wf; auto with wf
charguer's avatar
stdlib  
charguer committed
46
       | intros X IH; cont tt ]
charguer's avatar
cp  
charguer committed
47
     | fail 2 ]
charguer's avatar
stdlib  
charguer committed
48 49 50 51 52 53
  | _ => 
    pattern X; 
    applys well_founded_ind E; 
    clearX tt; 
    intros X IH; 
    cont tt
charguer's avatar
cp  
charguer committed
54 55
  end.

charguer's avatar
stdlib  
charguer committed
56 57 58
Ltac induction_wf_core IH E X :=
  induction_wf_core_then IH E X ltac:(fun _ => idtac).

charguer's avatar
cp  
charguer committed
59 60 61 62 63 64 65 66
Tactic Notation "induction_wf" ident(IH) ":" constr(E) ident(X) :=
  induction_wf_core IH E X.
Tactic Notation "induction_wf" ":" constr(E) ident(X) :=
  let IH := fresh "IH" in induction_wf IH: E X.
Tactic Notation "induction_wf" ":" constr(E) ident(X) :=
  induction_wf: E X.


charguer's avatar
stdlib  
charguer committed
67 68 69 70 71 72 73 74
(* FOR LibList. v *)

Lemma app_eq_prefix_inv_l : forall A (l1 l2 l2' : list A),
  l1 ++ l2 = l1 ++ l2' -> l2 = l2'.
Proof using.
  introv E. induction l1; rew_list in *. auto. inverts* E.
Qed.

charguer's avatar
cp  
charguer committed
75

charguer's avatar
charguer committed
76 77 78
(*--------------------------------------------------------*)
(* ** [=>] and [=>>] tactics for introduction *)

charguer's avatar
charguer committed
79 80 81
(* [=> I1 .. IN] is the same as [intros I1 .. IN] *)

Ltac ltac_intros_post := idtac.
charguer's avatar
charguer committed
82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118

Tactic Notation "=>" :=
  intros.
Tactic Notation "=>" simple_intropattern(I1) :=
  intros I1.
Tactic Notation "=>" simple_intropattern(I1) simple_intropattern(I2) :=
  intros I1 I2.
Tactic Notation "=>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) :=
  intros I1 I2 I3.
Tactic Notation "=>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) :=
  intros I1 I2 I3 I4.
Tactic Notation "=>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) :=
  intros I1 I2 I3 I4 I5.
Tactic Notation "=>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) :=
  intros I1 I2 I3 I4 I5 I6.
Tactic Notation "=>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) :=
  intros I1 I2 I3 I4 I5 I6 I7.
Tactic Notation "=>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) :=
  intros I1 I2 I3 I4 I5 I6 I7 I8.
Tactic Notation "=>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8)
 simple_intropattern(I9) :=
  intros I1 I2 I3 I4 I5 I6 I7 I8 I9.
Tactic Notation "=>" simple_intropattern(I1) simple_intropattern(I2) 
 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
charguer committed
119
  intros I1 I2 I3 I4 I5 I6 I7 I8 I9 I10.
charguer's avatar
init  
charguer committed
120

charguer's avatar
charguer committed
121 122 123 124 125 126
(* [=>>] first introduces all non-dependent variables,
   then behaves as [intros]. It unfolds the head of the goal using [hnf] 
   if there are not head visible quantifiers. 
   
   Remark: instances of [Inhab] are treated as non-dependent and
   are introduced automatically. *)
charguer's avatar
init  
charguer committed
127

charguer's avatar
charguer committed
128 129
Ltac intro_nondeps_aux is_already_hnf := 
  match goal with
charguer's avatar
cp  
charguer committed
130
  | |- (?P -> ?Q) => idtac
charguer's avatar
charguer committed
131
  | |- (Inhab _) -> _ => intro; intro_nondeps_aux true 
charguer's avatar
charguer committed
132
  | |- (forall _,_) => intros ?; intro_nondeps_aux true
charguer's avatar
charguer committed
133 134 135 136 137 138
  | |- _ => 
     match is_already_hnf with
     | true => idtac
     | false => hnf; intro_nondeps_aux true  
     end
  end.
charguer's avatar
init  
charguer committed
139

charguer's avatar
charguer committed
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178
Ltac intro_nondeps tt := intro_nondeps_aux false.

Tactic Notation "=>>" :=
  intro_nondeps tt.
Tactic Notation "=>>" simple_intropattern(I1) :=
  =>>; intros I1.
Tactic Notation "=>>" simple_intropattern(I1) simple_intropattern(I2) :=
  =>>; intros I1 I2.
Tactic Notation "=>>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) :=
  =>>; intros I1 I2 I3.
Tactic Notation "=>>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) :=
  =>>; intros I1 I2 I3 I4.
Tactic Notation "=>>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) :=
  =>>; intros I1 I2 I3 I4 I5.
Tactic Notation "=>>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) :=
  =>>; intros I1 I2 I3 I4 I5 I6.
Tactic Notation "=>>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) :=
  =>>; intros I1 I2 I3 I4 I5 I6 I7.
Tactic Notation "=>>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) :=
  =>>; intros I1 I2 I3 I4 I5 I6 I7 I8.
Tactic Notation "=>>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8)
 simple_intropattern(I9) :=
  =>>; intros I1 I2 I3 I4 I5 I6 I7 I8 I9.
Tactic Notation "=>>" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8)
 simple_intropattern(I9) simple_intropattern(I10) :=
  =>>; intros I1 I2 I3 I4 I5 I6 I7 I8 I9 I10.
charguer's avatar
init  
charguer committed
179 180 181 182 183





charguer's avatar
charguer committed
184
(* ********************************************************************** *)
charguer's avatar
charguer committed
185
(** * Introduction 
charguer's avatar
init  
charguer committed
186

charguer's avatar
charguer committed
187
Section IntrovTest.
charguer's avatar
init  
charguer committed
188

charguer's avatar
charguer committed
189
Variables P1 P2 P3 : nat -> Prop.
charguer's avatar
init  
charguer committed
190

charguer's avatar
charguer committed
191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206
Lemma demo_introv_1 :
  forall a b, P1 a -> P2 b -> forall c d, P3 c -> P1 d -> c = b.
Proof using.
  dup 4.
  (* [introv] introduces all the variables which are not hypotheses,
     more precisely all the variables used dependently. *) 
  introv.
  (* if there is no more head variables, and no definition can 
     be unfolded at head of the goal, it does not do anything *)
  introv. skip.
  (* [introv A] introduces all variables, then does [intros A] *)
  introv A. introv B. introv. intros C D. skip.
  (* [introv] may take several arguments, as illustrated below *)
  introv A B. introv. skip.
  introv A B C D. skip.
Qed.
charguer's avatar
init  
charguer committed
207

charguer's avatar
charguer committed
208

charguer's avatar
charguer committed
209 210
Definition Same (x y : nat) := True -> x = y.
Definition Sym (x:nat) := forall y, x = y -> Same y x.
charguer's avatar
init  
charguer committed
211

charguer's avatar
charguer committed
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226
Lemma demo_introv_2 :
  forall a, Sym a.
Proof using.
  dup 4.
  (* [introv] introduces a variable but no subsequent definition *)
  introv. 
  (* [introv] unfolds definition if no variable is visible *)
  introv. skip.
  (* [introv E] unfolds definitions until finding an hypothesis *)
  introv E. introv F. skip.
  (* [introv E F] unfolds several definitions if needed *)
  introv E F. skip.
  (* [introv] may unfold definition without any introduction *)
  introv E. introv. skip.
Qed.
charguer's avatar
init  
charguer committed
227

charguer's avatar
charguer committed
228 229 230 231 232 233 234 235 236 237 238 239 240 241 242
Lemma demo_introv_3 :
  forall a, a = 0 -> Sym a.
Proof using.
  dup 5. (* more examples *)
  (* introduces [a] only *)
  introv. skip.
  (* introduces [a = 0] *)
  introv E. skip.
  (* introduces [a = 0] and [a = y] *)
  introv E F. skip.
  (* introduces [a = 0] and [a = y] and [True] *)
  introv E F G. skip.
  (* introduction of more names fails *)
  try (introv E F G H). skip.
Qed.
charguer's avatar
charguer committed
243

charguer's avatar
charguer committed
244
Definition TestSym := (forall a, a = 0 -> Sym a).
charguer's avatar
charguer committed
245

charguer's avatar
charguer committed
246 247 248 249 250 251 252 253 254
Lemma demo_introv_4 :
  TestSym.
Proof using.
  dup 2. (* same as before, except the goal itself is a definition *)
  (* introduces [a] only *)
  introv. skip.
  (* introduces [a = 0] *)
  introv E. skip.
Qed.
charguer's avatar
charguer committed
255

charguer's avatar
charguer committed
256 257 258 259 260 261 262 263 264
Lemma demo_introv_5 :
  forall a, a = 0 -> ~ Sym a.
Proof using.
  dup 2. (* playing with negation *)
  (* introduces [a = 0] *)
  introv E. skip.
  (* introduces [a = 0] and [Sym a] *)
  introv E F. skip.
Qed.
charguer's avatar
charguer committed
265

charguer's avatar
charguer committed
266
(* Iterated unfolding to get hypotheses *)
charguer's avatar
charguer committed
267

charguer's avatar
charguer committed
268 269
Definition AllSameAs (x:nat) := forall y, Same y x.
Definition AllSame := forall x, AllSameAs x.
charguer's avatar
init  
charguer committed
270

charguer's avatar
charguer committed
271 272 273 274 275 276 277 278 279
Lemma demo_introv_6 :
  AllSame.
Proof using.
  dup 2. 
  (* introduces only [x], then only [y] *)
  introv. introv. skip.
  (* introduces [x] and [y] and [True] *)
  introv E. skip.
Qed.
charguer's avatar
init  
charguer committed
280

charguer's avatar
charguer committed
281
Definition AllSameAgain := AllSame.
charguer's avatar
init  
charguer committed
282

charguer's avatar
charguer committed
283 284 285 286 287 288 289 290 291
Lemma demo_introv_7 :
  AllSameAgain.
Proof using.
  dup 2.  
  (* introduces only [x], then only [y] *)
  introv. introv. skip.
  (* introduces [x] and [y] and [True] *)
  introv E. skip.
Qed.
charguer's avatar
init  
charguer committed
292

charguer's avatar
charguer committed
293 294 295 296 297 298 299 300 301
Lemma demo_introv_8 :
  forall a (c:nat) b, P1 a -> P2 b -> True.
Proof using.
  (* notice that variables which are not used dependently
     are treated as hypotheses, e.g. variable [c] below.
     This might not be the desired behaviour, but that's
     all I'm able to implement in Ltac. *)
  introv c E F. skip.
Qed.
charguer's avatar
init  
charguer committed
302

charguer's avatar
charguer committed
303
Definition IMP P A (x y : A) := P -> x = y.
charguer's avatar
init  
charguer committed
304

charguer's avatar
charguer committed
305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329
Lemma demo_intros_all :
     (forall a b, P1 a -> P2 b -> IMP H1 a b)
  /\ (forall a b, a = 0 -> b = 1 -> ~ (a = b)).
Proof using.
  split.
  (* [intros_all] introduces as many arguments as possible *)
  intros_all. skip.
  intros_all. skip.
Qed.

(* An example showing that [intro] is not very-well
   specified with respect to beta-reduction, explaining
   why [introv] isn't doing better. *)

Definition testing f :=
  forall (x:nat), f x -> True.

Lemma demo_introv_what_to_do : testing (fun a => a = 0).
Proof using.   
  dup.
    intro. skip. (* does beta-reduce f *)
    hnf. intro. skip. (* does not beta-reduce f *)
Qed.

End IntrovTest.
charguer's avatar
charguer committed
330
*)
charguer's avatar
charguer committed
331 332 333 334 335 336




(********************************************************************)
(* ** Shared auxiliary functions *)
charguer's avatar
init  
charguer committed
337 338 339


(*--------------------------------------------------------*)
charguer's avatar
charguer committed
340
(* ** Tools for manipulating post-conditions *)
charguer's avatar
init  
charguer committed
341

charguer's avatar
demo  
charguer committed
342
Ltac is_evar_as_bool E :=
charguer's avatar
charguer committed
343
  constr:(ltac:(first 
charguer's avatar
demo  
charguer committed
344
    [ is_evar E; exact true 
charguer's avatar
charguer committed
345
    | exact false ])).
charguer's avatar
demo  
charguer committed
346

charguer's avatar
charguer committed
347
Ltac cfml_get_postcondition tt :=
charguer's avatar
init  
charguer committed
348
  match goal with |- ?E => 
charguer's avatar
demo  
charguer committed
349 350 351
  match get_fun_arg E with (_,?Q) => constr:(Q) 
  end end.

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

charguer's avatar
cp  
charguer committed
355
Ltac cfml_postcondition_is_evar tt := 
charguer's avatar
charguer committed
356 357
  let Q := cfml_get_postcondition tt in
  is_evar_as_bool Q.
charguer's avatar
init  
charguer committed
358 359 360


(*--------------------------------------------------------*)
charguer's avatar
charguer committed
361
(* ** Tools for [xapp] *)
charguer's avatar
init  
charguer committed
362

charguer's avatar
charguer committed
363 364
(* [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
365

charguer's avatar
charguer committed
366
Ltac cfml_get_goal_fun tt :=
charguer's avatar
charguer committed
367
  match goal with 
charguer's avatar
charguer committed
368
  | |- spec ?f ?n ?P => constr:(f)
charguer's avatar
charguer committed
369
  | |- app ?f ?xs ?H ?Q => constr:(f)
charguer's avatar
charguer committed
370
  | |- tag tag_apply (app ?f ?xs) ?H ?Q => constr:(f)
charguer's avatar
charguer committed
371
  end.
charguer's avatar
init  
charguer committed
372

charguer's avatar
charguer committed
373 374
(* [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
375

charguer's avatar
charguer committed
376 377 378 379 380 381 382 383
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
384 385


charguer's avatar
cp  
charguer committed
386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 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 441 442 443 444 445 446 447 448 449 450 451
(*--------------------------------------------------------*)
(* ** Tools for showing types involved in [app] instances *)

(* [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
init  
charguer committed
452

charguer's avatar
charguer committed
453
(********************************************************************)
charguer's avatar
charguer committed
454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479
(* ** Simplification, Automation, and Cleaning  *)


(*--------------------------------------------------------*)
(* ** [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.

    Remark: this tactic is automatically called by [xextract]. 
*)

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
480

charguer's avatar
charguer committed
481

charguer's avatar
init  
charguer committed
482 483 484 485
(*--------------------------------------------------------*)
(* ** [xauto] *)

(* [xauto] is a specialized version of [auto] that works
charguer's avatar
charguer committed
486 487 488 489 490 491 492 493 494 495
   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
496

charguer's avatar
charguer committed
497 498 499
   [xsimpl~] is equivalent to [xsimpl; xauto~].
   [xsimpl*] is equivalent to [xsimpl; xauto*].
*)
charguer's avatar
init  
charguer committed
500

charguer's avatar
charguer committed
501 502 503 504 505 506
Ltac xok_core cont :=  (* see [xok] spec further *)
  solve [ cbv beta; apply rel_le_refl
        | apply pred_le_refl
        | apply hsimpl_to_qunit; reflexivity
        | hsimpl; cont tt ].

charguer's avatar
charguer committed
507
Ltac math_0 ::= xclean. (* TODO: why needed? *)
charguer's avatar
init  
charguer committed
508 509

Ltac xauto_common cont :=
charguer's avatar
charguer committed
510
  cfml_check_not_tagged tt;  
charguer's avatar
init  
charguer committed
511 512 513 514 515 516 517 518 519 520 521 522 523 524 525
  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 ]  ].

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
526

charguer's avatar
charguer committed
527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545
(*--------------------------------------------------------*)
(* ** [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
546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565
(*--------------------------------------------------------*)
(* ** [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
566 567 568 569 570 571 572 573
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
574 575 576 577 578 579 580 581 582 583 584 585 586

(*--------------------------------------------------------*)
(* ** [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
587 588
        | apply app_local; (* then prove [xs <> nil] *)
          let E := fresh in intro E; discriminate E
charguer's avatar
charguer committed
589 590
        | apply local_is_local 
        (*| apply app_local_pred  --TODO fix *)
charguer's avatar
charguer committed
591 592 593 594
        | match goal with H: is_local_pred ?S |- is_local (?S _) => apply H end ].



charguer's avatar
charguer committed
595

charguer's avatar
charguer committed
596 597 598 599 600 601 602 603 604
(********************************************************************)
(* ** 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
605
    It produces [F ?H' Q] and [H ==> ?H' \* \GC],
charguer's avatar
charguer committed
606 607 608 609
    where [Hexists HG, HG] can be instantiated with garbage
    to collect. *)

Tactic Notation "xpre" constr(H) :=
charguer's avatar
cp  
charguer committed
610
  eapply (@local_gc_pre H); [ try xlocal | | ].
charguer's avatar
charguer committed
611 612 613 614 615 616 617


(*--------------------------------------------------------*)
(* ** [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
618 619 620 621 622 623 624 625
    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
626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646


(* 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" :=
  eapply xpost_lemma; [ try xlocal | | ].

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
647 648 649 650 651 652 653 654 655 656
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
  | true => apply (@fix_post _ Q'); [ try xlocal | | apply rel_le_refl ]
  | false => apply (@fix_post _ Q'); [ try xlocal | | ]
  end.

charguer's avatar
charguer committed
657
Tactic Notation "xpost" constr(Q) := 
charguer's avatar
cp  
charguer committed
658
  xpost_core Q.
charguer's avatar
charguer committed
659 660


charguer's avatar
init  
charguer committed
661
(*--------------------------------------------------------*)
charguer's avatar
charguer committed
662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678
(* ** [xextract] *)

(** [xextract_check_not_needed tt] applies to a goal of the form [F H Q]
    and raises an error if [H] contains existentials or pure propositions
    that could have been extracted using [xextract] *)

Ltac xextract_check_not_needed tt :=
  match goal with |- ?R ?H ?Q => hextractible_rec H end.

(** Auxiliary definitions for [xextract]. *)

Ltac xextract_core :=
  match goal with
  | |- _ ==> _ => hextract; xclean
  | |- _ ===> _ => let r := fresh "r" in intros r; hextract; xclean
  | |- _ => simpl; hclean; instantiate 
  end.
charguer's avatar
init  
charguer committed
679

charguer's avatar
charguer committed
680 681 682 683 684 685
(** [xextract] extracts existentials and pure propositions from
    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
686

charguer's avatar
charguer committed
687 688
Tactic Notation "xextract" := 
  xextract_core; xclean.
charguer's avatar
init  
charguer committed
689

charguer's avatar
charguer committed
690 691 692 693 694 695 696 697
(** [xextracts] calls [xextract], assumes that this call produces
   an equality at the head of the goal, and it then substitutes 
   this equality away. *)

Tactic Notation "xextracts" :=
  let E := fresh "TEMP" in xextract; intros E; subst_hyp E.

(** DEPRECATED
charguer's avatar
charguer committed
698
   [xextract as I1 .. IN] should now be written [xextract. => I1 .. IN]
charguer's avatar
charguer committed
699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734

Tactic Notation "xextract" "as" simple_intropattern(I1) := 
  xextract; intros I1; xclean.
Tactic Notation "xextract" "as" simple_intropattern(I1) simple_intropattern(I2) := 
  xextract; intros I1 I2; xclean. 
Tactic Notation "xextract" "as" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) := 
  xextract; intros I1 I2 I3; xclean.
Tactic Notation "xextract" "as" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) := 
  xextract; intros I1 I2 I3 I4; xclean.
Tactic Notation "xextract" "as" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) := 
  xextract; intros I1 I2 I3 I4 I5; xclean.
Tactic Notation "xextract" "as" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) := 
  xextract; intros I1 I2 I3 I4 I5 I6; xclean.
Tactic Notation "xextract" "as" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) := 
  xextract; intros I1 I2 I3 I4 I5 I6 I7; xclean.
Tactic Notation "xextract" "as" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) := 
  xextract; intros I1 I2 I3 I4 I5 I6 I7 I8; xclean.
Tactic Notation "xextract" "as" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) 
 simple_intropattern(I9) := 
  xextract; intros I1 I2 I3 I4 I5 I6 I7 I8 I9; xclean.
Tactic Notation "xextract" "as" simple_intropattern(I1) simple_intropattern(I2) 
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5)
 simple_intropattern(I6) simple_intropattern(I7) simple_intropattern(I8) 
 simple_intropattern(I9) simple_intropattern(I10) := 
  xextract; intros I1 I2 I3 I4 I5 I6 I7 I8 I9 I10; xclean.
charguer's avatar
charguer committed
735
*)
charguer's avatar
charguer committed
736 737 738


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

charguer's avatar
charguer committed
741 742 743 744 745 746
(** [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
747
    It is equivalent to [xgc_but \[]].
charguer's avatar
charguer committed
748

charguer's avatar
cp  
charguer committed
749 750 751 752
    [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
charguer committed
753

charguer's avatar
charguer committed
754 755
Ltac xgc_remove_core H :=
  xextract_check_not_needed tt;
charguer's avatar
cp  
charguer committed
756
  eapply (@local_gc_pre_on H);
charguer's avatar
charguer committed
757 758 759
    [ try xlocal
    | hsimpl
    | ].
charguer's avatar
init  
charguer committed
760

charguer's avatar
charguer committed
761 762
Ltac xgc_keep_core H :=
  xextract_check_not_needed tt;
charguer's avatar
cp  
charguer committed
763
  eapply (@local_gc_pre H);
charguer's avatar
charguer committed
764 765 766
    [ try xlocal
    | hsimpl
    | ].
charguer's avatar
init  
charguer committed
767

charguer's avatar
cp  
charguer committed
768 769 770 771 772
Ltac xgc_post_core :=
  xextract_check_not_needed tt;
  eapply local_gc_post; 
  [ try xlocal | | ].

charguer's avatar
charguer committed
773 774
Tactic Notation "xgc" constr(H) := 
  xgc_remove_core H.
charguer's avatar
charguer committed
775

charguer's avatar
charguer committed
776 777
Tactic Notation "xgc_but" constr(H) := 
  xgc_keep_core H.
charguer's avatar
charguer committed
778

charguer's avatar
cp  
charguer committed
779 780 781
Tactic Notation "xgc_post" := 
  xgc_post_core.

charguer's avatar
lists  
charguer committed
782 783
(* DEPRECATED
Ltac xgc_post_if_not_evar_then cont :=
charguer's avatar
cp  
charguer committed
784
  match cfml_postcondition_is_evar tt with
charguer's avatar
lists  
charguer committed
785 786
  | true => cont tt
  | false => xgc_post; [ cont tt | ]
charguer's avatar
cp  
charguer committed
787
  end.
charguer's avatar
lists  
charguer committed
788
*)
charguer's avatar
cp  
charguer committed
789 790 791 792 793 794 795 796

(* 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
797
Proof using. intros. apply* (@local_gc_pre_on H). hsimpl. Qed.
charguer's avatar
charguer committed
798

charguer's avatar
charguer committed
799 800
Tactic Notation "xgc_all" := 
  eapply local_gc_pre_all; [ try xlocal | ].
charguer's avatar
charguer committed
801 802


charguer's avatar
cp  
charguer committed
803

charguer's avatar
init  
charguer committed
804
(*--------------------------------------------------------*)
charguer's avatar
charguer committed
805
(* ** [xframe] and [xframe_but] and [xframe_on] *)
charguer's avatar
init  
charguer committed
806

charguer's avatar
charguer committed
807 808
(** [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
809

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

charguer's avatar
charguer committed
812
(* Lemma used by [xframe] *)
charguer's avatar
init  
charguer committed
813

charguer's avatar
charguer committed
814 815 816 817 818 819
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
820
Proof using. intros. apply* local_frame. Qed.
charguer's avatar
init  
charguer committed
821

charguer's avatar
charguer committed
822 823 824 825 826 827 828
Ltac xframe_remove_core H :=
  xextract_check_not_needed tt;
  eapply xframe_lemma with (H2 := H);
    [ try xlocal
    | hsimpl
    | 
    | ].
charguer's avatar
init  
charguer committed
829

charguer's avatar
charguer committed
830 831
Tactic Notation "xframe" constr(H) := 
  xframe_remove_core H.
charguer's avatar
init  
charguer committed
832

charguer's avatar
charguer committed
833 834 835 836 837 838 839
Ltac xframe_keep_core H :=
  xextract_check_not_needed tt;
  eapply xframe_lemma with (H1 := H);
    [ try xlocal
    | hsimpl
    | 
    | ].
charguer's avatar
init  
charguer committed
840

charguer's avatar
charguer committed
841 842
Tactic Notation "xframe_but" constr(H) := 
  xframe_keep_core H.
charguer's avatar
init  
charguer committed
843 844


charguer's avatar
charguer committed
845 846 847 848
(** [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
849

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

charguer's avatar
charguer committed
852 853 854 855
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
856

charguer's avatar
charguer committed
857 858
Tactic Notation "xframes" constr(s1) := 
  xframes_core_1 s1.
charguer's avatar
init  
charguer committed
859

charguer's avatar
charguer committed
860 861 862 863 864
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
865

charguer's avatar
charguer committed
866 867
Tactic Notation "xframes" constr(s1) constr(s2) := 
  xframes_core_2 s1 s2.
charguer's avatar
init  
charguer committed
868

charguer's avatar
charguer committed
869 870 871 872 873 874 875
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
876

charguer's avatar
charguer committed
877 878
Tactic Notation "xframes" constr(s1) constr(s2) constr(s3) := 
  xframes_core_3 s1 s2 s3.
charguer's avatar
charguer committed
879

charguer's avatar
init  
charguer committed
880 881

(*--------------------------------------------------------*)
charguer's avatar
charguer committed
882
(* ** [xapply] and [xapplys] *)
charguer's avatar
init  
charguer committed
883

charguer's avatar
charguer committed
884 885 886
(** [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
887 888 889
    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
890

charguer's avatar
charguer committed
891 892
    [xapplys E] is like [xapply E] but also attemps to simplify
    the subgoals.
charguer's avatar
xapp  
charguer committed
893
*)
charguer's avatar
init  
charguer committed
894

charguer's avatar
charguer committed
895
Ltac xapply_core H cont1 cont2 :=
charguer's avatar
cp  
charguer committed
896
  forwards_nounfold_then H ltac:(fun K =>
charguer's avatar
lists  
charguer committed
897
    eapply local_frame_gc; [ xlocal | sapply K | cont1 tt | cont2 tt ]).
charguer's avatar
init  
charguer committed
898

charguer's avatar
charguer committed
899
Ltac xapply_base H :=
charguer's avatar
charguer committed
900
  xextract_check_not_needed tt;
charguer's avatar
charguer committed
901
  xapply_core H ltac:(fun tt => idtac) ltac:(fun tt => idtac). 
charguer's avatar
init  
charguer committed
902

charguer's avatar
charguer committed
903
Ltac xapplys_base H :=
charguer's avatar
charguer committed
904
  xextract_check_not_needed tt;
charguer's avatar
charguer committed
905
  xapply_core H ltac:(fun tt => hcancel) ltac:(fun tt => hsimpl). 
charguer's avatar
init  
charguer committed
906

charguer's avatar
charguer committed
907 908 909 910 911 912
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
913

charguer's avatar
charguer committed
914 915 916 917 918 919
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
920

charguer's avatar
xapp  
charguer committed
921 922 923 924 925 926 927 928 929 930 931
(* -- 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
932

charguer's avatar
charguer committed
933 934
(*--------------------------------------------------------*)
(* ** [xchange] *)
charguer's avatar
init  
charguer committed
935

charguer's avatar
charguer committed
936 937 938 939 940 941 942 943
(** [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
944

charguer's avatar
charguer committed
945 946
    [xchange <- E] is useful when [E] has type [H2 = H1]
      instead of [H1 = H2].
charguer's avatar
init  
charguer committed
947

charguer's avatar
charguer committed
948 949 950
    [xchange_show E] is useful to visualize the instantiation
    of the lemma used to implement [xchange].
    *)
charguer's avatar
charguer committed
951

charguer's avatar
charguer committed
952
(* Lemma used by [xchange] *)
charguer's avatar
charguer committed
953

charguer's avatar
charguer committed
954 955 956 957 958 959 960
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
961
  introv W1 L W2 M. applys local_frame __ \[]; eauto.
charguer's avatar
charguer committed
962 963
  hsimpl. hchange~ W2. hsimpl~. rew_heap~. 
Qed.
charguer's avatar
charguer committed
964

charguer's avatar
charguer committed
965 966 967
Ltac xchange_apply L cont :=
   eapply xchange_lemma; 
     [ try xlocal | applys L | cont tt | ].
charguer's avatar
init  
charguer committed
968

charguer's avatar
charguer committed
969 970 971 972 973 974 975 976 977 978 979 980
  (* 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
981

charguer's avatar
charguer committed
982 983 984
Ltac xchange_with_core cont H H' :=
  eapply xchange_lemma with (H1:=H) (H1':=H'); 
    [ try xlocal | | cont tt | ].
charguer's avatar
init  
charguer committed
985

charguer's avatar
charguer committed
986 987 988 989 990
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
991

charguer's avatar
charguer committed
992 993 994 995 996 997 998
Ltac xchange_base cont E modif :=
  xextract_check_not_needed tt;
  match goal with
  | |- _ ==> _ => hchange_base E modif
  | |- _ ===> _ => hchange_base E modif
  | _ => xchange_core cont E modif
  end.
charguer's avatar
init  
charguer committed
999

charguer's avatar
charguer committed
1000 1001 1002 1003 1004 1005
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
1006

charguer's avatar
charguer committed
1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022
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
1023 1024


charguer's avatar
charguer committed
1025
(* DEPRECATED: 
charguer's avatar
init  
charguer committed
1026

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

charguer's avatar
charguer committed
1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045
Tactic Notation "xchange" constr(E) "as" := 
  xchange E; try xextract.
Tactic Notation "xchange" constr(E) "as" simple_intropattern(I1) := 
  xchange E; try xextract as I1.
Tactic Notation "xchange" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2) 
  := 
  xchange E; try xextract as I1 I2.
Tactic Notation "xchange" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) := 
  xchange E; try xextract as I1 I2 I3.
Tactic Notation "xchange" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) := 
  xchange E; try xextract as I1 I2 I3 I4. 
Tactic Notation "xchange" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) := 
  xchange E; try xextract as I1 I2 I3 I4 I5. 
charguer's avatar
init  
charguer committed
1046

charguer's avatar
charguer committed
1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061
Tactic Notation "xchange" "~" constr(E) "as" := 
  xchange~ E; try xextract.
Tactic Notation "xchange" "~" constr(E) "as" simple_intropattern(I1) := 
  xchange~ E; try xextract as I1.
Tactic Notation "xchange" "~" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2) := 
  xchange~ E; try xextract as I1 I2.
Tactic Notation "xchange" "~" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) := 
  xchange~ E; try xextract as I1 I2 I3.
Tactic Notation "xchange" "~" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) := 
  xchange~ E; try xextract as I1 I2 I3 I4. 
Tactic Notation "xchange" "~" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) := 
  xchange~ E; try xextract as I1 I2 I3 I4 I5. 
charguer's avatar
ready  
charguer committed
1062

charguer's avatar
charguer committed
1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077
Tactic Notation "xchange" "*" constr(E) "as" := 
  xchange* E; try xextract.
Tactic Notation "xchange" "*" constr(E) "as" simple_intropattern(I1) := 
  xchange* E; try xextract as I1.
Tactic Notation "xchange" "*" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2) := 
  xchange* E; try xextract as I1 I2.
Tactic Notation "xchange" "*" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) := 
  xchange* E; try xextract as I1 I2 I3.
Tactic Notation "xchange" "*" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) := 
  xchange* E; try xextract as I1 I2 I3 I4. 
Tactic Notation "xchange" "*" constr(E) "as" simple_intropattern(I1) simple_intropattern(I2)
 simple_intropattern(I3) simple_intropattern(I4) simple_intropattern(I5) := 
  xchange* E; try xextract as I1 I2 I3 I4 I5.
charguer's avatar
init  
charguer committed
1078

charguer's avatar
charguer committed
1079
*)
charguer's avatar
init  
charguer committed
1080

charguer's avatar
charguer committed
1081 1082 1083 1084 1085 1086
(* 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
1087

charguer's avatar
charguer committed
1088

charguer's avatar
charguer committed
1089 1090
(************************************************************)
(* ** [xfocus] *)
charguer's avatar
init  
charguer committed
1091

charguer's avatar
charguer committed
1092 1093
(** [xfocus] is a tactic for applying [xchange] without having
    to explicitly specify the name of a focusing lemma.
charguer's avatar
charguer committed
1094

charguer's avatar
charguer committed
1095 1096 1097 1098 1099
    [xfocus p] applies to a goal of the form 
    [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
1100

charguer's avatar
charguer committed
1101 1102 1103
    [xfocus_show p] shows the lemma found, it is useful for debugging.
   
    Example for registering a focusing lemma:
charguer's avatar
init  
charguer committed
1104

charguer's avatar
charguer committed
1105 1106
     Hint Extern 1 (Register focus (Tree _)) => 
       Provide tree_focus_contents.
charguer's avatar
ready  
charguer committed
1107

charguer's avatar
charguer committed
1108
    Then, use: [xfocus p].  *)
charguer's avatar
ready  
charguer committed
1109

charguer's avatar
charguer committed
1110