BI.v 26.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 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 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147
Require Import PreoMet.
Require Import PCM.

Section CompleteBI.
  Context {T : Type}.

  Class topBI  := top  : T.
  Class botBI  := bot  : T.
  Class andBI  := and  : T -> T -> T.
  Class orBI   := or   : T -> T -> T.
  Class implBI := impl : T -> T -> T.
  Class scBI   := sc   : T -> T -> T.
  Class siBI   := si   : T -> T -> T.
  Class allBI  `{cmT : cmetric T} :=
    all  : forall {U} `{pU : cmetric U}, (U -n> T) -> T.
  Class xistBI `{cmT : cmetric T} :=
    xist : forall {U} `{pU : cmetric U}, (U -n> T) -> T.

  Section Lift.
    Context (f : T -> T -> T) `{cmT : cmetric T}
            {fequiv : Proper (equiv ==> equiv ==> equiv) f}
            {fdist : forall n, Proper (dist n ==> dist n ==> dist n) f}
            {U} `{cmU : cmetric U} (P : U -n> T) (Q : U -n> T).

    Local Obligation Tactic := intros; resp_set.

    Program Definition lift_bin : U -n> T :=
      n[(fun u => f (P u) (Q u))].

  End Lift.

  Class ComplBI `{pcmT : pcmType T, BIT : topBI, BIB : botBI, BIA : andBI,
                                    BIO : orBI, BII : implBI, BISC : scBI, BISI : siBI}
        {BIAll : allBI} {BIXist : xistBI} :=
    mkCBI {
        top_true    :  forall P, P  top;
        bot_false   :  forall P, bot  P;
        and_self    :  forall P, P  and P P;
        and_projL   :  forall P Q, and P Q  P;
        and_projR   :  forall P Q, and P Q  Q;
        and_equiv   :> Proper (equiv ==> equiv ==> equiv) and;
        and_dist n  :> Proper (dist n ==> dist n ==> dist n) and;
        and_pord    :> Proper (pord ==> pord ==> pord) and;
        and_impl    :  forall P Q R, and P Q  R <-> P  impl Q R;
        impl_equiv  :> Proper (equiv ==> equiv ==> equiv) impl;
        impl_dist n :> Proper (dist n ==> dist n ==> dist n) impl;
        impl_pord   :> Proper (pord --> pord ++> pord) impl;
        or_injL     :  forall P Q, P  or P Q;
        or_injR     :  forall P Q, Q  or P Q;
        or_self     :  forall P, or P P  P;
        or_equiv    :> Proper (equiv ==> equiv ==> equiv) or;
        or_dist n   :> Proper (dist n ==> dist n ==> dist n) or;
        or_pord     :> Proper (pord ==> pord ==> pord) or;
        sc_comm     :> Commutative sc;
        sc_assoc    :> Associative sc;
        sc_top_unit :  forall P, sc top P == P;
        sc_equiv    :> Proper (equiv ==> equiv ==> equiv) sc;
        sc_dist n   :> Proper (dist n ==> dist n ==> dist n) sc;
        sc_pord     :> Proper (pord ==> pord ==> pord) sc;
        sc_si       :  forall P Q R, sc P Q  R <-> P  si Q R;
        si_equiv    :> Proper (equiv ==> equiv ==> equiv) si;
        si_dist n   :> Proper (dist n ==> dist n ==> dist n) si;
        si_pord     :> Proper (pord --> pord ++> pord) si;
        all_R      U `{cmU : cmetric U} :
          forall P (Q : U -n> T), (forall u, P  Q u) <-> P  all Q;
        all_equiv  U `{cmU : cmetric U} :> Proper (equiv ==> equiv) all;
        all_dist   U `{cmU : cmetric U} n :> Proper (dist n ==> dist n) all;
        all_pord   U `{cmU : cmetric U} (P Q : U -n> T) :
          (forall u, P u  Q u) -> all P  all Q;
        xist_L     U `{cmU : cmetric U} :
          forall (P : U -n> T) Q, (forall u, P u  Q) <-> xist P  Q;
        xist_sc    U `{cmU : cmetric U} :
          forall (P : U -n> T) Q, sc (xist P) Q  xist (lift_bin sc P (umconst Q));
        xist_equiv U `{cmU : cmetric U} :> Proper (equiv ==> equiv) xist;
        xist_dist  U `{cmU : cmetric U} n :> Proper (dist n ==> dist n) xist;
        xist_pord  U `{cmU : cmetric U} (P Q : U -n> T) :
          (forall u, P u  Q u) -> xist P  xist Q
      }.

