weakestpre.v 13.9 KB
Newer Older
1
2
From iris.base_logic.lib Require Export fancy_updates.
From iris.program_logic Require Export language.
3
From iris.base_logic Require Import big_op.
4
From iris.proofmode Require Import tactics classes.
5
From iris.algebra Require Import auth.
6
7
Import uPred.

8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
Class irisG' (Λstate : Type) (Σ : gFunctors) : Set := IrisG {
  iris_invG :> invG Σ;
  state_inG :> inG Σ (authR (optionUR (exclR (leibnizC Λstate))));
  state_name : gname;
}.
Notation irisG Λ Σ := (irisG' (state Λ) Σ).

Definition ownP `{irisG' Λstate Σ} (σ : Λstate) : iProp Σ :=
  own state_name ( (Excl' σ)).
Typeclasses Opaque ownP.
Instance: Params (@ownP) 3.

Definition ownP_auth `{irisG' Λstate Σ} (σ : Λstate) : iProp Σ :=
  own state_name ( (Excl' (σ:leibnizC Λstate))).
Typeclasses Opaque ownP_auth.
Instance: Params (@ownP_auth) 4.

25
26
27
28
Definition wp_pre `{irisG Λ Σ}
    (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
    coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ, (
  (* value case *)
Ralf Jung's avatar
Ralf Jung committed
29
  ( v, to_val e1 = Some v  |={E}=> Φ v) 
30
  (* step case *)
Ralf Jung's avatar
Ralf Jung committed
31
32
33
  (to_val e1 = None   σ1,
     ownP_auth σ1 ={E,}= reducible e1 σ1 
       e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,E}=
34
35
       ownP_auth σ2  wp E e2 Φ 
       [ list] ef  efs, wp  ef (λ _, True)))%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
36

37
38
39
Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
Proof.
  rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
40
  repeat (f_contractive || f_equiv); apply Hwp.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
Qed.
42

43
44
Definition wp_def `{irisG Λ Σ} :
  coPset  expr Λ  (val Λ  iProp Σ)  iProp Σ := fixpoint wp_pre.
Ralf Jung's avatar
Ralf Jung committed
45
46
47
48
Definition wp_aux : { x | x = @wp_def }. by eexists. Qed.
Definition wp := proj1_sig wp_aux.
Definition wp_eq : @wp = @wp_def := proj2_sig wp_aux.

Janno's avatar
Janno committed
49
Arguments wp {_ _ _} _ _%E _.
50
Instance: Params (@wp) 5.
Robbert Krebbers's avatar
Robbert Krebbers committed
51

Janno's avatar
Janno committed
52
Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
53
  (at level 20, e, Φ at level 200,
54
   format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
Janno's avatar
Janno committed
55
Notation "'WP' e {{ Φ } }" := (wp  e%E Φ)
56
  (at level 20, e, Φ at level 200,
57
   format "'WP'  e  {{  Φ  } }") : uPred_scope.
58

Janno's avatar
Janno committed
59
Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q))
60
61
  (at level 20, e, Q at level 200,
   format "'WP'  e  @  E  {{  v ,  Q  } }") : uPred_scope.
Janno's avatar
Janno committed
62
Notation "'WP' e {{ v , Q } }" := (wp  e%E (λ v, Q))
63
64
65
  (at level 20, e, Q at level 200,
   format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.

Ralf Jung's avatar
Ralf Jung committed
66
(* Texan triples *)
67
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
Ralf Jung's avatar
Ralf Jung committed
68
  (  Φ,
69
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }})%I
Ralf Jung's avatar
Ralf Jung committed
70
    (at level 20, x closed binder, y closed binder,
71
72
     format "{{{  P  } } }  e  {{{  x .. y ,   RET  pat ;  Q } } }") : uPred_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
Ralf Jung's avatar
Ralf Jung committed
73
  (  Φ,
74
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})%I
Ralf Jung's avatar
Ralf Jung committed
75
    (at level 20, x closed binder, y closed binder,
76
77
     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q } } }") : uPred_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
