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

8
Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e Φ)
9 10 11 12 13
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  E  {{  Φ  } }") : uPred_scope.
Notation "{{ P } } e {{ Φ } }" := (ht  P e Φ)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  {{  Φ  } }") : uPred_scope.
14
Notation "{{ P } } e @ E {{ Φ } }" := (True  ht E P e Φ)
15 16 17 18 19
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
Notation "{{ P } } e {{ Φ } }" := (True  ht  P e Φ)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  {{  Φ  } }") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
20 21

Section hoare.
22
Context {Λ : language} {Σ : iFunctor}.
23 24
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ Ψ : val Λ  iProp Λ Σ.
25
Implicit Types v : val Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
26 27 28
Import uPred.

Global Instance ht_ne E n :
29
  Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (@ht Λ Σ E).
Ralf Jung's avatar
Ralf Jung committed
30
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
Global Instance ht_proper E :
32
  Proper (() ==> eq ==> pointwise_relation _ () ==> ()) (@ht Λ Σ E).
33 34 35
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 {{ Φ }}.
36
Proof. by intros; apply always_mono, impl_mono, wp_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
37
Global Instance ht_mono' E :
38
  Proper (flip () ==> eq ==> pointwise_relation _ () ==> ()) (@ht Λ Σ E).
39
Proof. by intros P P' HP e ? <- Φ Φ' HΦ; apply ht_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
40

41
Lemma ht_alt E P Φ e : (P  || e @ E {{ Φ }})  {{ P }} e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
42
Proof.
43
  intros; rewrite -{1}always_const. apply: always_intro. apply impl_intro_l.
44
  by rewrite always_const right_id.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
Qed.
46 47 48 49 50

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.

51 52 53
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
54
Proof.
55
  apply: always_intro. apply impl_intro_l.
56 57
  rewrite (assoc _ P) {1}/vs always_elim impl_elim_r.
  rewrite assoc pvs_impl_r pvs_always_r wp_always_r.
58
  rewrite -(pvs_wp E e Φ) -(wp_pvs E e Φ); apply pvs_mono, wp_mono=> v.
59
  by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Qed.
61

62
Lemma ht_atomic E1 E2 P P' Φ Φ' e :
Robbert Krebbers's avatar
Robbert Krebbers committed
63
  E2  E1  atomic e 
64 65
  ((P ={E1,E2}=> P')  {{ P' }} e @ E2 {{ Φ' }}   v, Φ' v ={E2,E1}=> Φ v)
   {{ P }} e @ E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Proof.
67
  intros ??; apply: always_intro. apply impl_intro_l.
68 69
  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
70
  rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
71
  by rewrite (forall_elim v) {1}/vs always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Qed.
73

74 75 76
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
77
Proof.
78
  intros; apply: always_intro. apply impl_intro_l.
79
  rewrite (assoc _ P) {1}/ht always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
  rewrite wp_always_r -wp_bind //; apply wp_mono=> v.
81
  by rewrite (forall_elim v) /ht always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Qed.
83

84 85
Lemma ht_mask_weaken E1 E2 P Φ e :
  E1  E2  {{ P }} e @ E1 {{ Φ }}  {{ P }} e @ E2 {{ Φ }}.
86
Proof. intros. by apply always_mono, impl_mono, wp_mask_frame_mono. Qed.
87

88 89
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
90
Proof.
91
  apply always_intro', impl_intro_l.
92
  rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
93
  by rewrite wp_frame_l.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
Qed.
95

96 97
Lemma ht_frame_r E P Φ R e :
  {{ P }} e @ E {{ Φ }}  {{ P  R }} e @ E {{ λ v, Φ v  R }}.
98
Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
99

100
Lemma ht_frame_later_l E P R e Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
101
  to_val e = None 
102
  {{ P }} e @ E {{ Φ }}  {{  R  P }} e @ E {{ λ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
Proof.
104
  intros; apply always_intro', impl_intro_l.
105
  rewrite always_and_sep_r -assoc (sep_and P) always_elim impl_elim_r.
Robbert Krebbers's avatar
Robbert Krebbers committed
106 107
  by rewrite wp_frame_later_l //; apply wp_mono=>v; rewrite pvs_frame_l.
Qed.
108

109
Lemma ht_frame_later_r E P Φ R e :
Robbert Krebbers's avatar
Robbert Krebbers committed
110
  to_val e = None 
111
  {{ P }} e @ E {{ Φ }}  {{ P   R }} e @ E {{ λ v, Φ v  R }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
112
Proof.
113
  rewrite (comm _ _ ( R)%I); setoid_rewrite (comm _ _ R).
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115
  apply ht_frame_later_l.
Qed.
116
End hoare.