lifting.v 4.38 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
Local Hint Extern 10 (_  _) => omega.
Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
Local Hint Extern 10 ({_} _) =>
6
7
8
  repeat match goal with
  | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
  end; solve_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
9
10

Section lifting.
11
12
13
14
15
Context {Λ : language} {Σ : iFunctor}.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Implicit Types σ : state Λ.
Implicit Types Q : val Λ  iProp Λ Σ.
16
Transparent uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
17

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

Robbert Krebbers's avatar
Robbert Krebbers committed
20
Lemma wp_lift_step E1 E2
21
    (φ : expr Λ  state Λ  option (expr Λ)  Prop) Q e1 σ1 :
Robbert Krebbers's avatar
Robbert Krebbers committed
22
  E1  E2  to_val e1 = None 
23
  reducible e1 σ1 
Robbert Krebbers's avatar
Robbert Krebbers committed
24
  ( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  φ e2 σ2 ef) 
25
26
  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
27
28
29
30
31
32
33
   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. }
34
  { by rewrite assoc. }
Robbert Krebbers's avatar
Robbert Krebbers committed
35
36
37
38
  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. }
39
  { rewrite (comm _ r2) -assoc; eauto using wsat_le. }
Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
  by exists r1', r2'; split_ands; [| |by intros ? ->].
Qed.
42

43
Lemma wp_lift_pure_step E (φ : expr Λ  option (expr Λ)  Prop) Q e1 :
Robbert Krebbers's avatar
Robbert Krebbers committed
44
  to_val e1 = None 
45
  ( σ1, reducible e1 σ1) 
Robbert Krebbers's avatar
Robbert Krebbers committed
46
  ( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  σ1 = σ2  φ e2 ef) 
47
  (  e2 ef,  φ e2 ef  wp E e2 Q  wp_fork ef)  wp E e1 Q.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Proof.
49
50
  intros He Hsafe Hstep r n ? Hwp; constructor; auto.
  intros rf k Ef σ1 ???; split; [done|]. destruct n as [|n]; first lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
  intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
52
  destruct (Hwp e2 ef r k) as (r1&r2&Hr&?&?); auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
53
54
  exists r1,r2; split_ands; [rewrite -Hr| |by intros ? ->]; eauto using wsat_le.
Qed.
55
56

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

60
61
Lemma wp_lift_atomic_step {E Q} e1
    (φ : val Λ  state Λ  option (expr Λ)  Prop) σ1 :
62
63
  to_val e1 = None 
  reducible e1 σ1 
64
65
66
67
  ( 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.
68
Proof.
69
70
  intros. rewrite -(wp_lift_step E E (λ e2 σ2 ef,  v2,
    to_val e2 = Some v2  φ v2 σ2 ef) _ e1 σ1) //; [].
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.
74
  rewrite always_and_sep_l -assoc -always_and_sep_l.
75
76
77
  apply const_elim_l=>-[v2' [Hv ?]] /=.
  rewrite -pvs_intro.
  rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //.
78
  by rewrite left_id wand_elim_r -(wp_value' _ _ e2' v2').
79
80
Qed.

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

97
Lemma wp_lift_pure_det_step {E Q} e1 e2 ef :
98
99
  to_val e1 = None 
  ( σ1, reducible e1 σ1) 
100
101
  ( σ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.
102
Proof.
103
104
  intros.
  rewrite -(wp_lift_pure_step E (λ e2' ef', e2 = e2'  ef = ef') _ e1) //=.
105
  apply later_mono, forall_intro=>e'; apply forall_intro=>ef'.
106
  by apply impl_intro_l, const_elim_l=>-[-> ->].
107
108
Qed.

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