78
  (  Φ, P -  (Q - Φ pat%V) - WP e {{ Φ }})%I
Ralf Jung's avatar
Ralf Jung committed
79
    (at level 20,
80
81
     format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : uPred_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
82
  (  Φ, P -  (Q - Φ pat%V) - WP e @ E {{ Φ }})%I
Ralf Jung's avatar
Ralf Jung committed
83
    (at level 20,
84
     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q } } }") : uPred_scope.
Ralf Jung's avatar
Ralf Jung committed
85

86
Notation "'{{{' P } } } e {{{ x .. y , 'RET' pat ; Q } } }" :=
87
  ( Φ : _  uPred _,
88
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e {{ Φ }})
89
    (at level 20, x closed binder, y closed binder,
90
91
     format "{{{  P  } } }  e  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
Notation "'{{{' P } } } e @ E {{{ x .. y , 'RET' pat ; Q } } }" :=
92
  ( Φ : _  uPred _,
93
      P -  ( x, .. ( y, Q - Φ pat%V) .. ) - WP e @ E {{ Φ }})
Ralf Jung's avatar
Ralf Jung committed
94
    (at level 20, x closed binder, y closed binder,
95
96
     format "{{{  P  } } }  e  @  E  {{{  x .. y ,  RET  pat ;  Q } } }") : C_scope.
Notation "'{{{' P } } } e {{{ 'RET' pat ; Q } } }" :=
97
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e {{ Φ }})
98
    (at level 20,
99
100
     format "{{{  P  } } }  e  {{{  RET  pat ;  Q } } }") : C_scope.
Notation "'{{{' P } } } e @ E {{{ 'RET' pat ; Q } } }" :=
101
  ( Φ : _  uPred _, P -  (Q - Φ pat%V) - WP e @ E {{ Φ }})
Ralf Jung's avatar
Ralf Jung committed
102
    (at level 20,
103
     format "{{{  P  } } }  e  @  E  {{{  RET  pat ;  Q } } }") : C_scope.
104

