hoare_lifting.v 5.7 KB
Newer Older
1
2
3
From iris.algebra Require Import upred_tactics.
From iris.program_logic Require Export hoare lifting.
From iris.program_logic Require Import ownership.
4
Import uPred.
Robbert Krebbers's avatar
Robbert Krebbers committed
5

6
7
Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
  (default True%I ef (λ e, ht E P e Φ))
8
9
  (at level 20, P, ef, Φ at level 200,
   format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : uPred_scope.
10
Local Notation "{{ P } } ef ?@ E {{ Φ } }" :=
11
  (True  default True ef (λ e, ht E P e Φ))
12
13
  (at level 20, P, ef, Φ at level 200,
   format "{{  P  } }  ef  ?@  E  {{  Φ  } }") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
14
15

Section lifting.
16
Context {Λ : language} {Σ : iFunctor}.
17
Implicit Types e : expr Λ.
18
19
Implicit Types P Q R : iProp Λ Σ.
Implicit Types Ψ : val Λ  iProp Λ Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
20
21

Lemma ht_lift_step E1 E2
22
    (φ : expr Λ  state Λ  option (expr Λ)  Prop) P P' Φ1 Φ2 Ψ e1 σ1 :
Ralf Jung's avatar
Ralf Jung committed
23
  E2  E1  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) 
Ralf Jung's avatar
Ralf Jung committed
26
27
28
29
  ((P ={E1,E2}=>  ownP σ1   P') 
   ( e2 σ2 ef,  φ e2 σ2 ef  ownP σ2  P' ={E2,E1}=> Φ1 e2 σ2 ef  Φ2 e2 σ2 ef) 
   ( e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }}) 
   ( e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@  {{ λ _, True }}))
30
   {{ P }} e1 @ E1 {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
Proof.
32
  intros ?? Hsafe Hstep; apply: always_intro. apply impl_intro_l.
33
  rewrite (assoc _ P) {1}/vs always_elim impl_elim_r pvs_always_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
  rewrite -(wp_lift_step E1 E2 φ _ e1 σ1) //; apply pvs_mono.
35
  rewrite always_and_sep_r -assoc; apply sep_mono_r.
Ralf Jung's avatar
Ralf Jung committed
36
  rewrite [(_  _)%I]later_intro -later_sep; apply later_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
  apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
Ralf Jung's avatar
Ralf Jung committed
38
  do 3 rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef).
39
  apply wand_intro_l; rewrite !always_and_sep_l.
40
  (* Apply the view shift. *)
41
  rewrite (assoc _ _ P') -(assoc _ _ _ P') assoc.
Robbert Krebbers's avatar
Robbert Krebbers committed
42
43
  rewrite {1}/vs -always_wand_impl always_elim wand_elim_r.
  rewrite pvs_frame_r; apply pvs_mono.
