Lvc.Constr.MapUpdate

Require Export Setoid Coq.Classes.Morphisms.
Require Import EqDec Computable Util LengthEq AutoIndTac Get LengthEq.
Require Export CSet Containers.SetDecide.
Require Export MapBasics MapLookup MapAgreement.

Set Implicit Arguments.

Section MapUpdate.
  Open Scope fmap_scope.
  Variable X : Type.
  Context `{OrderedType X}.
  Variable Y : Type.

  Fixpoint update_list (m:X → Y) (f:X → Y) (L:list X) :=
    match L with
      | nil ⇒ m
      | x::L ⇒ (update_list m f L) [x <- f x]
    end.

  Lemma update_list_agree_minus {R} `{Symmetric Y R} `{Transitive Y R} lv (E E´ f:X → Y) XL
  : agree_on R lv E´ E
     → agree_on R (lv\of_list XL) (update_list E´ f XL) E.

  Corollary update_list_agree_self {R} `{Equivalence Y R} lv (E:X → Y) L f
    : agree_on R (lv\of_list L) (update_list E f L) E.

  Lemma update_list_no_upd (m:X → Y) f L x
    : x ∉ of_list L
    → (update_list m f L) x === m x.

  Lemma update_list_upd R `{Equivalence Y R} (m:X → Y) f L x
    : x ∈ of_list L
    → Proper (_eq ==> R) f
    → (update_list m f L) x === f x.

End MapUpdate.

Section MapUpdateList.
  Variable X : Type.
  Context `{OrderedType X}.
  Variable Y : Type.

  Open Scope fmap_scope.

  Fixpoint update_with_list XL YL (m:X → Y) :=
    match XL, YL with
      | x::XL, y::YL ⇒ (update_with_list XL YL m)[x <- y]
      | _, _ ⇒ m
    end.

  Notation "f [ w <-- x ]" := (update_with_list w x f) (at level 29, left associativity).

  Lemma update_unique_commute `{OrderedType Y} (XL:list X) (VL:list Y) E D x y
  : length XL = length VL
    → unique (x::XL)
    → agree_on _eq D (E [x <- y] [XL <-- VL]) (E [XL <-- VL] [x <- y]).


  Context `{Equivalence Y}.

  Lemma update_with_list_agree lv (E E´:X → Y) XL YL
    : agree_on R (lv\of_list XL) E E´
    → length XL = length YL
    → agree_on R lv (E [ XL <-- YL]) (E´ [ XL <-- YL ]).

  Lemma update_with_list_no_update (E:X → Y) Y´ Z x
    : x ∉ of_list Z
    → (E [ Z <-- Y´ ]) x = E x.

  Lemma update_with_list_agree_minus lv (E E´:X → Y) XL YL
    : length XL = length YL
    → agree_on R lv E´ E
    → agree_on R (lv\of_list XL) (E´ [ XL <-- YL ]) E.

  Hint Resolve minus_single_singleton minus_single_singleton´ minus_single_singleton´´.

  Lemma update_with_list_agree_inv lv (E E´:X → Y) XL YL
  : length XL = length YL
    → agree_on R lv (E´ [ XL <-- YL ]) E
    → agree_on R (lv\of_list XL) E´ E.

  Lemma update_with_list_agree_self `{Defaulted X} lv (E:X → Y) XL YL
    : agree_on R (lv\of_list XL) (E [ XL <-- YL]) E.

  Lemma update_id `{OrderedType Y} (m:X → Y) x `{Proper _ (_eq ==> _eq) m}
    : @feq _ _ _eq (m [x <- m x]) m.

End MapUpdateList.

Notation "f [ w <-- x ]" := (update_with_list w x f) (at level 29, left associativity).

Lemma update_with_list_lookup_in_list X `{OrderedType X} B E
      (Z:list X) (Y:list B) z
: length Z = length Y
  → z ∈ of_list Z
  → ∃ n y z´, get Z n z´ ∧ get Y n y ∧ E [Z <-- Y] z === y ∧ z === z´.

