hoare.v 4.16 KB
Newer Older
1
Require Export program_logic.weakestpre program_logic.viewshifts.
Robbert Krebbers's avatar
Robbert Krebbers committed
2

3 4
Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
    (e : expr Λ) (Q : val Λ  iProp Λ Σ) : iProp Λ Σ :=
Robbert Krebbers's avatar
Robbert Krebbers committed
5
  ( (P  wp E e (λ v, pvs E E (Q v))))%I.
6
Instance: Params (@ht) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
7 8

Notation "{{ P } } e @ E {{ Q } }" := (ht E P e Q)
9
  (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : uPred_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
Notation "{{ P } } e @ E {{ Q } }" := (True  ht E P e Q)
11
  (at level 74, format "{{  P  } }  e  @  E  {{  Q  } }") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13

Section hoare.
14 15 16 17
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P : iProp Λ Σ.
Implicit Types Q : val Λ  iProp Λ Σ.
Implicit Types v : val Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
18 19 20
Import uPred.

Global Instance ht_ne E n :
21
  Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (@ht Λ Σ E).
Robbert Krebbers's avatar
Robbert Krebbers committed
22 23
Proof. by intros P P' HP e ? <- Q Q' HQ; rewrite /ht HP; setoid_rewrite HQ. Qed.
Global Instance ht_proper E :
24
  Proper (() ==> eq ==> pointwise_relation _ () ==> ()) (@ht Λ Σ E).
Robbert Krebbers's avatar
Robbert Krebbers committed
25 26 27 28 29
Proof. by intros P P' HP e ? <- Q Q' HQ; rewrite /ht HP; setoid_rewrite HQ. Qed.
Lemma ht_mono E P P' Q Q' e :
  P  P'  ( v, Q' v  Q v)  {{ P' }} e @ E {{ Q' }}  {{ P }} e @ E {{ Q }}.
Proof. by intros HP HQ; rewrite /ht -HP; setoid_rewrite HQ. Qed.
Global Instance ht_mono' E :
30
  Proper (flip () ==> eq ==> pointwise_relation _ () ==> ()) (@ht Λ Σ E).
Robbert Krebbers's avatar
Robbert Krebbers committed
31 32 33
Proof. by intros P P' HP e ? <- Q Q' HQ; apply ht_mono. Qed.

Lemma ht_val E v :
34
  {{ True : iProp Λ Σ }} of_val v @ E {{ λ v',  (v = v') }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
35
Proof.
36
  apply (always_intro' _ _), impl_intro_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
37 38 39 40 41 42
  by rewrite -wp_value -pvs_intro; apply const_intro.
Qed.
Lemma ht_vs E P P' Q Q' e :
  (P >{E}> P'  {{ P' }} e @ E {{ Q' }}   v, Q' v >{E}> Q v)
   {{ P }} e @ E {{ Q }}.
Proof.
43 44
  apply (always_intro' _ _), impl_intro_l.
  rewrite (associative _ P) {1}/vs always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46
  rewrite (associative _) pvs_impl_r pvs_always_r wp_always_r.
  rewrite wp_pvs; apply wp_mono=> v.
47
  by rewrite (forall_elim v) pvs_impl_r !pvs_trans'.
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49 50 51 52 53
Qed.
Lemma ht_atomic E1 E2 P P' Q Q' e :
  E2  E1  atomic e 
  (P >{E1,E2}> P'  {{ P' }} e @ E2 {{ Q' }}   v, Q' v >{E2,E1}> Q v)
   {{ P }} e @ E1 {{ Q }}.
Proof.
54 55
  intros ??; apply (always_intro' _ _), impl_intro_l.
  rewrite (associative _ P) {1}/vs always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57
  rewrite (associative _) pvs_impl_r pvs_always_r wp_always_r.
  rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
58
  rewrite (forall_elim v) pvs_impl_r -(pvs_intro E1) pvs_trans; solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
Qed.
60 61 62
Lemma ht_bind `{LanguageCtx Λ K} E P Q Q' e :
  ({{ P }} e @ E {{ Q }}   v, {{ Q v }} K (of_val v) @ E {{ Q' }})
   {{ P }} K e @ E {{ Q' }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Proof.
64 65
  intros; apply (always_intro' _ _), impl_intro_l.
  rewrite (associative _ P) {1}/ht always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  rewrite wp_always_r -wp_bind //; apply wp_mono=> v.
67
  rewrite (forall_elim v) pvs_impl_r wp_pvs; apply wp_mono=> v'.
Robbert Krebbers's avatar
Robbert Krebbers committed
68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
  by rewrite pvs_trans'.
Qed.
Lemma ht_mask_weaken E1 E2 P Q e :
  E1  E2  {{ P }} e @ E1 {{ Q }}  {{ P }} e @ E2 {{ Q }}.
Proof.
  intros; apply always_mono, impl_intro_l; rewrite impl_elim_r.
  by rewrite -(wp_mask_weaken E1) //; apply wp_mono=> v; apply pvs_mask_weaken.
Qed.
Lemma ht_frame_l E P Q R e :
  {{ P }} e @ E {{ Q }}  {{ R  P }} e @ E {{ λ v, R  Q v }}.
Proof.
  apply always_intro, impl_intro_l.
  rewrite always_and_sep_r -(associative _) (sep_and P) always_elim impl_elim_r.
  by rewrite wp_frame_l; apply wp_mono=>v; rewrite pvs_frame_l.
Qed.
Lemma ht_frame_r E P Q R e :
  {{ P }} e @ E {{ Q }}  {{ P  R }} e @ E {{ λ v, Q v  R }}.
Proof. setoid_rewrite (commutative _ _ R); apply ht_frame_l. Qed.
Lemma ht_frame_later_l E P R e Q :
  to_val e = None 
  {{ P }} e @ E {{ Q }}  {{  R  P }} e @ E {{ λ v, R  Q v }}.
Proof.
  intros; apply always_intro, impl_intro_l.
  rewrite always_and_sep_r -(associative _) (sep_and P) always_elim impl_elim_r.
  by rewrite wp_frame_later_l //; apply wp_mono=>v; rewrite pvs_frame_l.
Qed.
Lemma ht_frame_later_r E P R e Q :
  to_val e = None 
  {{ P }} e @ E {{ Q }}  {{ P   R }} e @ E {{ λ v, Q v  R }}.
Proof.
  rewrite (commutative _ _ ( R)%I); setoid_rewrite (commutative _ _ R).
  apply ht_frame_later_l.
Qed.
End hoare.