lifting.v 4.41 KB
Newer Older
1
Require Export program_logic.weakestpre.
Ralf Jung's avatar
Ralf Jung committed
2
Require Import program_logic.wsat program_logic.ownership.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
10 11 12 13 14
Context {Λ : language} {Σ : iFunctor}.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Implicit Types σ : state Λ.
Implicit Types Q : val Λ  iProp Λ Σ.
15
Transparent uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
16

17 18
Notation wp_fork ef := (default True ef (flip (wp coPset_all) (λ _, True)))%I.

Robbert Krebbers's avatar
Robbert Krebbers committed
19
Lemma wp_lift_step E1 E2
20
    (φ : expr Λ  state Λ  option (expr Λ)  Prop) Q e1 σ1 :
Robbert Krebbers's avatar
Robbert Krebbers committed
21
  E1  E2  to_val e1 = None 
22
  reducible e1 σ1 
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  ( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  φ e2 σ2 ef) 
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's avatar
Robbert Krebbers committed
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.
41

42
Lemma wp_lift_pure_step E (φ : expr Λ  option (expr Λ)  Prop) Q e1 :
Robbert Krebbers's avatar
Robbert Krebbers committed
43
  to_val e1 = None 
44
  ( σ1, reducible e1 σ1) 
Robbert Krebbers's avatar
Robbert Krebbers committed
45
  ( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  σ1 = σ2  φ e2 ef) 
46
  (  e2 ef,  φ e2 ef  wp E e2 Q  wp_fork ef)  wp E e1 Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
54 55

(** Derived lifting lemmas. *)
56 57
Opaque uPred_holds.
Import uPred.
58

59 60
Lemma wp_lift_atomic_step {E Q} e1
    (φ : val Λ  state Λ  option (expr Λ)  Prop) σ1 :
61 62
  to_val e1 = None 
  reducible e1 σ1 
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.
67
Proof.
68 69
  intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef,  v2,
    to_val e2 = Some v2  φ v2 σ2 ef) _ e1 σ1) //; [].
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 //.
77
  by rewrite left_id wand_elim_r -(wp_value' _ _ e2' v2').
78 79
Qed.

80
Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 ef :
81 82
  to_val e1 = None 
  reducible e1 σ1 
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.
86
Proof.
87 88
  intros. rewrite -(wp_lift_atomic_step _ (λ v2' σ2' ef',
    σ2 = σ2'  v2 = v2'  ef = ef') σ1) //; last naive_solver.
89
  apply sep_mono, later_mono; first done.
90
  apply forall_intro=>e2'; apply forall_intro=>σ2'; apply forall_intro=>ef'.
91
  apply wand_intro_l.
92
  rewrite always_and_sep_l' -associative -always_and_sep_l'.
93
  apply const_elim_l=>-[-> [-> ->]] /=. by rewrite wand_elim_r.
94 95
Qed.

96
Lemma wp_lift_pure_det_step {E Q} e1 e2 ef :
97 98
  to_val e1 = None 
  ( σ1, reducible e1 σ1) 
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.
101
Proof.
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'.
105
  by apply impl_intro_l, const_elim_l=>-[-> ->].
106 107
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
108
End lifting.
109