flat.v 12.4 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
(* Flat Combiner *)
Ralf Jung's avatar
Ralf Jung committed
2
From iris.program_logic Require Export weakestpre.
Zhen Zhang's avatar
Zhen Zhang committed
3
4
5
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
6
From iris.algebra Require Import auth frac agree excl agree gset gmap.
Ralf Jung's avatar
Ralf Jung committed
7
From iris.base_logic Require Import big_op saved_prop.
Zhen Zhang's avatar
Zhen Zhang committed
8
From iris_atomic Require Import misc peritem sync.
Zhen Zhang's avatar
Zhen Zhang committed
9
10
11
12

Definition doOp : val :=
  λ: "p",
     match: !"p" with
Zhen Zhang's avatar
Zhen Zhang committed
13
       InjL "req" => "p" <- InjR ((Fst "req") (Snd "req"))
Zhen Zhang's avatar
Zhen Zhang committed
14
15
16
17
     | InjR "_" => #()
     end.

Definition try_srv : val :=
18
  λ: "lk" "s",
Zhen Zhang's avatar
Zhen Zhang committed
19
20
    if: try_acquire "lk"
      then let: "hd" := !"s" in
21
           iter "hd" doOp;;
Zhen Zhang's avatar
Zhen Zhang committed
22
23
24
25
           release "lk"
      else #().

Definition loop: val :=
26
  rec: "loop" "p" "s" "lk" :=
Zhen Zhang's avatar
Zhen Zhang committed
27
28
    match: !"p" with
    InjL "_" =>
29
30
        try_srv "lk" "s";;
        "loop" "p" "s" "lk"
Zhen Zhang's avatar
Zhen Zhang committed
31
32
33
34
    | InjR "r" => "r"
    end.

Definition install : val :=
35
36
  λ: "f" "x" "s",
     let: "p" := ref (InjL ("f", "x")) in
Zhen Zhang's avatar
Zhen Zhang committed
37
38
39
40
     push "s" "p";;
     "p".

Definition mk_flat : val :=
41
  λ: <>,
Zhen Zhang's avatar
Zhen Zhang committed
42
43
   let: "lk" := newlock #() in
   let: "s" := new_stack #() in
44
45
46
   λ: "f" "x",
      let: "p" := install "f" "x" "s" in
      let: "r" := loop "p" "s" "lk" in
Zhen Zhang's avatar
Zhen Zhang committed
47
      "r".
Zhen Zhang's avatar
Zhen Zhang committed
48

49
Definition reqR := prodR fracR (agreeR valC). (* request x should be kept same *)
Zhen Zhang's avatar
Zhen Zhang committed
50
Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
Zhen Zhang's avatar
Zhen Zhang committed
51
52
Class flatG Σ := FlatG {
  req_G :> inG Σ reqR;
53
  sp_G  :> savedPropG Σ (ofe_funCF val idCF)
Zhen Zhang's avatar
Zhen Zhang committed
54
55
56
57
}.

Definition flatΣ : gFunctors :=
  #[ GFunctor (constRF reqR);
Zhen Zhang's avatar
Zhen Zhang committed
58
     savedPropΣ (ofe_funCF val idCF) ].
Zhen Zhang's avatar
Zhen Zhang committed
59
60

Instance subG_flatΣ {Σ} : subG flatΣ Σ  flatG Σ.
Zhen Zhang's avatar
Zhen Zhang committed
61
Proof. intros [?%subG_inG [? _]%subG_inv]%subG_inv. split; apply _. Qed.
Zhen Zhang's avatar
Zhen Zhang committed
62
63