End CompleteBI.

Arguments topBI  : default implicits.
Arguments botBI  : default implicits.
Arguments andBI  : default implicits.
Arguments orBI   : default implicits.
Arguments implBI : default implicits.
Arguments scBI   : default implicits.
Arguments siBI   : default implicits.
Arguments allBI  T {_ _ _}.
Arguments xistBI T {_ _ _}.
Arguments ComplBI T {_ _ _ _ _ _ _ _ _ _ _ _ _ _}.

Class Valid (T : Type) `{pcmT : pcmType T} :=
  { valid : T -> Prop;
    valid_top (t t' : T) (HV : valid t) : t'  t
  }.

Class Later (T : Type) `{pcmT : pcmType T} {vT : Valid T} :=
  { later : T -m> T;
    later_mon (t : T) : t  later t;
    later_contr : contractive later;
    loeb (t : T) (HL : later t  t) : valid t
  }.

Notation " ▹ p " := (later p) (at level 20) : bi_scope.

Require Import UPred.

Section UPredLater.
  Context Res `{preoRes : preoType Res}.
  Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.

  Global Program Instance valid_up : Valid (UPred Res) :=
    Build_Valid _ _ _ _ _ _ (fun p : UPred Res => forall n r, p n r) _.
  Next Obligation.
    intros n r _; apply HV.
  Qed.

  Global Instance later_up_mon : Proper (pord ==> pord) later_up.
  Proof.
    intros p q Hpq [| n] r; [intros; exact I | simpl; apply Hpq].
  Qed.

  Global Program Instance later_upred : Later (UPred Res) :=
    Build_Later _ _ _ _ _ _ _ m[(later_up)] _ _ _.
  Next Obligation.
    intros [| n] r Ht; [exact I | simpl].
    rewrite Le.le_n_Sn; assumption.
  Qed.
  Next Obligation.
    intros n p q Hpq [| m] r HLt; simpl; [tauto |].
    apply Hpq; auto with arith.
  Qed.
  Next Obligation.
    intros n r; induction n.
    - apply HL; exact I.
    - apply HL, IHn.
  Qed.

End UPredLater.

Section UPredBI.
  Context Res `{pcmRes : PCM Res}.
  Local Open Scope pcm_scope.
  Local Obligation Tactic := intros; eauto with typeclass_instances.

  (* Standard interpretations of propositional connectives. *)
148 149
  Global Program Instance top_up : topBI (UPred Res) := up_cr (const True).
  Global Program Instance bot_up : botBI (UPred Res) := up_cr (const False).
150

151
  Global Program Instance and_up : andBI (UPred Res) :=
152 153 154 155 156
    fun P Q =>
      mkUPred (fun n r => P n r /\ Q n r) _.
  Next Obligation.
    intros n m r1 r2 HLe HSub; rewrite HSub, HLe; tauto.
  Qed.
157
  Global Program Instance or_up : orBI (UPred Res) :=
158 159 160 161 162 163
    fun P Q =>
      mkUPred (fun n r => P n r \/ Q n r) _.
  Next Obligation.
    intros n m r1 r2 HLe HSub; rewrite HSub, HLe; tauto.
  Qed.

164
  Global Program Instance impl_up : implBI (UPred Res) :=
165 166 167 168 169 170 171 172
    fun P Q =>
      mkUPred (fun n r => forall m r', m <= n -> r  r' -> P m r' -> Q m r') _.
  Next Obligation.
    intros n m r1 r2 HLe HSub HImp k r3 HLe' HSub' HP.
    apply HImp; try (etransitivity; eassumption); assumption.
  Qed.

  (* BI connectives. *)
173
  Global Program Instance sc_up : scBI (UPred Res) :=
174
    fun P Q =>
175
      mkUPred (fun n r => exists r1 r2, Some r1 · Some r2 == Some r /\ P n r1 /\ Q n r2) _.
176
  Next Obligation.
