iris.v 4.18 KB
Newer Older
1
Require Import world_prop core_lang lang masks.
2
Require Import RecDom.PCM RecDom.UPred RecDom.BI RecDom.PreoMet RecDom.Finmap.
3 4 5 6

Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).

  Module Import L  := Lang RP RL C.
7
  Module R <: PCM_T.
8 9 10 11 12 13 14
    Definition res := (RP.res * RL.res)%type.
    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 28 29 30
  (** 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 := _.

  (** And now we're ready to build the IRIS-specific connectives! *)

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
  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.

    Program Definition always : Props -n> Props :=
      n[(fun p => m[(fun w => mkUPred (fun n r => p w n (pcm_unit _)) _)])].
    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}.

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

    Program Definition intEq (t1 t2 : T) : Props := pcmconst (intEqP t1 t2).

    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.
76

77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
    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.

  (** Invariants **)
  Definition invP (i : nat) (p : Props) (w : Wld) : UPred R.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.
100
  Next Obligation.
101 102 103
    intros w1 w2 EQw; unfold invP; simpl morph.
    destruct n; [apply dist_bound |].
    apply intEq_dist; [apply EQw | reflexivity].
104 105
  Qed.
  Next Obligation.
106 107 108 109 110
    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.
111 112
  Qed.
  Next Obligation.
113 114 115
    intros p1 p2 EQp w; unfold equiv, invP in *; simpl morph.
    apply intEq_equiv; [reflexivity |].
    rewrite EQp; reflexivity.
116 117
  Qed.
  Next Obligation.
118 119 120
    intros p1 p2 EQp w; unfold invP; simpl morph.
    apply intEq_dist; [reflexivity |].
    apply dist_mono, (met_morph_nonexp _ _ ı'), EQp.
121 122
  Qed.

123 124 125 126 127 128 129 130 131 132 133 134 135
  (** Ownership **)
  Definition own (r : R.res) : Props :=
    pcmconst (up_cr (pord r)).

  (** Physical part **)
  Definition ownP (r : RP.res) : Props :=
    own (r, pcm_unit _).

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

End Iris.