hoare.v 5.19 KB
Newer Older
1 2
From iris.program_logic Require Export weakestpre.
From iris.base_logic.lib Require Export viewshifts.
3
From iris.proofmode Require Import tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
4

5 6
Definition ht `{irisG Λ Σ} (E : coPset) (P : iProp Σ)
    (e : expr Λ) (Φ : val Λ  iProp Σ) : iProp Σ :=
7
  ( (P - WP e @ E {{ Φ }}))%I.
8
Instance: Params (@ht) 4.
Robbert Krebbers's avatar
Robbert Krebbers committed
9

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

23
Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P e%E (λ v, Q))
24 25
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : uPred_scope.
26
Notation "{{ P } } e {{ v , Q } }" := (ht  P e%E (λ v, Q))
27 28
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  {{  v ,  Q  } }") : uPred_scope.
29
Notation "{{ P } } e @ E {{ v , Q } }" := (True  ht E P e%E (λ v, Q))
30 31
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : C_scope.
32
Notation "{{ P } } e {{ v , Q } }" := (True  ht  P e%E (λ v, Q))
33 34 35
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  {{  v ,  Q  } }") : C_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
36
Section hoare.
37 38 39
Context `{irisG Λ Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ Ψ : val Λ  iProp Σ.
40
Implicit Types v : val Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42 43
Import uPred.

Global Instance ht_ne E n :
44
  Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (ht E).
Ralf Jung's avatar
Ralf Jung committed
45
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
Global Instance ht_proper E :
47
  Proper (() ==> eq ==> pointwise_relation _ () ==> ()) (ht E).
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Proof. solve_proper. Qed.
49
Lemma ht_mono E P P' Φ Φ' e :
50
  (P  P')  ( v, Φ' v  Φ v)  {{ P' }} e @ E {{ Φ' }}  {{ P }} e @ E {{ Φ }}.
51
Proof. by intros; apply always_mono, wand_mono, wp_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
Global Instance ht_mono' E :
53
  Proper (flip () ==> eq ==> pointwise_relation _ () ==> ()) (ht E).
Robbert Krebbers's avatar
Robbert Krebbers committed
54
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
55

56
Lemma ht_alt E P Φ e : (P  WP e @ E {{ Φ }})  {{ P }} e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
57
Proof. iIntros (Hwp) "!# HP". by iApply Hwp. Qed.
58

59
Lemma ht_val E v : {{ True }} of_val v @ E {{ v', v = v' }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Proof. iIntros "!# _". by iApply wp_value'. Qed.
61

62
Lemma ht_vs E P P' Φ Φ' e :
63
  (P ={E}=> P')  {{ P' }} e @ E {{ Φ' }}  ( v, Φ' v ={E}=> Φ v)
64
   {{ P }} e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Proof.
66
  iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("Hvs" with "HP") as "HP".
67
  iApply wp_fupd; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
68
  iIntros (v) "Hv". by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
69
Qed.
70

71
Lemma ht_atomic E1 E2 P P' Φ Φ' e :
72
  atomic e 
73
  (P ={E1,E2}=> P')  {{ P' }} e @ E2 {{ Φ' }}  ( v, Φ' v ={E2,E1}=> Φ v)
74
   {{ P }} e @ E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
75
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
  iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ E2); auto.
77
  iMod ("Hvs" with "HP") as "HP". iModIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
  iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
79
  iIntros (v) "Hv". by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
80
Qed.
81

82
Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
83
  {{ P }} e @ E {{ Φ }}  ( v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
84
   {{ P }} K e @ E {{ Φ' }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
  iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
  iApply wp_wand_r; iSplitL; [by iApply "Hwpe"|].
88
  iIntros (v) "Hv". by iApply "HwpK".
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Qed.
90

91
Lemma ht_mask_weaken E1 E2 P Φ e :
92
  E1  E2  {{ P }} e @ E1 {{ Φ }}  {{ P }} e @ E2 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
  iIntros (?) "#Hwp !# HP". iApply (wp_mask_mono E1 E2); try done.
Robbert Krebbers's avatar
Robbert Krebbers committed
95 96
  by iApply "Hwp".
Qed.
97

98
Lemma ht_frame_l E P Φ R e :
99
  {{ P }} e @ E {{ Φ }}  {{ R  P }} e @ E {{ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
Proof. iIntros "#Hwp !# [$ HP]". by iApply "Hwp". Qed.
101

102
Lemma ht_frame_r E P Φ R e :
103
  {{ P }} e @ E {{ Φ }}  {{ P  R }} e @ E {{ v, Φ v  R }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
Proof. iIntros "#Hwp !# [HP $]". by iApply "Hwp". Qed.
105

106 107
Lemma ht_frame_step_l E1 E2 P R1 R2 e Φ :
  to_val e = None  E2  E1 
108
  (R1 ={E1,E2}=>  |={E2,E1}=> R2)  {{ P }} e @ E2 {{ Φ }}
109
   {{ R1  P }} e @ E1 {{ λ v, R2  Φ v }}.
110
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
  iIntros (??) "[#Hvs #Hwp] !# [HR HP]".
112 113
  iApply (wp_frame_step_l E1 E2); try done.
  iSplitL "HR"; [by iApply "Hvs"|by iApply "Hwp"].
114 115
Qed.

116 117
Lemma ht_frame_step_r E1 E2 P R1 R2 e Φ :
  to_val e = None  E2  E1 
118
  (R1 ={E1,E2}=>  |={E2,E1}=> R2)  {{ P }} e @ E2 {{ Φ }}
119
   {{ P  R1 }} e @ E1 {{ λ v, Φ v  R2 }}.
120
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
121
  iIntros (??) "[#Hvs #Hwp] !# [HP HR]".
122 123
  iApply (wp_frame_step_r E1 E2); try done.
  iSplitR "HR"; [by iApply "Hwp"|by iApply "Hvs"].
124 125
Qed.

Ralf Jung's avatar
Ralf Jung committed
126
Lemma ht_frame_step_l' E P R e Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
127
  to_val e = None 
128
  {{ P }} e @ E {{ Φ }}  {{  R  P }} e @ E {{ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
  iIntros (?) "#Hwp !# [HR HP]".
Ralf Jung's avatar
Ralf Jung committed
131
  iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
Robbert Krebbers's avatar
Robbert Krebbers committed
132
Qed.
133

Ralf Jung's avatar
Ralf Jung committed
134
Lemma ht_frame_step_r' E P Φ R e :
Robbert Krebbers's avatar
Robbert Krebbers committed
135
  to_val e = None 
136
  {{ P }} e @ E {{ Φ }}  {{ P   R }} e @ E {{ v, Φ v  R }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
  iIntros (?) "#Hwp !# [HP HR]".
Ralf Jung's avatar
Ralf Jung committed
139
  iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
Robbert Krebbers's avatar
Robbert Krebbers committed
140
Qed.
141
End hoare.