lifting.v 4.41 KB
 Robbert Krebbers committed Feb 04, 2016 1 ``````Require Export program_logic.weakestpre. `````` Ralf Jung committed Feb 08, 2016 2 ``````Require Import program_logic.wsat program_logic.ownership. `````` Robbert Krebbers committed Jan 18, 2016 3 4 5 6 7 8 9 ``````Local Hint Extern 10 (_ ≤ _) => omega. Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of. Local Hint Extern 10 (✓{_} _) => repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end; solve_validN. Section lifting. `````` Robbert Krebbers committed Feb 01, 2016 10 11 12 13 14 ``````Context {Λ : language} {Σ : iFunctor}. Implicit Types v : val Λ. Implicit Types e : expr Λ. Implicit Types σ : state Λ. Implicit Types Q : val Λ → iProp Λ Σ. `````` Robbert Krebbers committed Jan 19, 2016 15 ``````Transparent uPred_holds. `````` Robbert Krebbers committed Jan 18, 2016 16 `````` `````` Robbert Krebbers committed Feb 04, 2016 17 18 ``````Notation wp_fork ef := (default True ef (flip (wp coPset_all) (λ _, True)))%I. `````` Robbert Krebbers committed Jan 18, 2016 19 ``````Lemma wp_lift_step E1 E2 `````` Robbert Krebbers committed Feb 01, 2016 20 `````` (φ : expr Λ → state Λ → option (expr Λ) → Prop) Q e1 σ1 : `````` Robbert Krebbers committed Jan 18, 2016 21 `````` E1 ⊆ E2 → to_val e1 = None → `````` Robbert Krebbers committed Jan 19, 2016 22 `````` reducible e1 σ1 → `````` Robbert Krebbers committed Jan 18, 2016 23 `````` (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → `````` Robbert Krebbers committed Feb 04, 2016 24 25 `````` pvs E2 E1 (ownP σ1 ★ ▷ ∀ e2 σ2 ef, (■ φ e2 σ2 ef ∧ ownP σ2) -★ pvs E1 E2 (wp E2 e2 Q ★ wp_fork ef)) `````` Robbert Krebbers committed Jan 18, 2016 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 `````` ⊑ wp E2 e1 Q. Proof. intros ? He Hsafe Hstep r n ? Hvs; constructor; auto. intros rf k Ef σ1' ???; destruct (Hvs rf (S k) Ef σ1') as (r'&(r1&r2&?&?&Hwp)&Hws); auto; clear Hvs; cofe_subst r'. destruct (wsat_update_pst k (E1 ∪ Ef) σ1 σ1' r1 (r2 ⋅ rf)) as [-> Hws']. { by apply ownP_spec; auto. } { by rewrite (associative _). } constructor; [done|intros e2 σ2 ef ?; specialize (Hws' σ2)]. destruct (λ H1 H2 H3, Hwp e2 σ2 ef (update_pst σ2 r1) k H1 H2 H3 rf k Ef σ2) as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'. { split. destruct k; try eapply Hstep; eauto. apply ownP_spec; auto. } { rewrite (commutative _ r2) -(associative _); eauto using wsat_le. } by exists r1', r2'; split_ands; [| |by intros ? ->]. Qed. `````` Ralf Jung committed Feb 02, 2016 41 `````` `````` Robbert Krebbers committed Feb 01, 2016 42 ``````Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Q e1 : `````` Robbert Krebbers committed Jan 18, 2016 43 `````` to_val e1 = None → `````` Robbert Krebbers committed Jan 19, 2016 44 `````` (∀ σ1, reducible e1 σ1) → `````` Robbert Krebbers committed Jan 18, 2016 45 `````` (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) → `````` Robbert Krebbers committed Feb 04, 2016 46 `````` (▷ ∀ e2 ef, ■ φ e2 ef → wp E e2 Q ★ wp_fork ef) ⊑ wp E e1 Q. `````` Robbert Krebbers committed Jan 18, 2016 47 48 49 50 51 52 53 ``````Proof. intros He Hsafe Hstep r [|n] ?; [done|]; intros Hwp; constructor; auto. intros rf k Ef σ1 ???; split; [done|]. intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst. destruct (Hwp e2 ef r k) as (r1&r2&Hr&?&?); auto; [by destruct k|]. exists r1,r2; split_ands; [rewrite -Hr| |by intros ? ->]; eauto using wsat_le. Qed. `````` Ralf Jung committed Feb 02, 2016 54 55 `````` (** Derived lifting lemmas. *) `````` Robbert Krebbers committed Feb 02, 2016 56 57 ``````Opaque uPred_holds. Import uPred. `````` Ralf Jung committed Feb 02, 2016 58 `````` `````` Robbert Krebbers committed Feb 04, 2016 59 60 ``````Lemma wp_lift_atomic_step {E Q} e1 (φ : val Λ → state Λ → option (expr Λ) → Prop) σ1 : `````` Ralf Jung committed Feb 02, 2016 61 62 `````` to_val e1 = None → reducible e1 σ1 → `````` Robbert Krebbers committed Feb 04, 2016 63 64 65 66 `````` (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → ∃ v2, to_val e2 = Some v2 ∧ φ v2 σ2 ef) → (ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■ φ v2 σ2 ef ∧ ownP σ2 -★ Q v2 ★ wp_fork ef) ⊑ wp E e1 Q. `````` Ralf Jung committed Feb 02, 2016 67 ``````Proof. `````` Robbert Krebbers committed Feb 04, 2016 68 69 `````` intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef, ∃ v2, to_val e2 = Some v2 ∧ φ v2 σ2 ef) _ e1 σ1) //; []. `````` Ralf Jung committed Feb 02, 2016 70 71 72 73 `````` rewrite -pvs_intro. apply sep_mono, later_mono; first done. apply forall_intro=>e2'; apply forall_intro=>σ2'. apply forall_intro=>ef; apply wand_intro_l. rewrite always_and_sep_l' -associative -always_and_sep_l'. `````` 74 75 76 `````` apply const_elim_l=>-[v2' [Hv ?]] /=. rewrite -pvs_intro. rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //. `````` Robbert Krebbers committed Feb 10, 2016 77 `````` by rewrite left_id wand_elim_r -(wp_value' _ _ e2' v2'). `````` Ralf Jung committed Feb 02, 2016 78 79 ``````Qed. `````` 80 ``````Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 ef : `````` Ralf Jung committed Feb 02, 2016 81 82 `````` to_val e1 = None → reducible e1 σ1 → `````` Robbert Krebbers committed Feb 04, 2016 83 84 85 `````` (∀ e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' → σ2 = σ2' ∧ to_val e2' = Some v2 ∧ ef = ef') → (ownP σ1 ★ ▷ (ownP σ2 -★ Q v2 ★ wp_fork ef)) ⊑ wp E e1 Q. `````` Ralf Jung committed Feb 02, 2016 86 ``````Proof. `````` Robbert Krebbers committed Feb 04, 2016 87 88 `````` intros. rewrite -(wp_lift_atomic_step _ (λ v2' σ2' ef', σ2 = σ2' ∧ v2 = v2' ∧ ef = ef') σ1) //; last naive_solver. `````` Ralf Jung committed Feb 02, 2016 89 `````` apply sep_mono, later_mono; first done. `````` 90 `````` apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'. `````` Ralf Jung committed Feb 02, 2016 91 `````` apply wand_intro_l. `````` Ralf Jung committed Feb 02, 2016 92 `````` rewrite always_and_sep_l' -associative -always_and_sep_l'. `````` Robbert Krebbers committed Feb 04, 2016 93 `````` apply const_elim_l=>-[-> [-> ->]] /=. by rewrite wand_elim_r. `````` Ralf Jung committed Feb 02, 2016 94 95 ``````Qed. `````` 96 ``````Lemma wp_lift_pure_det_step {E Q} e1 e2 ef : `````` Ralf Jung committed Feb 02, 2016 97 98 `````` to_val e1 = None → (∀ σ1, reducible e1 σ1) → `````` Robbert Krebbers committed Feb 04, 2016 99 100 `````` (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→ ▷ (wp E e2 Q ★ wp_fork ef) ⊑ wp E e1 Q. `````` Ralf Jung committed Feb 02, 2016 101 ``````Proof. `````` Robbert Krebbers committed Feb 04, 2016 102 103 `````` intros. rewrite -(wp_lift_pure_step E (λ e2' ef', e2 = e2' ∧ ef = ef') _ e1) //=. `````` 104 `````` apply later_mono, forall_intro=>e'; apply forall_intro=>ef'. `````` Robbert Krebbers committed Feb 04, 2016 105 `````` by apply impl_intro_l, const_elim_l=>-[-> ->]. `````` Ralf Jung committed Feb 02, 2016 106 107 ``````Qed. `````` Robbert Krebbers committed Jan 18, 2016 108 ``````End lifting. `````` 109