Finmap.v 45 KB
Newer Older
1 2
Require Import Ssreflect.ssreflect Omega.
Require Import Arith Min Max List ListSet Lists.
3 4
Require Import MetricCore.
Require Import PreoMet.
5
Require Import RA CMRA SPred.
6

Janno's avatar
Janno committed
7 8
Set Bullet Behavior "Strict Subproofs".

9

Ralf Jung's avatar
Ralf Jung committed
10 11 12 13
Delimit Scope finmap_scope with fm.
Local Open Scope finmap_scope.
Local Open Scope general_if_scope.
Infix "∈" := In (at level 31, no associativity) : finmap_scope.
14

Janno's avatar
Janno committed
15 16


Ralf Jung's avatar
Ralf Jung committed
17 18
Section Def.
  Context {K V : Type}.
19

Ralf Jung's avatar
Ralf Jung committed
20 21 22 23
  Definition findom_bound (finmap: K -> option V) (findom: list K): Prop :=
    forall k, finmap k <> None -> k  findom.
  Definition findom_approx (finmap: K -> option V) (findom: list K): Prop :=
    forall k, finmap k <> None <-> k  findom.
24

Ralf Jung's avatar
Ralf Jung committed
25 26 27 28
  Record FinMap `{eqK : DecEq K} :=
    mkFD {finmap :> K -> option V;
          findom : list K;
          findom_b : findom_approx finmap findom}.
29

Ralf Jung's avatar
Ralf Jung committed
30
  Context `{eqK : DecEq K}.
31

Janno's avatar
Janno committed
32
  Definition dom (f: FinMap) := filter_dupes ([]%list) (findom f).
33

Ralf Jung's avatar
Ralf Jung committed
34
  Lemma dom_nodup (f: FinMap): NoDup (dom f).
35
  Proof.
Ralf Jung's avatar
Ralf Jung committed
36
    unfold dom. apply filter_dupes_nodup.
37 38
  Qed.

Ralf Jung's avatar
Ralf Jung committed
39 40 41 42 43 44 45 46
  Fixpoint filter_None (f: K -> option V) (l: list K) :=
    match l with
    | [] => []
    | k::l => match f k with
              | Some _ => k::(filter_None f l)
              | None   => filter_None f l
              end
    end.
47

Ralf Jung's avatar
Ralf Jung committed
48 49
  Lemma filter_None_isin f l k:
    k  filter_None f l -> f k <> None.
50
  Proof.
Ralf Jung's avatar
Ralf Jung committed
51 52 53 54 55 56 57
    induction l.
    - intros [].
    - simpl. destruct (f a) eqn:EQf.
      + move=>[EQ|Hin].
        * subst a. rewrite EQf. discriminate.
        * apply IHl. exact Hin.
      + exact IHl.
58 59
  Qed.

Ralf Jung's avatar
Ralf Jung committed
60 61
  Lemma filter_None_in f l k:
    f k <> None -> k  l -> k  filter_None f l.
62
  Proof.
Ralf Jung's avatar
Ralf Jung committed
63 64 65 66 67 68
    induction l.
    - move=>_ [].
    - move=>Hneq [EQ|Hin].
      + subst a. simpl. destruct (f k); last (exfalso; now apply Hneq).
        left. reflexivity.
      + simpl. destruct (f a); first right; apply IHl; assumption.
69 70
  Qed.

Ralf Jung's avatar
Ralf Jung committed
71 72 73 74 75 76 77 78
  Program Definition mkFDbound (f: K -> option V) (l: list K)
          (Hbound: findom_bound f l) :=
    mkFD _ f (filter_None f l) _.
  Next Obligation.
    move=>k. split.
    - move=>Hnon. apply filter_None_in; first assumption.
      apply Hbound. assumption.
    - move/filter_None_isin. tauto.
79 80 81 82
  Qed.

End Def.

Ralf Jung's avatar
Ralf Jung committed
83 84 85 86 87 88 89
Arguments mkFD [K V] {eqK} _ _ _.
Arguments FinMap K V {_} : clear implicits.
Arguments finmap [K V] {eqK} _ _.
Arguments findom [K V] {eqK} _.
Arguments dom [K V] {eqK} _.
Arguments findom_b [K V] {eqK} _ {k}.
Notation "K '-f>' V" := (FinMap K V) (at level 45).
Janno's avatar
Janno committed
90 91
(* TODO: find out what this does if anything *)
Bind Scope finmap_scope with FinMap.
92 93

Section FinDom.
Ralf Jung's avatar
Ralf Jung committed
94
  Context {K} `{eqK : DecEq K}.
95 96 97 98

  Section Props.
    Context {V : Type} `{ev : Setoid V}.

Ralf Jung's avatar
Ralf Jung committed
99 100 101
    Program Definition fdEmpty : K -f> V := mkFD (fun _ => None) nil _.
    Next Obligation.
      move=>k /=. split; last tauto. move=>H. now apply H.
102 103
    Qed.

Ralf Jung's avatar
Ralf Jung committed
104
    Lemma fdLookup_notin_strong k (f : K -f> V) : (~ (k  dom f)) <-> f k = None.
105
    Proof.
Ralf Jung's avatar
Ralf Jung committed
106 107 108 109 110
      destruct f as [f fd fdb]; unfold dom in *; simpl in *. split.
      - destruct (f k) as [v|] eqn:EQf; last (move=>_; reflexivity).
        move=>Hin. exfalso. apply Hin=>{Hin}. apply filter_dupes_in; first tauto.
        apply fdb. rewrite EQf. discriminate.
      - move=>EQf Hin. apply filter_dupes_isin in Hin. eapply fdb; last eassumption. tauto.
111 112 113 114 115 116
    Qed.

    Lemma fdLookup_notin k (f : K -f> V) : (~ (k  dom f)) <-> f k == None.
    Proof.
      split ; intro H.
      + apply fdLookup_notin_strong in H ; rewrite H ; reflexivity.
Ralf Jung's avatar
Ralf Jung committed
117 118
      + destruct (f k) as [v|] eqn:EQf; first (contradiction H).
        apply fdLookup_notin_strong. assumption.
119 120
    Qed.
    
Ralf Jung's avatar
Ralf Jung committed
121
    Lemma fdLookup_in_strong (f : K -f> V) k: k  dom f <-> f k <> None.
122
    Proof.
Ralf Jung's avatar
Ralf Jung committed
123 124 125 126 127
      destruct f as [f fd fdb]; unfold dom; simpl. split.
      - move=>Hin. apply filter_dupes_isin in Hin.
        destruct (f k) as [v|] eqn:EQf; first discriminate. exfalso.
        eapply fdb; last eassumption. tauto.
      - move=>EQf. apply filter_dupes_in; first tauto. apply fdb. assumption.
128 129
    Qed.

Ralf Jung's avatar
Ralf Jung committed
130
    Lemma fdLookup_in : forall (f : K -f> V) k, k  dom f <-> f k =/= None.
131
    Proof.
Ralf Jung's avatar
Ralf Jung committed
132 133 134 135 136 137 138 139 140 141 142 143
      simpl. split.
      - move=>Hin. eapply fdLookup_in_strong in Hin. move=>Heq.
        apply Hin. destruct (f k); contradiction || reflexivity.
      - move=>Hneq. apply fdLookup_in_strong. destruct (f k); first discriminate.
        exfalso. now apply Hneq. 
    Qed.

    Program Definition fdLookup_indom f k (Hindom: k  dom f): V :=
      match f k with
      | Some v => v
      | None => !
      end.
144
    Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
145
      apply fdLookup_in_strong in Hindom. rewrite Heq_anonymous in Hindom. apply Hindom. reflexivity.
146 147
    Qed.

Ralf Jung's avatar
Ralf Jung committed
148 149
    Lemma fdLookup_indom_corr f k (Hindom: k  dom f) v:
      fdLookup_indom f k Hindom = v <-> f k = Some v.
150
    Proof.
