iris_vs.v 19.1 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
Require Import world_prop core_lang masks iris_core.
Require Import ModuRes.PCM ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap.

Module IrisVS (RL : PCM_T) (C : CORE_LANG).
  Module Export CORE := IrisCore RL C.

  Delimit Scope iris_scope with iris.
  Local Open Scope iris_scope.

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

    Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred res :=
Ralf Jung's avatar
Ralf Jung committed
16
      mkUPred (fun n r => forall w1 rf mf σ k (HSub : w  w1) (HLe : k < n)
Ralf Jung's avatar
Ralf Jung committed
17
                                 (HD : mf # m1  m2)
Ralf Jung's avatar
Ralf Jung committed
18 19
                                 (HE : wsat σ (m1  mf) (Some r · rf) w1 @ S k),
                          exists w2 r',
Ralf Jung's avatar
Ralf Jung committed
20
                            w1  w2 /\ p w2 (S k) r'
Ralf Jung's avatar
Ralf Jung committed
21
                            /\ wsat σ (m2  mf) (Some r' · rf) w2 @ S k) _.
Ralf Jung's avatar
Ralf Jung committed
22 23
    Next Obligation.
      intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
Ralf Jung's avatar
Ralf Jung committed
24
      destruct (HP w1 (Some rd · rf) mf σ k) as [w2 [r1' [HW [HP' HE'] ] ] ];
Ralf Jung's avatar
Ralf Jung committed
25
        try assumption; [now eauto with arith | |].
26
      - eapply wsat_equiv, HE; try reflexivity.
Ralf Jung's avatar
Ralf Jung committed
27 28 29
        rewrite assoc, (comm (Some r1)), HR; reflexivity.
      - rewrite assoc, (comm (Some r1')) in HE'.
        destruct (Some rd · Some r1') as [r2' |] eqn: HR';
30
          [| apply wsat_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
Ralf Jung's avatar
Ralf Jung committed
31
        exists w2 r2'; split; [assumption | split; [| assumption] ].
Ralf Jung's avatar
Ralf Jung committed
32 33 34 35 36 37 38 39 40
        eapply uni_pred, HP'; [| exists rd; rewrite HR']; reflexivity.
    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 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)).
Ralf Jung's avatar
Ralf Jung committed
41
        edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
42
        + eapply wsat_dist, HE; [symmetry; eassumption | now eauto with arith].
Ralf Jung's avatar
Ralf Jung committed
43 44
        + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
Ralf Jung's avatar
Ralf Jung committed
45
          exists (extend w1'' w2') r'; split; [assumption | split].
Ralf Jung's avatar
Ralf Jung committed
46
          * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
47
          * eapply wsat_dist, HE'; [symmetry; eassumption | now eauto with arith].
Ralf Jung's avatar
Ralf Jung committed
48
      - assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)).
Ralf Jung's avatar
Ralf Jung committed
49
        edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
50
        + eapply wsat_dist, HE; [symmetry; eassumption | now eauto with arith].
Ralf Jung's avatar
Ralf Jung committed
51 52
        + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
          assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
Ralf Jung's avatar
Ralf Jung committed
53
          exists (extend w1'' w2') r'; split; [assumption | split].
Ralf Jung's avatar
Ralf Jung committed
54
          * eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
55
          * eapply wsat_dist, HE'; [symmetry; eassumption | now eauto with arith].
Ralf Jung's avatar
Ralf Jung committed
56 57 58 59 60 61 62
    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 HLt; split; intros HP w1; intros.
Ralf Jung's avatar
Ralf Jung committed
63
      - edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
Ralf Jung's avatar
Ralf Jung committed
64 65
        clear HP; repeat (eexists; try eassumption); [].
        apply EQp; [now eauto with arith | assumption].
Ralf Jung's avatar
Ralf Jung committed
66
      - edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
Ralf Jung's avatar
Ralf Jung committed
67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
        clear HP; repeat (eexists; try eassumption); [].
        apply EQp; [now eauto with arith | assumption].
    Qed.

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

  End ViewShifts.

  Section ViewShiftProps.
    Local Open Scope mask_scope.
    Local Open Scope pcm_scope.
    Local Open Scope bi_scope.

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

    Definition mask_sing i := mask_set mask_emp i True.

    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.
Ralf Jung's avatar
Ralf Jung committed
90
      exists w1 rp; split; [reflexivity | split; [| assumption] ]; clear HE HD.
Ralf Jung's avatar
Ralf Jung committed
91 92 93 94 95 96 97 98 99 100
      destruct np as [| np]; [now inversion HLe0 |]; simpl in Hp.
      unfold lt in HLe0; rewrite HLe0.
      rewrite <- HSub; apply HTL, Hp; [reflexivity | assumption].
    Qed.

    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.
101
      do 14 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
Ralf Jung's avatar
Ralf Jung committed
102 103 104
      apply ı in HInv; rewrite (isoR p) in HInv.
      (* get rid of the invisible 1/2 *)
      do 8 red in HInv.
Ralf Jung's avatar
Ralf Jung committed
105
      destruct HE as [rs [HE HM] ].
Ralf Jung's avatar
Ralf Jung committed
106
      destruct (rs i) as [ri |] eqn: HLr.
107
      - rewrite comp_map_remove with (i := i) (r := ri) in HE by assumption.
Ralf Jung's avatar
Ralf Jung committed
108
        rewrite assoc, <- (assoc (Some r)), (comm rf), assoc in HE.
Ralf Jung's avatar
Ralf Jung committed
109
        destruct (Some r · Some ri) as [rri |] eqn: HR;
Ralf Jung's avatar
Ralf Jung committed
110 111 112
          [| erewrite !pcm_op_zero in HE by apply _; now contradiction].
        exists w' rri; split; [reflexivity |].
        split.
Ralf Jung's avatar
Ralf Jung committed
113 114 115 116 117 118 119
        + simpl; eapply HInv; [now auto with arith |].
          eapply uni_pred, HM with i;
            [| exists r; rewrite <- HR | | | rewrite HLr]; try reflexivity; [|].
          * left; unfold mask_sing, mask_set.
            destruct (Peano_dec.eq_nat_dec i i); tauto.
          * specialize (HSub i); rewrite HLu in HSub.
            symmetry; destruct (w' i); [assumption | contradiction].
Ralf Jung's avatar
Ralf Jung committed
120
        + exists (fdRemove i rs); split; [assumption | intros j Hm].
Ralf Jung's avatar
Ralf Jung committed
121
          destruct Hm as [| Hm]; [contradiction |]; specialize (HD j); simpl in HD.
122
          unfold mask_sing, mask_set, mcup in HD; destruct (Peano_dec.eq_nat_dec i j);
Ralf Jung's avatar
Ralf Jung committed
123
          [subst j; contradiction HD; tauto | clear HD].
124
          rewrite fdLookup_in; setoid_rewrite (fdRemove_neq _ _ _ n0); rewrite <- fdLookup_in; unfold mcup in HM; now auto.
Ralf Jung's avatar
Ralf Jung committed
125 126 127 128 129 130 131 132 133 134 135 136
      - 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.

    Lemma vsClose i p :
      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.
137
      do 14 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
Ralf Jung's avatar
Ralf Jung committed
138 139 140
      apply ı in HInv; rewrite (isoR p) in HInv.
      (* get rid of the invisible 1/2 *)
      do 8 red in HInv.
Ralf Jung's avatar
Ralf Jung committed
141 142 143
      destruct HE as [rs [HE HM] ].
      exists w' (pcm_unit _); split; [reflexivity | split; [exact I |] ].
      rewrite (comm (Some r)), <-assoc in HE.
Ralf Jung's avatar
Ralf Jung committed
144 145 146
      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].
Ralf Jung's avatar
Ralf Jung committed
147 148 149 150 151
        + erewrite pcm_op_unit by apply _.
          clear - HE EQR EQri. destruct (rs i) as [rsi |] eqn: EQrsi; subst.
          * erewrite <-comp_map_insert_old; try eassumption. rewrite<- EQR; reflexivity.
          * erewrite <-comp_map_insert_new; try eassumption. rewrite <-EQR.
            erewrite pcm_op_unit by apply _. assumption.
152
        + specialize (HD j); unfold mask_sing, mask_set, mcup in *; simpl in Hm, HD.
Ralf Jung's avatar
Ralf Jung committed
153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
          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
171 172 173
        clear - HE EQrsi EQR.
        assert (HH : rf · (Some r · comp_map rs) = 0); [clear HE | rewrite HH in HE; contradiction].
        eapply ores_equiv_eq; rewrite comp_map_remove by eassumption.
Ralf Jung's avatar
Ralf Jung committed
174 175 176 177 178 179 180 181 182
        rewrite (assoc (Some r)), (comm (Some r)), EQR, comm.
        erewrite !pcm_op_zero by apply _; reflexivity.
    Qed.

    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).
Ralf Jung's avatar
Ralf Jung committed
183
      edestruct Hpq as [w2 [rq [HSw12 [Hq HEq] ] ] ]; try eassumption; [|].
Ralf Jung's avatar
Ralf Jung committed
184 185 186 187 188
      { clear - HD HMS; intros j [Hmf Hm12]; apply (HD j); split; [assumption |].
        destruct Hm12 as [Hm1 | Hm2]; [left; assumption | apply HMS, Hm2].
      }
      clear HS; assert (HS : pcm_unit _  rq) by (exists rq; now erewrite comm, pcm_op_unit by apply _).
      rewrite <- HLe, HSub in Hqr; specialize (Hqr _ HSw12); clear Hpq HE w HSub Hp.
Ralf Jung's avatar
Ralf Jung committed
189
      edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [HSw23 [Hr HEr] ] ] ];
Ralf Jung's avatar
Ralf Jung committed
190 191 192 193 194 195 196 197 198 199 200 201 202
        try (reflexivity || eassumption); [now auto with arith | |].
      { clear - HD HMS; intros j [Hmf Hm23]; apply (HD j); split; [assumption |].
        destruct Hm23 as [Hm2 | Hm3]; [apply HMS, Hm2 | right; assumption].
      }
      clear HEq Hq HS.
      setoid_rewrite HSw12; eauto 8.
    Qed.

    Lemma vsEnt p q m :
       (p  q)  vs m m p q.
    Proof.
      intros w' n r1 Himp w HSub; rewrite HSub in Himp; clear w' HSub.
      intros np rp HLe HS Hp w1; intros.
Ralf Jung's avatar
Ralf Jung committed
203
      exists w1 rp; split; [reflexivity | split; [| assumption ] ].
Ralf Jung's avatar
Ralf Jung committed
204 205 206 207 208 209 210 211 212 213
      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.

    Lemma vsFrame p q r m1 m2 mf (HDisj : mf # m1  m2) :
      vs m1 m2 p q  vs (m1  mf) (m2  mf) (p * r) (q * r).
    Proof.
      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.
      assert (HS : pcm_unit _  rp) by (exists rp; now erewrite comm, pcm_op_unit by apply _).
Ralf Jung's avatar
Ralf Jung committed
214 215
      specialize (HVS _ _ HLe HS Hp w' (Some rr · rf) (mf  mf0) σ k); clear HS.
      destruct HVS as [w'' [rq [HSub' [Hq HEq] ] ] ]; try assumption; [| |].
Ralf Jung's avatar
Ralf Jung committed
216 217
      - (* disjointness of masks: possible lemma *)
        clear - HD HDisj; intros i [ [Hmf | Hmf] Hm12]; [eapply HDisj; now eauto |].
218
        unfold mcup in *; eapply HD; split; [eassumption | tauto].
219
      - rewrite assoc, HR; eapply wsat_equiv, HE; try reflexivity; [].
220
        clear; intros i; unfold mcup; tauto.
Ralf Jung's avatar
Ralf Jung committed
221
      - rewrite assoc in HEq; destruct (Some rq · Some rr) as [rqr |] eqn: HR';
222
        [| apply wsat_not_empty in HEq; [contradiction | now erewrite !pcm_op_zero by apply _] ].
Ralf Jung's avatar
Ralf Jung committed
223
        exists w'' rqr; split; [assumption | split].
Ralf Jung's avatar
Ralf Jung committed
224 225
        + unfold lt in HLe0; rewrite HSub, HSub', <- HLe0 in Hr; exists rq rr.
          rewrite HR'; split; now auto.
226
        + eapply wsat_equiv, HEq; try reflexivity; [].
227
          clear; intros i; unfold mcup; tauto.
Ralf Jung's avatar
Ralf Jung committed
228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244
    Qed.

    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.

245 246 247 248 249 250 251 252 253 254
    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.
Ralf Jung's avatar
Ralf Jung committed
255 256 257 258 259 260 261

    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].
Ralf Jung's avatar
Ralf Jung committed
262
      destruct HE as [rs HE].
Ralf Jung's avatar
Ralf Jung committed
263 264
      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'.
Ralf Jung's avatar
Ralf Jung committed
265
      destruct (Some (rdp, rl') · rf · comp_map rs) as [t |] eqn: EQt;
Ralf Jung's avatar
Ralf Jung committed
266
        [| destruct HE as [HES _]; setoid_rewrite EQt in HES; contradiction].
Ralf Jung's avatar
Ralf Jung committed
267
      assert (EQt' : Some (rdp, rl') · rf · comp_map rs == Some t) by (rewrite EQt; reflexivity).
Ralf Jung's avatar
Ralf Jung committed
268 269
      clear EQt; rename EQt' into EQt.
      destruct rf as [ [rfp rfl] |]; [| now erewrite (comm _ 0), !pcm_op_zero in EQt by apply _].
Ralf Jung's avatar
Ralf Jung committed
270
      destruct (comp_map rs) as [ [sp sl] |] eqn:EQrs; [| now erewrite (comm _ 0), pcm_op_zero in EQt by apply _].
Ralf Jung's avatar
Ralf Jung committed
271 272 273 274 275 276 277 278 279
      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 _ ].
Ralf Jung's avatar
Ralf Jung committed
280
        exists w' (rdp, rsl'); split; [reflexivity | split].
Ralf Jung's avatar
Ralf Jung committed
281 282 283 284
        + 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].
Ralf Jung's avatar
Ralf Jung committed
285
        + destruct HE as [HES HEL]. exists rs. split; [| assumption]; clear HEL.
Ralf Jung's avatar
Ralf Jung committed
286 287
          assert (HT := ores_equiv_eq _ _ _ EQt); setoid_rewrite EQdf in HES;
          setoid_rewrite HT in HES; clear HT; destruct t as [tp tl].
Ralf Jung's avatar
Ralf Jung committed
288
          rewrite EQrs; clear rs EQrs.
Ralf Jung's avatar
Ralf Jung committed
289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347
          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 *)

    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; destruct n as [| n]; [apply dist_bound |].
      simpl in EQi; rewrite EQi; reflexivity.
    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.
      }
Ralf Jung's avatar
Ralf Jung committed
348
      exists (fdUpdate i (ı' p) w) (pcm_unit _); split; [assumption | split].
349
      - exists (exist _ i Hm); do 22 red.
Ralf Jung's avatar
Ralf Jung committed
350 351
        unfold proj1_sig; rewrite fdUpdate_eq; reflexivity.
      - erewrite pcm_op_unit by apply _.
Ralf Jung's avatar
Ralf Jung committed
352 353
        destruct HE as [rs [HE HM] ].
        exists (fdUpdate i r rs).
Ralf Jung's avatar
Ralf Jung committed
354
        assert (HRi : rs i = None).
355
        { destruct (HM i) as [HDom _]; unfold mcup; [tauto |].
Ralf Jung's avatar
Ralf Jung committed
356 357
          rewrite <- fdLookup_notin_strong, HDom, fdLookup_notin_strong; assumption.
        }
Ralf Jung's avatar
Ralf Jung committed
358 359 360 361 362 363
        split.
        {
          rewrite <-comp_map_insert_new by assumption.
          rewrite assoc, (comm rf). assumption.
        }
        intros j Hm'.
Ralf Jung's avatar
Ralf Jung committed
364 365 366 367 368 369 370 371 372 373 374 375
        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.

  End ViewShiftProps.

End IrisVS.