Instance update_inst X `{OrderedType X} Y `{OrderedType Y} :
  Proper ((@feq _ _ _eq) ==> _eq ==> _eq ==> (@feq _ _ _eq)) (@update X Y _).

Lemma update_with_list_id X `{OrderedType X} (l:list X)
  : @feq _ _ _eq (update_with_list l l id) id.

Lemma update_with_list_lookup_in {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y) Z Z´ x
  : length Z = length Z´
  → x ∈ of_list Z
  → f [ Z <-- Z´ ] x ∈ of_list Z´.

Instance proper_update X `{OrderedType X} Y `{OrderedType Y} (ϱ:X → Y) (x : X) (y :Y)
: Proper (_eq ==> _eq) ϱ
  → Proper (_eq ==> _eq) (update ϱ x y).

Instance proper_update_with_list X `{OrderedType X} Y `{OrderedType Y} (f:X→Y) Z Z´
: Proper (_eq ==> _eq) f
  → Proper (_eq ==> _eq) (f [Z <-- Z´]).

Lemma lookup_set_update_not_in_Z´ X `{OrderedType X} Y `{OrderedType Y}
  Z Z´ (f: X→ Y) x
  : f [Z <-- Z´] x ∉ of_list Z´ → f [Z <-- Z´] x = f x.

Lemma lookup_set_update_not_in_Z X `{OrderedType X} Y
  Z Z´ (f: X→ Y) x
  : x ∉ of_list Z → f [Z <-- Z´] x = f x.

Lemma lookup_set_update_not_in_Z´_not_in_Z {X} `{OrderedType X} {Y} `{OrderedType Y}
  (f: X→ Y) `{Proper _ (_eq ==> _eq) f} x Z Z´
: length Z = length Z´
  → f [Z <-- Z´] x ∉ of_list Z´ → x ∉ of_list Z.

Lemma update_with_list_lookup_not_in {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y) (Z:list X) (Z´:list Y) x y
  : x ∉ of_list Z
    → f [ Z <-- Z´ ] x === y
    → f x === y.

Lemma update_with_list_lookup_set_incl {X} `{OrderedType X} {Y} `{OrderedType Y}
(f:X→Y) Z Z´ `{Proper _ (_eq ==> _eq) f} D
  : length Z = length Z´
  → D ⊆ of_list Z
  → lookup_set (f [ Z <-- Z´ ]) D ⊆ of_list Z´.

Instance update_list_morphism {X} `{OrderedType X} {Y} `{OrderedType Y}
  : Proper (@feq X _ _eq ==> @feq X _ _eq ==> eq ==> (@feq _ _ _eq)) (@update_list X _ Y).

Lemma lookup_set_add_update {X} `{OrderedType X} {Y} `{OrderedType Y} (ϱ:X→Y) D x y
      `{Proper _ (_eq ==> _eq) ϱ}
: x ∉ D
  → lookup_set (update ϱ x y) {x; D} [=] {y; lookup_set ϱ D}.

Lemma lookup_update_same X `{OrderedType X} x Z (ϱ:X→X)
: x ∈ of_list Z
  → ϱ [Z <-- Z] x === x.

Hint Resolve proper_update proper_update_with_list.

Lemma lookup_set_update_union_minus X `{OrderedType X} Y `{OrderedType Y}
 (f: X→Y) D x y `{Proper _ (_eq ==> _eq) f}
  : lookup_set (update f x y) D \ {{y}} [=] lookup_set f (D \ {{x}}) \ {{ y }}.

Lemma lookup_set_update_union_minus_list X `{OrderedType X} Y `{OrderedType Y}
 (f:X→Y) D Z Z´ `{Proper _ (_eq ==> _eq) f}
: length Z = length Z´
  → lookup_set (f[ Z <-- Z´]) D \ of_list Z´ [=] lookup_set f (D \ of_list Z) \ of_list Z´.

Lemma update_with_list_lookup_list {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
      `{Proper _ (_eq ==> _eq) f} Z Z´
: length Z = length Z´
  → unique Z
  → lookup_set (f [ Z <-- Z´ ]) (of_list Z) ⊆ of_list Z´.