Lvc.Constr.Map

Require Export Setoid Coq.Classes.Morphisms.
Require Import EqDec Computable Util AutoIndTac.
Require Export CSet Containers.SetDecide.

Require Export MapBasics MapLookup MapLookupList MapAgreement MapInjectivity MapUpdate MapAgreeSet MapInverse MapComposition.

Lemma inverse_on_update_lookup_set {X} `{OrderedType X} {Y} `{OrderedType Y} (D:set X) (f:X→Y) g
   `{Proper _ (_eq ==> _eq) f} x y
  : inverse_on D (f [x <- y]) (g [y <- x])
  → y ∉ lookup_set f (D\{{x}}).

Lemma lookup_set_update_with_list_in_union {X} `{OrderedType X} {Y} `{OrderedType Y}
  Z Z´ f D `{Proper _ (_eq ==> _eq) f}
  : lookup_set (update_with_list Z Z´ f) D ⊆ lookup_set f D ∪ of_list Z´.

Lemma lookup_set_update_in_union {X} `{OrderedType X} {Y} `{OrderedType Y}
 f D x y `{Proper _ (_eq ==> _eq) f}
  : lookup_set (f[x <- y]) D ⊆ lookup_set f (D \ {{x}}) ∪ {{y}}.

Lemma lookup_set_update_with_list_in_union_length {X} `{OrderedType X} {Y} `{OrderedType Y}
  Z Z´ f D `{Proper _ (_eq ==> _eq) f}
  : length Z = length Z´
    → lookup_set (update_with_list Z Z´ f) D ⊆ (lookup_set f (D \ of_list Z)) ∪ of_list Z´.

Lemma inverse_on_update_inverse {X} `{OrderedType X} {Y} `{OrderedType Y}
  D x y ϱ ϱ´ `{Proper _ (_eq ==> _eq) ϱ}
  : inverse_on (D\{{x}}) ϱ ϱ´
    → y ∉ lookup_set ϱ (D\{{x}})
    → inverse_on D (ϱ [x <- y]) (ϱ´ [y <- x]).