Robbert Krebbers's avatar
Robbert Krebbers committed
105
Section wp.
106
107
108
Context `{irisG Λ Σ}.
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
109
110
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
111

112
(* Physical state *)
113
Lemma ownP_twice σ1 σ2 : ownP σ1  ownP σ2  False.
114
Proof. rewrite /ownP -own_op own_valid. by iIntros (?). Qed.
115
116
117
Global Instance ownP_timeless σ : TimelessP (@ownP (state Λ) Σ _ σ).
Proof. rewrite /ownP; apply _. Qed.

Ralf Jung's avatar
Ralf Jung committed
118
Lemma ownP_agree σ1 σ2 : ownP_auth σ1  ownP σ2  ⌜σ1 = σ2.
119
Proof.
120
  rewrite /ownP /ownP_auth -own_op own_valid -auth_both_op.
121
122
  by iIntros ([[[] [=]%leibniz_equiv] _]%auth_valid_discrete).
Qed.
123
Lemma ownP_update σ1 σ2 : ownP_auth σ1  ownP σ1 == ownP_auth σ2  ownP σ2.
124
125
126
127
128
129
Proof.
  rewrite /ownP -!own_op.
  by apply own_update, auth_update, option_local_update, exclusive_local_update.
Qed.

(* Weakest pre *)
130
131
132
Lemma wp_unfold E e Φ : WP e @ E {{ Φ }}  wp_pre wp E e Φ.
Proof. rewrite wp_eq. apply (fixpoint_unfold wp_pre). Qed.

133
Global Instance wp_ne E e n :
134
  Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
135
Proof.
136
  revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
137
138
139
140
141
142
  rewrite !wp_unfold /wp_pre.
  (* FIXME: figure out a way to properly automate this proof *)
  (* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
  is very slow here *)
  do 18 (f_contractive || f_equiv). apply IH; first lia.
  intros v. eapply dist_le; eauto with omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
143
144
Qed.
Global Instance wp_proper E e :
145
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ E e).
Robbert Krebbers's avatar
Robbert Krebbers committed
146
Proof.
147
  by intros Φ Φ' ?; apply equiv_dist=>n; apply wp_ne=>v; apply equiv_dist.
Robbert Krebbers's avatar
Robbert Krebbers committed
148
Qed.
149

150
Lemma wp_value' E Φ v : Φ v  WP of_val v @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
Proof.
152
153
  iIntros "HΦ". rewrite wp_unfold /wp_pre.
  iLeft; iExists v; rewrite to_of_val; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
Qed.
155
Lemma wp_value_inv E Φ v : WP of_val v @ E {{ Φ }} ={E}= Φ v.
Ralf Jung's avatar
Ralf Jung committed
156
Proof.
157
158
  rewrite wp_unfold /wp_pre to_of_val. iIntros "[H|[% _]]"; [|done].
  by iDestruct "H" as (v') "[% ?]"; simplify_eq.
Ralf Jung's avatar
Ralf Jung committed
159
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
160

161
Lemma wp_strong_mono E1 E2 e Φ Ψ :
162
  E1  E2  ( v, Φ v ={E2}= Ψ v)  WP e @ E1 {{ Φ }}  WP e @ E2 {{ Ψ }}.
163
Proof.
164
  iIntros (?) "[HΦ H]". iLöb as "IH" forall (e). rewrite !wp_unfold /wp_pre.
165
166
  iDestruct "H" as "[Hv|[% H]]"; [iLeft|iRight].
  { iDestruct "Hv" as (v) "[% Hv]". iExists v; iSplit; first done.
167
    iApply ("HΦ" with ">[-]"). by iApply (fupd_mask_mono E1 _). }
168
  iSplit; [done|]; iIntros (σ1) "Hσ".
169
170
171
172
173
  iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
  iMod ("H" $! σ1 with "Hσ") as "[$ H]".
  iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
  iMod ("H" $! _ σ2 efs with "[#]") as "($ & H & $)"; auto.
  iMod "Hclose" as "_". by iApply ("IH" with "HΦ").
174
175
Qed.

176
Lemma fupd_wp E e Φ : (|={E}=> WP e @ E {{ Φ }})  WP e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
177
Proof.
178
179
  rewrite wp_unfold /wp_pre. iIntros "H". destruct (to_val e) as [v|] eqn:?.
  { iLeft. iExists v; iSplit; first done.
180
    by iMod "H" as "[H|[% ?]]"; [iDestruct "H" as (v') "[% ?]"|]; simplify_eq. }
181
  iRight; iSplit; [done|]; iIntros (σ1) "Hσ1".
182
  iMod "H" as "[H|[% H]]"; last by iApply "H".
183
  iDestruct "H" as (v') "[% ?]"; simplify_eq.
184
Qed.
185
Lemma wp_fupd E e Φ : WP e @ E {{ v, |={E}=> Φ v }}  WP e @ E {{ Φ }}.
186
Proof. iIntros "H". iApply (wp_strong_mono E); try iFrame; auto. Qed.
187

188
Lemma wp_atomic E1 E2 e Φ :
189
  atomic e 
190
  (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }})  WP e @ E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
191
Proof.
192
  iIntros (Hatomic) "H". destruct (to_val e) as [v|] eqn:He.
193
  { apply of_to_val in He as <-. iApply wp_fupd. iApply wp_value'.
194
    iMod "H". by iMod (wp_value_inv with "H"). }
195
  setoid_rewrite wp_unfold; rewrite /wp_pre. iRight; iSplit; auto.
196
  iIntros (σ1) "Hσ". iMod "H" as "[H|[_ H]]".
197
  { iDestruct "H" as (v') "[% ?]"; simplify_eq. }
198
199
  iMod ("H" $! σ1 with "Hσ") as "[$ H]".
  iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
200
201
202
203
204
205
206
207
  iMod ("H" with "* []") as "(Hphy & H & $)"; first done.
  rewrite wp_unfold /wp_pre. iDestruct "H" as "[H|H]".
  - iDestruct "H" as (v) "[% >>?]". iModIntro. iFrame.
    rewrite -(of_to_val e2 v) //. by iApply wp_value'.
  - iDestruct "H" as "[_ H]".
    iMod ("H" with "* Hphy") as "[H _]".
    iDestruct "H" as %(? & ? & ? & ?). exfalso.
    by eapply (Hatomic _ _ _ _ Hstep).
Robbert Krebbers's avatar
Robbert Krebbers committed
208
Qed.
209

210
Lemma wp_fupd_step E1 E2 e P Φ :
211
  to_val e = None  E2  E1 
212
  (|={E1,E2}=> P) - WP e @ E2 {{ v, P ={E1}= Φ v }} - WP e @ E1 {{ Φ }}.
213
Proof.
214
  rewrite !wp_unfold /wp_pre. iIntros (??) "HR [Hv|[_ H]]".
215
216
  { iDestruct "Hv" as (v) "[% Hv]"; simplify_eq. }
  iRight; iSplit; [done|]. iIntros (σ1) "Hσ".
217
218
219
  iMod "HR". iMod ("H" $! _ with "Hσ") as "[$ H]".
  iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
  iMod ("H" $! e2 σ2 efs with "[%]") as "($ & H & $)"; auto.
220
221
  iMod "HR". iModIntro. iApply (wp_strong_mono E2); first done.
  iSplitR "H"; last iExact "H". iIntros (v) "H". by iApply "H".
Robbert Krebbers's avatar
Robbert Krebbers committed
222
Qed.
223

224
Lemma wp_bind K `{!LanguageCtx Λ K} E e Φ :
225
  WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }}  WP K e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
