iris.v 77.3 KB
Newer Older
1
Require Import world_prop core_lang lang masks.
2
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.
3

4
Module Iris (RL : PCM_T) (C : CORE_LANG).
5

6
  Module Import L  := Lang C.
7
  Module Import R <: PCM_T.
8
    Definition res := (pcm_res_ex state * RL.res)%type.
9 10 11 12 13 14
    Instance res_op   : PCM_op res := _.
    Instance res_unit : PCM_unit res := _.
    Instance res_pcm  : PCM res := _.
  End R.
  Module Import WP := WorldProp R.

15 16 17
  Delimit Scope iris_scope with iris.
  Local Open Scope iris_scope.

18 19 20 21 22 23 24 25 26 27
  (** The final thing we'd like to check is that the space of
      propositions does indeed form a complete BI algebra.

      The following instance declaration checks that an instance of
      the complete BI class can be found for Props (and binds it with
      a low priority to potentially speed up the proof search).
   *)

  Instance Props_BI : ComplBI Props | 0 := _.
  Instance Props_Later : Later Props | 0 := _.
28
  Set Printing All.
29
  
30 31
  (** And now we're ready to build the IRIS-specific connectives! *)

32 33 34 35 36 37
  Section Necessitation.
    (** Note: this could be moved to BI, since it's possible to define
        for any UPred over a monoid. **)

    Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.

38
    Program Definition box : Props -n> Props :=
39
      n[(fun p => m[(fun w => mkUPred (fun n r => p w n (pcm_unit _)) _)])].
40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
    Next Obligation.
      intros n m r s HLe _ Hp; rewrite HLe; assumption.
    Qed.
    Next Obligation.
      intros w1 w2 EQw m r HLt; simpl.
      eapply (met_morph_nonexp _ _ p); eassumption.
    Qed.
    Next Obligation.
      intros w1 w2 Subw n r; simpl.
      apply p; assumption.
    Qed.
    Next Obligation.
      intros p1 p2 EQp w m r HLt; simpl.
      apply EQp; assumption.
    Qed.

  End Necessitation.

  (** "Internal" equality **)
  Section IntEq.
    Context {T} `{mT : metric T}.

62
    Program Definition intEqP (t1 t2 : T) : UPred res :=
63 64 65 66 67
      mkUPred (fun n r => t1 = S n = t2) _.
    Next Obligation.
      intros n1 n2 _ _ HLe _; apply mono_dist; now auto with arith.
    Qed.

68
    Definition intEq (t1 t2 : T) : Props := pcmconst (intEqP t1 t2).
69 70 71 72 73 74 75 76

    Instance intEq_equiv : Proper (equiv ==> equiv ==> equiv) intEqP.
    Proof.
      intros l1 l2 EQl r1 r2 EQr n r.
      split; intros HEq; do 2 red.
      - rewrite <- EQl, <- EQr; assumption.
      - rewrite EQl, EQr; assumption.
    Qed.
77

78 79 80 81 82 83 84 85 86 87 88 89 90 91
    Instance intEq_dist n : Proper (dist n ==> dist n ==> dist n) intEqP.
    Proof.
      intros l1 l2 EQl r1 r2 EQr m r HLt.
      split; intros HEq; do 2 red.
      - etransitivity; [| etransitivity; [apply HEq |] ];
        apply mono_dist with n; eassumption || now auto with arith.
      - etransitivity; [| etransitivity; [apply HEq |] ];
        apply mono_dist with n; eassumption || now auto with arith.
    Qed.

  End IntEq.

  Notation "t1 '===' t2" := (intEq t1 t2) (at level 70) : iris_scope.

92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
  Section Invariants.

    (** Invariants **)
    Definition invP (i : nat) (p : Props) (w : Wld) : UPred res :=
      intEqP (w i) (Some (ı' p)).
    Program Definition inv i : Props -n> Props :=
      n[(fun p => m[(invP i p)])].
    Next Obligation.
      intros w1 w2 EQw; unfold equiv, invP in *.
      apply intEq_equiv; [apply EQw | reflexivity].
    Qed.
    Next Obligation.
      intros w1 w2 EQw; unfold invP; simpl morph.
      destruct n; [apply dist_bound |].
      apply intEq_dist; [apply EQw | reflexivity].
    Qed.
    Next Obligation.
      intros w1 w2 Sw; unfold invP; simpl morph.
      intros n r HP; do 2 red; specialize (Sw i); do 2 red in HP.
      destruct (w1 i) as [μ1 |]; [| contradiction].
      destruct (w2 i) as [μ2 |]; [| contradiction]; simpl in Sw.
      rewrite <- Sw; assumption.
    Qed.
    Next Obligation.
      intros p1 p2 EQp w; unfold equiv, invP in *; simpl morph.
      apply intEq_equiv; [reflexivity |].
      rewrite EQp; reflexivity.
    Qed.
    Next Obligation.
      intros p1 p2 EQp w; unfold invP; simpl morph.
      apply intEq_dist; [reflexivity |].
      apply dist_mono, (met_morph_nonexp _ _ ı'), EQp.
    Qed.

  End Invariants.
127

128 129 130 131 132 133 134 135 136 137 138 139 140
  Notation "□ p" := (box p) (at level 30, right associativity) : iris_scope.
  Notation "⊤" := (top : Props) : iris_scope.
  Notation "⊥" := (bot : Props) : iris_scope.
  Notation "p ∧ q" := (and p q : Props) (at level 40, left associativity) : iris_scope.
  Notation "p ∨ q" := (or p q : Props) (at level 50, left associativity) : iris_scope.
  Notation "p * q" := (sc p q : Props) (at level 40, left associativity) : iris_scope.
  Notation "p → q" := (BI.impl p q : Props) (at level 55, right associativity) : iris_scope.
  Notation "p '-*' q" := (si p q : Props) (at level 55, right associativity) : iris_scope.
  Notation "∀ x , p" := (all n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
  Notation "∃ x , p" := (all n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
  Notation "∀ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
  Notation "∃ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.

141 142 143 144 145 146 147 148
  Lemma valid_iff p :
    valid p <-> (  p).
  Proof.
    split; intros Hp.
    - intros w n r _; apply Hp.
    - intros w n r; apply Hp; exact I.
  Qed.

149 150 151 152 153
  (** Ownership **)
  Definition ownR (r : res) : Props :=
    pcmconst (up_cr (pord r)).

  (** Physical part **)
154
  Definition ownRP (r : pcm_res_ex state) : Props :=
155 156 157 158 159 160
    ownR (r, pcm_unit _).

  (** Logical part **)
  Definition ownRL (r : RL.res) : Props :=
    ownR (pcm_unit _, r).

161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176
  (** Proper physical state: ownership of the machine state **)
  Instance state_type : Setoid state := discreteType.
  Instance state_metr : metric state := discreteMetric.
  Instance state_cmetr : cmetric state := discreteCMetric.

  Program Definition ownS : state -n> Props :=
    n[(fun s => ownRP (ex_own _ s))].
  Next Obligation.
    intros r1 r2 EQr. hnf in EQr. now rewrite EQr.
  Qed.
  Next Obligation.
    intros r1 r2 EQr; destruct n as [| n]; [apply dist_bound |].
    simpl in EQr. subst; reflexivity.
  Qed.

  (** Proper ghost state: ownership of logical w/ possibility of undefined **)
177
  Lemma ores_equiv_eq T `{pcmT : PCM T} (r1 r2 : option T) (HEq : r1 == r2) : r1 = r2.
178 179 180 181 182
  Proof.
    destruct r1 as [r1 |]; destruct r2 as [r2 |]; try contradiction;
    simpl in HEq; subst; reflexivity.
  Qed.

183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198
  Instance logR_metr : metric RL.res := discreteMetric.
  Instance logR_cmetr : cmetric RL.res := discreteCMetric.

  Program Definition ownL : (option RL.res) -n> Props :=
    n[(fun r => match r with
                  | Some r => ownRL r
                  | None => 
                end)].
  Next Obligation.
    intros r1 r2 EQr; apply ores_equiv_eq in EQr; now rewrite EQr.
  Qed.
  Next Obligation.
    intros r1 r2 EQr; destruct n as [| n]; [apply dist_bound |].
    destruct r1 as [r1 |]; destruct r2 as [r2 |]; try contradiction; simpl in EQr; subst; reflexivity.
  Qed.

199 200 201 202 203 204 205 206 207 208 209 210 211 212 213
  (** Lemmas about box **)
  Lemma box_intro p q (Hpq :  p  q) :
     p   q.
  Proof.
    intros w n r Hp; simpl; apply Hpq, Hp.
  Qed.

  Lemma box_elim p :
     p  p.
  Proof.
    intros w n r Hp; simpl in Hp.
    eapply uni_pred, Hp; [reflexivity |].
    exists r; now erewrite comm, pcm_op_unit by apply _.
  Qed.

214 215 216 217 218
  Lemma box_top :  ==  .
  Proof.
    intros w n r; simpl; unfold const; reflexivity.
  Qed.

219 220 221 222 223 224
  Lemma box_disj p q :
     (p  q) ==  p   q.
  Proof.
    intros w n r; reflexivity.
  Qed.

225 226 227 228 229 230
  (** Ghost state ownership **)
  Lemma ownL_sc (u t : option RL.res) :
    ownL (u · t)%pcm == ownL u * ownL t.
  Proof.
    intros w n r; split; [intros Hut | intros [r1 [r2 [EQr [Hu Ht] ] ] ] ].
    - destruct (u · t)%pcm as [ut |] eqn: EQut; [| contradiction].
231
      do 15 red in Hut; rewrite <- Hut.
232 233 234
      destruct u as [u |]; [| now erewrite pcm_op_zero in EQut by apply _].
      assert (HT := comm (Some u) t); rewrite EQut in HT.
      destruct t as [t |]; [| now erewrite pcm_op_zero in HT by apply _]; clear HT.
235
      exists (pcm_unit (pcm_res_ex state), u) (pcm_unit (pcm_res_ex state), t).
236
      split; [unfold pcm_op, res_op, pcm_op_prod | split; do 15 red; reflexivity].
237 238 239 240 241 242 243 244 245 246 247 248 249 250
      now erewrite pcm_op_unit, EQut by apply _.
    - destruct u as [u |]; [| contradiction]; destruct t as [t |]; [| contradiction].
      destruct Hu as [ru EQu]; destruct Ht as [rt EQt].
      rewrite <- EQt, assoc, (comm (Some r1)) in EQr.
      rewrite <- EQu, assoc, <- (assoc (Some rt · Some ru)%pcm) in EQr.
      unfold pcm_op at 3, res_op at 4, pcm_op_prod at 1 in EQr.
      erewrite pcm_op_unit in EQr by apply _; clear EQu EQt.
      destruct (Some u · Some t)%pcm as [ut |];
        [| now erewrite comm, pcm_op_zero in EQr by apply _].
      destruct (Some rt · Some ru)%pcm as [rut |];
        [| now erewrite pcm_op_zero in EQr by apply _].
      exists rut; assumption.
  Qed.

251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278
  (** Timeless *)

  Definition timelessP (p : Props) w n :=
    forall w' k r (HSw : w  w') (HLt : k < n) (Hp : p w' k r), p w' (S k) r.

  Program Definition timeless (p : Props) : Props :=
    m[(fun w => mkUPred (fun n r => timelessP p w n) _)].
  Next Obligation.
    intros n1 n2 _ _ HLe _ HT w' k r HSw HLt Hp; eapply HT, Hp; [eassumption |].
    now eauto with arith.
  Qed.
  Next Obligation.
    intros w1 w2 EQw n rr; simpl; split; intros HT k r HLt;
    [rewrite <- EQw | rewrite EQw]; apply HT; assumption.
  Qed.
  Next Obligation.
    intros w1 w2 EQw k; simpl; intros _ HLt; destruct n as [| n]; [now inversion HLt |].
    split; intros HT w' m r HSw HLt' Hp.
    - symmetry in EQw; assert (HD := extend_dist _ _ _ _ EQw HSw); assert (HS := extend_sub _ _ _ _ EQw HSw).
      apply (met_morph_nonexp _ _ p) in HD; apply HD, HT, HD, Hp; now (assumption || eauto with arith).
    - assert (HD := extend_dist _ _ _ _ EQw HSw); assert (HS := extend_sub _ _ _ _ EQw HSw).
      apply (met_morph_nonexp _ _ p) in HD; apply HD, HT, HD, Hp; now (assumption || eauto with arith).
  Qed.
  Next Obligation.
    intros w1 w2 HSw n; simpl; intros _ HT w' m r HSw' HLt Hp.
    eapply HT, Hp; [etransitivity |]; eassumption.
  Qed.

279 280
  Section Erasure.
    Local Open Scope pcm_scope.
281 282 283 284 285 286 287
    Local Open Scope bi_scope.

    (* First, we need to erase a finite map. This won't be pretty, for
       now, since the library does not provide enough
       constructs. Hopefully we can provide a fold that'd work for
       that at some point
     *)
288
    Fixpoint comp_list (xs : list res) : option res :=
289 290
      match xs with
        | nil => 1
291
        | (x :: xs)%list => Some x · comp_list xs
292 293 294
      end.

    Definition cod (m : nat -f> res) : list res := List.map snd (findom_t m).
295
    Definition erase (m : nat -f> res) : option res := comp_list (cod m).
296 297

    Lemma erase_remove (rs : nat -f> res) i r (HLu : rs i = Some r) :
298
      erase rs == Some r · erase (fdRemove i rs).
299
    Proof.
300 301
      destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
      induction rs as [| [j s] ]; [discriminate |]; simpl comp_list; simpl in HLu.
302
      destruct (comp i j); [inversion HLu; reflexivity | discriminate |].
303 304
      simpl comp_list; rewrite IHrs by eauto using SS_tail.
      rewrite !assoc, (comm (Some s)); reflexivity.
305 306 307
    Qed.

    Lemma erase_insert_new (rs : nat -f> res) i r (HNLu : rs i = None) :
308
      Some r · erase rs == erase (fdUpdate i r rs).
309
    Proof.
310 311
      destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
      induction rs as [| [j s] ]; [reflexivity | simpl comp_list; simpl in HNLu].
312
      destruct (comp i j); [discriminate | reflexivity |].
313 314
      simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
      rewrite !assoc, (comm (Some r)); reflexivity.
315 316
    Qed.

317 318 319
    Lemma erase_insert_old (rs : nat -f> res) i r1 r2 r
          (HLu : rs i = Some r1) (HEq : Some r1 · Some r2 == Some r) :
      Some r2 · erase rs == erase (fdUpdate i r rs).
320
    Proof.
321 322
      destruct rs as [rs rsP]; unfold erase, cod, findom_f in *; simpl findom_t in *.
      induction rs as [| [j s] ]; [discriminate |]; simpl comp_list; simpl in HLu.
323
      destruct (comp i j); [inversion HLu; subst; clear HLu | discriminate |].
324 325 326
      - simpl comp_list; rewrite assoc, (comm (Some r2)), <- HEq; reflexivity.
      - simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
        rewrite !assoc, (comm (Some r2)); reflexivity.
327 328
    Qed.

329 330 331 332 333
    Definition erase_state (r: option res) σ: Prop := match r with
    | Some (ex_own s, _) => s = σ
    | _ => False
    end.

334
    Global Instance preo_unit : preoType () := disc_preo ().
335

336
    Program Definition erasure (σ : state) (m : mask) (r s : option res) (w : Wld) : UPred () :=
337
       (mkUPred (fun n _ =>
338
                    erase_state (r · s) σ
339
                    /\ exists rs : nat -f> res,
340
                         erase rs == s /\
341 342 343 344
                         forall i (Hm : m i),
                           (i  dom rs <-> i  dom w) /\
                           forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
                             ı π w n ri) _).
345
    Next Obligation.
346 347
      intros n1 n2 _ _ HLe _ [HES HRS]; split; [assumption |].
      setoid_rewrite HLe; eassumption.
348 349
    Qed.

350
    Global Instance erasure_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv ==> equiv) (erasure σ).
