proofmode.v 7.28 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export weakestpre.
From iris.heap_lang Require Export wp_tactics heap.
Import uPred.

6
Ltac wp_strip_later ::= iNext.
Robbert Krebbers's avatar
Robbert Krebbers committed
7 8 9 10 11 12

Section heap.
Context {Σ : gFunctors} `{heapG Σ}.
Implicit Types N : namespace.
Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val  iPropG heap_lang Σ.
13
Implicit Types Δ : envs (iResUR heap_lang (globalF Σ)).
Robbert Krebbers's avatar
Robbert Krebbers committed
14

15 16 17
Global Instance into_sep_mapsto l q v :
  IntoSep false (l {q} v) (l {q/2} v) (l {q/2} v).
Proof. by rewrite /IntoSep heap_mapsto_op_split. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
18 19

Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
20
  to_val e = Some v 
21
  (Δ  heap_ctx N)  nclose N  E 
22
  IntoLaterEnvs Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  ( l,  Δ'',
24
    envs_app false (Esnoc Enil j (l  v)) Δ' = Some Δ'' 
25
    (Δ''  |={E}=> Φ (LitV (LitLoc l)))) 
Robbert Krebbers's avatar
Robbert Krebbers committed
26 27
  Δ  WP Alloc e @ E {{ Φ }}.
Proof.
28 29
  intros ???? HΔ. rewrite -wp_alloc // -always_and_sep_l.
  apply and_intro; first done.
30
  rewrite into_later_env_sound; apply later_mono, forall_intro=> l.
Robbert Krebbers's avatar
Robbert Krebbers committed
31 32 33 34 35
  destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
  by rewrite right_id HΔ'.
Qed.

Lemma tac_wp_load Δ Δ' N E i l q v Φ :
36
  (Δ  heap_ctx N)  nclose N  E 
37
  IntoLaterEnvs Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
38
  envs_lookup i Δ' = Some (false, l {q} v)%I 
39
  (Δ'  |={E}=> Φ v) 
40
  Δ  WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
Proof.
Ralf Jung's avatar
Ralf Jung committed
42
  intros. rewrite -wp_load // -always_and_sep_l. apply and_intro; first done.
43
  rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
44 45 46 47 48
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

Lemma tac_wp_store Δ Δ' Δ'' N E i l v e v' Φ :
  to_val e = Some v' 
49
  (Δ  heap_ctx N)  nclose N  E 
50
  IntoLaterEnvs Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
51 52
  envs_lookup i Δ' = Some (false, l  v)%I 
  envs_simple_replace i false (Esnoc Enil i (l  v')) Δ' = Some Δ'' 
53 54
  (Δ''  |={E}=> Φ (LitV LitUnit)) 
  Δ  WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
Proof.
56
  intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
57
  rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59 60 61 62
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.

Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ :
  to_val e1 = Some v1  to_val e2 = Some v2 
63
  (Δ  heap_ctx N)  nclose N  E 
64
  IntoLaterEnvs Δ Δ' 
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  envs_lookup i Δ' = Some (false, l {q} v)%I  v  v1 
66
  (Δ'  |={E}=> Φ (LitV (LitBool false))) 
67
  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
Proof.
69
  intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
70
  rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
71 72 73
  by apply later_mono, sep_mono_r, wand_mono.
Qed.

74
Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l v e1 v1 e2 v2 Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
75
  to_val e1 = Some v1  to_val e2 = Some v2 
76
  (Δ  heap_ctx N)  nclose N  E 
77
  IntoLaterEnvs Δ Δ' 
78
  envs_lookup i Δ' = Some (false, l  v)%I  v = v1 
Robbert Krebbers's avatar
Robbert Krebbers committed
79
  envs_simple_replace i false (Esnoc Enil i (l  v2)) Δ' = Some Δ'' 
80 81
  (Δ''  |={E}=> Φ (LitV (LitBool true))) 
  Δ  WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Proof.
83 84
  intros; subst.
  rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
85
  rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
86 87 88 89 90
  rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
End heap.

Tactic Notation "wp_apply" open_constr(lem) :=
91
  lazymatch goal with
Robbert Krebbers's avatar
Robbert Krebbers committed
92 93
  | |- _  wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
    wp_bind K; iApply lem; try iNext)
94
  | _ => fail "wp_apply: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
95 96 97
  end.

Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
98
  lazymatch goal with
99 100 101 102 103 104 105 106 107
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
         match eval hnf in e' with Alloc _ => wp_bind K end)
      |fail 1 "wp_alloc: cannot find 'Alloc' in" e];
    eapply tac_wp_alloc with _ _ H _;
      [let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_alloc:" e' "not a value"
      |iAssumption || fail "wp_alloc: cannot find heap_ctx"
108
      |solve_ndisj
109 110 111 112 113
      |apply _
      |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
        eexists; split;
          [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
          |wp_finish]]
114
  | _ => fail "wp_alloc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
115
  end.
116

117 118
Tactic Notation "wp_alloc" ident(l) :=
  let H := iFresh in wp_alloc l as H.
Robbert Krebbers's avatar
Robbert Krebbers committed
119 120

Tactic Notation "wp_load" :=
121
  lazymatch goal with
122 123 124 125 126 127 128
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
         match eval hnf in e' with Load _ => wp_bind K end)
      |fail 1 "wp_load: cannot find 'Load' in" e];
    eapply tac_wp_load;
      [iAssumption || fail "wp_load: cannot find heap_ctx"
129
      |solve_ndisj
130 131
      |apply _
      |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
132
       iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
133
      |wp_finish]
134
  | _ => fail "wp_load: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
135 136 137
  end.

Tactic Notation "wp_store" :=
138
  lazymatch goal with
139 140 141 142 143 144 145 146 147
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
         match eval hnf in e' with Store _ _ => wp_bind K end)
      |fail 1 "wp_store: cannot find 'Store' in" e];
    eapply tac_wp_store;
      [let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_store:" e' "not a value"
      |iAssumption || fail "wp_store: cannot find heap_ctx"
148
      |solve_ndisj
149 150 151 152
      |apply _
      |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
       iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
      |env_cbv; reflexivity
153
      |wp_finish]
154
  | _ => fail "wp_store: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
155 156 157
  end.

Tactic Notation "wp_cas_fail" :=
158
  lazymatch goal with
159 160 161 162 163 164 165 166 167 168 169
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
         match eval hnf in e' with CAS _ _ _ => wp_bind K end)
      |fail 1 "wp_cas_fail: cannot find 'CAS' in" e];
    eapply tac_wp_cas_fail;
      [let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_cas_fail:" e' "not a value"
      |let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_cas_fail:" e' "not a value"
      |iAssumption || fail "wp_cas_fail: cannot find heap_ctx"
170
      |solve_ndisj
171 172 173 174 175
      |apply _
      |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
       iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
      |try congruence
      |wp_finish]
176
  | _ => fail "wp_cas_fail: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
177 178 179
  end.

Tactic Notation "wp_cas_suc" :=
180
  lazymatch goal with
181 182 183 184 185 186 187 188 189 190 191
  | |- _  wp ?E ?e ?Q =>
    first
      [reshape_expr e ltac:(fun K e' =>
         match eval hnf in e' with CAS _ _ _ => wp_bind K end)
      |fail 1 "wp_cas_suc: cannot find 'CAS' in" e];
    eapply tac_wp_cas_suc;
      [let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_cas_suc:" e' "not a value"
      |let e' := match goal with |- to_val ?e' = _ => e' end in
       wp_done || fail "wp_cas_suc:" e' "not a value"
      |iAssumption || fail "wp_cas_suc: cannot find heap_ctx"
192
      |solve_ndisj
193 194 195 196 197 198
      |apply _
      |let l := match goal with |- _ = Some (_, (?l {_} _)%I) => l end in
       iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
      |try congruence
      |env_cbv; reflexivity
      |wp_finish]
199
  | _ => fail "wp_cas_suc: not a 'wp'"
Robbert Krebbers's avatar
Robbert Krebbers committed
200
  end.