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

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

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

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

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

32
Lemma ht_alt E P Q e : (P  wp E e Q)  {{ P }} e @ E {{ Q }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
Proof.
34 35
  intros; rewrite -{1}always_const. apply (always_intro _ _), impl_intro_l.
  by rewrite always_const right_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
Qed.
37 38 39 40 41

Lemma ht_val E v :
  {{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}.
Proof. apply ht_alt. by rewrite -wp_value'; apply const_intro. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
42
Lemma ht_vs E P P' Q Q' e :
43
  ((P ={E}=> P')  {{ P' }} e @ E {{ Q' }}   v, Q' v ={E}=> Q v)
Robbert Krebbers's avatar
Robbert Krebbers committed
44 45
   {{ P }} e @ E {{ Q }}.
Proof.
46
  apply (always_intro _ _), impl_intro_l.
47 48
  rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
  rewrite assoc pvs_impl_r pvs_always_r wp_always_r.
49 50
  rewrite -(pvs_wp E e Q) -(wp_pvs E e Q); apply pvs_mono, wp_mono=> v.
  by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
Qed.
52

Robbert Krebbers's avatar
Robbert Krebbers committed
53 54
Lemma ht_atomic E1 E2 P P' Q Q' e :
  E2  E1  atomic e 
55
  ((P ={E1,E2}=> P')  {{ P' }} e @ E2 {{ Q' }}   v, Q' v ={E2,E1}=> Q v)
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57
   {{ P }} e @ E1 {{ Q }}.
Proof.
58
  intros ??; apply (always_intro _ _), impl_intro_l.
59 60
  rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
  rewrite assoc pvs_impl_r pvs_always_r wp_always_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
61
  rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
62
  by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Qed.
64

65 66 67
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
68
Proof.
69
  intros; apply (always_intro _ _), impl_intro_l.
70
  rewrite (assoc _ P) {1}/ht always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
  rewrite wp_always_r -wp_bind //; apply wp_mono=> v.
72
  by rewrite (forall_elim v) /ht always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
Qed.
74

Robbert Krebbers's avatar
Robbert Krebbers committed
75 76
Lemma ht_mask_weaken E1 E2 P Q e :
  E1  E2  {{ P }} e @ E1 {{ Q }}  {{ P }} e @ E2 {{ Q }}.
77
Proof. intros. by apply always_mono, impl_mono, wp_mask_frame_mono. Qed.
78

Robbert Krebbers's avatar
Robbert Krebbers committed
79 80 81
Lemma ht_frame_l E P Q R e :
  {{ P }} e @ E {{ Q }}  {{ R  P }} e @ E {{ λ v, R  Q v }}.
Proof.
82
  apply always_intro', impl_intro_l.
83
  rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
84
  by rewrite wp_frame_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Qed.
86

Robbert Krebbers's avatar
Robbert Krebbers committed
87 88
Lemma ht_frame_r E P Q R e :
  {{ P }} e @ E {{ Q }}  {{ P  R }} e @ E {{ λ v, Q v  R }}.
89
Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
90

Robbert Krebbers's avatar
Robbert Krebbers committed
91 92 93 94
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.
95
  intros; apply always_intro', impl_intro_l.
96
  rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
97 98
  by rewrite wp_frame_later_l //; apply wp_mono=>v; rewrite pvs_frame_l.
Qed.
99

Robbert Krebbers's avatar
Robbert Krebbers committed
100 101 102 103
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.
104
  rewrite (comm _ _ ( R)%I); setoid_rewrite (comm _ _ R).
Robbert Krebbers's avatar
Robbert Krebbers committed
105 106
  apply ht_frame_later_l.
Qed.
107

108
End hoare.