351
    Proof.
352 353
      intros m1 m2 EQm r r' EQr s s' EQs w1 w2 EQw [| n] []; [reflexivity |];
      apply ores_equiv_eq in EQr; apply ores_equiv_eq in EQs; subst r' s'.
354
      split; intros [HES [rs [HE HM] ] ]; (split; [tauto | clear HES; exists rs]).
Filip Sieczkowski's avatar
Filip Sieczkowski committed
355
      - split; [assumption | intros; apply EQm in Hm; split; [| setoid_rewrite <- EQw; apply HM, Hm] ].
356 357
        destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
        rewrite fdLookup_in; setoid_rewrite EQw; rewrite <- fdLookup_in; reflexivity.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
358
      - split; [assumption | intros; apply EQm in Hm; split; [| setoid_rewrite EQw; apply HM, Hm] ].
359 360
        destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
        rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity.
361 362 363 364 365
    Qed.

    Global Instance erasure_dist n σ m r s : Proper (dist n ==> dist n) (erasure σ m r s).
    Proof.
      intros w1 w2 EQw [| n'] [] HLt; [reflexivity |]; destruct n as [| n]; [now inversion HLt |].
366 367 368 369
      split; intros [HES [rs [HE HM] ] ]; (split; [tauto | clear HES; exists rs]).
      - split; [assumption | split; [rewrite <- (domeq _ _ _ EQw); apply HM, Hm |] ].
        intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
        assert (EQπ := EQw i); rewrite HLw in EQπ; clear HLw.
370 371 372
        destruct (w1 i) as [π' |]; [| contradiction]; do 3 red in EQπ.
        apply ı in EQπ; apply EQπ; [now auto with arith |].
        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [now auto with arith |].
373 374 375 376
        apply HR; [reflexivity | assumption].
      - split; [assumption | split; [rewrite (domeq _ _ _ EQw); apply HM, Hm |] ].
        intros; destruct (HM _ Hm) as [_ HR]; clear HE HM Hm.
        assert (EQπ := EQw i); rewrite HLw in EQπ; clear HLw.
377 378 379
        destruct (w2 i) as [π' |]; [| contradiction]; do 3 red in EQπ.
        apply ı in EQπ; apply EQπ; [now auto with arith |].
        apply (met_morph_nonexp _ _ (ı π')) in EQw; apply EQw; [now auto with arith |].
380
        apply HR; [reflexivity | assumption].
381 382
    Qed.

383 384 385 386
    Lemma erasure_not_empty σ m r s w k (HN : r · s == 0) :
      ~ erasure σ m r s w (S k) tt.
    Proof.
      intros [HD _]; apply ores_equiv_eq in HN; setoid_rewrite HN in HD.
387
      exact HD.
388 389
    Qed.

390 391
  End Erasure.

392
  Check erasure.
393

394 395 396 397 398 399
  Notation " p @ k " := ((p : UPred ()) k tt) (at level 60, no associativity).

  Section ViewShifts.
    Local Open Scope mask_scope.
    Local Open Scope pcm_scope.
    Local Obligation Tactic := intros.
400 401

    Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred res :=
402 403 404 405 406 407
      mkUPred (fun n r => forall w1 rf s mf σ k (HSub : w  w1) (HLe : k < n)
                                 (HD : mf # m1  m2)
                                 (HE : erasure σ (m1  mf) (Some r · rf) s w1 @ S k),
                          exists w2 r' s',
                            w1  w2 /\ p w2 (S k) r'
                            /\ erasure σ (m2  mf) (Some r' · rf) s' w2 @ S k) _.
408
    Next Obligation.
409
      intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
410 411 412 413 414 415 416 417 418
      destruct (HP w1 (Some rd · rf) s mf σ k) as [w2 [r1' [s' [HW [HP' HE'] ] ] ] ];
        try assumption; [now eauto with arith | |].
      - eapply erasure_equiv, HE; try reflexivity.
        rewrite assoc, (comm (Some r1)), HR; reflexivity.
      - rewrite assoc, (comm (Some r1')) in HE'.
        destruct (Some rd · Some r1') as [r2' |] eqn: HR';
          [| apply erasure_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
        exists w2 r2' s'; split; [assumption | split; [| assumption] ].
        eapply uni_pred, HP'; [| exists rd; rewrite HR']; reflexivity.
419 420 421 422 423 424 425 426 427 428 429 430 431 432 433
    Qed.

    Program Definition pvs (m1 m2 : mask) : Props -n> Props :=
      n[(fun p => m[(preVS m1 m2 p)])].
    Next Obligation.
      intros w1 w2 EQw n r; split; intros HP w2'; intros.
      - eapply HP; try eassumption; [].
        rewrite EQw; assumption.
      - eapply HP; try eassumption; [].
        rewrite <- EQw; assumption.
    Qed.
    Next Obligation.
      intros w1 w2 EQw n' r HLt; destruct n as [| n]; [now inversion HLt |]; split; intros HP w2'; intros.
      - symmetry in EQw; assert (HDE := extend_dist _ _ _ _ EQw HSub).
        assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w1)).
434
        edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
435 436
        + eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
        + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
437 438
          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
          exists (extend w1'' w2') r' s'; split; [assumption | split].
439 440 441
          * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
          * eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith].
      - assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)).
442
        edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
443 444
        + eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
        + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
445 446
          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
          exists (extend w1'' w2') r' s'; split; [assumption | split].
447 448 449 450 451 452 453 454 455 456 457 458 459 460
          * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
          * eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith].
    Qed.
    Next Obligation.
      intros w1 w2 EQw n r HP w2'; intros; eapply HP; try eassumption; [].
      etransitivity; eassumption.
    Qed.
    Next Obligation.
      intros p1 p2 EQp w n r; split; intros HP w1; intros.
      - setoid_rewrite <- EQp; eapply HP; eassumption.
      - setoid_rewrite EQp; eapply HP; eassumption.
    Qed.
    Next Obligation.
      intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros.
461
      - edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
462
        clear HP; repeat (eexists; try eassumption); [].
463
        apply EQp; [now eauto with arith | assumption].
464
      - edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
465
        clear HP; repeat (eexists; try eassumption); [].
466 467 468 469 470 471 472 473
        apply EQp; [now eauto with arith | assumption].
    Qed.

    Definition vs (m1 m2 : mask) (p q : Props) : Props :=
       (p  pvs m1 m2 q).

  End ViewShifts.

474 475
  Check vs.

476 477 478 479
  Section ViewShiftProps.
    Local Open Scope mask_scope.
    Local Open Scope pcm_scope.
    Local Open Scope bi_scope.
480 481

    Implicit Types (p q r : Props) (i : nat) (m : mask).
482 483 484

    Definition mask_sing i := mask_set mask_emp i True.

485 486 487 488 489 490 491 492 493 494 495
    Lemma vsTimeless m p :
      timeless p  vs m m ( p) p.
    Proof.
      intros w' n r1 HTL w HSub; rewrite HSub in HTL; clear w' HSub.
      intros np rp HLe HS Hp w1; intros.
      exists w1 rp s; split; [reflexivity | split; [| assumption] ]; clear HE HD.
      destruct np as [| np]; [now inversion HLe0 |]; simpl in Hp.
      unfold lt in HLe0; rewrite HLe0.
      rewrite <- HSub; apply HTL, Hp; [reflexivity | assumption].
    Qed.

496 497 498 499 500 501 502 503 504 505 506
    Lemma vsOpen i p :
      valid (vs (mask_sing i) mask_emp (inv i p) ( p)).
    Proof.
      intros pw nn r w _; clear r pw.
      intros n r _ _ HInv w'; clear nn; intros.
      do 12 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
      apply ı in HInv; rewrite (isoR p) in HInv.
      (* get rid of the invisible 1/2 *)
      do 8 red in HInv.
      destruct HE as [HES [rs [HE HM] ] ].
      destruct (rs i) as [ri |] eqn: HLr.
507
      - rewrite erase_remove with (i := i) (r := ri) in HE by assumption.
508 509 510 511
        assert (HR : Some r · rf · s == Some r · Some ri · rf · erase (fdRemove i rs))
          by (rewrite <- HE, assoc, <- (assoc (Some r)), (comm rf), assoc; reflexivity).
        apply ores_equiv_eq in HR; setoid_rewrite HR in HES; clear HR.
        destruct (Some r · Some ri) as [rri |] eqn: HR;
Ralf Jung's avatar
Ralf Jung committed
512
          [| erewrite !pcm_op_zero in HES by apply _; now contradiction].
513 514
        exists w' rri (erase (fdRemove i rs)); split; [reflexivity |].
        split; [| split; [assumption |] ].
515
        + simpl; eapply HInv; [now auto with arith |].
516 517
          eapply uni_pred, HM with i;
            [| exists r; rewrite <- HR | | | rewrite HLr]; try reflexivity; [|].
518 519
          * left; unfold mask_sing, mask_set.
            destruct (Peano_dec.eq_nat_dec i i); tauto.
520 521 522
          * specialize (HSub i); rewrite HLu in HSub.
            symmetry; destruct (w' i); [assumption | contradiction].
        + exists (fdRemove i rs); split; [reflexivity | intros j Hm].
523 524 525 526 527 528 529 530 531 532 533
          destruct Hm as [| Hm]; [contradiction |]; specialize (HD j); simpl in HD.
          unfold mask_sing, mask_set in HD; destruct (Peano_dec.eq_nat_dec i j);
          [subst j; contradiction HD; tauto | clear HD].
          rewrite fdLookup_in; setoid_rewrite (fdRemove_neq _ _ _ n0); rewrite <- fdLookup_in; now auto.
      - rewrite <- fdLookup_notin_strong in HLr; contradiction HLr; clear HLr.
        specialize (HSub i); rewrite HLu in HSub; clear - HM HSub.
        destruct (HM i) as [HD _]; [left | rewrite HD, fdLookup_in_strong; destruct (w' i); [eexists; reflexivity | contradiction] ].
        clear; unfold mask_sing, mask_set.
        destruct (Peano_dec.eq_nat_dec i i); tauto.
    Qed.

534
    Lemma vsClose i p :
535 536 537 538 539 540 541 542 543
      valid (vs mask_emp (mask_sing i) (inv i p *  p) ).
    Proof.
      intros pw nn r w _; clear r pw.
      intros n r _ _ [r1 [r2 [HR [HInv HP] ] ] ] w'; clear nn; intros.
      do 12 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
      apply ı in HInv; rewrite (isoR p) in HInv.
      (* get rid of the invisible 1/2 *)
      do 8 red in HInv.
      destruct HE as [HES [rs [HE HM] ] ].
544 545
      exists w' (pcm_unit _) (Some r · s); split; [reflexivity | split; [exact I |] ].
      assert (HR' : Some r · rf · s = rf · (Some r · s))
546
        by (eapply ores_equiv_eq; rewrite assoc, (comm rf); reflexivity).
547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574
      setoid_rewrite HR' in HES; erewrite pcm_op_unit by apply _.
      split; [assumption |].
      remember (match rs i with Some ri => ri | None => pcm_unit _ end) as ri eqn: EQri.
      destruct (Some ri · Some r) as [rri |] eqn: EQR.
      - exists (fdUpdate i rri rs); split; [| intros j Hm].
        + symmetry; rewrite <- HE; clear - EQR EQri; destruct (rs i) as [rsi |] eqn: EQrsi; subst;
          [eapply erase_insert_old; [eassumption | rewrite <- EQR; reflexivity] |].
          erewrite pcm_op_unit in EQR by apply _; rewrite EQR.
          now apply erase_insert_new.
        + specialize (HD j); unfold mask_sing, mask_set in *; simpl in Hm, HD.
          destruct (Peano_dec.eq_nat_dec i j);
            [subst j; clear Hm |
             destruct Hm as [Hm | Hm]; [contradiction | rewrite fdLookup_in_strong, fdUpdate_neq, <- fdLookup_in_strong by assumption; now auto] ].
          rewrite !fdLookup_in_strong, fdUpdate_eq.
          destruct n as [| n]; [now inversion HLe | simpl in HP].
          rewrite HSub in HP; specialize (HSub i); rewrite HLu in HSub.
          destruct (w' i) as [π' |]; [| contradiction].
          split; [intuition now eauto | intros].
          simpl in HLw, HLrs, HSub; subst ri0; rewrite <- HLw, <- HSub.
          apply HInv; [now auto with arith |].
          eapply uni_pred, HP; [now auto with arith |].
          assert (HT : Some ri · Some r1 · Some r2 == Some rri)
            by (rewrite <- EQR, <- HR, assoc; reflexivity); clear - HT.
          destruct (Some ri · Some r1) as [rd |];
            [| now erewrite pcm_op_zero in HT by apply _].
          exists rd; assumption.
      - destruct (rs i) as [rsi |] eqn: EQrsi; subst;
        [| erewrite pcm_op_unit in EQR by apply _; discriminate].
Ralf Jung's avatar
Ralf Jung committed
575 576
        clear - HE HES EQrsi EQR.
        assert (HH : rf · (Some r · s) = 0); [clear HES | rewrite HH in HES; contradiction].
577
        eapply ores_equiv_eq; rewrite <- HE, erase_remove by eassumption.
578 579 580
        rewrite (assoc (Some r)), (comm (Some r)), EQR, comm.
        erewrite !pcm_op_zero by apply _; reflexivity.
    Qed.
581 582 583 584 585 586

    Lemma vsTrans p q r m1 m2 m3 (HMS : m2  m1  m3) :
      vs m1 m2 p q  vs m2 m3 q r  vs m1 m3 p r.
    Proof.
      intros w' n r1 [Hpq Hqr] w HSub; specialize (Hpq _ HSub); rewrite HSub in Hqr; clear w' HSub.
      intros np rp HLe HS Hp w1; intros; specialize (Hpq _ _ HLe HS Hp).
587
      edestruct Hpq as [w2 [rq [sq [HSw12 [Hq HEq] ] ] ] ]; try eassumption; [|].
588
      { clear - HD HMS; intros j [Hmf Hm12]; apply (HD j); split; [assumption |].
589 590
        destruct Hm12 as [Hm1 | Hm2]; [left; assumption | apply HMS, Hm2].
      }
591
      clear HS; assert (HS : pcm_unit _  rq) by (exists rq; now erewrite comm, pcm_op_unit by apply _).
592
      rewrite <- HLe, HSub in Hqr; specialize (Hqr _ HSw12); clear Hpq HE w HSub Hp.
593
      edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [sR [HSw23 [Hr HEr] ] ] ] ];
594
        try (reflexivity || eassumption); [now auto with arith | |].
595
      { clear - HD HMS; intros j [Hmf Hm23]; apply (HD j); split; [assumption |].
596 597 598
        destruct Hm23 as [Hm2 | Hm3]; [apply HMS, Hm2 | right; assumption].
      }
      clear HEq Hq HS.
599
      setoid_rewrite HSw12; eauto 8.
600 601
    Qed.

602 603
    Lemma vsEnt p q m :
       (p  q)  vs m m p q.
604
    Proof.
605 606
      intros w' n r1 Himp w HSub; rewrite HSub in Himp; clear w' HSub.
      intros np rp HLe HS Hp w1; intros.
607
      exists w1 rp s; split; [reflexivity | split; [| assumption ] ].
608 609 610
      eapply Himp; [assumption | now eauto with arith | exists rp; now erewrite comm, pcm_op_unit by apply _ |].
      unfold lt in HLe0; rewrite HLe0, <- HSub; assumption.
    Qed.
611

612
    Lemma vsFrame p q r m1 m2 mf (HDisj : mf # m1  m2) :
613 614
      vs m1 m2 p q  vs (m1  mf) (m2  mf) (p * r) (q * r).
    Proof.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
615 616
      intros w' n r1 HVS w HSub; specialize (HVS _ HSub); clear w' r1 HSub.
      intros np rpr HLe _ [rp [rr [HR [Hp Hr] ] ] ] w'; intros.
617 618
      assert (HS : pcm_unit _  rp) by (exists rp; now erewrite comm, pcm_op_unit by apply _).
      specialize (HVS _ _ HLe HS Hp w' (Some rr · rf) s (mf  mf0) σ k); clear HS.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
619
      destruct HVS as [w'' [rq [s' [HSub' [Hq HEq] ] ] ] ]; try assumption; [| |].
620
      - (* disjointness of masks: possible lemma *)
Filip Sieczkowski's avatar
Filip Sieczkowski committed
621 622 623 624
        clear - HD HDisj; intros i [ [Hmf | Hmf] Hm12]; [eapply HDisj; now eauto |].
        eapply HD; split; [eassumption | tauto].
      - rewrite assoc, HR; eapply erasure_equiv, HE; try reflexivity; [].
        clear; intros i; tauto.
625 626 627 628 629 630
      - rewrite assoc in HEq; destruct (Some rq · Some rr) as [rqr |] eqn: HR';
        [| apply erasure_not_empty in HEq; [contradiction | now erewrite !pcm_op_zero by apply _] ].
        exists w'' rqr s'; split; [assumption | split].
        + unfold lt in HLe0; rewrite HSub, HSub', <- HLe0 in Hr; exists rq rr.
          rewrite HR'; split; now auto.
        + eapply erasure_equiv, HEq; try reflexivity; [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
631
          clear; intros i; tauto.
632
    Qed.
633

634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668
    Instance LP_optres (P : option RL.res -> Prop) : LimitPreserving P.
    Proof.
      intros σ σc HPc; simpl; unfold option_compl.
      generalize (@eq_refl _ (σ 1%nat)).
      pattern (σ 1%nat) at 1 3; destruct (σ 1%nat); [| intros HE; rewrite HE; apply HPc].
      intros HE; simpl; unfold discreteCompl, unSome.
      generalize (@eq_refl _ (σ 2)); pattern (σ 2) at 1 3; destruct (σ 2).
      + intros HE'; rewrite HE'; apply HPc.
      + intros HE'; exfalso; specialize (σc 1 1 2)%nat.
        rewrite <- HE, <- HE' in σc; contradiction σc; auto with arith.
    Qed.

    Definition ownLP (P : option RL.res -> Prop) : {s : option RL.res | P s} -n> Props :=
      ownL <M< inclM.

Lemma pcm_op_split rp1 rp2 rp sp1 sp2 sp :
  Some (rp1, sp1) · Some (rp2, sp2) == Some (rp, sp) <->
  Some rp1 · Some rp2 == Some rp /\ Some sp1 · Some sp2 == Some sp.
Proof.
  unfold pcm_op at 1, res_op at 2, pcm_op_prod at 1.
  destruct (Some rp1 · Some rp2) as [rp' |]; [| simpl; tauto].
  destruct (Some sp1 · Some sp2) as [sp' |]; [| simpl; tauto].
  simpl; split; [| intros [EQ1 EQ2]; subst; reflexivity].
  intros EQ; inversion EQ; tauto.
Qed.

    Lemma vsGhostUpd m rl (P : option RL.res -> Prop)
          (HU : forall rf (HD : rl · rf <> None), exists sl, P sl /\ sl · rf <> None) :
      valid (vs m m (ownL rl) (xist (ownLP P))).
    Proof.
      unfold ownLP; intros _ _ _ w _ n [rp' rl'] _ _ HG w'; intros.
      destruct rl as [rl |]; simpl in HG; [| contradiction].
      destruct HG as [ [rdp rdl] EQr]; rewrite pcm_op_split in EQr; destruct EQr as [EQrp EQrl].
      erewrite comm, pcm_op_unit in EQrp by apply _; simpl in EQrp; subst rp'.
      destruct (Some (rdp, rl') · rf · s) as [t |] eqn: EQt;
Ralf Jung's avatar
Ralf Jung committed
669
        [| destruct HE as [HES _]; setoid_rewrite EQt in HES; contradiction].
670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705
      assert (EQt' : Some (rdp, rl') · rf · s == Some t) by (rewrite EQt; reflexivity).
      clear EQt; rename EQt' into EQt.
      destruct rf as [ [rfp rfl] |]; [| now erewrite (comm _ 0), !pcm_op_zero in EQt by apply _].
      destruct s as [ [sp sl] |]; [| now erewrite (comm _ 0), pcm_op_zero in EQt by apply _].
      destruct (Some (rdp, rl') · Some (rfp, rfl)) as [ [rdfp rdfl] |] eqn: EQdf;
        setoid_rewrite EQdf in EQt; [| now erewrite pcm_op_zero in EQt by apply _].
      destruct (HU (Some rdl · Some rfl · Some sl)) as [rsl [HPrsl HCrsl] ].
      - intros HEq; destruct t as [tp tl]; apply pcm_op_split in EQt; destruct EQt as [_ EQt].
        assert (HT : Some (rdp, rl') · Some (rfp, rfl) == Some (rdfp, rdfl)) by (rewrite EQdf; reflexivity); clear EQdf.
        apply pcm_op_split in HT; destruct HT as [_ EQdf].
        now rewrite <- EQdf, <- EQrl, (comm (Some rdl)), <- (assoc (Some rl)), <- assoc, HEq in EQt.
      - destruct (rsl · Some rdl) as [rsl' |] eqn: EQrsl;
        [| contradiction HCrsl; eapply ores_equiv_eq; now erewrite !assoc, EQrsl, !pcm_op_zero by apply _ ].
        exists w' (rdp, rsl') (Some (sp, sl)); split; [reflexivity | split].
        + exists (exist _ rsl HPrsl); destruct rsl as [rsl |];
          [simpl | now erewrite pcm_op_zero in EQrsl by apply _].
          exists (rdp, rdl); rewrite pcm_op_split.
          split; [now erewrite comm, pcm_op_unit by apply _ | now rewrite comm, EQrsl].
        + destruct HE as [HES HEL]; split; [| assumption]; clear HEL.
          assert (HT := ores_equiv_eq _ _ _ EQt); setoid_rewrite EQdf in HES;
          setoid_rewrite HT in HES; clear HT; destruct t as [tp tl].
          destruct (rsl · (Some rdl · Some rfl · Some sl)) as [tl' |] eqn: EQtl;
          [| now contradiction HCrsl]; clear HCrsl.
          assert (HT : Some (rdp, rsl') · Some (rfp, rfl) · Some (sp, sl) = Some (tp, tl')); [| setoid_rewrite HT; apply HES].
          rewrite <- EQdf, <- assoc in EQt; clear EQdf; eapply ores_equiv_eq; rewrite <- assoc.
          destruct (Some (rfp, rfl) · Some (sp, sl)) as [ [up ul] |] eqn: EQu;
            setoid_rewrite EQu in EQt; [| now erewrite comm, pcm_op_zero in EQt by apply _].
          apply pcm_op_split in EQt; destruct EQt as [EQt _]; apply pcm_op_split; split; [assumption |].
          assert (HT : Some rfl · Some sl == Some ul);
            [| now rewrite <- EQrsl, <- EQtl, <- HT, !assoc].
          apply (proj2 (A := Some rfp · Some sp == Some up)), pcm_op_split.
          now erewrite EQu.
    Qed.
    (* The above proof is rather ugly in the way it handles the monoid elements,
       but it works *)

706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761
    Global Instance nat_type : Setoid nat := discreteType.
    Global Instance nat_metr : metric nat := discreteMetric.
    Global Instance nat_cmetr : cmetric nat := discreteCMetric.

    Program Definition inv' m : Props -n> {n : nat | m n} -n> Props :=
      n[(fun p => n[(fun n => inv n p)])].
    Next Obligation.
      intros i i' EQi; simpl in EQi; rewrite EQi; reflexivity.
    Qed.
    Next Obligation.
      intros i i' EQi; destruct n as [| n]; [apply dist_bound |].
      simpl in EQi; rewrite EQi; reflexivity.
    Qed.
    Next Obligation.
      intros p1 p2 EQp i; simpl morph.
      apply (morph_resp (inv (` i))); assumption.
    Qed.
    Next Obligation.
      intros p1 p2 EQp i; simpl morph.
      apply (inv (` i)); assumption.
    Qed.

    Lemma fresh_region (w : Wld) m (HInf : mask_infinite m) :
      exists i, m i /\ w i = None.
    Proof.
      destruct (HInf (S (List.last (dom w) 0%nat))) as [i [HGe Hm] ];
      exists i; split; [assumption |]; clear - HGe.
      rewrite <- fdLookup_notin_strong.
      destruct w as [ [| [n v] w] wP]; unfold dom in *; simpl findom_t in *; [tauto |].
      simpl List.map in *; rewrite last_cons in HGe.
      unfold ge in HGe; intros HIn; eapply Gt.gt_not_le, HGe.
      apply Le.le_n_S, SS_last_le; assumption.
    Qed.

    Instance LP_mask m : LimitPreserving m.
    Proof.
      intros σ σc Hp; apply Hp.
    Qed.

    Lemma vsNewInv p m (HInf : mask_infinite m) :
      valid (vs m m ( p) (xist (inv' m p))).
    Proof.
      intros pw nn r w _; clear r pw.
      intros n r _ _ HP w'; clear nn; intros.
      destruct n as [| n]; [now inversion HLe | simpl in HP].
      rewrite HSub in HP; clear w HSub; rename w' into w.
      destruct (fresh_region w m HInf) as [i [Hm HLi] ].
      assert (HSub : w  fdUpdate i (ı' p) w).
      { intros j; destruct (Peano_dec.eq_nat_dec i j); [subst j; rewrite HLi; exact I|].
        now rewrite fdUpdate_neq by assumption.
      }
      exists (fdUpdate i (ı' p) w) (pcm_unit _) (Some r · s); split; [assumption | split].
      - exists (exist _ i Hm); do 16 red.
        unfold proj1_sig; rewrite fdUpdate_eq; reflexivity.
      - erewrite pcm_op_unit by apply _.
        assert (HR : rf · (Some r · s) = Some r · rf · s)
762
          by (eapply ores_equiv_eq; rewrite assoc, (comm rf); reflexivity).
763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778
        destruct HE as [HES [rs [HE HM] ] ].
        split; [setoid_rewrite HR; assumption | clear HR].
        assert (HRi : rs i = None).
        { destruct (HM i) as [HDom _]; [tauto |].
          rewrite <- fdLookup_notin_strong, HDom, fdLookup_notin_strong; assumption.
        }
        exists (fdUpdate i r rs); split; [now rewrite <- erase_insert_new, HE by assumption | intros j Hm'].
        rewrite !fdLookup_in_strong; destruct (Peano_dec.eq_nat_dec i j).
        + subst j; rewrite !fdUpdate_eq; split; [intuition now eauto | intros].
          simpl in HLw, HLrs; subst ri; rewrite <- HLw, isoR, <- HSub.
          eapply uni_pred, HP; [now auto with arith | reflexivity].
        + rewrite !fdUpdate_neq, <- !fdLookup_in_strong by assumption.
          setoid_rewrite <- HSub.
          apply HM; assumption.
    Qed.

Filip Sieczkowski's avatar
Filip Sieczkowski committed
779 780 781 782 783 784 785 786 787 788 789
  End ViewShiftProps.

  Section HoareTriples.
  (* Quadruples, really *)
    Local Open Scope mask_scope.
    Local Open Scope pcm_scope.
    Local Open Scope bi_scope.
    Local Open Scope lang_scope.

    Global Instance expr_type : Setoid expr := discreteType.
    Global Instance expr_metr : metric expr := discreteMetric.
790 791 792 793 794
    Global Instance expr_cmetr : cmetric expr := discreteCMetric.
    Instance LP_isval : LimitPreserving is_value.
    Proof.
      intros σ σc HC; apply HC.
    Qed.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
795 796 797 798 799 800

    Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (w : Wld) (φ : value -n> Props) (r : res).

    Local Obligation Tactic := intros; eauto with typeclass_instances.

    Definition wpFP m (WP : expr -n> (value -n> Props) -n> Props) e φ w n r :=
801 802
      forall w' k s rf mf σ (HSw : w  w') (HLt : k < n) (HD : mf # m)
             (HE : erasure σ (m  mf) (Some r · rf) s w' @ S k),
Filip Sieczkowski's avatar
Filip Sieczkowski committed
803
        (forall (HV : is_value e),
804
         exists w'' r' s', w'  w'' /\ φ (exist _ e HV) w'' (S k) r'
805
                           /\ erasure σ (m  mf) (Some r' · rf) s' w'' @ S k) /\
Filip Sieczkowski's avatar
Filip Sieczkowski committed
806 807
        (forall σ' ei ei' K (HDec : e = K [[ ei ]])
                (HStep : prim_step (ei, σ) (ei', σ')),
808
         exists w'' r' s', w'  w'' /\ WP (K [[ ei' ]]) φ w'' k r'
809
                           /\ erasure σ' (m  mf) (Some r' · rf) s' w'' @ k) /\
810
        (forall e' K (HDec : e = K [[ fork e' ]]),
811 812 813
         exists w'' rfk rret s', w'  w''
                                 /\ WP (K [[ fork_ret ]]) φ w'' k rret
                                 /\ WP e' (umconst ) w'' k rfk
814
                                 /\ erasure σ (m  mf) (Some rfk · Some rret · rf) s' w'' @ k).
Filip Sieczkowski's avatar
Filip Sieczkowski committed
815 816 817 818

    Program Definition wpF m : (expr -n> (value -n> Props) -n> Props) -n> expr -n> (value -n> Props) -n> Props :=
      n[(fun WP => n[(fun e => n[(fun φ => m[(fun w => mkUPred (wpFP m WP e φ w) _)])])])].
    Next Obligation.
819
      intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k s rf mf σ HSw HLt HD HE.
820
      rewrite <- EQr, (comm (Some rd)), <- assoc in HE.
821
      specialize (Hp w' k s (Some rd · rf) mf σ); destruct Hp as [HV [HS HF] ];
822
      [| now eauto with arith | ..]; try assumption; [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
823
      split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843
      - specialize (HV HV0); destruct HV as [w'' [r1' [s' [HSw' [Hφ HE'] ] ] ] ].
        rewrite assoc, (comm (Some r1')) in HE'.
        destruct (Some rd · Some r1') as [r2' |] eqn: HR;
          [| apply erasure_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
        exists w'' r2' s'; split; [assumption | split; [| assumption] ].
        eapply uni_pred, Hφ; [| eexists; rewrite <- HR]; reflexivity.
      - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [s' [HSw' [HWP HE'] ] ] ] ].
        rewrite assoc, (comm (Some r1')) in HE'.
        destruct k as [| k]; [exists w'' r1' s'; simpl erasure; tauto |].
        destruct (Some rd · Some r1') as [r2' |] eqn: HR;
          [| apply erasure_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
        exists w'' r2' s'; split; [assumption | split; [| assumption] ].
        eapply uni_pred, HWP; [| eexists; rewrite <- HR]; reflexivity.
      - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
        destruct k as [| k]; [exists w'' rfk rret1 s'; simpl erasure; tauto |].
        rewrite assoc, <- (assoc (Some rfk)), (comm (Some rret1)) in HE'.
        destruct (Some rd · Some rret1) as [rret2 |] eqn: HR;
          [| apply erasure_not_empty in HE'; [contradiction | now erewrite (comm _ 0), !pcm_op_zero by apply _] ].
        exists w'' rfk rret2 s'; repeat (split; try assumption); [].
        eapply uni_pred, HWR; [| eexists; rewrite <- HR]; reflexivity.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
844 845 846 847 848 849 850 851 852 853 854 855 856
    Qed.
    Next Obligation.
      intros w1 w2 EQw n r; simpl.
      split; intros Hp w'; intros; eapply Hp; try eassumption.
      - rewrite EQw; assumption.
      - rewrite <- EQw; assumption.
    Qed.
    Next Obligation.
      intros w1 w2 EQw n' r HLt; simpl; destruct n as [| n]; [now inversion HLt |]; split; intros Hp w2'; intros.
      - symmetry in EQw; assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
        edestruct (Hp (extend w2' w1)) as [HV [HS HF] ]; try eassumption;
        [eapply erasure_dist, HE; [eassumption | now eauto with arith] |].
        split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
857
        + specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
858 859
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
860 861
          exists (extend w1'' w2') r' s'; split; [assumption |].
          split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
862
          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
863
        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
864 865
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
866 867
          exists (extend w1'' w2') r' s'; split; [assumption |].
          split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
868
          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
869
        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HWR [HWF HE'] ] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
870 871
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
872
          exists (extend w1'' w2') rfk rret s'; split; [assumption |].
873 874
          split; [| split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ];
          eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
875 876 877 878
      - assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
        edestruct (Hp (extend w2' w2)) as [HV [HS HF] ]; try eassumption;
        [eapply erasure_dist, HE; [eassumption | now eauto with arith] |].
        split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
879
        + specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
880 881
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
882 883
          exists (extend w1'' w2') r' s'; split; [assumption |].
          split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
884
          eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
885
        + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
886 887
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
888 889
          exists (extend w1'' w2') r' s'; split; [assumption |].
          split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
890
          eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
891
        + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HWR [HWF HE'] ] ] ] ] ] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
892 893
          assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
          assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
894
          exists (extend w1'' w2') rfk rret s'; split; [assumption |].
895 896
          split; [| split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ];
          eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
Filip Sieczkowski's avatar
Filip Sieczkowski committed
897 898 899 900 901 902 903 904 905 906 907 908 909
    Qed.
    Next Obligation.
      intros w1 w2 Sw n r; simpl; intros Hp w'; intros; eapply Hp; try eassumption.
      etransitivity; eassumption.
    Qed.
    Next Obligation.
      intros φ1 φ2 EQφ w n r; simpl.
      unfold wpFP; setoid_rewrite EQφ; reflexivity.
    Qed.
    Next Obligation.
      intros φ1 φ2 EQφ w k r HLt; simpl; destruct n as [| n]; [now inversion HLt |].
      split; intros Hp w'; intros; edestruct Hp as [HV [HS HF] ]; try eassumption; [|].
      - split; [| split]; intros.
910 911
        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
          exists w'' r' s'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
912
          apply EQφ, Hφ; now eauto with arith.
913 914
        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
          exists w'' r' s'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
915
          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [symmetry; eassumption | now eauto with arith].
916 917
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
          exists w'' rfk rret s'; repeat (split; try assumption); [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
918 919
          eapply (met_morph_nonexp _ _ (WP _)), HWR; [symmetry; eassumption | now eauto with arith].
      - split; [| split]; intros.
920 921
        + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
          exists w'' r' s'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
922
          apply EQφ, Hφ; now eauto with arith.
923 924
        + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
          exists w'' r' s'; split; [assumption | split; [| assumption] ].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
925
          eapply (met_morph_nonexp _ _ (WP _)), Hφ; [eassumption | now eauto with arith].
926 927
        + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
          exists w'' rfk rret s'; repeat (split; try assumption); [].
Filip Sieczkowski's avatar
Filip Sieczkowski committed
928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945
          eapply (met_morph_nonexp _ _ (WP _)), HWR; [eassumption | now eauto with arith].
    Qed.
    Next Obligation.
      intros e1 e2 EQe φ w n r; simpl.
      simpl in EQe; subst e2; reflexivity.
    Qed.
    Next Obligation.
      intros e1 e2 EQe φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
      simpl in EQe; subst e2; reflexivity.
    Qed.
    Next Obligation.
      intros WP1 WP2 EQWP e φ w n r; simpl.
      unfold wpFP; setoid_rewrite EQWP; reflexivity.
    Qed.
    Next Obligation.
      intros WP1 WP2 EQWP e φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
      split; intros Hp w'; intros; edestruct Hp as [HF [HS HV] ]; try eassumption; [|].
      - split; [assumption | split; intros].