lifting.v 4.64 KB
 Robbert Krebbers committed Feb 04, 2016 1 2 ``````Require Export program_logic.weakestpre. Require Import program_logic.wsat. `````` 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 17 `````` Lemma wp_lift_step E1 E2 `````` Robbert Krebbers committed Feb 01, 2016 18 `````` (φ : expr Λ → state Λ → option (expr Λ) → Prop) Q e1 σ1 : `````` Robbert Krebbers committed Jan 18, 2016 19 `````` E1 ⊆ E2 → to_val e1 = None → `````` Robbert Krebbers committed Jan 19, 2016 20 `````` reducible e1 σ1 → `````` Robbert Krebbers committed Jan 18, 2016 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 `````` (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → pvs E2 E1 (ownP σ1 ★ ▷ ∀ e2 σ2 ef, (■ φ e2 σ2 ef ∧ ownP σ2) -★ pvs E1 E2 (wp E2 e2 Q ★ default True ef (flip (wp coPset_all) (λ _, True)))) ⊑ 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 39 `````` `````` Robbert Krebbers committed Feb 01, 2016 40 ``````Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Q e1 : `````` Robbert Krebbers committed Jan 18, 2016 41 `````` to_val e1 = None → `````` Robbert Krebbers committed Jan 19, 2016 42 `````` (∀ σ1, reducible e1 σ1) → `````` Robbert Krebbers committed Jan 18, 2016 43 44 45 46 47 48 49 50 51 52 53 `````` (∀ σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → σ1 = σ2 ∧ φ e2 ef) → (▷ ∀ e2 ef, ■ φ e2 ef → wp E e2 Q ★ default True ef (flip (wp coPset_all) (λ _, True))) ⊑ wp E e1 Q. 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 `````` `````` 59 ``````Lemma wp_lift_atomic_step {E Q} e1 (φ : val Λ → state Λ → option (expr Λ) → Prop) σ1 : `````` Ralf Jung committed Feb 02, 2016 60 61 `````` to_val e1 = None → reducible e1 σ1 → `````` 62 63 64 65 `````` (∀ e' σ' ef, prim_step e1 σ1 e' σ' ef → ∃ v', to_val e' = Some v' ∧ φ v' σ' ef) → (ownP σ1 ★ ▷ ∀ v2 σ2 ef, ■ φ v2 σ2 ef ∧ ownP σ2 -★ Q v2 ★ default True ef (flip (wp coPset_all) (λ _, True))) ⊑ wp E e1 Q. `````` Ralf Jung committed Feb 02, 2016 66 67 68 ``````Proof. intros He Hsafe Hstep. rewrite -(wp_lift_step E E `````` 69 `````` (λ e' σ' ef, ∃ v', to_val e' = Some v' ∧ φ v' σ' 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 04, 2016 77 `````` by rewrite left_id wand_elim_r -(wp_value' _ _ e2'). `````` 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 → `````` 83 84 85 86 `````` (∀ e' σ' ef', prim_step e1 σ1 e' σ' ef' → ef' = ef ∧ e' = of_val v2 ∧ σ' = σ2) → (ownP σ1 ★ ▷ (ownP σ2 -★ Q v2 ★ default True ef (flip (wp coPset_all) (λ _, True)))) ⊑ wp E e1 Q. `````` Ralf Jung committed Feb 02, 2016 87 88 ``````Proof. intros He Hsafe Hstep. `````` 89 90 `````` rewrite -(wp_lift_atomic_step _ (λ v' σ' ef', v' = v2 ∧ σ' = σ2 ∧ ef' = ef) σ1) //; last first. `````` Ralf Jung committed Feb 02, 2016 91 92 93 `````` { intros. exists v2. apply Hstep in H. destruct_conjs; subst. eauto using to_of_val. } apply sep_mono, later_mono; first done. `````` 94 `````` apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'. `````` Ralf Jung committed Feb 02, 2016 95 `````` apply wand_intro_l. `````` Ralf Jung committed Feb 02, 2016 96 `````` rewrite always_and_sep_l' -associative -always_and_sep_l'. `````` 97 `````` apply const_elim_l=>-[-> [-> ->]] /=. `````` Ralf Jung committed Feb 02, 2016 98 99 100 `````` by rewrite wand_elim_r. Qed. `````` 101 ``````Lemma wp_lift_pure_det_step {E Q} e1 e2 ef : `````` Ralf Jung committed Feb 02, 2016 102 103 `````` to_val e1 = None → (∀ σ1, reducible e1 σ1) → `````` 104 105 `````` (∀ σ1 e' σ' ef', prim_step e1 σ1 e' σ' ef' → σ1 = σ' ∧ ef' = ef ∧ e' = e2) → ▷ (wp E e2 Q ★ default True ef (flip (wp coPset_all) (λ _, True))) ⊑ wp E e1 Q. `````` Ralf Jung committed Feb 02, 2016 106 ``````Proof. `````` 107 108 109 `````` intros. rewrite -(wp_lift_pure_step E (λ e' ef', ef' = ef ∧ e' = e2) _ e1) //=. apply later_mono, forall_intro=>e'; apply forall_intro=>ef'. apply impl_intro_l, const_elim_l=>-[-> ->] /=; done. `````` Ralf Jung committed Feb 02, 2016 110 111 ``````Qed. `````` Robbert Krebbers committed Jan 18, 2016 112 ``````End lifting. `````` 113