wp_tactics.v 4.42 KB
 Robbert Krebbers committed Mar 10, 2016 1 ``````From iris.algebra Require Export upred_tactics. `````` Robbert Krebbers committed Jul 19, 2016 2 ``````From iris.heap_lang Require Export tactics derived. `````` Robbert Krebbers committed Feb 16, 2016 3 4 ``````Import uPred. `````` Ralf Jung committed Feb 20, 2016 5 ``````(** wp-specific helper tactics *) `````` Robbert Krebbers committed Feb 16, 2016 6 7 8 ``````Ltac wp_bind K := lazymatch eval hnf in K with | [] => idtac `````` Ralf Jung committed Mar 05, 2016 9 `````` | _ => etrans; [|fast_by apply (wp_bind K)]; simpl `````` Robbert Krebbers committed Feb 16, 2016 10 `````` end. `````` Robbert Krebbers committed Apr 09, 2016 11 `````` `````` Robbert Krebbers committed Jul 19, 2016 12 ``````(* Solves side-conditions generated by the wp tactics *) `````` Robbert Krebbers committed Jul 15, 2016 13 ``````Ltac wp_done := `````` Robbert Krebbers committed Jul 19, 2016 14 15 `````` match goal with | |- Closed _ _ => solve_closed `````` Robbert Krebbers committed Jul 19, 2016 16 `````` | |- is_Some (to_val _) => solve_to_val `````` Robbert Krebbers committed Jul 19, 2016 17 18 19 20 `````` | |- to_val _ = Some _ => solve_to_val | |- language.to_val _ = Some _ => solve_to_val | _ => fast_done end. `````` Robbert Krebbers committed Mar 06, 2016 21 `````` `````` Robbert Krebbers committed Jun 30, 2016 22 23 24 25 26 27 28 ``````(* sometimes, we will have to do a final view shift, so only apply pvs_intro if we obtain a consecutive wp *) Ltac wp_strip_pvs := lazymatch goal with | |- _ ⊢ |={?E}=> _ => etrans; [|apply pvs_intro]; match goal with |- _ ⊢ wp E _ _ => simpl | _ => fail end `````` Robbert Krebbers committed Apr 11, 2016 29 30 `````` end. `````` Robbert Krebbers committed Jun 30, 2016 31 32 ``````Ltac wp_value_head := etrans; [|eapply wp_value_pvs; wp_done]; lazy beta. `````` Robbert Krebbers committed Jun 27, 2016 33 34 ``````Ltac wp_strip_later := idtac. (* a hook to be redefined later *) `````` 35 36 ``````Ltac wp_seq_head := lazymatch goal with `````` Robbert Krebbers committed Jun 30, 2016 37 38 `````` | |- _ ⊢ wp ?E (Seq _ _) ?Q => etrans; [|eapply wp_seq; wp_done]; wp_strip_later `````` 39 40 `````` end. `````` Robbert Krebbers committed Apr 11, 2016 41 ``````Ltac wp_finish := intros_revert ltac:( `````` Robbert Krebbers committed Jun 30, 2016 42 43 44 45 46 47 48 49 `````` rewrite /= ?to_of_val; try wp_strip_later; repeat lazymatch goal with | |- _ ⊢ wp ?E (Seq _ _) ?Q => etrans; [|eapply wp_seq; wp_done]; wp_strip_later | |- _ ⊢ wp ?E _ ?Q => wp_value_head | |- _ ⊢ |={_}=> _ => wp_strip_pvs end). `````` Robbert Krebbers committed Apr 11, 2016 50 51 `````` Tactic Notation "wp_value" := `````` Robbert Krebbers committed May 10, 2016 52 `````` lazymatch goal with `````` Robbert Krebbers committed Apr 11, 2016 53 `````` | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => `````` Robbert Krebbers committed May 10, 2016 54 55 `````` wp_bind K; wp_value_head) || fail "wp_value: cannot find value in" e | _ => fail "wp_value: not a wp" `````` Robbert Krebbers committed Apr 11, 2016 56 57 `````` end. `````` Robbert Krebbers committed Apr 09, 2016 58 ``````Tactic Notation "wp_rec" := `````` Robbert Krebbers committed Apr 11, 2016 59 60 61 `````` lazymatch goal with | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => match eval hnf in e' with App ?e1 _ => `````` Robbert Krebbers committed Mar 04, 2016 62 63 ``````(* hnf does not reduce through an of_val *) (* match eval hnf in e1 with Rec _ _ _ => *) `````` Robbert Krebbers committed May 10, 2016 64 `````` wp_bind K; etrans; [|eapply wp_rec; wp_done]; simpl_subst; wp_finish `````` Robbert Krebbers committed May 10, 2016 65 66 67 ``````(* end *) end) || fail "wp_rec: cannot find 'Rec' in" e | _ => fail "wp_rec: not a 'wp'" end. `````` Ralf Jung committed Feb 20, 2016 68 `````` `````` Robbert Krebbers committed Apr 09, 2016 69 ``````Tactic Notation "wp_lam" := `````` Robbert Krebbers committed May 10, 2016 70 `````` lazymatch goal with `````` Ralf Jung committed Mar 10, 2016 71 `````` | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => `````` Robbert Krebbers committed Mar 04, 2016 72 73 `````` match eval hnf in e' with App ?e1 _ => (* match eval hnf in e1 with Rec BAnon _ _ => *) `````` Robbert Krebbers committed Mar 06, 2016 74 `````` wp_bind K; etrans; [|eapply wp_lam; wp_done]; simpl_subst; wp_finish `````` Robbert Krebbers committed May 10, 2016 75 76 ``````(* end *) end) || fail "wp_lam: cannot find 'Lam' in" e | _ => fail "wp_lam: not a 'wp'" `````` 77 78 79 80 81 `````` end. Tactic Notation "wp_let" := wp_lam. Tactic Notation "wp_seq" := wp_let. `````` Robbert Krebbers committed Apr 09, 2016 82 ``````Tactic Notation "wp_op" := `````` Robbert Krebbers committed May 10, 2016 83 `````` lazymatch goal with `````` Ralf Jung committed Mar 10, 2016 84 `````` | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => `````` Ralf Jung committed Jul 27, 2016 85 `````` lazymatch eval hnf in e' with `````` Robbert Krebbers committed Feb 16, 2016 86 87 88 89 `````` | BinOp LtOp _ _ => wp_bind K; apply wp_lt; wp_finish | BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish | BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish | BinOp _ _ _ => `````` Ralf Jung committed Mar 05, 2016 90 `````` wp_bind K; etrans; [|eapply wp_bin_op; try fast_done]; wp_finish `````` Robbert Krebbers committed Feb 16, 2016 91 `````` | UnOp _ _ => `````` Ralf Jung committed Mar 05, 2016 92 `````` wp_bind K; etrans; [|eapply wp_un_op; try fast_done]; wp_finish `````` Robbert Krebbers committed May 10, 2016 93 94 `````` end) || fail "wp_op: cannot find 'BinOp' or 'UnOp' in" e | _ => fail "wp_op: not a 'wp'" `````` Robbert Krebbers committed Feb 16, 2016 95 `````` end. `````` Ralf Jung committed Feb 20, 2016 96 `````` `````` Robbert Krebbers committed Apr 09, 2016 97 ``````Tactic Notation "wp_proj" := `````` Robbert Krebbers committed May 10, 2016 98 `````` lazymatch goal with `````` Ralf Jung committed Mar 10, 2016 99 `````` | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => `````` Ralf Jung committed Mar 05, 2016 100 `````` match eval hnf in e' with `````` Robbert Krebbers committed Mar 06, 2016 101 102 `````` | Fst _ => wp_bind K; etrans; [|eapply wp_fst; wp_done]; wp_finish | Snd _ => wp_bind K; etrans; [|eapply wp_snd; wp_done]; wp_finish `````` Robbert Krebbers committed May 10, 2016 103 104 `````` end) || fail "wp_proj: cannot find 'Fst' or 'Snd' in" e | _ => fail "wp_proj: not a 'wp'" `````` Ralf Jung committed Mar 05, 2016 105 106 `````` end. `````` Robbert Krebbers committed Apr 09, 2016 107 ``````Tactic Notation "wp_if" := `````` Robbert Krebbers committed May 10, 2016 108 `````` lazymatch goal with `````` Ralf Jung committed Mar 10, 2016 109 `````` | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => `````` Robbert Krebbers committed May 10, 2016 110 111 112 113 114 115 `````` match eval hnf in e' with | If _ _ _ => wp_bind K; etrans; [|eapply wp_if_true || eapply wp_if_false]; wp_finish end) || fail "wp_if: cannot find 'If' in" e | _ => fail "wp_if: not a 'wp'" `````` Robbert Krebbers committed Feb 16, 2016 116 `````` end. `````` Ralf Jung committed Feb 20, 2016 117 `````` `````` Robbert Krebbers committed Jun 23, 2016 118 ``````Tactic Notation "wp_match" := `````` Robbert Krebbers committed May 10, 2016 119 `````` lazymatch goal with `````` Ralf Jung committed Mar 10, 2016 120 `````` | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => `````` Robbert Krebbers committed May 10, 2016 121 122 `````` match eval hnf in e' with | Case _ _ _ => `````` Robbert Krebbers committed Mar 06, 2016 123 `````` wp_bind K; `````` Robbert Krebbers committed Jun 23, 2016 124 125 126 127 `````` etrans; [|first[eapply wp_match_inl; wp_done|eapply wp_match_inr; wp_done]]; simpl_subst; wp_finish end) || fail "wp_match: cannot find 'Match' in" e | _ => fail "wp_match: not a 'wp'" `````` Ralf Jung committed Mar 05, 2016 128 129 `````` end. `````` Robbert Krebbers committed Feb 16, 2016 130 ``````Tactic Notation "wp_focus" open_constr(efoc) := `````` Robbert Krebbers committed May 10, 2016 131 `````` lazymatch goal with `````` Ralf Jung committed Mar 10, 2016 132 `````` | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' => `````` Robbert Krebbers committed May 10, 2016 133 134 135 136 `````` match e' with | efoc => unify e' efoc; wp_bind K end) || fail "wp_focus: cannot find" efoc "in" e | _ => fail "wp_focus: not a 'wp'" `````` Robbert Krebbers committed Feb 16, 2016 137 `` end.``