44
  (* Now we're almost done. *)
Ralf Jung's avatar
Ralf Jung committed
45
  sep_split left: [Φ1 _ _ _; {{ Φ1 _ _ _ }} e2 @ E1 {{ Ψ }}]%I.
46
47
48
  - rewrite {1}/ht -always_wand_impl always_elim wand_elim_r //.
  - destruct ef as [e'|]; simpl; [|by apply const_intro].
    rewrite {1}/ht -always_wand_impl always_elim wand_elim_r //.
Robbert Krebbers's avatar
Robbert Krebbers committed
49
Qed.
50

51
52
Lemma ht_lift_atomic_step
    E (φ : expr Λ  state Λ  option (expr Λ)  Prop) P e1 σ1 :
Robbert Krebbers's avatar
Robbert Krebbers committed
53
  atomic e1 
54
  reducible e1 σ1 
Robbert Krebbers's avatar
Robbert Krebbers committed
55
  ( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  φ e2 σ2 ef) 
56
  ( e2 σ2 ef, {{  φ e2 σ2 ef  P }} ef ?@  {{ λ _, True }}) 
57
  {{  ownP σ1   P }} e1 @ E {{ λ v,  σ2 ef, ownP σ2   φ (of_val v) σ2 ef }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
59
60
61
62
Proof.
  intros ? Hsafe Hstep; set (φ' e σ ef := is_Some (to_val e)  φ e σ ef).
  rewrite -(ht_lift_step E E φ'  _ P
    (λ e2 σ2 ef, ownP σ2   (φ' e2 σ2 ef))%I
    (λ e2 σ2 ef,  φ e2 σ2 ef  P)%I);
63
    try by (rewrite /φ'; eauto using atomic_not_val, atomic_step).
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
  apply and_intro; [by rewrite -vs_reflexive; apply const_intro|].
  apply and_intro; [|apply and_intro; [|done]].
Ralf Jung's avatar
Ralf Jung committed
66
67
  - apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
    rewrite -vs_impl; apply: always_intro. apply impl_intro_l.
68
    rewrite and_elim_l !assoc; apply sep_mono; last done.
69
    rewrite -!always_and_sep_l -!always_and_sep_r; apply const_elim_l=>-[??].
Robbert Krebbers's avatar
Robbert Krebbers committed
70
    by repeat apply and_intro; try apply const_intro.
Ralf Jung's avatar
Ralf Jung committed
71
72
  - apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
    apply (always_intro _ _), impl_intro_l; rewrite and_elim_l.
73
    rewrite -always_and_sep_r; apply const_elim_r=>-[[v Hv] ?].
74
    rewrite -(of_to_val e2 v) // -wp_value'; [].
75
    rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
76
    by rewrite -always_and_sep_r; apply and_intro; try apply const_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
Qed.
78

79
Lemma ht_lift_pure_step E (φ : expr Λ  option (expr Λ)  Prop) P P' Ψ e1 :
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  to_val e1 = None 
81
  ( σ1, reducible e1 σ1) 
Robbert Krebbers's avatar
Robbert Krebbers committed
82
  ( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  σ1 = σ2  φ e2 ef) 
Ralf Jung's avatar
Ralf Jung committed
83
84
  (( e2 ef, {{  φ e2 ef  P }} e2 @ E {{ Ψ }}) 
   ( e2 ef, {{  φ e2 ef  P' }} ef ?@  {{ λ _, True }}))
85
   {{ (P  P') }} e1 @ E {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
Proof.
87
  intros ? Hsafe Hstep; apply: always_intro. apply impl_intro_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
  rewrite -(wp_lift_pure_step E φ _ e1) //.
Ralf Jung's avatar
Ralf Jung committed
89
  rewrite [(_   _, _)%I]later_intro -later_and; apply later_mono.
Robbert Krebbers's avatar
Robbert Krebbers committed
90
  apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l.
Ralf Jung's avatar
Ralf Jung committed
91
  do 2 rewrite (forall_elim e2) (forall_elim ef).
92
  rewrite always_and_sep_l !always_and_sep_r {1}(always_sep_dup ( _)).
93
  sep_split left: [ φ _ _; P; {{  φ _ _  P }} e2 @ E {{ Ψ }}]%I.
94
  - rewrite assoc {1}/ht -always_wand_impl always_elim wand_elim_r //.
95
96
  - destruct ef as [e'|]; simpl; [|by apply const_intro].
    rewrite assoc {1}/ht -always_wand_impl always_elim wand_elim_r //.
Robbert Krebbers's avatar
Robbert Krebbers committed
97
Qed.
98

99
Lemma ht_lift_pure_det_step
100
    E (φ : expr Λ  option (expr Λ)  Prop) P P' Ψ e1 e2 ef :
Robbert Krebbers's avatar
Robbert Krebbers committed
101
  to_val e1 = None 
102
  ( σ1, reducible e1 σ1) 
Robbert Krebbers's avatar
Robbert Krebbers committed
103
  ( σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef'  σ1 = σ2  e2 = e2'  ef = ef')
104
  ({{ P }} e2 @ E {{ Ψ }}  {{ P' }} ef ?@  {{ λ _, True }})
105
   {{ (P  P') }} e1 @ E {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
107
108
Proof.
  intros ? Hsafe Hdet.
  rewrite -(ht_lift_pure_step _ (λ e2' ef', e2 = e2'  ef = ef')); eauto.
Ralf Jung's avatar
Ralf Jung committed
109
110
111
  apply and_mono.
  - apply forall_intro=>e2'; apply forall_intro=>ef'.
    apply: always_intro. apply impl_intro_l.
112
    rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
    by rewrite /ht always_elim impl_elim_r.
Ralf Jung's avatar
Ralf Jung committed
114
115
  - apply forall_intro=>e2'; apply forall_intro=>ef'.
    destruct ef' as [e'|]; simpl; [|by apply const_intro].
116
    apply: always_intro. apply impl_intro_l.
117
    rewrite -always_and_sep_l -assoc; apply const_elim_l=>-[??]; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
119
    by rewrite /= /ht always_elim impl_elim_r.
Qed.
120

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