177 178
    intros n m r1 r2 HLe [rd HEq] [r11 [r12 [HEq' [HP HQ]]]].
    rewrite <- HEq', assoc in HEq; setoid_rewrite HLe.
179 180
    destruct (Some rd · Some r11) as [r11' |] eqn: HEq'';
      [| erewrite pcm_op_zero in HEq by apply _; contradiction].
181
    repeat eexists; [eassumption | | assumption].
182 183
    eapply uni_pred, HP; [reflexivity |].
    exists rd; rewrite HEq''; reflexivity.
184 185
  Qed.

186
  Global Program Instance si_up : siBI (UPred Res) :=
187
    fun P Q =>
188
      mkUPred (fun n r => forall m r' rr, Some r · Some r' == Some rr -> m <= n -> P m r' -> Q m rr) _.
189
  Next Obligation.
190 191
    intros n m r1 r2 HLe [r12 HEq] HSI k r rr HEq' HSub HP.
    rewrite comm in HEq; rewrite <- HEq, <- assoc in HEq'.
192 193 194 195
    destruct (Some r12 · Some r) as [r' |] eqn: HEq'';
      [| erewrite comm, pcm_op_zero in HEq' by apply _; contradiction].
    eapply HSI; [eassumption | etransitivity; eassumption |].
    eapply uni_pred, HP; [| exists r12; rewrite HEq'']; reflexivity.
196 197 198
  Qed.

  (* Quantifiers. *)
199
  Global Program Instance all_up : allBI (UPred Res) :=
200 201 202 203 204 205
    fun T eqT mT cmT R =>
      mkUPred (fun n r => forall t, R t n r) _.
  Next Obligation.
    intros n m r1 r2 HLe HSub HR t; rewrite HLe, <- HSub; apply HR.
  Qed.

206
  Global Program Instance xist_up : xistBI (UPred Res) :=
207 208 209 210 211 212
    fun T eqT mT cmT R =>
      mkUPred (fun n r => exists t, R t n r) _.
  Next Obligation.
    intros n m r1 r2 HLe HSub [t HR]; exists t; rewrite HLe, <- HSub; apply HR.
  Qed.

213 214
  (* For some reason tc inference gets confused otherwise *)
  Existing Instance up_type.
215

216
  (* All of the above preserve all the props it should. *)
217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 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 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300
  Global Instance and_up_equiv : Proper (equiv ==> equiv ==> equiv) and_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ n r; simpl.
    rewrite EQP, EQQ; tauto.
  Qed.
  Global Instance and_up_dist n : Proper (dist n ==> dist n ==> dist n) and_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ m r HLt; simpl.
    split; intros; (split; [apply EQP | apply EQQ]; now auto with arith).
  Qed.
  Global Instance and_up_ord : Proper (pord ==> pord ==> pord) and_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ n r; simpl.
    rewrite EQP, EQQ; tauto.
  Qed.

  Global Instance or_up_equiv : Proper (equiv ==> equiv ==> equiv) or_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ n r; simpl.
    rewrite EQP, EQQ; tauto.
  Qed.
  Global Instance or_up_dist n : Proper (dist n ==> dist n ==> dist n) or_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ m r HLt; simpl.
    split; (intros [HP | HQ]; [left; apply EQP | right; apply EQQ]; now auto with arith).
  Qed.
  Global Instance or_up_ord : Proper (pord ==> pord ==> pord) or_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ n r; simpl.
    rewrite EQP, EQQ; tauto.
  Qed.

  Global Instance impl_up_equiv : Proper (equiv ==> equiv ==> equiv) impl_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ n r; simpl.
    setoid_rewrite EQP; setoid_rewrite EQQ; tauto.
  Qed.
  Global Instance impl_up_dist n : Proper (dist n ==> dist n ==> dist n) impl_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ m r HLt; simpl.
    split; intros; apply EQQ, H, EQP; now eauto with arith.
  Qed.
  Global Instance impl_up_ord : Proper (pord --> pord ++> pord) impl_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ n r HP m r'.
    rewrite <- EQP, <- EQQ; apply HP.
  Qed.

  Global Instance sc_up_equiv : Proper (equiv ==> equiv ==> equiv) sc_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ n r; simpl.
    setoid_rewrite EQP; setoid_rewrite EQQ; tauto.
  Qed.
  Global Instance sc_up_dist n : Proper (dist n ==> dist n ==> dist n) sc_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ m r HLt; simpl.
    split; intros [r1 [r2 [EQr [HP HQ]]]]; exists r1; exists r2;
    (split; [assumption | split; [apply EQP | apply EQQ]; now auto with arith]).
  Qed.
  Global Instance sc_up_ord : Proper (pord ==> pord ==> pord) sc_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ n r HH; simpl.
    setoid_rewrite <- EQP; setoid_rewrite <- EQQ; apply HH.
  Qed.

  Global Instance si_up_equiv : Proper (equiv ==> equiv ==> equiv) si_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ n r; simpl.
    setoid_rewrite EQP; setoid_rewrite EQQ; tauto.
  Qed.
  Global Instance si_up_dist n : Proper (dist n ==> dist n ==> dist n) si_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ m r HLt; simpl.
    split; intros; eapply EQQ, H, EQP; now eauto with arith.
  Qed.
  Global Instance si_up_ord : Proper (pord --> pord ++> pord) si_up.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ n r HP m r' rr.
    rewrite <- EQP, <- EQQ; apply HP.
  Qed.

  Section Quantifiers.
    Context V `{pU : cmetric V}.

301 302
    Existing Instance nonexp_type.

303
    Global Instance all_up_equiv : Proper (equiv (T := V -n> UPred Res) ==> equiv) all.
304 305 306 307
    Proof.
      intros R1 R2 EQR n r; simpl.
      setoid_rewrite EQR; tauto.
    Qed.
308
    Global Instance all_up_dist n : Proper (dist (T := V -n> UPred Res) n ==> dist n) all.
309 310 311 312 313
    Proof.
      intros R1 R2 EQR m r HLt; simpl.
      split; intros; apply EQR; now auto.
    Qed.

314
    Global Instance xist_up_equiv : Proper (equiv (T := V -n> UPred Res) ==> equiv) xist.
315 316 317 318
    Proof.
      intros R1 R2 EQR n r; simpl.
      setoid_rewrite EQR; tauto.
    Qed.
319
    Global Instance xist_up_dist n : Proper (dist (T := V -n> UPred Res)n ==> dist n) xist.
320 321 322 323 324 325 326
    Proof.
      intros R1 R2 EQR m r HLt; simpl.
      split; intros [t HR]; exists t; apply EQR; now auto.
    Qed.

  End Quantifiers.

327
  Global Program Instance bi_up : ComplBI (UPred Res).
328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362
  Next Obligation.
    intros n r _; exact I.
  Qed.
  Next Obligation.
    intros n r HC; contradiction HC.
  Qed.
  Next Obligation.
    intros n r; simpl; tauto.
  Qed.
  Next Obligation.
    intros n r [HP HQ]; assumption.
  Qed.
  Next Obligation.
    intros n r [HP HQ]; assumption.
  Qed.
  Next Obligation.
    split; intros HH n r.
    - intros HP m r' HLe HSub HQ; apply HH; split; [rewrite HLe, <- HSub |]; assumption.
    - intros [HP HQ]; eapply HH; eassumption || reflexivity.
  Qed.
  Next Obligation.
    intros n r HP; left; assumption.
  Qed.
  Next Obligation.
    intros n r HQ; right; assumption.
  Qed.
  Next Obligation.
    intros n r; simpl; tauto.
  Qed.
  Next Obligation.
    intros P Q n r; simpl.
    setoid_rewrite (comm (Commutative := pcm_op_comm _)) at 1.
    firstorder.
  Qed.
  Next Obligation.
363
    intros P Q R n r; split.
364
    - intros [r1 [rr [EQr [HP [r2 [r3 [EQrr [HQ HR]]]]]]]].
365
      rewrite <- EQrr, assoc in EQr.
366 367 368 369
      destruct (Some r1 · Some r2) as [r12 |] eqn: EQr';
        [| now erewrite pcm_op_zero in EQr by apply _].
      exists r12 r3; split; [assumption | split; [| assumption] ].
      exists r1 r2; split; [rewrite EQr'; reflexivity | split; assumption].
370
    - intros [rr [r3 [EQr [[r1 [r2 [EQrr [HP HQ]]]] HR]]]].
371 372 373 374 375
      rewrite <- EQrr, <- assoc in EQr; clear EQrr.
      destruct (Some r2 · Some r3) as [r23 |] eqn: EQ23;
        [| now erewrite comm, pcm_op_zero in EQr by apply _].
      exists r1 r23; split; [assumption | split; [assumption |] ].
      exists r2 r3; split; [rewrite EQ23; reflexivity | split; assumption].
376 377
  Qed.
  Next Obligation.
378
    intros n r; split.
379
    - intros [r1 [r2 [EQr [_ HP]]]].
380
      eapply uni_pred, HP; [| exists r1]; trivial.
381 382 383
    - intros HP; exists (pcm_unit _) r; split;
      [erewrite pcm_op_unit by apply _; reflexivity |].
      simpl; unfold const; tauto.
384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 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 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 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 669 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 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 762 763 764 765 766 767 768 769 770 771 772 773 774
  Qed.
  Next Obligation.
    split; intros HH n r.
    - intros HP m r' rr EQrr HLe HQ; apply HH; rewrite <- HLe in HP.
      eexists; eexists; split; [eassumption | tauto].
    - intros [r1 [r2 [EQr [HP HQ]]]]; eapply HH; eassumption || reflexivity.
  Qed.
  Next Obligation.
    split.
    - intros HH n r HP u; apply HH; assumption.
    - intros HH u n r HP; apply HH; assumption.
  Qed.
  Next Obligation.
    intros n r HA u; apply H, HA.
  Qed.
  Next Obligation.
    split.
    - intros HH n r [u HP]; eapply HH; eassumption.
    - intros HH u n r HP; apply HH; exists u; assumption.
  Qed.
  Next Obligation.
    intros n t [t1 [t2 [EQt [[u HP] HQ]]]]; exists u t1 t2; tauto.
  Qed.
  Next Obligation.
    intros n r [u HA]; exists u; apply H, HA.
  Qed.

End UPredBI.

(* This class describes a type that can close over "future Us",
   thus making a nonexpansive map monotone *)
Class MonotoneClosure T `{pcmT : pcmType T} :=
  { mclose : forall {U} `{pcmU : pcmType U} {eU : extensible U},
               (U -n> T) -n> U -m> T;
    mclose_cl : forall {U} `{pcmU : pcmType U} {eU : extensible U} (f : U -n> T) u,
                  mclose f u  f u;
    mclose_fw : forall {U} `{pcmU : pcmType U} {eU : extensible U} (f : U -n> T) u t
                       (HFW : forall u' (HS : u  u'), t  f u'),
                  t  mclose f u
  }.
Arguments Build_MonotoneClosure {_ _ _ _ _ _} _ {_ _}.

Section MonotoneExt.
  Context B `{BBI : ComplBI B} {MCB : MonotoneClosure B}
          T `{pcmT' : pcmType T} {eT : extensible T}.
  Local Obligation Tactic := intros; resp_set || mono_resp || eauto with typeclass_instances.

  Global Instance top_mm : topBI (T -m> B) := pcmconst top.
  Global Instance bot_mm : botBI (T -m> B) := pcmconst bot.

  Global Program Instance and_mm : andBI (T -m> B) :=
    fun P Q => m[(lift_bin and P Q)].
  Global Program Instance or_mm  : orBI  (T -m> B) :=
    fun P Q => m[(lift_bin or P Q)].

  Global Instance impl_mm : implBI (T -m> B) :=
    fun P Q => mclose (lift_bin impl P Q).

  Global Program Instance sc_mm  : scBI  (T -m> B) :=
    fun P Q => m[(lift_bin sc P Q)].

  Global Instance si_mm : siBI (T -m> B) :=
    fun P Q => mclose (lift_bin si P Q).

  Global Program Instance all_mm : allBI (T -m> B) :=
    fun U eqU mU cmU R =>
      m[(fun t => all n[(fun u => R u t)])].
  Next Obligation.
    intros t1 t2 EQt; apply all_dist; intros u; simpl morph.
    rewrite EQt; reflexivity.
  Qed.
  Next Obligation.
    intros t1 t2 Subt; apply all_pord; intros u; simpl morph.
    rewrite Subt; reflexivity.
  Qed.

  Global Program Instance xist_mm : xistBI (T -m> B) :=
    fun U eqU mU cmU R =>
      m[(fun t => xist n[(fun u => R u t)])].
  Next Obligation.
    intros t1 t2 EQt; apply xist_dist; intros u; simpl morph.
    rewrite EQt; reflexivity.
  Qed.
  Next Obligation.
    intros t1 t2 Subt; apply xist_pord; intros u; simpl morph.
    rewrite Subt; reflexivity.
  Qed.

  (* All of the above preserve all the props it should. *)
  Global Instance and_mm_equiv : Proper (equiv ==> equiv ==> equiv) and_mm.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ t; simpl morph.
    apply and_equiv; [apply EQP | apply EQQ].
  Qed.
  Global Instance and_mm_dist n : Proper (dist n ==> dist n ==> dist n) and_mm.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ t; simpl morph.
    apply and_dist; [apply EQP | apply EQQ].
  Qed.
  Global Instance and_mm_ord : Proper (pord ==> pord ==> pord) and_mm.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ t; simpl morph.
    apply and_pord; [apply EQP | apply EQQ].
  Qed.

  Global Instance or_mm_equiv : Proper (equiv ==> equiv ==> equiv) or_mm.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ t; simpl morph.
    apply or_equiv; [apply EQP | apply EQQ].
  Qed.
  Global Instance or_mm_dist n : Proper (dist n ==> dist n ==> dist n) or_mm.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ t; simpl morph.
    apply or_dist; [apply EQP | apply EQQ].
  Qed.
  Global Instance or_mm_ord : Proper (pord ==> pord ==> pord) or_mm.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ t; simpl morph.
    apply or_pord; [apply EQP | apply EQQ].
  Qed.

  Global Instance impl_mm_equiv : Proper (equiv ==> equiv ==> equiv) impl_mm.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ; unfold impl_mm.
    apply (morph_resp mclose); intros t; simpl morph.
    apply impl_equiv; [apply EQP | apply EQQ].
  Qed.
  Global Instance impl_mm_dist n : Proper (dist n ==> dist n ==> dist n) impl_mm.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ; apply met_morph_nonexp; intros t; simpl morph.
    apply impl_dist; [apply EQP | apply EQQ].
  Qed.
  Global Instance impl_mm_ord : Proper (pord --> pord ++> pord) impl_mm.
  Proof.
    intros P1 P2 SubP Q1 Q2 SubQ t; unfold flip in SubP; unfold impl, impl_mm.
    apply mclose_fw; intros t' Subt; rewrite Subt; clear t Subt; simpl morph.
    rewrite SubP, <- SubQ; apply mclose_cl.
  Qed.

  Global Instance sc_mm_equiv : Proper (equiv ==> equiv ==> equiv) sc_mm.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ t; simpl morph.
    apply sc_equiv; [apply EQP | apply EQQ].
  Qed.
  Global Instance sc_mm_dist n : Proper (dist n ==> dist n ==> dist n) sc_mm.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ t; simpl morph.
    apply sc_dist; [apply EQP | apply EQQ].
  Qed.
  Global Instance sc_mm_ord : Proper (pord ==> pord ==> pord) sc_mm.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ t; simpl morph.
    apply sc_pord; [apply EQP | apply EQQ].
  Qed.

  Global Instance si_mm_equiv : Proper (equiv ==> equiv ==> equiv) si_mm.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ; apply (morph_resp mclose); intros t; simpl morph.
    apply si_equiv; [apply EQP | apply EQQ].
  Qed.
  Global Instance si_mm_dist n : Proper (dist n ==> dist n ==> dist n) si_mm.
  Proof.
    intros P1 P2 EQP Q1 Q2 EQQ; apply met_morph_nonexp; intros t; simpl morph.
    apply si_dist; [apply EQP | apply EQQ].
  Qed.
  Global Instance si_mm_ord : Proper (pord --> pord ++> pord) si_mm.
  Proof.
    intros P1 P2 SubP Q1 Q2 SubQ t; unfold flip in SubP; unfold impl, impl_mm.
    apply mclose_fw; intros t' Subt; rewrite Subt; clear t Subt; simpl morph.
    rewrite SubP, <- SubQ; apply mclose_cl.
  Qed.

  Section Quantifiers.
    Context V `{cmV : cmetric V}.

    Global Instance all_mm_equiv : Proper (equiv (T := V -n> T -m> B) ==> equiv) all.
    Proof.
      intros R1 R2 EQR t; simpl morph.
      apply all_equiv; intros u; simpl morph; apply EQR.
    Qed.
    Global Instance all_mm_dist n : Proper (dist (T := V -n> T -m> B) n ==> dist n) all.
    Proof.
      intros R1 R2 EQR t; simpl morph.
      apply all_dist; intros u; simpl morph; apply EQR.
    Qed.

    Global Instance xist_mm_equiv : Proper (equiv (T := V -n> T -m> B) ==> equiv) xist.
    Proof.
      intros R1 R2 EQR t; simpl.
      apply xist_equiv; intros u; simpl; apply EQR.
    Qed.
    Global Instance xist_mm_dist n : Proper (dist (T := V -n> T -m> B)n ==> dist n) xist.
    Proof.
      intros R1 R2 EQR t; simpl morph.
      apply xist_dist; intros u; simpl morph; apply EQR.
    Qed.

  End Quantifiers.

  Global Program Instance bi_mm : ComplBI (T -m> B).
  Next Obligation.
    intros t; apply top_true.
  Qed.
  Next Obligation.
    intros t; apply bot_false.
  Qed.
  Next Obligation.
    intros t; simpl morph; apply and_self.
  Qed.
  Next Obligation.
    intros t; simpl morph; apply and_projL.
  Qed.
  Next Obligation.
    intros t; simpl morph; apply and_projR.
  Qed.
  Next Obligation.
    split; intros HH t; simpl morph.
    - apply mclose_fw; intros t' Subt; specialize (HH t'); simpl morph in *.
      rewrite Subt, <- and_impl; assumption.
    - rewrite and_impl, (HH t); apply mclose_cl.
  Qed.
  Next Obligation.
    intros t; simpl morph; apply or_injL.
  Qed.
  Next Obligation.
    intros t; simpl morph; apply or_injR.
  Qed.
  Next Obligation.
    intros t; simpl morph; apply or_self.
  Qed.
  Next Obligation.
    intros f1 f2 t; simpl morph; apply comm.
  Qed.
  Next Obligation.
    intros f1 f2 f3 t; simpl morph; apply assoc.
  Qed.
  Next Obligation.
    intros t; simpl morph; apply sc_top_unit.
  Qed.
  Next Obligation.
    split; intros HH t; simpl morph.
    - apply mclose_fw; intros t' Subt; specialize (HH t'); simpl morph in *.
      rewrite Subt, <- sc_si; assumption.
    - rewrite sc_si, (HH t); apply mclose_cl.
  Qed.
  Next Obligation.
    split.
    - intros HH t; simpl morph; rewrite <- all_R; intros u; simpl morph; apply HH.
    - intros HH u t; specialize (HH t); simpl morph in *; rewrite <- all_R in HH.
      simpl morph in HH; apply HH.
  Qed.
  Next Obligation.
    intros t; apply all_pord; intros u; simpl morph; apply H.
  Qed.
  Next Obligation.
    split.
    - intros HH t; simpl morph; rewrite <- xist_L; intros u; simpl morph; apply HH.
    - intros HH u t; specialize (HH t); simpl morph in *.
      rewrite <- xist_L in HH; simpl morph in HH; apply HH.
  Qed.
  Next Obligation.
    intros t; simpl morph.
    rewrite xist_sc; eapply xist_pord; intros u; simpl morph.
    reflexivity.
  Qed.
  Next Obligation.
    intros t; apply xist_pord; intros u; apply H.
  Qed.

End MonotoneExt.

Section MonotoneLater.
  Context T U `{LT : Later T} `{pcmU : pcmType U}.
  Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.

  Global Program Instance valid_mon : Valid (U -m> T) :=
    Build_Valid _ _ _ _ _ _ (fun f : U -m> T => forall u, valid (f u)) _.
  Next Obligation.
    intros u; apply valid_top, HV.
  Qed.

  Global Program Instance later_mon_morph : Later (U -m> T) :=
    Build_Later _ _ _ _ _ _ _ m[(fun f => m[(fun u => later (f u))])] _ _ _.
  Next Obligation.
    intros u; simpl morph; apply later_mon.
  Qed.
  Next Obligation.
    intros n f g Hfg u; simpl morph; apply later_contr, Hfg.
  Qed.
  Next Obligation.
    intros u; apply loeb, HL.
  Qed.

End MonotoneLater.

Section MComplUP.

  Context V `{pV : preoType V}.
  Local Obligation Tactic := intros; try resp_set.

  Section Def.
    Context T `{pcmT : pcmType T} {eT : extensible T}.

    Program Definition mclose_up : (T -n> UPred V) -n> T -m> UPred V :=
      n[(fun f => m[(fun t => mkUPred (fun n v => forall t', t  t' -> f t' n v) _)])].
    Next Obligation.
      intros n m v1 v2 HLe HSubv HT t' HSubt.
      rewrite HLe, <- HSubv; apply HT, HSubt.
    Qed.
    Next Obligation.
      intros t1 t2 EQt m v HLt; split; intros HT t' Subt;
      (destruct n as [| n]; [now inversion HLt |]).
      - symmetry in EQt.
        assert (HH : f t' = S n = f (extend t' t1)) by (eapply f, extend_dist; eassumption).
        apply HH; [assumption |].
        eapply HT, extend_sub; eassumption.
      - assert (HH : f t' = S n = f (extend t' t2)) by (eapply f, extend_dist; eassumption).
        apply HH; [assumption |].
        eapply HT, extend_sub; eassumption.
    Qed.
    Next Obligation.
      intros t1 t2 Subt n v HT t' Subt'; apply HT; etransitivity; eassumption.
    Qed.
    Next Obligation.
      intros f1 f2 EQf u m v HLt; split; intros HH u' HSub; apply EQf, HH; assumption.
    Qed.

  End Def.

  Global Program Instance MCl_up : MonotoneClosure (UPred V) :=
    Build_MonotoneClosure mclose_up.
  Next Obligation.
    intros n v HH; apply HH; reflexivity.
  Qed.
  Next Obligation.
    intros n v HH u' HSub; apply HFW; assumption.
  Qed.

End MComplUP.

(* The above suffice for showing that the eqn used in Rose actually forms a Complete BI.
   The following would allow for further monotone morphisms to be added. *)

Section MComplMM.
  Context B `{BBI : ComplBI B} {MCB : MonotoneClosure B}
          V `{pcmV : pcmType V} {eT : extensible V}.
  Local Obligation Tactic := intros; resp_set || mono_resp || eauto with typeclass_instances.

  Section Def.
    Context U `{pcmU : pcmType U} {eU : extensible U}.

    Program Instance extensible_prod : extensible (U * V) :=
      mkExtend (fun uv1 uv2 => (extend (fst uv1) (fst uv2), extend (snd uv1) (snd uv2))).
    Next Obligation.
      destruct vd as [ud vd]; destruct ve as [ue ve].
      destruct HD as [HDu HDv]; destruct HS as [HSu HSv].
      split; eapply extend_dist; eassumption.
    Qed.
    Next Obligation.
      destruct vd as [ud vd]; destruct ve as [ue ve].
      destruct HD as [HDu HDv]; destruct HS as [HSu HSv].
      split; eapply extend_sub; eassumption.
    Qed.

    Program Definition mclose_mm : (U -n> V -m> B) -n> U -m> V -m> B :=
      n[(fun f => mcurry (mclose n[(fun uv => f (fst uv) (snd uv))]))].
    Next Obligation.
      intros [u1 v1] [u2 v2] [EQu EQv]; simpl morph.
      unfold fst, snd in *; rewrite EQu, EQv; reflexivity.
    Qed.
    Next Obligation.
      intros f1 f2 EQf u v; simpl morph.
      apply mclose; clear u v; intros [u v]; simpl morph.
      apply EQf.
    Qed.

  End Def.

  Global Program Instance MCl_mm : MonotoneClosure (V -m> B) := Build_MonotoneClosure mclose_mm.
  Next Obligation.
    intros v; simpl morph.
    rewrite mclose_cl; reflexivity.
  Qed.
  Next Obligation.
    intros v; simpl morph.
    apply mclose_fw; intros [u' v'] [HSubu HSubv]; simpl morph.
    rewrite HSubv; apply HFW; assumption.
  Qed.

End MComplMM.

775
Section BIValid.
776 777 778 779 780 781 782 783
  Local Obligation Tactic := intros.

  Global Program Instance BI_valid T `{ComplBI T} : Valid T :=
    Build_Valid _ _ _ _ _ _ (fun t => top  t) _.
  Next Obligation.
    etransitivity; [apply top_true | assumption].
  Qed.

784
End BIValid.