226
Proof.
227
  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite wp_unfold /wp_pre.
228
229
  iDestruct "H" as "[Hv|[% H]]".
  { iDestruct "Hv" as (v) "[Hev Hv]"; iDestruct "Hev" as % <-%of_to_val.
230
    by iApply fupd_wp. }
231
  rewrite wp_unfold /wp_pre. iRight; iSplit; eauto using fill_not_val.
232
233
  iIntros (σ1) "Hσ". iMod ("H" $! _ with "Hσ") as "[% H]".
  iModIntro; iSplit.
234
  { iPureIntro. unfold reducible in *. naive_solver eauto using fill_step. }
235
236
  iNext; iIntros (e2 σ2 efs Hstep).
  destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
237
  iMod ("H" $! e2' σ2 efs with "[%]") as "($ & H & $)"; auto.
238
  by iApply "IH".
Robbert Krebbers's avatar
Robbert Krebbers committed
239
240
Qed.

241
(** * Derived rules *)
242
Lemma wp_mono E e Φ Ψ : ( v, Φ v  Ψ v)  WP e @ E {{ Φ }}  WP e @ E {{ Ψ }}.
243
244
Proof.
  iIntros (HΦ) "H"; iApply (wp_strong_mono E E); auto.
245
  iFrame. iIntros (v) "?". by iApply HΦ.
246
247
248
Qed.
Lemma wp_mask_mono E1 E2 e Φ : E1  E2  WP e @ E1 {{ Φ }}  WP e @ E2 {{ Φ }}.
Proof. iIntros (?) "H"; iApply (wp_strong_mono E1 E2); auto. iFrame; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
249
Global Instance wp_mono' E e :
250
  Proper (pointwise_relation _ () ==> ()) (@wp Λ Σ _ E e).
251
Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
252

253
Lemma wp_value E Φ e v : to_val e = Some v  Φ v  WP e @ E {{ Φ }}.
254
Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed.
255
256
257
Lemma wp_value_fupd' E Φ v : (|={E}=> Φ v)  WP of_val v @ E {{ Φ }}.
Proof. intros. by rewrite -wp_fupd -wp_value'. Qed.
Lemma wp_value_fupd E Φ e v :
258
  to_val e = Some v  (|={E}=> Φ v)  WP e @ E {{ Φ }}.
259
Proof. intros. rewrite -wp_fupd -wp_value //. Qed.
260

261
Lemma wp_frame_l E e Φ R : R  WP e @ E {{ Φ }}  WP e @ E {{ v, R  Φ v }}.
262
Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed.
263
Lemma wp_frame_r E e Φ R : WP e @ E {{ Φ }}  R  WP e @ E {{ v, Φ v  R }}.
264
265
Proof. iIntros "[??]". iApply (wp_strong_mono E E _ Φ); try iFrame; eauto. Qed.

266
267
268
269
270
271
272
Lemma wp_frame_step_l E1 E2 e Φ R :
  to_val e = None  E2  E1 
  (|={E1,E2}=> R)  WP e @ E2 {{ Φ }}  WP e @ E1 {{ v, R  Φ v }}.
Proof.
  iIntros (??) "[Hu Hwp]". iApply (wp_fupd_step with "Hu"); try done.
  iApply (wp_mono with "Hwp"). by iIntros (?) "$$".
Qed.
273
274
Lemma wp_frame_step_r E1 E2 e Φ R :
  to_val e = None  E2  E1 
275
  WP e @ E2 {{ Φ }}  (|={E1,E2}=> R)  WP e @ E1 {{ v, Φ v  R }}.
Ralf Jung's avatar
Ralf Jung committed
276
Proof.
277
  rewrite [(WP _ @ _ {{ _ }}  _)%I]comm; setoid_rewrite (comm _ _ R).
278
  apply wp_frame_step_l.
Ralf Jung's avatar
Ralf Jung committed
279
280
Qed.
Lemma wp_frame_step_l' E e Φ R :
281
  to_val e = None   R  WP e @ E {{ Φ }}  WP e @ E {{ v, R  Φ v }}.
282
283
Proof. iIntros (?) "[??]". iApply (wp_frame_step_l E E); try iFrame; eauto. Qed.
Lemma wp_frame_step_r' E e Φ R :
284
  to_val e = None  WP e @ E {{ Φ }}   R  WP e @ E {{ v, Φ v  R }}.
285
286
Proof. iIntros (?) "[??]". iApply (wp_frame_step_r E E); try iFrame; eauto. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
287
Lemma wp_wand E e Φ Ψ :
288
  WP e @ E {{ Φ }} - ( v, Φ v - Ψ v) - WP e @ E {{ Ψ }}.
289
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
290
  iIntros "Hwp H". iApply (wp_strong_mono E); auto.
291
292
  iFrame "Hwp". iIntros (?) "?". by iApply "H".
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
293
294
295
Lemma wp_wand_l E e Φ Ψ :
  ( v, Φ v - Ψ v)  WP e @ E {{ Φ }}  WP e @ E {{ Ψ }}.
Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
296
Lemma wp_wand_r E e Φ Ψ :
297
  WP e @ E {{ Φ }}  ( v, Φ v - Ψ v)  WP e @ E {{ Ψ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
298
Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
299
End wp.
300
301
302
303
304
305
306
307
308
309
310

(** Proofmode class instances *)
Section proofmode_classes.
  Context `{irisG Λ Σ}.
  Implicit Types P Q : iProp Σ.
  Implicit Types Φ : val Λ  iProp Σ.

  Global Instance frame_wp E e R Φ Ψ :
    ( v, Frame R (Φ v) (Ψ v))  Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
  Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.

311
312
  Global Instance is_except_0_wp E e Φ : IsExcept0 (WP e @ E {{ Φ }}).
  Proof. by rewrite /IsExcept0 -{2}fupd_wp -except_0_fupd -fupd_intro. Qed.
313

314
315
316
  Global Instance elim_modal_bupd_wp E e P Φ :
    ElimModal (|==> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
  Proof. by rewrite /ElimModal (bupd_fupd E) fupd_frame_r wand_elim_r fupd_wp. Qed.
317

318
319
320
  Global Instance elim_modal_fupd_wp E e P Φ :
    ElimModal (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
  Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
321

322
323
  (* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
  Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
324
    atomic e 
325
    ElimModal (|={E1,E2}=> P) P
326
            (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
327
  Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
328

329
End proofmode_classes.
330

331
Hint Extern 0 (atomic _) => assumption : typeclass_instances.