Commit 8e61fbb0 by Dan Frumin

### Employ the notation in `monad.v` and `translation.v`

parent 1cfdc584
 ... ... @@ -102,8 +102,8 @@ Section a_wp_rules. Context `{amonadG Σ}. Lemma a_wp_awp R Φ Ψ e : awp e R Φ -∗ (∀ v : val, awp v R Φ -∗ Ψ v) -∗ AWP e @ R {{ Φ }} -∗ (∀ v : val, AWP v @ R {{ Φ }} -∗ Ψ v) -∗ WP e {{ Ψ }}. Proof. iIntros "Hwp H". rewrite /awp /=. iApply (wp_wand with "Hwp"). ... ... @@ -111,17 +111,17 @@ Section a_wp_rules. Qed. Lemma wp_awp_bind R Φ K e : WP e {{ v, awp (fill K (of_val v)) R Φ }} -∗ awp (fill K e) R Φ. WP e {{ v, AWP (fill K (of_val v)) @ R {{ Φ }} }} -∗ AWP (fill K e) @ R {{ Φ }}. Proof. by apply: wp_bind. Qed. Lemma wp_awp_bind_inv R Φ K e : awp (fill K e) R Φ -∗ WP e {{ v, awp (fill K (of_val v)) R Φ }}. AWP (fill K e) @ R {{ Φ }} -∗ WP e {{ v, AWP (fill K (of_val v)) @ R {{ Φ }} }}. Proof. by apply: wp_bind_inv. Qed. Lemma awp_insert_res e Φ R1 R2 : ▷ R1 -∗ awp e (R1 ∗ R2) Φ -∗ awp e R2 Φ. AWP e @ (R1 ∗ R2) {{ Φ }} -∗ AWP e @ R2 {{ Φ }}. Proof. iIntros "HR1 Hawp". rewrite /awp /=. iApply (wp_wand with "Hawp"). ... ... @@ -136,9 +136,9 @@ Section a_wp_rules. Qed. Lemma awp_wand e (Φ Ψ : val → iProp Σ) R : awp e R Φ -∗ AWP e @ R {{ Φ }} -∗ (∀ v, Φ v -∗ Ψ v) -∗ awp e R Ψ. AWP e @ R {{ Ψ }}. Proof. iIntros "HAWP Hv". rewrite /awp /=. iApply (wp_wand with "HAWP"). ... ... @@ -151,15 +151,15 @@ Section a_wp_rules. Lemma awp_pure K φ e1 e2 R Φ : PureExec φ e1 e2 → φ → ▷ awp (fill K e2) R Φ -∗ awp (fill K e1) R Φ. ▷ AWP (fill K e2) @ R {{ Φ }} -∗ AWP (fill K e1) @ R {{ Φ }}. Proof. iIntros (? Hφ) "Hawp". iApply wp_awp_bind. wp_pure _. by iApply wp_awp_bind_inv. Qed. Lemma awp_ret e R Φ : WP e {{ Φ }} -∗ awp (a_ret e) R Φ. WP e {{ Φ }} -∗ AWP (a_ret e) @ R {{ Φ }}. Proof. iIntros "Hwp". rewrite /awp /a_ret /=. wp_apply (wp_wand with "Hwp"). iIntros (v) "HΦ". wp_lam. ... ... @@ -168,8 +168,8 @@ Section a_wp_rules. Lemma awp_bind (f e : expr) R Φ : AsVal f → awp e R (λ ev, awp (f ev) R Φ) -∗ awp (a_bind f e) R Φ. AWP e @ R {{ ev, AWP (f ev) @ R {{ Φ }} }} -∗ AWP (a_bind f e) @ R {{ Φ }}. Proof. iIntros ([fv <-]) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e. iApply (wp_wand with "Hwp"). iIntros (ev) "Hwp". wp_lam. ... ... @@ -181,8 +181,8 @@ Section a_wp_rules. Lemma awp_atomic (e : expr) (ev : val) R Φ : IntoVal e ev → (R -∗ ∃ R', R' ∗ awp (ev #()) R' (λ w, R' -∗ R ∗ Φ w)) -∗ awp (a_atomic e) R Φ. (R -∗ ∃ R', R' ∗ AWP (ev #()) @ R' {{ w, R' -∗ R ∗ Φ w }}) -∗ AWP (a_atomic e) @ R {{ Φ }}. Proof. iIntros (<-) "Hwp". rewrite /awp /a_atomic /=. wp_lam. iIntros (γ π env l) "#Hlock1 #Hres Hunfl1". do 2 wp_let. ... ... @@ -208,7 +208,7 @@ Section a_wp_rules. IntoVal e ev → (∀ env, env_inv env -∗ R -∗ WP ev env {{ w, env_inv env ∗ R ∗ Φ w }}) -∗ awp (a_atomic_env e) R Φ. AWP (a_atomic_env e) @ R {{ Φ }}. Proof. iIntros (<-) "Hwp". rewrite /awp /a_atomic_env /=. wp_lam. iIntros (γ π env l) "#Hlock #Hres Hunfl". do 2 wp_lam. ... ... @@ -223,10 +223,10 @@ Section a_wp_rules. Qed. Lemma awp_par (Ψ1 Ψ2 : val → iProp Σ) e1 e2 R (Φ : val → iProp Σ) : awp e1 R Ψ1 -∗ ▷ awp e2 R Ψ2 -∗ AWP e1 @ R {{ Ψ1 }} -∗ ▷ AWP e2 @ R {{ Ψ2 }} -∗ ▷ (∀ w1 w2, Ψ1 w1 -∗ Ψ2 w2 -∗ ▷ Φ (w1,w2)%V) -∗ awp (a_par e1 e2) R Φ. AWP (a_par e1 e2) @ R {{ Φ }}. Proof. iIntros "Hwp1 Hwp2 HΦ". rewrite /a_par /awp /=. wp_bind e1. iApply (wp_wand with "Hwp1"). ... ... @@ -249,7 +249,7 @@ Section a_wp_run. Lemma awp_run (e : expr) R Φ : AsVal e → R -∗ (∀ `{amonadG Σ}, awp e R (λ w, ▷ R ={⊤}=∗ Φ w)) -∗ R -∗ (∀ `{amonadG Σ}, AWP e @ R {{ w, ▷ R ={⊤}=∗ Φ w }}) -∗ WP a_run e {{ Φ }}. Proof. iIntros ([ev <-]) "HR Hwp". rewrite /awp /a_run /=. wp_let. ... ...
 ... ... @@ -82,8 +82,8 @@ Section proofs. Context `{amonadG Σ}. Lemma a_alloc_spec R Φ e : awp e R (λ v, ∀ l, l ↦C v -∗ Φ #l) -∗ awp (a_alloc e) R Φ. AWP e @ R {{ v, ∀ l : loc, l ↦C v -∗ Φ #l }} -∗ AWP allocᶜ e @ R {{ Φ }}. Proof. iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam. iApply awp_bind. ... ... @@ -175,8 +175,8 @@ Section proofs. Qed. Lemma a_load_spec_exists_frac R Φ e : awp e R (λ v, ∃ (l : loc) (q: frac) (w : val), ⌜v = #l⌝ ∗ l ↦C{q} w ∗ (l ↦C{q} w -∗ Φ w)) -∗ awp (a_load e) R Φ. AWP e @ R {{ v, ∃ (l : loc) (q : Qp) (w : val), ⌜v = #l⌝ ∗ l ↦C{q} w ∗ (l ↦C{q} w -∗ Φ w) }} -∗ AWP ∗ᶜe @ R {{ Φ }}. Proof. iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam. ... ... @@ -212,8 +212,8 @@ Section proofs. Qed. Lemma a_load_spec R Φ q e : awp e R (λ v, ∃ (l : loc) (w : val), ⌜v = #l⌝ ∗ l ↦C{q} w ∗ (l ↦C{q} w -∗ Φ w)) -∗ awp (a_load e) R Φ. AWP e @ R {{ v, ∃ (l : loc) (w : val), ⌜v = #l⌝ ∗ l ↦C{q} w ∗ (l ↦C{q} w -∗ Φ w) }} -∗ AWP ∗ᶜe @ R {{ Φ }}. Proof. iIntros "H". iApply a_load_spec_exists_frac. ... ... @@ -223,8 +223,8 @@ Section proofs. Qed. Lemma a_un_op_spec R Φ e op: awp e R (λ v, ∃ w, ⌜un_op_eval op v = Some w⌝ ∧ Φ w) -∗ awp (a_un_op op e) R Φ. AWP e @ R {{ v, ∃ w : val, ⌜un_op_eval op v = Some w⌝ ∧ Φ w }} -∗ AWP (a_un_op op) e @ R {{ Φ }}. Proof. iIntros "H". awp_apply (a_wp_awp with "H"); iIntros (v) "HΦ"; awp_lam. ... ... @@ -235,10 +235,10 @@ Section proofs. Qed. Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) : awp e1 R Ψ1 -∗ awp e2 R Ψ2 -∗ AWP e1 @ R {{ Ψ1 }} -∗ AWP e2 @ R {{ Ψ2 }} -∗ ▷ (∀ v1 v2, Ψ1 v1 -∗ Ψ2 v2 -∗ ∃ w, ⌜bin_op_eval op v1 v2 = Some w⌝ ∧ Φ w)-∗ awp (a_bin_op op e1 e2) R Φ. AWP (a_bin_op op e1 e2) @ R {{ Φ }}. Proof. iIntros "H1 H2 HΦ". awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam. ... ... @@ -253,7 +253,7 @@ Section proofs. Lemma a_seq_spec R Φ : U (Φ #()) -∗ awp (a_seq #()) R Φ. AWP (a_seq #()) @ R {{ Φ }}. Proof. iIntros "HΦ". rewrite /a_seq. awp_lam. iApply awp_atomic_env. ... ... @@ -280,8 +280,8 @@ Section proofs. Lemma a_sequence_spec R Φ (f e : expr) : AsVal f → ▷ awp e R (λ v, U (awp (f v) R Φ)) -∗ awp (a_seq_bind f e) R Φ. ▷ AWP e @ R {{ v, U (AWP (f v) @ R {{ Φ }}) }} -∗ AWP a_seq_bind f e @ R {{ Φ }}. Proof. iIntros ([fv <-]) "H". rewrite /a_seq_bind /=. awp_lam. awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam. ... ... @@ -292,8 +292,8 @@ Section proofs. Lemma a_sequence_spec' R Φ (e e' : expr) : Closed [] e' → ▷ awp e R (λ v, U (awp e' R Φ)) -∗ awp (a_seq_bind (λ: <>, e') e)%E R Φ. ▷ AWP e @ R {{ v, U (AWP e' @ R {{ Φ }}) }} -∗ AWP a_seq_bind (λ: <>, e') e @ R {{ Φ }}. Proof. iIntros (?) "He". iApply a_sequence_spec. ... ... @@ -313,9 +313,9 @@ Section proofs. Lemma a_if_spec R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} : AsVal e1 → AsVal e2 → awp e R (λ v, (⌜v = #true⌝ ∧ awp (e1 #()) R Φ) ∨ (⌜v = #false⌝ ∧ awp (e2 #()) R Φ)) -∗ awp (a_if e e1 e2) R Φ. AWP e @ R {{ v, (⌜v = #true⌝ ∧ AWP e1 #() @ R {{ Φ }}) ∨ (⌜v = #false⌝ ∧ AWP e2 #() @ R {{ Φ }}) }} -∗ AWP a_if e e1 e2 @ R {{ Φ }}. Proof. iIntros ([v1 <-] [v2 <-]) "H". awp_apply (a_wp_awp with "H"). iIntros (v) "H". do 3 awp_lam. ... ... @@ -324,9 +324,9 @@ Section proofs. Qed. Lemma a_if_spec' R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} : awp e R (λ v, (⌜v = #true⌝ ∧ awp e1 R Φ) ∨ (⌜v = #false⌝ ∧ awp e2 R Φ)) -∗ awp (a_if e (λ: <>, e1) (λ: <>, e2))%E R Φ. AWP e @ R {{ v, (⌜v = #true⌝ ∧ AWP e1 @ R {{ Φ }}) ∨ (⌜v = #false⌝ ∧ AWP e2 @ R {{ Φ }}) }} -∗ AWP ifᶜ (e) { e1 } elseᶜ { e2 } @ R {{ Φ }}. Proof. iIntros "He". iApply a_if_spec. iApply (awp_wand with "He"). ... ... @@ -334,10 +334,9 @@ Section proofs. Qed. Lemma a_while_spec' R Φ (c b: expr) `{Closed [] c} `{Closed [] b} : ▷ awp c R (λ v, (⌜v = #true⌝ ∧ awp b R (λ _, U (awp (a_while (λ:<>, c) (λ:<>, b))%E R Φ))) ∨ (⌜v = #false⌝ ∧ awp (a_seq #()) R Φ)) -∗ awp (a_while (λ:<>, c) (λ:<>, b))%E R Φ. ▷ AWP c @ R {{ v, ⌜v = #true⌝ ∧ AWP b @ R {{ _, U (AWP whileᶜ (c) { b } @ R {{ Φ }}) }} ∨ ⌜v = #false⌝ ∧ AWP a_seq #() @ R {{ Φ }} }} -∗ AWP whileᶜ (c) { b } @ R {{ Φ }}. Proof. iIntros "H". awp_lam. awp_lam. awp_seq. ... ... @@ -350,9 +349,9 @@ Section proofs. Lemma a_invoke_spec (ef ea : expr) (R : iProp Σ) Ψ Φ (f : val) : IntoVal ef f → awp ea R Ψ -∗ (∀ a, Ψ a -∗ U (R -∗ ∃ R', R' ∗ (awp (ef a) R' (λ v, R' -∗ R ∗ Φ v)))) -∗ awp (a_invoke ef ea) R Φ. AWP ea @ R {{ Ψ }} -∗ (∀ a, Ψ a -∗ U (R -∗ ∃ R', R' ∗ (AWP ef a @ R' {{ v, R' -∗ R ∗ Φ v }}))) -∗ AWP a_invoke ef ea @ R {{ Φ }}. Proof. rewrite /IntoVal. iIntros (<-) "Ha Hfa". rewrite /a_invoke. awp_lam. ... ... @@ -370,7 +369,8 @@ Section proofs. Qed. Lemma a_if_true_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ : awp e1 R Φ -∗ awp (a_if (a_ret #true) (λ: <>, e1) (λ: <>, e2))%E R Φ. AWP e1 @ R {{ Φ }} -∗ AWP ifᶜ (♯true) { e1 } elseᶜ { e2 } @ R {{ Φ }}. Proof. iIntros "HΦ". iApply a_if_spec. ... ... @@ -379,7 +379,8 @@ Section proofs. Qed. Lemma a_if_false_spec R (e1 e2 : expr) `{Closed [] e1, Closed [] e2} Φ : awp e2 R Φ -∗ awp (a_if (a_ret #false) (λ: <>, e1) (λ: <>, e2))%E R Φ. AWP e2 @ R {{ Φ }} -∗ AWP ifᶜ (♯false) { e1 } elseᶜ { e2 } @ R {{ Φ }}. Proof. iIntros "HΦ". iApply a_if_spec. ... ... @@ -389,9 +390,9 @@ Section proofs. Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} : I -∗ □ (I -∗ awp c R (λ v, (⌜v = #false⌝ ∧ U (Φ #())) ∨ (⌜v = #true⌝ ∧ ▷ (awp b R (λ _, U I))))%I) -∗ awp (a_while (λ:<>, c) (λ:<>, b))%E R Φ. □ (I -∗ AWP c @ R {{ v, (⌜v = #false⌝ ∧ U (Φ #())) ∨ (⌜v = #true⌝ ∧ ▷ (AWP b @ R {{ _, U I }})) }}) -∗ AWP whileᶜ (c) { b } @ R {{ Φ }}. Proof. iIntros "Hi #Hinv". iLöb as "IH". iApply a_while_spec. iNext. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!