Lvc.Constr.MapInverse

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

Set Implicit Arguments.

Require Import MapBasics MapInjectivity MapLookupList.

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

  Open Scope fmap_scope.

  Definition inverse_on (D:set X) (E:X → Y) (E´: Y → X)
    := ∀ x, x ∈ D → E´ (E x) === x.

  Lemma inverse_on_incl (D D´:set X) (E:X → Y) (E´:Y → X)
    : D´ ⊆ D → inverse_on D E E´ → inverse_on D´ E E´.

  Lemma inverse_on_update (D:set X) (E:X → Y) (E´: Y → X) x
    : inverse_on D E E´
    → injective_on D E
    → x ∈ D
    → inverse_on D (E [x <- E x]) (E´ [E x <- x]).

  Lemma inverse_on_update_minus (D:set X) (E:X → Y) (E´: Y → X) x
    : inverse_on (D\{{x}}) E E´
    → injective_on (D ∪ {{x}}) E
    → inverse_on D (E [x <- E x]) (E´ [E x <- x]).

  Lemma inverse_on_lookup_list lv ϱ ϱ´ L
    : inverse_on lv ϱ ϱ´
    → of_list L ⊆ lv
    → lookup_list ϱ´ (lookup_list ϱ L) === L.

  Lemma update_with_list_proper (ϱ:X→Y) (ϱ´:Y→X) Z
    : Proper (_eq ==> _eq) ϱ → Proper (_eq ==> _eq) ϱ´ →
      Proper (_eq ==> _eq) (update_with_list (lookup_list ϱ Z) Z ϱ´).
End MapInverse.


Lemma inverse_on_lookup_list_eq {X} `{OrderedType X} {Y} `{OrderedType Y}
  lv (ϱ:X→Y) (ϱ´:Y→X) Z `{Proper _ (_eq ==> _eq) ϱ} `{Proper _ (_eq ==> _eq) ϱ´}
: inverse_on lv ϱ ϱ´
  → of_list Z ⊆ lv
  → @fpeq _ _ _eq _ _ (update_with_list (lookup_list ϱ Z) Z ϱ´) ϱ´.

Global Instance inverse_on_morphism {X} `{OrderedType X} {Y} `{OrderedType Y}
  : Proper (Subset ==> (@fpeq X Y _eq _ _)==> (@fpeq Y X _eq _ _) ==> flip impl) inverse_on.

Global Instance inverse_on_morphism_full {X} `{OrderedType X} {Y} `{OrderedType Y}
  : Proper (Equal ==> (@fpeq X Y _eq _ _)==> (@fpeq Y X _eq _ _) ==> iff) inverse_on.

Global Instance inverse_on_morphism_eq {X} `{OrderedType X} {Y}
  : Proper (Subset ==> eq ==> eq ==> flip impl) (@inverse_on X _ Y).

Global Instance inverse_on_morphism_eq_eq {X} `{OrderedType X} {Y}
  : Proper (Equal ==> eq ==> eq ==> flip impl) (@inverse_on X _ Y).

Global Instance inverse_on_morphism_full_eq {X} `{OrderedType X} {Y} `{OrderedType Y}
  : Proper (Equal ==> eq ==> eq ==> iff) (@inverse_on X _ Y).

Lemma inverse_on_update_with_list {X} `{OrderedType X} {Y} `{OrderedType Y}
  (ϱ:X→Y) (ϱ´:Y→X) Z lv `{Proper _ (_eq ==> _eq) ϱ} `{Proper _ (_eq ==> _eq) ϱ´}
: injective_on (lv ∪ of_list Z) ϱ
  → inverse_on (lv \ of_list Z) ϱ ϱ´
  → inverse_on (lv) ϱ (update_with_list (lookup_list ϱ Z) Z ϱ´).

Lemma inverse_on_union {X} `{OrderedType X} {Y} (f:X→Y) (g:Y→X) D D´
  : inverse_on D f g
  → inverse_on D´ f g
  → inverse_on (D ∪ D´) f g.

Lemma lookup_list_inverse_on {X} `{OrderedType X} {Y} `{OrderedType Y} f g
  `{Proper _ (_eq ==> _eq) f} `{Proper _ (_eq ==> _eq) g} L L´
  : lookup_list f L === L´
  → lookup_list g L´ === L
  → inverse_on (of_list L) f g.

Lemma update_with_list_inverse_on {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y) (g:Y→X) D Z Z´
  : length Z = length Z´
  → inverse_on D (update_with_list Z Z´ f) (update_with_list Z´ Z g)
  → inverse_on (D \ of_list Z) f g.

Lemma inverse_on_sym {X} `{OrderedType X} D f g
  `{Proper _ (_eq ==> _eq) f} `{Proper _ (_eq ==> _eq) g}
  : inverse_on D f g
  → inverse_on (lookup_set f D) g f.

Lemma inverse_on_agree_on_2 {X} `{OrderedType X} {Y} `{OrderedType Y}
  D (f f´ : X → Y) (g g´: Y → X) `{Proper _ (_eq ==> _eq) f} `{Proper _ (_eq ==> _eq) g}
`{Proper _ (_eq ==> _eq) f´} `{Proper _ (_eq ==> _eq) g´}
 : inverse_on D f g
   → inverse_on D f´ g´
   → agree_on _eq D f f´
   → agree_on _eq (lookup_set f D) g g´.

Lemma inverse_on_agree_on {X} `{OrderedType X} {Y} `{OrderedType Y}
      (f f´: X → Y) (g g´: Y → X) (G:set X)
 `{Proper _ (_eq ==> _eq) f}
 `{Proper _ (_eq ==> _eq) g´}
  : inverse_on G f g
    → agree_on _eq G f f´
    → agree_on _eq (lookup_set f G) g g´
    → inverse_on G f´ g´.

Lemma inverse_on_injective_on {X} `{OrderedType X} {Y} `{OrderedType Y}
      (f: X → Y) (g: Y → X) `{Proper _ (_eq ==> _eq) g} G
  : inverse_on G f g → injective_on G f.

Lemma inverse_on_id {X} `{OrderedType X} (G:set X)
  : inverse_on G id id.

Lemma inverse_on_update_fresh X `{OrderedType X} (D:set X) (Z Z´:list X) (ϱ ϱ´ : X → X) `{Proper _ (_eq ==> _eq) ϱ}
 : inverse_on (D \ of_list Z) ϱ ϱ´
  → unique Z´
  → length Z = length Z´
  → disj (of_list Z´) (lookup_set ϱ (D \ of_list Z))
  → inverse_on D (update_with_list Z Z´ ϱ)
                 (update_with_list Z´ Z ϱ´).

Lemma inverse_on_dead_update X `{OrderedType X} Y `{OrderedType Y} (ra:X→Y) ira (x:X) (y:Y) s
: inverse_on s (update ra x y) (update ira y x)
  → inverse_on (s \ {{x}}) ra ira.