cofe_maps.v 6.09 KB
Newer Older
1
Require Export modures.cofe prelude.fin_maps.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
Require Import prelude.pmap prelude.gmap prelude.natmap.
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
Local Obligation Tactic := idtac.

(** option *)
Inductive option_dist `{Dist A} : Dist (option A) :=
  | option_0_dist (x y : option A) : x ={0}= y
  | Some_dist n x y : x ={n}= y  Some x ={n}= Some y
  | None_dist n : None ={n}= None.
Existing Instance option_dist.
Program Definition option_chain `{Cofe A}
    (c : chain (option A)) (x : A) (H : c 1 = Some x) : chain A :=
  {| chain_car n := from_option x (c n) |}.
Next Obligation.
  intros A ???? c x ? n i ?; simpl; destruct (decide (i = 0)) as [->|].
  { by replace n with 0 by lia. }
  feed inversion (chain_cauchy c 1 i); auto with lia congruence.
  feed inversion (chain_cauchy c n i); simpl; auto with lia congruence.
Qed.
Instance option_compl `{Cofe A} : Compl (option A) := λ c,
  match Some_dec (c 1) with
  | inleft (exist x H) => Some (compl (option_chain c x H)) | inright _ => None
  end.
Instance option_cofe `{Cofe A} : Cofe (option A).
Proof.
  split.
  * intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
    intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
    by intros n; feed inversion (Hxy n).
  * intros n; split.
    + by intros [x|]; constructor.
    + by destruct 1; constructor.
    + destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
  * by inversion_clear 1; constructor; apply dist_S.
  * constructor.
  * intros c n; unfold compl, option_compl.
    destruct (decide (n = 0)) as [->|]; [constructor|].
    destruct (Some_dec (c 1)) as [[x Hx]|].
    { assert (is_Some (c n)) as [y Hy].
      { feed inversion (chain_cauchy c 1 n); try congruence; eauto with lia. }
      rewrite Hy; constructor.
      by rewrite (conv_compl (option_chain c x Hx) n); simpl; rewrite Hy. }
    feed inversion (chain_cauchy c 1 n); auto with lia congruence; constructor.
Qed.
Instance Some_ne `{Dist A} : Proper (dist n ==> dist n) Some.
Proof. by constructor. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
47 48 49 50
Instance None_timeless `{Dist A, Equiv A} : Timeless (@None A).
Proof. inversion_clear 1; constructor. Qed.
Instance Some_timeless `{Dist A, Equiv A} x : Timeless x  Timeless (Some x).
Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
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
Instance option_fmap_ne `{Dist A, Dist B} (f : A  B) n:
  Proper (dist n ==> dist n) f  Proper (dist n==>dist n) (fmap (M:=option) f).
Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.

(** Finite maps *)
Section map.
  Context `{FinMap K M}.
  Global Instance map_dist `{Dist A} : Dist (M A) := λ n m1 m2,
     i, m1 !! i ={n}= m2 !! i.
  Program Definition map_chain `{Dist A} (c : chain (M A))
    (k : K) : chain (option A) := {| chain_car n := c n !! k |}.
  Next Obligation. by intros A ? c k n i ?; apply (chain_cauchy c). Qed.
  Global Instance map_compl `{Cofe A} : Compl (M A) := λ c,
    map_imap (λ i _, compl (map_chain c i)) (c 1).
  Global Instance map_cofe `{Cofe A} : Cofe (M A).
  Proof.
    split.
    * intros m1 m2; split.
      + by intros Hm n k; apply equiv_dist.
      + intros Hm k; apply equiv_dist; intros n; apply Hm.
    * intros n; split.
      + by intros m k.
      + by intros m1 m2 ? k.
      + by intros m1 m2 m3 ?? k; transitivity (m2 !! k).
    * by intros n m1 m2 ? k; apply dist_S.
    * by intros m1 m2 k.
    * intros c n k; unfold compl, map_compl; rewrite lookup_imap.
      destruct (decide (n = 0)) as [->|]; [constructor|].
      feed inversion (λ H, chain_cauchy c 1 n H k); simpl; auto with lia.
      by rewrite conv_compl; simpl; apply reflexive_eq.
  Qed.
  Global Instance lookup_ne `{Dist A} n k :
    Proper (dist n ==> dist n) (lookup k : M A  option A).
  Proof. by intros m1 m2. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
  Global Instance insert_ne `{Dist A} (i : K) n :
    Proper (dist n ==> dist n ==> dist n) (insert (M:=M A) i).
  Proof.
    intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_equality;
      [by constructor|by apply lookup_ne].
  Qed.
  Global Instance delete_ne `{Dist A} (i : K) n :
    Proper (dist n ==> dist n) (delete (M:=M A) i).
  Proof.
    intros m m' ? j; destruct (decide (i = j)); simplify_map_equality;
      [by constructor|by apply lookup_ne].
  Qed.
  Global Instance map_empty_timeless `{Dist A, Equiv A} : Timeless ( : M A).
  Proof.
    intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
    inversion_clear Hm; constructor.
  Qed.
  Global Instance map_lookup_timeless `{Cofe A} (m : M A) i :
    Timeless m  Timeless (m !! i).
  Proof.
    intros ? [x|] Hx; [|by symmetry; apply (timeless _)].
    rewrite (timeless m (<[i:=x]>m)), lookup_insert; auto.
    by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id.
  Qed.
  Global Instance map_ra_insert_timeless `{Cofe A} (m : M A) i x :
    Timeless x  Timeless m  Timeless (<[i:=x]>m).
  Proof.
    intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_equality.
    { by apply (timeless _); rewrite <-Hm, lookup_insert. }
    by apply (timeless _); rewrite <-Hm, lookup_insert_ne by done.
  Qed.
  Global Instance map_ra_singleton_timeless `{Cofe A} (i : K) (x : A) :
    Timeless x  Timeless ({[ i, x ]} : M A) := _.
118 119 120 121 122 123
  Instance map_fmap_ne `{Dist A, Dist B} (f : A  B) n :
    Proper (dist n ==> dist n) f  Proper (dist n ==> dist n) (fmap (M:=M) f).
  Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
  Definition mapC (A : cofeT) : cofeT := CofeT (M A).
  Definition mapC_map {A B} (f: A -n> B) : mapC A -n> mapC B :=
    CofeMor (fmap f : mapC A  mapC B).
Robbert Krebbers's avatar
Robbert Krebbers committed
124
  Global Instance mapC_map_ne {A B} n :
125 126
    Proper (dist n ==> dist n) (@mapC_map A B).
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
    intros f g Hf m k; simpl; rewrite !lookup_fmap.
128 129 130 131 132 133 134 135 136 137
    destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
  Qed.
End map.
Arguments mapC {_} _ {_ _ _ _ _ _ _ _ _} _.

Canonical Structure natmapC := mapC natmap.
Definition natmapC_map {A B}
  (f : A -n> B) : natmapC A -n> natmapC B := mapC_map f.
Canonical Structure PmapC := mapC Pmap.
Definition PmapC_map {A B} (f : A -n> B) : PmapC A -n> PmapC B := mapC_map f.
Robbert Krebbers's avatar
Robbert Krebbers committed
138 139 140
Canonical Structure gmapC K `{Countable K} := mapC (gmap K).
Definition gmapC_map `{Countable K} {A B}
  (f : A -n> B) : gmapC K A -n> gmapC K B := mapC_map f.