Ralf Jung's avatar
Ralf Jung committed
151 152 153 154 155 156 157
      split.
      - rewrite /fdLookup_indom. ddes (f k) at 1 3 as [v'|] deqn:EQf.
        + move=><-. now symmetry.
        + unfold False_rect. destruct (_:False).
      - rewrite /fdLookup_indom. ddes (f k) at 1 3 4 as [v'|] deqn:EQf.
        + by move=>[EQ].
        + move=>?. discriminate.
158
    Qed.
159

160 161 162 163 164 165 166 167
    Lemma fdLookup_indom_pi f k (Hindom1: k  dom f) (Hindom2: k  dom f):
      fdLookup_indom f k Hindom1 = fdLookup_indom f k Hindom2.
    Proof.
      rewrite /fdLookup_indom. ddes (f k) at 1 3 7 as [v|] deqn:EQf.
      - reflexivity.
      - exfalso. apply fdLookup_in_strong in Hindom1. apply Hindom1. now rewrite -EQf.
    Qed.

168 169 170
  End Props.

  Section Instances.
171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
    Context {V: Type}.

    Definition equal_fd (f1 f2 : K -f> V):Prop :=
      (forall k, f1 k = f2 k) /\ dom f1 = dom f2.

    Global Instance equal_fd_e: Equivalence equal_fd.
    Proof.
      split.
      - intros m. split; intros; reflexivity.
      - intros m1 m2 [Hf Hdom]. split; intros; symmetry; now auto.
      - intros m1 m2 m3 [Hf12 Hdom12] [Hf23 Hdom23]. split; intros; etransitivity; now eauto.
    Qed.

    Global Instance equal_fd_lookup:
      Proper (equal_fd ==> eq ==> eq) (finmap (eqK:=eqK)).
    Proof.
      move=>f1 f2 EQf k1 k2 EQk. subst k1. apply EQf.
    Qed.

    Global Instance equal_fd_dom:
      Proper (equal_fd ==> eq) (dom (eqK:=eqK)).
    Proof.
      move=>f1 f2 EQf. apply EQf.
    Qed.

    Context `{cV : pcmType V}.
197 198

    Definition equiv_fd (f1 f2 : K -f> V) := forall k, f1 k == f2 k.
199 200 201

    Global Instance equiv_fd_e: Equivalence equiv_fd.
    Proof.
202 203 204 205 206
      split.
      - intros m k; reflexivity.
      - intros m1 m2 HS k; symmetry; apply HS.
      - intros m1 m2 m3 H12 H23 k; etransitivity; [apply H12 | apply H23].
    Qed.
207
    
208
    Global Program Instance type_findom : Setoid (K -f> V) := mkType equiv_fd.
209

Ralf Jung's avatar
Ralf Jung committed
210
    Global Instance fdLookup_proper : Proper (equiv ==> eq ==> equiv) (finmap (V := V)).
211 212 213 214
    Proof.
      intros f1 f2 HEqf k1 k2 HEqk; subst; apply HEqf.
    Qed.

Ralf Jung's avatar
Ralf Jung committed
215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232
    Lemma dom_proper {f1 f2}:
      f1 == f2 -> (forall k, k  dom f1 <-> k  dom f2).
    Proof.
      move=>EQf k. split; rewrite !fdLookup_in; move=>Hin.
      - now rewrite -EQf.
      - now rewrite EQf.
    Qed.
    
    Lemma fdEmpty_dom f:
      f == fdEmpty <-> (forall k, ~k  dom f).
    Proof.
      split.
      - move=>Hemp k Hin. apply (dom_proper Hemp) in Hin. exact Hin.
      - move=>Hemp k. destruct (f k) as [v|] eqn:EQf.
        + exfalso. apply (Hemp k). apply fdLookup_in_strong. rewrite EQf. discriminate.
        + reflexivity.
    Qed.

233
    Definition dist_fd n (f1 f2 : K -f> V) :=
Ralf Jung's avatar
Ralf Jung committed
234
      forall k, f1 k = n = f2 k.
235

236
    Global Program Instance metric_findom : metric (K -f> V) := mkMetr dist_fd.
237
    Next Obligation.
238
      intros f1 f2 EQf g1 g2 EQg; split;
David Swasey's avatar
David Swasey committed
239
      intros EQ k; [symmetry in EQf, EQg |]; rewrite -> EQf, EQg; apply EQ.
240 241 242
    Qed.
    Next Obligation.
      split; intros HEq.
243
      - intros k; rewrite <- dist_refl; intros n. apply (HEq n k).
Ralf Jung's avatar
Ralf Jung committed
244
      - intros n; intros k. apply dist_refl. apply HEq.
245 246
    Qed.
    Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
247
      revert n; intros n x y HS; intros k; symmetry; apply HS.
248 249
    Qed.
    Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
250
      revert n; intros n x y z Hxy Hyz; intros k; etransitivity; [apply Hxy | apply Hyz].
251 252
    Qed.
    Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
253 254 255 256
      intros k; eapply dist_mono, H.
    Qed.
    Next Obligation.
      move=>k. apply dist_bound.
257
    Qed.
Janno's avatar
Janno committed
258
    
Ralf Jung's avatar
Ralf Jung committed
259
    Global Instance lookup_dist n : Proper (dist n ==> eq ==> dist n) (finmap (V := V)).
Janno's avatar
Janno committed
260 261 262 263 264
    Proof.
      intros f1 f2 HEqf k1 k2 HEqk; subst. 
      destruct n; first now auto.
      now apply HEqf.
    Qed.
265

Ralf Jung's avatar
Ralf Jung committed
266 267
    Definition finmap_chainx (σ : chain (K -f> V)) {σc : cchain σ} x : chain (option V) :=
      fun n => (σ n) x.
268

Ralf Jung's avatar
Ralf Jung committed
269 270 271 272 273
    Program Instance finmap_chainx_cauchy (σ : chain (K -f> V)) {σc : cchain σ} x :
      cchain (finmap_chainx σ x).
    Next Obligation.
      assert (σc':=σc).
      specialize (σc' n i j HLei HLej x). unfold finmap_chainx. assumption.
274
    Qed.
Janno's avatar
Janno committed
275
    
Ralf Jung's avatar
Ralf Jung committed
276 277
    Program Definition findom_lub (σ : chain (K -f> V)) (σc : cchain σ) : K -f> V :=
      mkFDbound (fun x => compl (finmap_chainx σ x)) (findom (σ 1)) _.
Janno's avatar
Janno committed
278
    Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
279 280 281 282 283 284 285
      move=>k /= Hin.
      assert(H:=conv_cauchy (finmap_chainx σ k) 1 1 (le_refl _)).
      simpl in Hin. assert (Hin': (finmap_chainx σ k) 1 <> None).
      { move=>EQ. rewrite EQ in H. apply Hin. symmetry in H. simpl in H.
        destruct (option_compl (finmap_chainx σ k)); first contradiction.
        reflexivity. }
      clear Hin. apply (findom_b (σ 1)). assumption.
286 287
    Qed.

288
    Global Program Instance findom_cmetric : cmetric (K -f> V) := mkCMetr findom_lub.
289
    Next Obligation.
290
      move => n i LEi k. unfold findom_lub. simpl finmap.
Ralf Jung's avatar
Ralf Jung committed
291
      assert (H := conv_cauchy (finmap_chainx σ k) _ _ LEi). exact H.
292 293 294 295 296 297 298
    Qed.

    Local Existing Instance option_preo_bot.
    Local Existing Instance option_pcm_bot.

    Definition extOrd (m1 m2 : K -f> V) := forall k, m1 k  m2 k.

David Swasey's avatar
David Swasey committed
299
    Global Program Instance extOrd_preo : preoType (K -f> V) := mkPOType extOrd _.
300 301 302 303 304
    Next Obligation.
      split.
      - intros m k; reflexivity.
      - intros m1 m2 m3 S12 S23 k; etransitivity; [apply (S12 k) | apply (S23 k) ].
    Qed.
David Swasey's avatar
David Swasey committed
305 306 307 308
    Next Obligation.
      move=> f1 f2 Rf g1 g2 Rg H k.
      by rewrite -(Rf k) -(Rg k).
    Qed.
309 310 311 312

    Global Instance findom_pcmType : pcmType (K -f> V).
    Proof.
      split.
Ralf Jung's avatar
Ralf Jung committed
313
      - intros σ ρ σc ρc HSub k.
314
        eapply pcm_respC; [now auto with typeclass_instances | intros].
Ralf Jung's avatar
Ralf Jung committed
315
        apply: HSub.
316 317 318 319
    Qed.

    Lemma dom_ext (m1 m2 : K -f> V) k (HSub : m1  m2) (HIn : k  dom m1) : k  dom m2.
    Proof.
Ralf Jung's avatar
Ralf Jung committed
320 321 322 323 324
      specialize (HSub k).
      apply fdLookup_in in HIn.
      apply fdLookup_in. destruct (m2 k) as [v'|].
      - move=>[].
      - exfalso. apply HIn. destruct (m1 k); contradiction || reflexivity.
325 326 327 328
    Qed.

  End Instances.

329 330 331 332 333 334 335 336 337
  Section Update.
    Context {V: Type} `{eqV: Setoid V}.
    
    (* The definition of the domain here is carefully tuned to make the recursion principle
       less painful. *)
    Definition fdStrongUpdate_dom k (v: option V) (f: K -f> V) :=
      match v with
      | Some _ => k::(dom f)
      | None => match (dom f) with [] => []
Janno's avatar
Janno committed
338
                          | k'::dom' => if dec_eq k k' then dom' else filter_dupes ([k]%list) (dom f) end
339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358
      end.
    Program Definition fdStrongUpdate k v (f : K -f> V) : K -f> V :=
      mkFD (fun k' => if dec_eq k k' then v else f k')
           (fdStrongUpdate_dom k v f)
           _.
    Next Obligation.
      move=>k'. simpl. unfold fdStrongUpdate_dom. destruct v as [v|]; destruct (dec_eq k k') as [EQ|NEQ]; split; intros Hin.
      - left. assumption.
      - discriminate.
      - right. apply fdLookup_in_strong. assumption.
      - apply fdLookup_in_strong. destruct Hin as [EQ|?]; last assumption. contradiction.
      - exfalso. now apply Hin.
      - exfalso. subst k'. destruct (dom f) as [|k' d] eqn:EQdf; first contradiction.
        destruct (dec_eq k k') as [EQ|NEQ].
        + subst k'. assert (Hndup := dom_nodup f). rewrite EQdf in Hndup. inversion Hndup; subst. contradiction.
        + eapply filter_dupes_notin, Hin. left. reflexivity.
      - apply fdLookup_in_strong in Hin. destruct (dom f) as [|k'' dom'] eqn:Hdom; first assumption.
        destruct (dec_eq k k'') as [EQ'|NEQ'].
        + subst k''. destruct Hin as [?|?]; first contradiction. assumption.
        + unfold dom in Hdom. rewrite -Hdom in Hin.
359
          rewrite Hdom in Hin. apply filter_dupes_in.
360
          * move=>[EQk|[]]. contradiction.
361
          * assumption.
362 363 364
      - apply fdLookup_in_strong. destruct (dom f) as [|k'' dom'] eqn:Hdom; first assumption.
        destruct (dec_eq k k'') as [EQ'|NEQ'].
        + subst k''. right. assumption.
365
        + apply filter_dupes_isin in Hin. tauto.
366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390
    Qed.
      
    Lemma fdStrongUpdate_eq k v f : fdStrongUpdate k v f k = v.
    Proof.
      simpl finmap. rewrite DecEq_refl. reflexivity.
    Qed.

    Lemma fdStrongUpdate_neq k k' v f (Hneq : k <> k') : fdStrongUpdate k v f k' = f k'.
    Proof.
      simpl finmap. destruct (dec_eq k k') as [EQ|NEQ]; first contradiction. reflexivity.
    Qed.

    Lemma fdStrongUpdateShadow k v1 v2 f:
      fdStrongUpdate k v1 (fdStrongUpdate k v2 f) == fdStrongUpdate k v1 f.
    Proof.
      move=>i. simpl. destruct (dec_eq k i); reflexivity.
    Qed.

    Lemma fdStrongUpdateCommute k1 v1 k2 v2 f:
      k1 <> k2 -> fdStrongUpdate k1 v1 (fdStrongUpdate k2 v2 f) == fdStrongUpdate k2 v2 (fdStrongUpdate k1 v1 f).
    Proof.
      move=>Hineq i. simpl. destruct (dec_eq k1 i) as [EQ1|NEQ1], (dec_eq k2 i) as [EQ2|NEQ2]; try reflexivity; [].
      subst. exfalso. now apply Hineq.
    Qed.

391 392 393 394 395 396 397 398
    Global Instance fdStrongUpdate_equal k v:
      Proper (equal_fd ==> equal_fd) (fdStrongUpdate k v).
    Proof.
      move=>f1 f2 [Hf Hdom]. split.
      - move=>k'. simpl. rewrite Hf. reflexivity.
      - rewrite /fdStrongUpdate /dom /= /fdStrongUpdate_dom. rewrite Hdom. reflexivity.
    Qed.

399 400 401
  End Update.


402
  Section Map.
Ralf Jung's avatar
Ralf Jung committed
403
    Context {U V} `{pcmU : pcmType U} `{cmV : pcmType V}.
404

Ralf Jung's avatar
Ralf Jung committed
405 406
    Definition fdMap_pre (m : U -> V) (f: K -f> U) : K -> option V :=
      fun k => match (f k) with None => None | Some v => Some (m v) end.
407

Ralf Jung's avatar
Ralf Jung committed
408 409
    (* The nicest solution here would be to have a map on option... *)
    Program Definition fdMapRaw (m : U -> V) : (K -f> U) -> (K -f> V) :=
410
      fun f => mkFD (fdMap_pre m f) (findom f) _.
Ralf Jung's avatar
Ralf Jung committed
411
    Next Obligation.
412 413 414
      unfold fdMap_pre, findom_approx. move=>k. rewrite -(findom_b f).
      destruct (f k); last tauto.
      split; discriminate.
415
    Qed.
Ralf Jung's avatar
Ralf Jung committed
416 417 418 419 420 421 422 423
    
    Program Definition fdMapMorph (m : U -n> V) : (K -f> U) -n> (K -f> V) :=
      n[(fdMapRaw m)].
    Next Obligation.
      unfold fdMapRaw, fdMap_pre.
      intros m1 m2 HEq; destruct n as [| n]; [apply dist_bound |]; intros k; simpl; specialize (HEq k).
      destruct (m1 k) as [u1 |] eqn: HFnd1; destruct (m2 k) as [u2 |] eqn: HFnd2; try contradiction HEq; [|exact I].
      apply met_morph_nonexp. exact HEq.
424 425
    Qed.

Ralf Jung's avatar
Ralf Jung committed
426 427
    Program Definition fdMap (m : U -m> V) : (K -f> U) -m> (K -f> V) :=
      m[(fdMapMorph m)].
428
    Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
429 430 431
      move=>f1 f2 EQf k.
      change (fdMapMorph m f1 k = n = fdMapMorph m f2 k).
      now apply (met_morph_nonexp (fdMapMorph m)).
432 433
    Qed.
    Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
434 435 436 437
      unfold fdMapRaw, fdMap_pre. intros m1 m2 Subm k; specialize (Subm k); destruct (m1 k) as [u1 |] eqn: HFnd1.
      - rewrite /= HFnd1 /=. destruct (m2 k) as [u2 |] eqn: HFnd2; [| contradiction Subm].
        apply mu_mono, Subm.
      - rewrite /= HFnd1 /=. destruct (m2 k); exact I.
438 439 440 441
    Qed.

    Global Instance fdMap_resp : Proper (equiv ==> equiv) fdMap.
    Proof.
Ralf Jung's avatar
Ralf Jung committed
442 443 444
      intros f1 f2 EQf m k; rewrite /opt_eq /fdMap /= /fdMap_pre. destruct (m k).
      - apply EQf.
      - reflexivity.
445 446 447 448
    Qed.

    Global Instance fdMap_nonexp n : Proper (dist n ==> dist n) fdMap.
    Proof.
Ralf Jung's avatar
Ralf Jung committed
449 450 451 452
      intros f1 f2 EQf m k. destruct n as [|n]; first exact: dist_bound.
      rewrite /opt_eq /fdMap /= /fdMap_pre. destruct (m k).
      - apply EQf.
      - reflexivity.
453 454 455 456
    Qed.

    Global Instance fdMap_monic : Proper (pord ==> pord) fdMap.
    Proof.
Ralf Jung's avatar
Ralf Jung committed
457 458 459
      intros f1 f2 EQf m k; rewrite /opt_eq /fdMap /= /fdMap_pre. destruct (m k) as [u |] eqn: HFnd.
      - simpl. apply EQf.
      - reflexivity.
460 461
    Qed.

Ralf Jung's avatar
Ralf Jung committed
462 463
  End Map.

Janno's avatar
Janno committed
464 465 466 467 468 469 470 471
End FinDom.

Notation "f + '[fd' k <- v ']'" := (fdStrongUpdate k (Some v) f) (at level 0) : finmap_scope.
Notation "f \ x" := (fdStrongUpdate x None f) (at level 35) : finmap_scope.

Section FinDom2.
  
  Context {K} `{eqK : DecEq K}.
Ralf Jung's avatar
Ralf Jung committed
472 473 474 475 476 477 478

  Section MapProps.

    Context U V W `{pcmU : pcmType U} `{cmV : pcmType V} `{cmW : pcmType W}.

    Lemma fdMap_comp (f : U -m> V) (g : V -m> W) :
      (fdMap g  fdMap f == fdMap (g  f))%pm.
479
    Proof.
Ralf Jung's avatar
Ralf Jung committed
480 481
      intros m k. rewrite /= /fdMap /fdMapRaw /fdMap_pre /=.
      destruct (m k); reflexivity.
482 483
    Qed.

Ralf Jung's avatar
Ralf Jung committed
484
    Lemma fdMap_id : fdMap (pid U) == (pid (K -f> U)).
485
    Proof.
Ralf Jung's avatar
Ralf Jung committed
486 487 488 489
      intros w k; rewrite /= /fdMap /fdMap_pre /=.
      destruct (w k); reflexivity.
    Qed.
  End MapProps.
490

Ralf Jung's avatar
Ralf Jung committed
491 492
    
(*  Section Filter.
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
    Context V `{cmV : cmetric V}.

    Lemma filter_split A (p : A -> bool) x xs ys (HEq : x :: xs = filter p ys) :
      exists ysf, exists yst, ys = ysf ++ x :: yst /\ xs = filter p yst /\ filter p ysf = nil.
    Proof.
      induction ys; simpl in *; [discriminate |].
      destruct (p a) eqn: PA; [inversion HEq; subst | specialize (IHys HEq) ].
      + eexists nil; exists ys; tauto.
      + destruct IHys as [ysf [yst [EQ1 [EQ2 EQ3]]]]; exists (a :: ysf); exists yst.
        simpl; subst; rewrite PA; tauto.
    Qed.

    Lemma SS_app xs ys (HSS : StrictSorted (xs ++ ys)) :
      StrictSorted xs /\ StrictSorted ys.
    Proof.
      induction xs; simpl in *; [split; [apply SS_nil | assumption] |].
      assert (HSS' : StrictSorted xs /\ StrictSorted ys) by (eapply IHxs, SS_tail, HSS).
      clear IHxs; destruct HSS' as [HSSxs HSSys]; split; [| assumption]; clear HSSys.
      destruct xs; [apply SS_sing | apply SS_cons; [assumption |]].
      inversion HSS; subst; assumption.
    Qed.

    Program Definition fdFilter (p : V -> bool) (m : K -f> V) : K -f> V :=
      mkFD (filter (fun a : K * V => p (snd a)) (findom_t m)) _.
    Next Obligation.
      destruct m as [ms mP]; unfold findom_f in *; simpl in *.
      remember (filter (fun a => p (snd a)) ms) as ns.
      generalize dependent ms; induction ns; intros; [apply SS_nil |].
      apply filter_split in Heqns; destruct Heqns as [msf [mst [EQ1 [EQ2 _]]]]; subst.
      rewrite map_app in mP; apply SS_app in mP; destruct mP as [_ mP].
      specialize (IHns mst (SS_tail _ _ mP) (eq_refl _)).
      remember (filter (fun a => p (snd a)) mst) as ns; destruct ns; [apply SS_sing |].
      apply SS_cons; [assumption |]; clear IHns.
      apply filter_split in Heqns; destruct Heqns as [nsf [nst [EQ1 [EQ2 EQ3]]]]; subst.
      clear - mP compK; induction nsf; [simpl; inversion mP; subst; assumption |].
      apply IHnsf; clear IHnsf.
      destruct nsf; simpl in *.
      + inversion mP; subst; clear mP.
        inversion HS; subst; clear HS.
        apply comp_Lt_lt in HLt; apply comp_Lt_lt in HLt0; destruct HLt, HLt0.
        apply SS_cons; [assumption | apply comp_lt_Lt; split; [etransitivity; eassumption | ]].
        intros EQ; rewrite EQ in H.
        apply H2, ord_part; split; assumption.
      + inversion mP; subst; clear mP.
        inversion HS; subst; clear HS.
        apply comp_Lt_lt in HLt; apply comp_Lt_lt in HLt0; destruct HLt, HLt0.
        apply SS_cons; [assumption | apply comp_lt_Lt; split; [etransitivity; eassumption | ]].
        intros EQ; rewrite EQ in H.
        apply H2, ord_part; split; assumption.
    Qed.

Ralf Jung's avatar
Ralf Jung committed
544
  End Filter.*)
545

Ralf Jung's avatar
Ralf Jung committed
546 547 548 549 550
  Section Induction.
    Context {V : Type} `{eV : Setoid V}.

    Section Recursion.
      Context (T: (K -f> V) -> Type)
551
              (Text: forall (f1 f2: K -f> V), equal_fd f1 f2 -> T f1 -> T f2)
Ralf Jung's avatar
Ralf Jung committed
552
              (Temp: T fdEmpty).
Janno's avatar
Janno committed
553
      Context (Tstep: forall (k:K) (v:V) (f: K -f> V), ~(k  dom f) -> T f -> T (f + [fd k <- v ] )).
Ralf Jung's avatar
Ralf Jung committed
554 555 556 557 558

      Definition fdRectInner: forall l f, dom f = l -> T f.
      Proof.
        refine (fix F (l: list K) :=
                  match l as l return (forall f, dom f = l -> T f) with
559
                  | [] => fun f Hdom => Text fdEmpty f _ Temp
560 561 562
                  | k::l' => fun f Hdom => let f' := f \ k in
                                           let Hindom: k  dom f := _ in
                                           let v' := fdLookup_indom f k Hindom in
Janno's avatar
Janno committed
563
                                           Text (f' + [fd k <- v' ]) f _
564
                                                (Tstep k v' f' _ (F l' f' _))
Ralf Jung's avatar
Ralf Jung committed
565
                  end); clear F.
566 567 568
        - split.
          + move=>k /=. symmetry. apply fdLookup_notin_strong. rewrite Hdom. tauto.
          + rewrite Hdom. reflexivity.
Ralf Jung's avatar
Ralf Jung committed
569
        - rewrite Hdom. left. reflexivity.
570 571 572 573 574 575 576 577
        - subst f'. split.
          + move=>k'. destruct (dec_eq k k') as [EQ|NEQ].
            * subst k'. rewrite fdStrongUpdate_eq. subst v'. symmetry. eapply fdLookup_indom_corr.
              reflexivity.
            * erewrite !fdStrongUpdate_neq by assumption. reflexivity.
          + rewrite Hdom /dom /=. f_equal. rewrite /dom /= Hdom.
            rewrite DecEq_refl.
            assert (Hnod := dom_nodup f). rewrite Hdom in Hnod.
Janno's avatar
Janno committed
578
            assert (Hfilt1: (filter_dupes ([])%list l') = l').
579 580
            { apply filter_dupes_id. simpl. inversion Hnod; subst. assumption. }
            rewrite Hfilt1. apply filter_dupes_id. assumption.
Ralf Jung's avatar
Ralf Jung committed
581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597
        - subst f'. apply fdLookup_notin. rewrite fdStrongUpdate_eq. reflexivity.
        - subst f'. rewrite /dom /fdStrongUpdate /=.
          rewrite Hdom. destruct (dec_eq k k) as [_|NEQ]; last (exfalso; now apply NEQ).
          apply filter_dupes_id with (dupes:=[]); simpl.
          assert (Hno:= dom_nodup f). rewrite Hdom in Hno.
          inversion Hno; subst. assumption.
      Defined.

      Definition fdRect: forall f, T f :=
        fun f => fdRectInner (dom f) f eq_refl.
    End Recursion.

    Section Fold.
      Context {T: Type}.
      Context (Temp: T) (Tstep: K -> V -> T -> T).
      
      Definition fdFold: (K -f> V) -> T :=
598
        fdRect (fun _ => T) (fun _ _ _ => id) (Temp)
Ralf Jung's avatar
Ralf Jung committed
599 600 601 602 603 604 605 606 607
               (fun k v _ _ => Tstep k v).

      Lemma fdFoldEmpty: fdFold fdEmpty = Temp.
      Proof.
        reflexivity.
      Qed.

      Lemma fdRectInner_eqLF l1 f1 l2 f2 (Heq1: dom f1 = l1) (Heq2: dom f2 = l2):
        l1 = l2 -> (forall k, f1 k = f2 k) ->
608 609
        fdRectInner (fun _ => T) (fun _ _ _ => id) (Temp) (fun k v _ _ => Tstep k v) l1 f1 Heq1 =
        fdRectInner (fun _ => T) (fun _ _ _ => id) (Temp) (fun k v _ _ => Tstep k v) l2 f2 Heq2.
Ralf Jung's avatar
Ralf Jung committed
610
      Proof.
611
        move=>Heql Heqf. assert (Heq': dom f2 = l1).
Ralf Jung's avatar
Ralf Jung committed
612
        { now subst l2. }
613 614 615 616 617
        revert f1 f2 l2 Heq' Heq1 Heq2 Heql Heqf. induction l1; intros.
        - destruct l2; last discriminate. reflexivity.
        - destruct l2; first discriminate. inversion Heql; subst; clear Heql.
          assert (Hf: exists v, f1 k = Some v /\ f2 k = Some v).
          { destruct (f1 k) as [v|] eqn:EQf.
Ralf Jung's avatar
Ralf Jung committed
618 619 620 621
            - exists v. split; first reflexivity. rewrite -Heqf. assumption.
            - exfalso. apply fdLookup_notin_strong in EQf. apply EQf. rewrite Heq1.
              left. reflexivity. }
          destruct Hf as [v [Heqf1 Heqf2]].
622 623 624 625 626 627 628 629 630 631 632 633
          simpl. f_equal. f_equal.
          + eapply fdLookup_indom_corr in Heqf1. erewrite Heqf1.
            eapply fdLookup_indom_corr in Heqf2. erewrite Heqf2.
            reflexivity.
          + apply IHl1.
            * rewrite /fdStrongUpdate /dom /=. rewrite Heq' DecEq_refl.
              eapply filter_dupes_id. simpl.
              move:(dom_nodup f2). rewrite Heq'. intros Hnd. inversion Hnd; subst. assumption.
            * reflexivity.
            * intros. destruct (dec_eq k k0) as [EQ|NEQ].
              { subst k0. rewrite !fdStrongUpdate_eq. reflexivity. }
              erewrite !fdStrongUpdate_neq by assumption. now apply Heqf.
Ralf Jung's avatar
Ralf Jung committed
634 635
      Qed.

636 637
      Global Instance fdFoldExtF:
        Proper (equal_fd ==> eq) fdFold.
638
      Proof.
639
        move=>f1 f2 [Heq Hdom]. rewrite /fdFold /fdRect. eapply fdRectInner_eqLF; assumption.
640 641
      Qed.

642
      Lemma fdFoldAdd f k v:
Ralf Jung's avatar
Ralf Jung committed
643
        ~k  (dom f) ->
Janno's avatar
Janno committed
644
        fdFold (f + [fd k <- v ] ) = Tstep k v (fdFold f).
Ralf Jung's avatar
Ralf Jung committed
645 646
      Proof.
        move=>Hindom. rewrite /fdFold /fdRect {2}/dom /=.
Janno's avatar
Janno committed
647
        assert (Hl: f + [fd k <- v ] k = Some v).
Ralf Jung's avatar
Ralf Jung committed
648 649 650 651 652 653 654 655 656 657 658 659
        { apply fdStrongUpdate_eq. }
        eapply fdLookup_indom_corr in Hl. erewrite Hl.
        unfold id. f_equal.
        apply fdRectInner_eqLF.
        - apply filter_dupes_id. apply NoDup_cons.
          + exact Hindom.
          + apply filter_dupes_nodup.
        - move=>k'. destruct (dec_eq k k') as [EQ|NEQ].
          + subst k'. rewrite fdStrongUpdate_eq. symmetry. apply fdLookup_notin_strong. assumption.
          + erewrite !fdStrongUpdate_neq by assumption. reflexivity.
      Qed.

660 661
      Lemma fdFoldRedundantRemove f k:
        ~k  (dom f) ->
Janno's avatar
Janno committed
662
        fdFold (f \ k) = fdFold f.
663 664 665 666 667 668 669
      Proof.
        move=>Hindom. eapply fdFoldExtF. split.
        - move=>k'. simpl. apply fdLookup_notin_strong in Hindom.
          destruct (dec_eq k k').
          + subst. now rewrite Hindom.
          + reflexivity.
        - rewrite /fdStrongUpdate /dom /= /dom. rewrite /dom in Hindom.
Janno's avatar
Janno committed
670
          destruct (filter_dupes ([])%list (findom f)) as [|k' dom'] eqn:Hdom'.
671 672 673 674 675 676 677 678 679
          + reflexivity.
          + destruct (dec_eq k k') as [EQ|NEQ].
            * subst k'. exfalso. apply Hindom. now left.
            * erewrite filter_dupes_id by apply filter_dupes_nodup.
              erewrite filter_dupes_id; first reflexivity. simpl.
              constructor; first assumption.
              rewrite -Hdom'. apply filter_dupes_nodup.
      Qed.

Ralf Jung's avatar
Ralf Jung committed
680 681 682 683 684 685 686 687 688
      (* Alternative, more direct formulation of fold. *)
      Definition fdFold'Inner fLookup k: T -> T :=
        fun t => match fLookup k with
                 | Some v => Tstep k v t
                 (* We know this case never happens, but that would be very annoying to make use of here. *)
                 | None => t end.
      Definition fdFold' (f: K -f> V): T :=
        fold_right (fdFold'Inner f) Temp (dom f).

689 690 691 692 693 694 695 696 697 698
      Global Instance fdFold'ExtF:
        Proper (equal_fd ==> eq) fdFold'.
      Proof.
        move=>f1 f2 [Heq Hdom]. rewrite /fdFold' /fdFold'Inner. apply fold_ext_restr.
          + assumption.
          + reflexivity.
          + move=>k t _. rewrite Heq. reflexivity.
      Qed.


Ralf Jung's avatar
Ralf Jung committed
699 700 701 702 703
      (* They are equivalent. *)
      Lemma fdFoldBehavior f:
        fdFold f = fdFold' f.
      Proof.
        revert f. elim/fdRect.
704 705
        - move=>f1 f2 EQf EQfold. erewrite <-fdFoldExtF by eexact EQf.
          rewrite EQfold. rewrite EQf. reflexivity.
Ralf Jung's avatar
Ralf Jung committed
706
        - reflexivity.
707
        - move=>k v f Hnin Heq. erewrite fdFoldAdd by assumption.
Ralf Jung's avatar
Ralf Jung committed
708 709 710 711 712 713 714 715 716 717 718 719 720
          rewrite /fdFold' /= /fdFold'Inner.
          destruct (dec_eq k k) as [_|NEQ]; last (exfalso; now apply NEQ). f_equal. rewrite Heq.
          rewrite /fdFold' /fdFold'Inner. apply fold_ext_restr.
          + symmetry. apply filter_dupes_id. apply NoDup_cons; first assumption.
            apply dom_nodup.
          + reflexivity.
          + clear -Hnin. move=>k' t Hin.
            destruct (dec_eq k k'); last reflexivity. exfalso.
            subst k'. contradiction.
      Qed.

    End Fold.

721 722 723
    Section FoldExtStep.
      (* One can change the step function *)
      Context {T: Type} {eqT: relation T} {eqRT: Equivalence eqT}.
Ralf Jung's avatar
Ralf Jung committed
724

725 726 727 728
      Context (Tstep1 Tstep2: K -> V -> T -> T).
      Context {Tstep1_proper: Proper (eq ==> eq ==> eqT ==> eqT) Tstep1}.
      Context {Tstep2_proper: Proper (eq ==> eq ==> eqT ==> eqT) Tstep2}.
      Context {Tstep_eq: forall k v t, eqT (Tstep1 k v t) (Tstep2 k v t)}.
Ralf Jung's avatar
Ralf Jung committed
729

730 731 732
      Lemma fdFoldExtT:
        forall Temp1 Temp2, eqT Temp1 Temp2 ->
                            forall f, eqT (fdFold Temp1 Tstep1 f) (fdFold Temp2 Tstep2 f).
Ralf Jung's avatar
Ralf Jung committed
733
      Proof.
734 735
        move=>Temp1 Temp2 EQemp f.
        rewrite !fdFoldBehavior /fdFold'.
Ralf Jung's avatar
Ralf Jung committed
736 737 738 739 740
        apply fold_ext.
        - move=>k k' EQk v1 v2 EQv. subst k'. rewrite /fdFold'Inner. destruct (f k).
          + rewrite EQv. reflexivity.
          + assumption.
        - move=>k t. rewrite /fdFold'Inner. destruct (f k); last reflexivity.
741
          apply Tstep_eq.
Ralf Jung's avatar
Ralf Jung committed
742 743
        - assumption.
      Qed.
744 745 746 747 748 749
    End FoldExtStep.

    Section FoldExtPerm.        
      (* If the step function is commutative, one can change the finmap. *)
      Context {T: Type} `{Setoid T}.
      Context (Temp: T) (Tstep: K -> V -> T -> T).
Ralf Jung's avatar
Ralf Jung committed
750

751
      Definition fdStep_comm: Prop :=
Ralf Jung's avatar
Ralf Jung committed
752 753 754
        forall (k1 k2:K) (v1 v2:V),
          compose (Tstep k1 v1) (Tstep k2 v2) == compose (Tstep k2 v2) (Tstep k1 v1).

755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788
      Context (Tstep_comm: fdStep_comm).

      Global Instance fdFoldExtP {Tstep_proper: Proper (eq ==> equiv ==> equiv ==> equiv) Tstep}:
          Proper (equiv ==> equiv) (fdFold Temp Tstep).
      Proof.
        move=>f1 f2 EQf. rewrite !fdFoldBehavior /fdFold'.
        rewrite /fdFold'. etransitivity; last eapply fold_perm.
        - eapply fold_ext.
          + move=>k k' EQk v1 v2 EQv. subst k'. rewrite /fdFold'Inner.
            destruct (f1 k); last assumption. rewrite EQv. reflexivity.
          + move=>k t. rewrite /fdFold'Inner. specialize (EQf k). destruct (f1 k), (f2 k); try contradiction.
            * simpl in EQf. rewrite EQf. reflexivity.
            * reflexivity.
          + reflexivity.
        - move=>k k' EQk v1 v2 EQv. subst k'. rewrite /fdFold'Inner.
          destruct (f2 k); last assumption. rewrite EQv. reflexivity.
        - move=>v1 v2 t. rewrite /fdFold'Inner /=.
          destruct (f2 v1), (f2 v2); try reflexivity; [].
          apply Tstep_comm.
        - split; last split.
          + apply dom_nodup.
          + apply dom_nodup.
          + move=>k. rewrite !fdLookup_in_strong. specialize (EQf k).
            destruct (f1 k), (f2 k); try contradiction; last tauto; [].
            split; discriminate.
      Qed.
    End FoldExtPerm.

    Section FoldExtPermDist.
      (* The same, up to n-equality. TODO: Figure out a way not to repeat all this. *)
      Context {mV: metric V} {cmV: cmetric V}.
      Context {T: Type} `{cmetric T}.
      Context (Temp: T) (Tstep: K -> V -> T -> T).
      Context (Tstep_comm: fdStep_comm Tstep).
Ralf Jung's avatar
Ralf Jung committed
789
        
790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815
      Lemma fdFoldExtP_dist n {Tstep_proper: Proper (eq ==> dist n ==> dist n ==> dist n) Tstep}:
        Proper (dist n ==> dist n) (fdFold Temp Tstep).
      Proof.
        move=>f1 f2 EQf. rewrite !fdFoldBehavior /fdFold'.
        destruct n as [|n]; first exact:dist_bound.
        rewrite /fdFold'. etransitivity; last eapply fold_perm.
        - eapply fold_ext.
          + move=>k k' EQk v1 v2 EQv. subst k'. rewrite /fdFold'Inner.
            destruct (f1 k); last assumption. apply Tstep_proper; reflexivity || assumption.
          + move=>k t. rewrite /fdFold'Inner.
            specialize (EQf k). destruct (f1 k), (f2 k); try (now destruct EQf).
            * simpl in EQf. apply Tstep_proper; reflexivity || assumption.
          + reflexivity.
        - move=>k k' EQk v1 v2 EQv. subst k'. rewrite /fdFold'Inner.
          destruct (f2 k); last assumption. rewrite EQv. reflexivity.
        - move=>v1 v2 t. rewrite /fdFold'Inner /=.
          destruct (f2 v1), (f2 v2); try reflexivity; [].
          apply dist_refl, Tstep_comm.
        - split; last split.
          + apply dom_nodup.
          + apply dom_nodup.
          + move=>k. rewrite !fdLookup_in_strong. specialize (EQf k).
            destruct (f1 k), (f2 k); split; intro; try (assumption || discriminate || contradiction).
      Qed.
                  
    End FoldExtPermDist.
Ralf Jung's avatar
Ralf Jung committed
816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834

  End Induction.

  Section Compose.
    Context {V : Type} `{eV : Setoid V}.
    Context (op: option V -> option V -> option V).
    Context {op_nongen: op None None = None}.

    Program Definition fdCompose (f1 f2: K -f> V): K -f> V :=
      mkFDbound (fun i => op (f1 i) (f2 i)) (findom f1 ++ findom f2) _.
    Next Obligation.
      move=>k /= Hin. apply in_app_iff.
      destruct (f1 k) eqn:EQf1, (f2 k) eqn:EQf2.
      - left. apply findom_b. rewrite EQf1. discriminate.
      - left. apply findom_b. rewrite EQf1. discriminate.
      - right. apply findom_b. rewrite EQf2. discriminate.
      - contradiction.
    Qed.

835 836 837 838 839 840
    Lemma fdComposeRed (f1 f2: K -f> V) i:
      fdCompose f1 f2 i = op (f1 i) (f2 i).
    Proof.
      reflexivity.
    Qed.

Janno's avatar
Janno committed
841
  End Compose.
842

Janno's avatar
Janno committed
843
End FinDom2.
844

Ralf Jung's avatar
Ralf Jung committed
845
(*Arguments fdMap {K cT ord equ preo ord_part compK U V eqT mT cmT pTA pcmU eqT0 mT0 cmT0 pTA0 cmV} _.*)
846 847

Section RA.
Ralf Jung's avatar
Ralf Jung committed
848
  Context {I : Type} {S : Type} `{eqI : DecEq I} `{RAS : RA S}.
849 850 851
  Implicit Type (i : I) (s : S) (f g : I -f> S).

  Local Open Scope ra_scope.
Ralf Jung's avatar
Ralf Jung committed
852
  Local Open Scope finmap_scope.
853 854
  
  Global Instance ra_type_finprod : Setoid (I -f> S) := _.
Ralf Jung's avatar
Ralf Jung committed
855 856 857 858
  Global Program Instance ra_unit_finprod : RA_unit (I -f> S) :=
    fdMapRaw ra_unit.

  Definition finprod_op (s1 s2: option S) :=
Ralf Jung's avatar
Ralf Jung committed
859 860 861 862 863 864
    match s1 with
    | None => s2
    | Some s1 => match s2 with
                   Some s2 => Some (s1 · s2)
                 | None    => Some s1
                 end
Ralf Jung's avatar
Ralf Jung committed
865 866 867 868 869
    end.
  Global Program Instance ra_op_finprod : RA_op (I -f> S) :=
    fdCompose finprod_op.                                
  Global Instance ra_valid_finprod : RA_valid (I -f> S) :=
    fun f => forall i, match f i with Some s => ra_valid s | None => True end.
Janno's avatar
Janno committed
870
  
871 872 873
  Global Instance ra_finprod : RA (I -f> S).
  Proof.
    split; repeat intro.
Ralf Jung's avatar
Ralf Jung committed
874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897
    - simpl. specialize (H k). specialize (H0 k).
      destruct (x k), (y k), (x0 k), (y0 k); try contradiction; simpl; try reflexivity; try assumption; [].
      simpl in H. simpl in H0. rewrite H H0. reflexivity.
    - simpl. destruct (t1 k), (t2 k), (t3 k); try reflexivity; [].
      simpl. rewrite assoc. reflexivity.
    - simpl. destruct (t1 k), (t2 k); try reflexivity; [].
      simpl. now rewrite comm.
    - simpl. rewrite /fdMap_pre. destruct (t k); last reflexivity.
      simpl. rewrite ra_op_unit. reflexivity.
    - simpl. specialize (H k). rewrite /fdMap_pre.
      destruct (x k), (y k); try (reflexivity || assumption); [].
      simpl in H. simpl. rewrite H. reflexivity.
    - pose (op := fun (os1 os2: option S) =>
                    match os1, os2 with
                    | Some s, Some s' => Some (proj1_sig (ra_unit_mono s s'))
                    | Some s, None    => None
                    | None  , Some s' => Some (ra_unit s')
                    | None  , None    => None end).
      exists (fdCompose op (op_nongen := eq_refl) t t').
      move=>k. simpl. rewrite /fdMap_pre /ra_op /=.
      destruct (t k), (t' k); simpl; try (reflexivity || tauto); [].
      move:(ra_unit_mono s s0)=>[t'' Heq] /=. assumption.
    - simpl. rewrite /fdMap_pre /ra_unit /= /fdMap_pre.
      destruct (t k); last reflexivity.
898
      apply option_eq_Some, ra_unit_idem.
Ralf Jung's avatar
Ralf Jung committed
899 900 901 902 903
    - split; rewrite /ra_valid /=; move =>Hval i; specialize (H i); specialize (Hval i); destruct (x i), (y i); try (contradiction || tauto); [|].
      + simpl in H. rewrite -H. assumption.
      + simpl in H. rewrite H. assumption.
    - move:(H i)=>{H}. rewrite /=. destruct (t1 i), (t2 i); simpl; try tauto; [].
      apply ra_op_valid.
904
  Qed.
905 906 907 908 909

  (* The RA order on finmaps is the same as the fpfun order over the RA order *)
  Lemma ra_pord_iff_ext_pord {f g}:
    pord (preoType:=pord_ra) f g <-> pord (preoType:=extOrd_preo) f g.
  Proof.
Janno's avatar
Janno committed
910
    split.
Ralf Jung's avatar
Ralf Jung committed
911 912 913 914 915
    { move => [h Hhf] i. move:(Hhf i)=>{Hhf} /=.
      destruct (f i), (g i), (h i); simpl; try tauto; [|].
      - move=>Heq. exists s1. assumption.
      - move=>Heq. rewrite Heq. reflexivity. }
    move:g f. apply: fdRect.
916
    - move=>f1 f2 [Heqf _] Hleeq f Hle.
Ralf Jung's avatar
Ralf Jung committed
917 918 919 920 921 922
      destruct (Hleeq f).
      + move=>k. rewrite (Heqf k). now apply Hle.
      + exists x. move=>k. rewrite -Heqf. apply H.
    - move=>f Hle. exists (fdEmpty (V:=S)). move=>k. simpl.
      specialize (Hle k). destruct (f k); last reflexivity.
      contradiction Hle.
Janno's avatar
Janno committed
923
    - move=>k v f Hnin IH g Hle. destruct (IH (g \ k)) as [h Hh]=>{IH}.
Ralf Jung's avatar
Ralf Jung committed
924 925 926 927 928 929
      + move=>i. destruct (dec_eq k i) as [EQ|NEQ].
        * subst i. rewrite fdStrongUpdate_eq. exact Logic.I.
        * erewrite fdStrongUpdate_neq by assumption.
          etransitivity; first now apply Hle.
          erewrite fdStrongUpdate_neq by assumption. reflexivity.
      + specialize (Hle k). rewrite fdStrongUpdate_eq in Hle. destruct (g k) eqn:EQg; last first.
Janno's avatar
Janno committed
930
        { exists (h + [fd k <-  v ] ). move=>i /= {Hle}. specialize (Hh i). simpl in Hh.
Ralf Jung's avatar
Ralf Jung committed
931 932 933
          destruct (dec_eq k i) as [EQ|NEQ].
          - subst i. rewrite EQg. reflexivity.
          - assumption. }
Janno's avatar
Janno committed
934 935
        destruct Hle as [s' Hle].
        exists (h + [fd k <- s'] ). move=>i /=.
Ralf Jung's avatar
Ralf Jung committed
936 937 938
        specialize (Hh i). simpl in Hh. destruct (dec_eq k i) as [EQ|NEQ].
        * subst i. rewrite EQg. simpl. assumption.
        * assumption.
939
  Qed.
940
End RA.
Ralf Jung's avatar
Ralf Jung committed
941 942

Section VIRA.
Ralf Jung's avatar
Ralf Jung committed
943
  Context {I : Type} `{eqI : DecEq I}.
Ralf Jung's avatar
Ralf Jung committed
944 945 946 947
  Context {T: Type} `{raT: RA T}.

  Global Instance vira_finmap: VIRA (I -f> T).
  Proof.
Ralf Jung's avatar
Ralf Jung committed
948
    eexists fdEmpty. move=>i. exact Logic.I.
Ralf Jung's avatar
Ralf Jung committed
949 950 951 952 953
  Qed.
    
End VIRA.


954
Section CMRA.
Ralf Jung's avatar
Ralf Jung committed
955
  Context {I : Type} `{eqI : DecEq I}.
956
  Context {T: Type} `{cmraT: CMRA T}.
Janno's avatar
Janno committed
957
  
Ralf Jung's avatar
Ralf Jung committed
958 959
  Local Open Scope ra_scope.
  Local Open Scope finmap_scope.
960

961 962 963 964 965 966 967
  Global Instance ra_finmap_pcm: pcmType (pTA:=pord_ra) (I -f> T).
  Proof.
    split. intros σ ρ σc ρc HC.
    apply ra_pord_iff_ext_pord.
    eapply pcm_respC; first by apply _.
    move=>i. apply ra_pord_iff_ext_pord. by apply: HC.
  Qed.
968

Ralf Jung's avatar
Ralf Jung committed
969 970 971 972
  Definition finmap_cmra_valid_op (f: I -f> T) n :=
    forall i, match f i with Some s => cmra_valid s n
                        | None => True end.
                            
973
  Global Program Instance finmap_cmra_valid: CMRA_valid (I -f> T) :=
974
    fun f => p[(finmap_cmra_valid_op f)].
975 976 977 978
  Next Obligation.
    move=>i. destruct (f i); last tauto.
    exact: bpred.
  Qed.
979
  Next Obligation.
Ralf Jung's avatar
Ralf Jung committed
980 981 982
    move=>n m Hle /= H i. specialize (H i).
    destruct (f i); last tauto.
    eapply dpred, H. assumption.
983 984
  Qed.
    
985 986
  Global Instance finmap_cmra : CMRA (I -f> T).
  Proof.
987
    split.
Ralf Jung's avatar
Ralf Jung committed
988 989 990 991 992 993 994 995 996
    - move=>n f1 f2 EQf g1 g2 EQg k.
      destruct n as [|n]; first exact:dist_bound.
      specialize (EQf k). specialize (EQg k). simpl.
      destruct (f1 k), (f2 k), (g1 k), (g2 k); simpl; try (contradiction || assumption || tauto); [].
      simpl in EQf. simpl in EQg. rewrite EQf EQg. reflexivity.
    - move=>n f1 f2 EQf k.
      destruct n as [|n]; first exact:dist_bound.
      specialize (EQf k). rewrite /= /fdMap_pre.
      destruct (f1 k), (f2 k); try (contradiction || assumption); [].
997
      simpl in EQf. simpl. rewrite EQf. reflexivity.
Ralf Jung's avatar
Ralf Jung committed
998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013
    - move=>n f1 f2 EQf.
      destruct n as [|n]; first exact:dist_bound.
      move=>m Hle. split; move=>Hval i; specialize (EQf i); specialize (Hval i); destruct (f1 i), (f2 i); simpl; try (contradiction || tauto); [|].
      + simpl in EQf. eapply spredNE, Hval.
        eapply mono_dist; last (now rewrite EQf). omega.
      + simpl in EQf. eapply spredNE, Hval.
        eapply mono_dist; last (now rewrite EQf). omega.
    - move => f1. split => [H|H n] i. 
      + destruct (f1 i) eqn:EQf; last tauto.
        eapply cmra_ra_valid =>n.
        specialize (H n i). rewrite EQf in H. assumption.
      + specialize (H i). destruct (f1 i); last tauto.
        now apply cmra_ra_valid.
    - move=>t1 t2 n H i. move:(H i)=>{H}.
      rewrite /=. destruct (t1 i), (t2 i); simpl; try tauto; [].
      apply cmra_op_valid.
1014
  Qed.
1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111

  Section CMRAExt.
    Context {cmraText: CMRAExt T}.

    (* It is crucial for the lower cmra_extend function to be called only once per element
       (or we would need proof irrelevance). So we first define both witnesses at once, and then
       show their projections constitute a finite partial function. *)
    Program Definition finmap_cmra_extend {n} {f1 f11 f12 f2: I -f> T}
            (EQf: f1 = S n = f2) (EQf1: f1 == f11 · f12) i : option T * option T :=
      match f1 i, f2 i with
      | Some t1, Some t2 => match f11 i, f12 i with
                            | Some t11, Some t12 => let E := cmra_extend (S n) t1 t11 t12 t2 _ _ in
                                                    (Some (projT1 E), Some (projT1 (projT2 E)))
                            | Some t11, None     => (Some t2, None)
                            | None    , Some t12 => (None, Some t2)
                            | None    , None     => (None, None) end
      (* Unfortunately, Program does not like us to use a wildcard here. *)
      | Some _ , None    => (None, None)
      | None   , Some _  => (None, None)
      | None   , None    => (None, None) end.
    Next Obligation.
      specialize (EQf i). rewrite -Heq_anonymous -Heq_anonymous0 in EQf.
      exact EQf.
    Qed.
    Next Obligation.
      specialize (EQf1 i). rewrite /ra_op /= -Heq_anonymous -Heq_anonymous1 -Heq_anonymous2 /= in EQf1.
      exact EQf1.
    Qed.

    Program Definition finmap_cmra_extend_t21 {n} {f1 f11 f12 f2: I -f> T}
            (EQf: f1 = S n = f2) (EQf1: f1 == f11 · f12) : I -f> T :=
      mkFDbound (fun i => fst (finmap_cmra_extend EQf EQf1 i)) (findom f1) _.
    Next Obligation.
      move=>k. rewrite -(findom_b f1) /finmap_cmra_extend.
      ddes (f1 k) at 1 3 11 as [v1|] deqn:EQf1v.
      - ddes (f2 k) at 1 3 as [v2|] deqn:EQf2v; last discriminate.
        ddes (f11 k) at 1 3 as [v11|] deqn:EQf11v.
        + ddes (f12 k) at 1 3 as [v12|] deqn:EQf12v; discriminate.
        + ddes (f12 k) at 1 3 as [v12|] deqn:EQf12v; discriminate.
      - ddes (f2 k) at 1 3 as [v2|] deqn:EQf2v; tauto.
    Qed.

    Program Definition finmap_cmra_extend_t22 {n} {f1 f11 f12 f2: I -f> T}
            (EQf: f1 = S n = f2) (EQf1: f1 == f11 · f12) : I -f> T :=
      mkFDbound (fun i => snd (finmap_cmra_extend EQf EQf1 i)) (findom f1) _.
    Next Obligation.
      move=>k. rewrite /findom_approx -(findom_b f1) /finmap_cmra_extend.
      ddes (f1 k) at 1 3 11 as [v1|] deqn:EQf1v.
      - ddes (f2 k) at 1 3 as [v2|] deqn:EQf2v.
        + ddes (f11 k) at 1 3 as [v11|] deqn:EQf11v; last discriminate.
          ddes (f12 k) at 1 3 as [v12|] deqn:EQf12v; discriminate.
        + discriminate.
      - ddes (f2 k) at 1 3 as [v2|] deqn:EQf2v; tauto.
    Qed.

    Global Instance finmap_CMRAExt: CMRAExt (I -f> T).
    Proof.
      intros n f1 f11 f12 f2 EQf EQf1. destruct n.
      { exists (1 f2) f2. split; last exact:dist_bound. now rewrite ra_op_unit. }
      exists (finmap_cmra_extend_t21 EQf EQf1).
      exists (finmap_cmra_extend_t22 EQf EQf1).
      cut (forall i, f2 i ==
                     finprod_op (finmap_cmra_extend_t21 EQf EQf1 i) (finmap_cmra_extend_t22 EQf EQf1 i) /\
                     f11 i = S n = finmap_cmra_extend_t21 EQf EQf1 i /\
                     f12 i = S n = finmap_cmra_extend_t22 EQf EQf1 i).
      { move=>Heq. split; last split.
        - move=>i. specialize (Heq i). tauto.
        - move=>i. specialize (Heq i). tauto.
        - move=>i. specialize (Heq i). tauto. }
      move=>i. rewrite /= /finmap_cmra_extend /=.
      ddes (f1 i) at 1 3 11 19 27 as [v1|] deqn:EQf1v.
      - ddes (f2 i) at 1 3 4 8 12 16 as [v2|] deqn:EQf2v; last first.
        { exfalso. specialize (EQf i). rewrite -EQf1v -EQf2v in EQf. exact EQf. }
        ddes (f11 i) at 1 3 11 19 20 28 as [v11|] deqn:EQf11v.
        + ddes (f12 i) at 1 3 7 11 15 16 as [v12|] deqn:EQf12v; simpl; last first.
          { specialize (EQf1 i). rewrite /ra_op /= -EQf1v -EQf11v -EQf12v /= in EQf1.
            specialize (EQf i). rewrite -EQf1v -EQf2v /= in EQf. split; first reflexivity.
            split; last tauto. rewrite -EQf1. assumption. }
          destruct (cmra_extend (S n) v1 v11 v12 v2
                                (finmap_cmra_extend_obligation_1 n f1 f11 f12 f2 EQf EQf1 i v1 v2
                                                                 EQf1v EQf2v v11 v12 EQf11v EQf12v)
                                (finmap_cmra_extend_obligation_2 n f1 f11 f12 f2 EQf EQf1 i v1 v2
                                                                 EQf1v EQf2v v11 v12 EQf11v EQf12v)) as [t21 [t22 [EQ2 [EQd1 EQd2]]]].
          simpl. split_conjs; assumption.
        + ddes (f12 i) at 1 3 7 11 15 16 as [v12|] deqn:EQf12v; simpl.
          { specialize (EQf1 i). rewrite /ra_op /= -EQf1v -EQf11v -EQf12v /= in EQf1.
            specialize (EQf i). rewrite -EQf1v -EQf2v /= in EQf. split; first reflexivity.
            split; first tauto. rewrite -EQf1. assumption. }
          exfalso. specialize (EQf1 i). rewrite /ra_op /= -EQf1v -EQf11v -EQf12v /= in EQf1. exact EQf1.
      - ddes (f2 i) at 1 3 4 8 12 16 as [v2|] deqn:EQf2v.
        + exfalso. specialize (EQf i). rewrite -EQf1v -EQf2v /= in EQf. exact EQf.
        + simpl. split; first tauto.
          specialize (EQf1 i). rewrite /ra_op /= -EQf1v /= in EQf1.
          destruct (f11 i), (f12 i); contradiction || split; reflexivity.
    Qed.
    
  End CMRAExt.
1112
  
1113
End CMRA.
1114

1115
Section RAMap.
Ralf Jung's avatar
Ralf Jung committed
1116
  Context {I : Type} `{CI : DecEq I}.
1117
  Context {T U: Type} `{cmraT: CMRA T} `{cmraU: CMRA U}.
1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141

  Local Instance ra_force_pord_T: preoType (I -f> T) := pord_ra.
  Local Instance ra_force_pord_U: preoType (I -f> U) := pord_ra.

  Program Definition fdRAMap