hoare.v 5.93 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.
4
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
5

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

11 12 13 14
Notation "{{ P } } e @ p ; E {{ Φ } }" := (ht p E P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  p ;  E  {{  Φ  } }") : C_scope.
Notation "{{ P } } e @ E {{ Φ } }" := (ht true E P%I e%E Φ%I)
15 16
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
17 18 19 20
Notation "{{ P } } e @ E ? {{ Φ } }" := (ht false E P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  E  ? {{  Φ  } }") : C_scope.
Notation "{{ P } } e {{ Φ } }" := (ht true  P%I e%E Φ%I)
21 22
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  {{  Φ  } }") : C_scope.
23 24 25
Notation "{{ P } } e ? {{ Φ } }" := (ht false  P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  ? {{  Φ  } }") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
26

27 28 29 30
Notation "{{ P } } e @ p ; E {{ v , Q } }" := (ht p E P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  p ;  E  {{  v ,  Q  } }") : C_scope.
Notation "{{ P } } e @ E {{ v , Q } }" := (ht true E P%I e%E (λ v, Q)%I)
31 32
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : C_scope.
33 34 35 36
Notation "{{ P } } e @ E ? {{ v , Q } }" := (ht false E P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  E  ? {{  v ,  Q  } }") : C_scope.
Notation "{{ P } } e {{ v , Q } }" := (ht true  P%I e%E (λ v, Q)%I)
37 38
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  {{  v ,  Q  } }") : C_scope.
39 40 41
Notation "{{ P } } e ? {{ v , Q } }" := (ht false  P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  ? {{  v ,  Q  } }") : C_scope.
42

Robbert Krebbers's avatar
Robbert Krebbers committed
43
Section hoare.
44 45 46
Context `{irisG Λ Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ Ψ : val Λ  iProp Σ.
47
Implicit Types v : val Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
48 49
Import uPred.

50 51
Global Instance ht_ne p E n :
  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (ht p E).
Ralf Jung's avatar
Ralf Jung committed
52
Proof. solve_proper. Qed.
53 54
Global Instance ht_proper p E :
  Proper (() ==> eq ==> pointwise_relation _ () ==> ()) (ht p E).
Robbert Krebbers's avatar
Robbert Krebbers committed
55
Proof. solve_proper. Qed.
56 57
Lemma ht_mono p E P P' Φ Φ' e :
  (P  P')  ( v, Φ' v  Φ v)  {{ P' }} e @ p; E {{ Φ' }}  {{ P }} e @ p; E {{ Φ }}.
58
Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
59 60
Global Instance ht_mono' p E :
  Proper (flip () ==> eq ==> pointwise_relation _ () ==> ()) (ht p E).
Robbert Krebbers's avatar
Robbert Krebbers committed
61
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
62

63
Lemma ht_alt p E P Φ e : (P  WP e @ p; E {{ Φ }})  {{ P }} e @ p; E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Proof. iIntros (Hwp) "!# HP". by iApply Hwp. Qed.
65

66
Lemma ht_val p E v : {{ True }} of_val v @ p; E {{ v', v = v' }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
Proof. iIntros "!# _". by iApply wp_value'. Qed.
68

69 70 71
Lemma ht_vs p E P P' Φ Φ' e :
  (P ={E}=> P')  {{ P' }} e @ p; E {{ Φ' }}  ( v, Φ' v ={E}=> Φ v)
   {{ P }} e @ p; E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Proof.
73
  iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("Hvs" with "HP") as "HP".
Robbert Krebbers's avatar
Robbert Krebbers committed
74
  iApply wp_fupd. iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
75
  iIntros (v) "Hv". by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Qed.
77

78 79 80 81
Lemma ht_atomic p E1 E2 P P' Φ Φ' e :
  StronglyAtomic e 
  (P ={E1,E2}=> P')  {{ P' }} e @ p; E2 {{ Φ' }}  ( v, Φ' v ={E2,E1}=> Φ v)
   {{ P }} e @ p; E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Proof.
83
  iIntros (?) "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ _ E2); auto.
84
  iMod ("Hvs" with "HP") as "HP". iModIntro.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
  iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
86
  iIntros (v) "Hv". by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
87
Qed.
88

89 90 91
Lemma ht_bind `{LanguageCtx Λ K} p E P Φ Φ' e :
  {{ P }} e @ p; E {{ Φ }}  ( v, {{ Φ v }} K (of_val v) @ p; E {{ Φ' }})
   {{ P }} K e @ p; E {{ Φ' }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
  iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
  iApply (wp_wand with "[HP]"); [by iApply "Hwpe"|].
95
  iIntros (v) "Hv". by iApply "HwpK".
Robbert Krebbers's avatar
Robbert Krebbers committed
96
Qed.
97

98 99 100 101 102 103 104 105
Lemma ht_forget_progress E P Φ e :
  {{ P }} e @ E {{ Φ }}  {{ P }} e @ E ?{{ Φ }}.
Proof.
  by iIntros "#Hwp !# ?"; iApply wp_forget_progress; iApply "Hwp".
Qed.

Lemma ht_mask_weaken p E1 E2 P Φ e :
  E1  E2  {{ P }} e @ p; E1 {{ Φ }}  {{ P }} e @ p; E2 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
Proof.
107
  iIntros (?) "#Hwp !# HP". iApply (wp_mask_mono _ E1 E2); try done.
Robbert Krebbers's avatar
Robbert Krebbers committed
108 109
  by iApply "Hwp".
Qed.
110

111 112
Lemma ht_frame_l p E P Φ R e :
  {{ P }} e @ p; E {{ Φ }}  {{ R  P }} e @ p; E {{ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
113
Proof. iIntros "#Hwp !# [$ HP]". by iApply "Hwp". Qed.
114

115 116
Lemma ht_frame_r p E P Φ R e :
  {{ P }} e @ p; E {{ Φ }}  {{ P  R }} e @ p; E {{ v, Φ v  R }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Proof. iIntros "#Hwp !# [HP $]". by iApply "Hwp". Qed.
118

119
Lemma ht_frame_step_l p E1 E2 P R1 R2 e Φ :
120
  to_val e = None  E2  E1 
121 122
  (R1 ={E1,E2}=>  |={E2,E1}=> R2)  {{ P }} e @ p; E2 {{ Φ }}
   {{ R1  P }} e @ p; E1 {{ λ v, R2  Φ v }}.
123
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
  iIntros (??) "[#Hvs #Hwp] !# [HR HP]".
125
  iApply (wp_frame_step_l _ E1 E2); try done.
126
  iSplitL "HR"; [by iApply "Hvs"|by iApply "Hwp"].
127 128
Qed.

129
Lemma ht_frame_step_r p E1 E2 P R1 R2 e Φ :
130
  to_val e = None  E2  E1 
131 132
  (R1 ={E1,E2}=>  |={E2,E1}=> R2)  {{ P }} e @ p; E2 {{ Φ }}
   {{ P  R1 }} e @ p; E1 {{ λ v, Φ v  R2 }}.
133
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
  iIntros (??) "[#Hvs #Hwp] !# [HP HR]".
135
  iApply (wp_frame_step_r _ E1 E2); try done.
136
  iSplitR "HR"; [by iApply "Hwp"|by iApply "Hvs"].
137 138
Qed.

139
Lemma ht_frame_step_l' p E P R e Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
140
  to_val e = None 
141
  {{ P }} e @ p; E {{ Φ }}  {{  R  P }} e @ p; E {{ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
  iIntros (?) "#Hwp !# [HR HP]".
Ralf Jung's avatar
Ralf Jung committed
144
  iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Qed.
146

147
Lemma ht_frame_step_r' p E P Φ R e :
Robbert Krebbers's avatar
Robbert Krebbers committed
148
  to_val e = None 
149
  {{ P }} e @ p; E {{ Φ }}  {{ P   R }} e @ p; E {{ v, Φ v  R }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
  iIntros (?) "#Hwp !# [HP HR]".
Ralf Jung's avatar
Ralf Jung committed
152
  iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
Robbert Krebbers's avatar
Robbert Krebbers committed
153
Qed.
154
End hoare.