hoare.v 4.15 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 Λ) (Φ : val Λ  iProp Λ Σ) : iProp Λ Σ := ( (P  wp E e Φ))%I.
5
Instance: Params (@ht) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
6

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

Section hoare.
13
Context {Λ : language} {Σ : iFunctor}.
14 15
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ Ψ : val Λ  iProp Λ Σ.
16
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).
21
Proof. by intros P P' HP e ? <- Φ Φ' HΦ; rewrite /ht HP; setoid_rewrite HΦ. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
Global Instance ht_proper E :
23
  Proper (() ==> eq ==> pointwise_relation _ () ==> ()) (@ht Λ Σ E).
24 25 26
Proof. by intros P P' HP e ? <- Φ Φ' HΦ; rewrite /ht HP; setoid_rewrite HΦ. Qed.
Lemma ht_mono E P P' Φ Φ' e :
  P  P'  ( v, Φ' v  Φ v)  {{ P' }} e @ E {{ Φ' }}  {{ P }} e @ E {{ Φ }}.
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).
30
Proof. by intros P P' HP e ? <- Φ Φ' HΦ; apply ht_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
31

32
Lemma ht_alt E P Φ e : (P  wp E e Φ)  {{ P }} e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
Proof.
34
  intros; rewrite -{1}always_const. apply: always_intro. apply impl_intro_l.
35
  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.

42 43 44
Lemma ht_vs E P P' Φ Φ' e :
  ((P ={E}=> P')  {{ P' }} e @ E {{ Φ' }}   v, Φ' v ={E}=> Φ v)
   {{ P }} e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
Proof.
46
  apply: always_intro. apply 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
  rewrite -(pvs_wp E e Φ) -(wp_pvs E e Φ); apply pvs_mono, wp_mono=> v.
50
  by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
Qed.
52

53
Lemma ht_atomic E1 E2 P P' Φ Φ' e :
Robbert Krebbers's avatar
Robbert Krebbers committed
54
  E2  E1  atomic e 
55 56
  ((P ={E1,E2}=> P')  {{ P' }} e @ E2 {{ Φ' }}   v, Φ' v ={E2,E1}=> Φ v)
   {{ P }} e @ E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
57
Proof.
58
  intros ??; apply: always_intro. apply 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 Φ Φ' e :
  ({{ P }} e @ E {{ Φ }}   v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
   {{ P }} K e @ E {{ Φ' }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
Proof.
69
  intros; apply: always_intro. apply 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

75 76
Lemma ht_mask_weaken E1 E2 P Φ e :
  E1  E2  {{ P }} e @ E1 {{ Φ }}  {{ P }} e @ E2 {{ Φ }}.
77
Proof. intros. by apply always_mono, impl_mono, wp_mask_frame_mono. Qed.
78

79 80
Lemma ht_frame_l E P Φ R e :
  {{ P }} e @ E {{ Φ }}  {{ R  P }} e @ E {{ λ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
81
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

87 88
Lemma ht_frame_r E P Φ R e :
  {{ P }} e @ E {{ Φ }}  {{ P  R }} e @ E {{ λ v, Φ v  R }}.
89
Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
90

91
Lemma ht_frame_later_l E P R e Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
92
  to_val e = None 
93
  {{ P }} e @ E {{ Φ }}  {{  R  P }} e @ E {{ λ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
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

100
Lemma ht_frame_later_r E P Φ R e :
Robbert Krebbers's avatar
Robbert Krebbers committed
101
  to_val e = None 
102
  {{ P }} e @ E {{ Φ }}  {{ P   R }} e @ E {{ λ v, Φ v  R }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
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
End hoare.