Section proof.
Zhen Zhang's avatar
Zhen Zhang committed
64
  Context `{!heapG Σ, !lockG Σ, !flatG Σ} (N: namespace).
Zhen Zhang's avatar
Zhen Zhang committed
65
66

  Definition init_s (ts: toks) :=
Zhen Zhang's avatar
Zhen Zhang committed
67
    let '(_, γ1, γ3, _, _) := ts in (own γ1 (Excl ())  own γ3 (Excl ()))%I.
Zhen Zhang's avatar
Zhen Zhang committed
68

69
  Definition installed_s R (ts: toks) (f x: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
70
    let '(γx, γ1, _, γ4, γq) := ts in
71
    ( (P: val  iProp Σ) Q,
72
       own γx ((1/2)%Qp, to_agree x)  P x  ({{ R  P x }} f x {{ v, R  Q x v }}) 
Zhen Zhang's avatar
Zhen Zhang committed
73
       saved_prop_own γq (Q x)  own γ1 (Excl ())  own γ4 (Excl ()))%I.
Zhen Zhang's avatar
Zhen Zhang committed
74
75

  Definition received_s (ts: toks) (x: val) γr :=
Zhen Zhang's avatar
Zhen Zhang committed
76
    let '(γx, _, _, γ4, _) := ts in
77
    (own γx ((1/2/2)%Qp, to_agree x)  own γr (Excl ())  own γ4 (Excl ()))%I.
Zhen Zhang's avatar
Zhen Zhang committed
78

Zhen Zhang's avatar
Zhen Zhang committed
79
  Definition finished_s (ts: toks) (x y: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
80
81
    let '(γx, γ1, _, γ4, γq) := ts in
    ( Q: val  val  iProp Σ,
82
       own γx ((1/2)%Qp, to_agree x)  saved_prop_own γq (Q x) 
Zhen Zhang's avatar
Zhen Zhang committed
83
       Q x y  own γ1 (Excl ())  own γ4 (Excl ()))%I.
Zhen Zhang's avatar
Zhen Zhang committed
84
  
Zhen Zhang's avatar
Zhen Zhang committed
85
86
87
88
89
90
91
92
93
  Definition p_inv R (γm γr: gname) (ts: toks) (p : loc) :=
    ( (* INIT *)
      ( y: val, p  InjRV y  init_s ts) 
      (* INSTALLED *)
      ( f x: val, p  InjLV (f, x)  installed_s R ts f x) 
      (* RECEIVED *)
      ( f x: val, p  InjLV (f, x)  received_s ts x γr) 
      (* FINISHED *)
      ( x y: val, p  InjRV y  finished_s ts x y))%I.
Zhen Zhang's avatar
Zhen Zhang committed
94

Zhen Zhang's avatar
Zhen Zhang committed
95
96
  Definition p_inv' R γm γr : val  iProp Σ :=
    (λ v: val,  ts (p: loc), v = #p  inv N (p_inv R γm γr ts p))%I.
Zhen Zhang's avatar
Zhen Zhang committed
97

Zhen Zhang's avatar
Zhen Zhang committed
98
  Definition srv_bag R γm γr s := ( xs, is_bag_R N (p_inv' R γm γr) xs s)%I.
Zhen Zhang's avatar
Zhen Zhang committed
99

100
  Definition installed_recp (ts: toks) (x: val) (Q: val  iProp Σ) :=
Zhen Zhang's avatar
Zhen Zhang committed
101
    let '(γx, _, γ3, _, γq) := ts in
102
    (own γ3 (Excl ())  own γx ((1/2)%Qp, to_agree x)  saved_prop_own γq Q)%I.
Zhen Zhang's avatar
Zhen Zhang committed
103

Zhen Zhang's avatar
Zhen Zhang committed
104
105
106
107
  Lemma install_spec R P Q (f x: val) (γm γr: gname) (s: loc):
    {{{ inv N (srv_bag R γm γr s)  P  ({{ R  P }} f x {{ v, R  Q v }}) }}}
      install f x #s
    {{{ p ts, RET #p; installed_recp ts x Q  inv N (p_inv R γm γr ts p) }}}.
Zhen Zhang's avatar
Zhen Zhang committed
108
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
109
    iIntros (Φ) "(#? & HP & Hf) HΦ".
110
    wp_seq. wp_let. wp_let. wp_alloc p as "Hl".
Ralf Jung's avatar
Ralf Jung committed
111
112
113
114
    iApply fupd_wp.
    iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
    iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
    iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
115
    iMod (own_alloc (1%Qp, to_agree x)) as (γx) "Hx"; first done.
116
    iMod (saved_prop_alloc (F:=(ofe_funCF val idCF)) Q) as (γq) "#?".
Zhen Zhang's avatar
Zhen Zhang committed
117
118
119
120
121
122
123
124
125
126
127
128
129
130
    iDestruct (own_update with "Hx") as ">[Hx1 Hx2]"; first by apply pair_l_frac_op_1'.
    iModIntro. wp_let. wp_bind (push _ _).
    iMod (inv_alloc N _ (p_inv R γm γr (γx, γ1, γ3, γ4, γq) p)
          with "[-HΦ Hx2 Ho3]") as "#HRx"; first eauto.
    { iNext. iRight. iLeft. iExists f, x. iFrame.
      iExists (λ _, P), (λ _ v, Q v).
      iFrame. iFrame "#". }
    iApply (push_spec N (p_inv' R γm γr) s #p
            with "[-HΦ Hx2 Ho3]")=>//.
    { iFrame "#". iExists (γx, γ1, γ3, γ4, γq), p.
      iSplitR; first done. iFrame "#". }
    iNext. iIntros "?".
    wp_seq. iApply ("HΦ" $! p (γx, γ1, γ3, γ4, γq)).
    iFrame. iFrame "#".
Zhen Zhang's avatar
Zhen Zhang committed
131
132
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
133
  Lemma doOp_f_spec R γm γr (p: loc) ts:
Zhen Zhang's avatar
Zhen Zhang committed
134
    f_spec N (p_inv R γm γr ts p) doOp (own γr (Excl ())  R)%I #p.
Zhen Zhang's avatar
Zhen Zhang committed
135
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
    iIntros (Φ) "(#H1 & Hor & HR) HΦ".
    wp_rec. wp_bind (! _)%E.
    iInv N as "Hp" "Hclose".
    iDestruct "Hp" as "[Hp | [Hp | [Hp | Hp]]]"; subst.
    - iDestruct "Hp" as (y) "[>Hp Hts]".
      wp_load. iMod ("Hclose" with "[-Hor HR HΦ]").
      { iNext. iFrame "#". iLeft. iExists y. iFrame. }
      iModIntro. wp_match. iApply ("HΦ" with "[Hor HR]"). iFrame.
    - destruct ts as [[[[γx γ1] γ3] γ4] γq].
      iDestruct "Hp" as (f x) "(>Hp & Hts)".
      iDestruct "Hts" as (P Q) "(>Hx & Hpx & Hf' & HoQ & >Ho1 & >Ho4)".
      iAssert (|==> own γx (((1/2/2)%Qp, to_agree x) 
                            ((1/2/2)%Qp, to_agree x)))%I with "[Hx]" as ">[Hx1 Hx2]".
      { iDestruct (own_update with "Hx") as "?"; last by iAssumption.
        rewrite -{1}(Qp_div_2 (1/2)%Qp).
        by apply pair_l_frac_op'. }
      wp_load. iMod ("Hclose" with "[-Hf' Ho1 Hx2 HoQ HR HΦ Hpx]").
      { iNext. iFrame. iFrame "#". iRight. iRight. iLeft. iExists f, x. iFrame. }
      iModIntro. wp_match. wp_proj. wp_proj.
      wp_bind (f _). iApply wp_wand_r. iSplitL "Hpx Hf' HR".
      { iApply "Hf'". iFrame. }
157
      iIntros (v) "[HR HQ]".
Zhen Zhang's avatar
Zhen Zhang committed
158
159
160
      iInv N as "Hx" "Hclose".
      iDestruct "Hx" as "[Hp | [Hp | [Hp | Hp]]]"; subst.
      * iDestruct "Hp" as (?) "(_ & >Ho1' & _)".
Zhen Zhang's avatar
Zhen Zhang committed
161
        iApply excl_falso. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
162
163
164
165
166
167
168
      * iDestruct "Hp" as (? ?) "[>? Hs]". iDestruct "Hs" as (? ?) "(_ & _ & _ & _ & >Ho1' & _)".
        iApply excl_falso. iFrame.
      * iDestruct "Hp" as (? x5) ">(Hp & Hx & Hor & Ho4)".
        wp_store. iDestruct (m_frag_agree' with "[Hx Hx2]") as "[Hx %]"; first iFrame.
        subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ]").
        { iNext. iDestruct "Hp" as "[Hp1 Hp2]". iRight. iRight.
          iRight. iExists x5, v. iFrame. iExists Q. iFrame. }
169
        iApply "HΦ". iFrame. done.
Zhen Zhang's avatar
Zhen Zhang committed
170
171
172
173
174
      * iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
        iApply excl_falso. iFrame.
    - destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (? x) "(_ & _ & >Ho2' & _)".
      iApply excl_falso. iFrame.
    - destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (x' y) "[Hp Hs]".
Zhen Zhang's avatar
Zhen Zhang committed
175
        iDestruct "Hs" as (Q) "(>Hx & HoQ & HQxy & >Ho1 & >Ho4)".
Zhen Zhang's avatar
Zhen Zhang committed
176
177
178
        wp_load. iMod ("Hclose" with "[-HΦ HR Hor]").
        { iNext. iRight. iRight. iRight. iExists x', y. iFrame. iExists Q. iFrame. }
        iModIntro. wp_match. iApply "HΦ". iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
179
180
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
181
  Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
Zhen Zhang's avatar
Zhen Zhang committed
182
  Definition finished_recp (ts: toks) (x y: val) :=
Zhen Zhang's avatar
Zhen Zhang committed
183
    let '(γx, _, _, _, γq) := ts in
184
    ( Q, own γx ((1 / 2)%Qp, to_agree x)  saved_prop_own γq (Q x)  Q x y)%I.
Zhen Zhang's avatar
Zhen Zhang committed
185

Zhen Zhang's avatar
Zhen Zhang committed
186
187
188
189
190
191
192
193
  Lemma loop_iter_doOp_spec R (γm γr: gname) xs:
   (hd: loc),
    {{{ is_list_R N (p_inv' R γm γr) hd xs  own γr (Excl ())  R }}}
      iter #hd doOp
    {{{ RET #(); own γr (Excl ())  R }}}.
  Proof.
    induction xs as [|x xs' IHxs].
    - iIntros (hd Φ) "[Hxs ?] HΦ".
194
      simpl. wp_rec. wp_let.
Zhen Zhang's avatar
Zhen Zhang committed
195
196
197
198
      iDestruct "Hxs" as (?) "Hhd".
      wp_load. wp_match. by iApply "HΦ".
    - iIntros (hd Φ) "[Hxs HRf] HΦ". simpl.
      iDestruct "Hxs" as (hd' ?) "(Hhd & #Hinv & Hxs')".
199
      wp_rec. wp_let. wp_bind (! _)%E.
Zhen Zhang's avatar
Zhen Zhang committed
200
201
202
203
204
205
206
207
208
209
      iInv N as "H" "Hclose".
      iDestruct "H" as (ts p) "[>% #?]". subst.
      wp_load. iMod ("Hclose" with "[]").
      { iNext. iExists ts, p. eauto. }
      iModIntro. wp_match. wp_proj. wp_bind (doOp _).
      iDestruct (doOp_f_spec R γm γr p ts) as "Hf".
      iApply ("Hf" with "[HRf]").
      { iFrame. iFrame "#". }
      iNext. iIntros "HRf".
      wp_seq. wp_proj. iApply (IHxs with "[-HΦ]")=>//.
210
      iFrame "#"; first by iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
211
212
213
214
  Qed.

  Lemma try_srv_spec R (s: loc) (lk: val) (γr γm γlk: gname) Φ :
    inv N (srv_bag R γm γr s) 
Zhen Zhang's avatar
Zhen Zhang committed
215
    is_lock N γlk lk (own γr (Excl ())  R)  Φ #()
216
     WP try_srv lk #s {{ Φ }}.
Zhen Zhang's avatar
Zhen Zhang committed
217
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
218
    iIntros "(#? & #? & HΦ)". wp_seq. wp_let.
219
220
    wp_bind (try_acquire _). iApply (try_acquire_spec with "[]"); first done.
    iNext. iIntros ([]); last by (iIntros; wp_if).
221
    iIntros "[Hlocked [Ho2 HR]]".
Zhen Zhang's avatar
Zhen Zhang committed
222
    wp_if. wp_bind (! _)%E.
Zhen Zhang's avatar
Zhen Zhang committed
223
224
225
226
    iInv N as "H" "Hclose".
    iDestruct "H" as (xs' hd') "[>Hs Hxs]".
    wp_load. iDestruct (dup_is_list_R with "[Hxs]") as ">[Hxs1 Hxs2]"; first by iFrame.
    iMod ("Hclose" with "[Hs Hxs1]").
Zhen Zhang's avatar
Zhen Zhang committed
227
    { iNext. iFrame. iExists xs', hd'. by iFrame. }
Zhen Zhang's avatar
Zhen Zhang committed
228
    iModIntro. wp_let. wp_bind (iter _ _).
Zhen Zhang's avatar
Zhen Zhang committed
229
    iApply wp_wand_r. iSplitL "HR Ho2 Hxs2".
Zhen Zhang's avatar
Zhen Zhang committed
230
231
232
233
    { iApply (loop_iter_doOp_spec R _ _ _ _ (λ _, own γr (Excl ())  R)%I with "[-]")=>//.
      iFrame "#". iFrame. eauto. }
    iIntros (f') "[Ho HR]". wp_seq.
    iApply (release_spec with "[Hlocked Ho HR]"); first iFrame "#∗".
234
    iNext. iIntros. done.
Zhen Zhang's avatar
Zhen Zhang committed
235
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
236

237
  Lemma loop_spec R (p s: loc) (lk: val)
Zhen Zhang's avatar
Zhen Zhang committed
238
239
240
241
242
        (γs γr γm γlk: gname) (ts: toks):
    {{{ inv N (srv_bag R γm γr s)  inv N (p_inv R γm γr ts p) 
        is_lock N γlk lk (own γr (Excl ())  R)  own_γ3 ts }}}
      loop #p #s lk
    {{{ x y, RET y; finished_recp ts x y }}}.
Zhen Zhang's avatar
Zhen Zhang committed
243
  Proof.
Zhen Zhang's avatar
Zhen Zhang committed
244
    iIntros (Φ) "(#? & #? & #? & Ho3) HΦ".
Zhen Zhang's avatar
Zhen Zhang committed
245
    iLöb as "IH". wp_rec. repeat wp_let.
Zhen Zhang's avatar
Zhen Zhang committed
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
    wp_bind (! _)%E. iInv N as "Hp" "Hclose".
    destruct ts as [[[[γx γ1] γ3] γ4] γq].
    iDestruct "Hp" as "[Hp | [Hp | [ Hp | Hp]]]".
    + iDestruct "Hp" as (?) "(_ & _ & >Ho3')".
      iApply excl_falso. iFrame.
    + iDestruct "Hp" as (f x) "(>Hp & Hs')".
      wp_load. iMod ("Hclose" with "[Hp Hs']").
      { iNext. iFrame. iRight. iLeft. iExists f, x. iFrame. }
      iModIntro. wp_match. wp_bind (try_srv _ _). iApply try_srv_spec=>//.
      iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
    + iDestruct "Hp" as (f x) "(Hp & Hx & Ho2 & Ho4)".
      wp_load. iMod ("Hclose" with "[-Ho3 HΦ]").
      { iNext. iFrame. iRight. iRight. iLeft. iExists f, x. iFrame. }
      iModIntro. wp_match.
      wp_bind (try_srv _ _). iApply try_srv_spec=>//.
      iFrame "#". wp_seq. iApply ("IH" with "Ho3"); eauto.
    + iDestruct "Hp" as (x y) "[>Hp Hs']".
      iDestruct "Hs'" as (Q) "(>Hx & HoQ & HQ & >Ho1 & >Ho4)".
      wp_load. iMod ("Hclose" with "[-Ho4 HΦ Hx HoQ HQ]").
      { iNext. iFrame. iLeft. iExists y. iFrame. }
      iModIntro. wp_match. iApply ("HΦ" with "[-]"). iFrame.
      iExists Q. iFrame.
Zhen Zhang's avatar
Zhen Zhang committed
268
269
  Qed.

Zhen Zhang's avatar
Zhen Zhang committed
270
  Lemma mk_flat_spec (γm: gname): mk_syncer_spec mk_flat.
Zhen Zhang's avatar
Zhen Zhang committed
271
  Proof.
272
    iIntros (R Φ) "HR HΦ".
Ralf Jung's avatar
Ralf Jung committed
273
    iMod (own_alloc (Excl ())) as (γr) "Ho2"; first done.
Zhen Zhang's avatar
Zhen Zhang committed
274
    wp_seq. wp_bind (newlock _).
275
    iApply (newlock_spec _ (own γr (Excl ())  R)%I with "[$Ho2 $HR]")=>//.
276
    iNext. iIntros (lk γlk) "#Hlk".
Zhen Zhang's avatar
Zhen Zhang committed
277
    wp_let. wp_bind (new_stack _).
Zhen Zhang's avatar
Zhen Zhang committed
278
279
    iApply (new_bag_spec N (p_inv' R γm γr))=>//.
    iNext. iIntros (s) "#Hss".
280
    wp_let. iApply "HΦ". rewrite /synced.
Zhen Zhang's avatar
Zhen Zhang committed
281
    iAlways. iIntros (f). wp_let. iAlways.
282
    iIntros (P Q x) "#Hf".
Zhen Zhang's avatar
Zhen Zhang committed
283
284
    iIntros "!# Hp". wp_let. wp_bind (install _ _ _).
    iApply (install_spec R P Q f x γm γr s with "[-]")=>//.
285
    { iFrame. iFrame "#". }
Zhen Zhang's avatar
Zhen Zhang committed
286
    iNext. iIntros (p [[[[γx γ1] γ3] γ4] γq]) "[(Ho3 & Hx & HoQ) #?]".
287
    wp_let. wp_bind (loop _ _ _).
Zhen Zhang's avatar
Zhen Zhang committed
288
289
290
    iApply (loop_spec with "[-Hx HoQ]")=>//.
    { iFrame "#". iFrame. }
    iNext. iIntros (? ?) "Hs".
Zhen Zhang's avatar
Zhen Zhang committed
291
292
    iDestruct "Hs" as (Q') "(Hx' & HoQ' & HQ')".
    destruct (decide (x = a)) as [->|Hneq].
293
    - iDestruct (saved_prop_agree with "[$HoQ] [HoQ']") as "Heq"; first by iFrame.
294
      wp_let. iDestruct (uPred.ofe_funC_equivI with "Heq") as "Heq".
295
      iSpecialize ("Heq" $! a0). by iRewrite -"Heq" in "HQ'".
Zhen Zhang's avatar
Zhen Zhang committed
296
    - iExFalso. iCombine "Hx" "Hx'" as "Hx".
Zhen Zhang's avatar
Zhen Zhang committed
297
      iDestruct (own_valid with "Hx") as %[_ H1].
298
299
      rewrite //= in H1.
      by apply agree_op_inv' in H1.
Zhen Zhang's avatar
Zhen Zhang committed
300
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
301
302

End proof.