lifting.v 4.48 KB
Newer Older
1
2
From program_logic Require Export weakestpre.
From program_logic Require Import wsat ownership.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
Local Hint Extern 10 (_  _) => omega.
4
Local Hint Extern 100 (@eq coPset _ _) => set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
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
Context {Λ : language} {Σ : iFunctor}.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Implicit Types σ : state Λ.
15
16
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ : val Λ  iProp Λ Σ.
17
Transparent uPred_holds.
Robbert Krebbers's avatar
Robbert Krebbers committed
18

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

Robbert Krebbers's avatar
Robbert Krebbers committed
21
Lemma wp_lift_step E1 E2
22
    (φ : expr Λ  state Λ  option (expr Λ)  Prop) Φ e1 σ1 :
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  E1  E2  to_val e1 = None 
24
  reducible e1 σ1 
Robbert Krebbers's avatar
Robbert Krebbers committed
25
  ( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  φ e2 σ2 ef) 
26
  (|={E2,E1}=> ownP σ1    e2 σ2 ef,
27
28
    ( φ e2 σ2 ef  ownP σ2) - |={E1,E2}=> || e2 @ E2 {{ Φ }}  wp_fork ef)
   || e1 @ E2 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
29
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  intros ? He Hsafe Hstep n r ? Hvs; constructor; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33
34
  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. }
35
  { by rewrite assoc. }
Robbert Krebbers's avatar
Robbert Krebbers committed
36
  constructor; [done|intros e2 σ2 ef ?; specialize (Hws' σ2)].
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  destruct (λ H1 H2 H3, Hwp e2 σ2 ef k (update_pst σ2 r1) H1 H2 H3 rf k Ef σ2)
Robbert Krebbers's avatar
Robbert Krebbers committed
38
39
    as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'.
  { split. destruct k; try eapply Hstep; eauto. apply ownP_spec; auto. }
40
  { rewrite (comm _ r2) -assoc; eauto using wsat_le. }
41
  by exists r1', r2'; split_and?; [| |by intros ? ->].
Robbert Krebbers's avatar
Robbert Krebbers committed
42
Qed.
43

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

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

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

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

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

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