flat.v 12.6 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
(* Flat Combiner *)
2
From iris.program_logic Require Export weakestpre.
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.
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;
Ralf Jung's avatar
Ralf Jung committed
53
  sp_G  :> savedAnythingG Σ ( (ofe_funCF val idCF))
Zhen Zhang's avatar
Zhen Zhang committed
54 55 56 57
}.

Definition flatΣ : gFunctors :=
  #[ GFunctor (constRF reqR);
Ralf Jung's avatar
Ralf Jung committed
58
     savedAnythingΣ ( (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) :=
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 }}) 
Ralf Jung's avatar
Ralf Jung committed
73
       saved_anything_own γq (Next $ 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 Σ,
Ralf Jung's avatar
Ralf Jung committed
82
       own γx ((1/2)%Qp, to_agree x)  saved_anything_own γq (Next $ Q x) 
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
Ralf Jung's avatar
Ralf Jung committed
102
    (own γ3 (Excl ())  own γx ((1/2)%Qp, to_agree x)  saved_anything_own γq (Next 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".
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.
Ralf Jung's avatar
Ralf Jung committed
116
    iMod (saved_anything_alloc (F:=( (ofe_funCF val idCF))) (Next 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
Ralf Jung's avatar
Ralf Jung committed
184
    ( Q, own γx ((1 / 2)%Qp, to_agree x)  saved_anything_own γq (Next $ 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) 
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Φ".
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].
Ralf Jung's avatar
Ralf Jung committed
293 294 295 296 297
    - iDestruct (saved_anything_agree with "[$HoQ] [HoQ']") as "Heq"; first by iFrame.
      (* FIXME: 
      iDestruct (uPred.later_equivI with "Heq") as "Heq".
      does the wrong thing. *)
      rewrite uPred.later_equivI.
298
      wp_let. iDestruct (uPred.ofe_funC_equivI with "Heq") as "Heq".
299
      iSpecialize ("Heq" $! a0). by iRewrite -"Heq" in "HQ'".
Zhen Zhang's avatar
Zhen Zhang committed
300
    - iExFalso. iCombine "Hx" "Hx'" as "Hx".
Zhen Zhang's avatar
Zhen Zhang committed
301
      iDestruct (own_valid with "Hx") as %[_ H1].
302 303
      rewrite //= in H1.
      by apply agree_op_inv' in H1.
Zhen Zhang's avatar
Zhen Zhang committed
304
  Qed.
Zhen Zhang's avatar
Zhen Zhang committed
305 306

End proof.