hoare.v 4 KB
Newer Older
1
Require Export program_logic.weakestpre program_logic.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
32
Proof. by intros P P' HP e ? <- Q Q' HQ; apply ht_mono. Qed.

Lemma ht_val E v :
33
  {{ True : iProp Λ Σ }} of_val v @ E {{ λ v', v = v' }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
Proof.
35
  apply (always_intro' _ _), impl_intro_l.
36
  by rewrite -wp_value; apply const_intro.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
38
Qed.
Lemma ht_vs E P P' Q Q' e :
39
  ((P ={E}=> P')  {{ P' }} e @ E {{ Q' }}   v, Q' v ={E}=> Q v)
Robbert Krebbers's avatar
Robbert Krebbers committed
40
41
   {{ P }} e @ E {{ Q }}.
Proof.
42
43
  apply (always_intro' _ _), impl_intro_l.
  rewrite (associative _ P) {1}/vs always_elim impl_elim_r.
44
45
46
  rewrite associative pvs_impl_r pvs_always_r wp_always_r.
  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
47
48
49
Qed.
Lemma ht_atomic E1 E2 P P' Q Q' e :
  E2  E1  atomic e 
50
  ((P ={E1,E2}=> P')  {{ P' }} e @ E2 {{ Q' }}   v, Q' v ={E2,E1}=> Q v)
Robbert Krebbers's avatar
Robbert Krebbers committed
51
52
   {{ P }} e @ E1 {{ Q }}.
Proof.
53
54
  intros ??; apply (always_intro' _ _), impl_intro_l.
  rewrite (associative _ P) {1}/vs always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
56
  rewrite (associative _) pvs_impl_r pvs_always_r wp_always_r.
  rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
57
  by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
Qed.
59
60
61
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
62
Proof.
63
64
  intros; apply (always_intro' _ _), impl_intro_l.
  rewrite (associative _ P) {1}/ht always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
  rewrite wp_always_r -wp_bind //; apply wp_mono=> v.
66
  by rewrite (forall_elim v) /ht always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
68
69
Qed.
Lemma ht_mask_weaken E1 E2 P Q e :
  E1  E2  {{ P }} e @ E1 {{ Q }}  {{ P }} e @ E2 {{ Q }}.
70
Proof. intros. by apply always_mono, impl_mono, wp_mask_frame_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
72
73
74
75
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.
76
  by rewrite wp_frame_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
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.
96
End hoare.