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:XY) (: YX)
    := x, x D (E x) === x.

  Lemma inverse_on_incl (D :set X) (E:XY) (:YX)
    : Dinverse_on D E inverse_on E .
  Proof.
    intros; firstorder.
  Qed.

  Lemma inverse_on_update (D:set X) (E:XY) (: YX) x
    : inverse_on D E
    → injective_on D E
    → x D
    → inverse_on D (E [x <- E x]) ( [E x <- x]).
  Proof.
    intros. hnf. intros. lud.
    eapply H2; eauto.
    exfalso; eapply H5; eauto.
    eapply H1; eauto.
  Qed.

  Lemma inverse_on_update_minus (D:set X) (E:XY) (: YX) x
    : inverse_on (D\{{x}}) E
    → injective_on (D {{x}}) E
    → inverse_on D (E [x <- E x]) ( [E x <- x]).
  Proof.
    intros. hnf. intros. lud.
    eapply H2; eauto; cset_tac; intuition.
    rewrite <- e. eapply H1. cset_tac; intuition.
    eapply H1. cset_tac; intuition.
  Qed.

  Lemma inverse_on_lookup_list lv ϱ ϱ´ L
    : inverse_on lv ϱ ϱ´
    → of_list L lv
    → lookup_list ϱ´ (lookup_list ϱ L) === L.
  Proof.
    general induction L; simpl; eauto.
    econstructor. eapply H1; eapply H2; simpl; eapply add_1; eauto.
    eapply IHL; eauto. hnf; intros. eapply H2. simpl. eapply add_2; eauto.
  Qed.

  Lemma update_with_list_proper (ϱ:XY) (ϱ´:YX) Z
    : Proper (_eq ==> _eq) ϱProper (_eq ==> _eq) ϱ´
      Proper (_eq ==> _eq) (update_with_list (lookup_list ϱ Z) Z ϱ´).
  Proof.
    intros; unfold Proper, respectful; intros. general induction Z; simpl.
    rewrite H3. eauto.
    lud. exfalso. eapply H6. eauto. exfalso; eauto.
    eapply IHZ. intuition. intuition. eauto.
  Qed.
End MapInverse.

Arguments inverse_on {X} {H} {Y} D E .

Lemma inverse_on_lookup_list_eq {X} `{OrderedType X} {Y} `{OrderedType Y}
  lv (ϱ:XY) (ϱ´:YX) Z `{Proper _ (_eq ==> _eq) ϱ} `{Proper _ (_eq ==> _eq) ϱ´}
: inverse_on lv ϱ ϱ´
  → of_list Z lv
  → @fpeq _ _ _eq _ _ (update_with_list (lookup_list ϱ Z) Z ϱ´) ϱ´.
Proof.
  general induction Z; simpl; eauto. split. reflexivity. eauto.
  split. edestruct IHZ; eauto.
  + hnf; intros. eapply H4; simpl; eapply add_2; eauto.
  + decompose records. erewrite H5; eauto. intro.
    lud. rewrite <- H3. rewrite e. reflexivity.
    eapply H4; simpl; eapply add_1; eauto.
  + split. hnf; intros.
    lud; isabsurd.
    eapply update_with_list_proper; intuition.
    intuition.
Qed.

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.
Proof.
  unfold Proper, respectful, flip, impl; intros; hnf; intros.
  destruct H2 as [A [B C]]. destruct H3 as [ [ ]].
  setoid_rewrite <- H4 at 3. hnf in . rewrite .
  hnf in A. rewrite A. eauto. eapply H1; eauto.
Qed.

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.
Proof.
  unfold Proper, respectful, flip, impl; intros.
  split; intros; eapply inverse_on_morphism; eauto.
  rewrite H1; reflexivity.
  destruct H2; split; eauto. symmetry; eauto. intuition.
  destruct H3; split; eauto. symmetry; eauto. intuition.
Qed.

Global Instance inverse_on_morphism_eq {X} `{OrderedType X} {Y}
  : Proper (Subset ==> eq ==> eq ==> flip impl) (@inverse_on X _ Y).
Proof.
  unfold Proper, respectful, flip, impl; intros; hnf; intros.
  subst. setoid_rewrite <- H3 at 3. reflexivity. eapply H0; eauto.
Qed.

Global Instance inverse_on_morphism_eq_eq {X} `{OrderedType X} {Y}
  : Proper (Equal ==> eq ==> eq ==> flip impl) (@inverse_on X _ Y).
Proof.
  unfold Proper, respectful, flip, impl; intros; hnf; intros.
  subst. setoid_rewrite <- H3 at 3. reflexivity. eapply H0; eauto.
Qed.

Global Instance inverse_on_morphism_full_eq {X} `{OrderedType X} {Y} `{OrderedType Y}
  : Proper (Equal ==> eq ==> eq ==> iff) (@inverse_on X _ Y).
Proof.
  unfold Proper, respectful, flip, impl; split; intros; hnf; intros; subst.
  - rewrite H4; eauto. rewrite H1; eauto.
  - rewrite H1 in H5; eauto.
Qed.

Lemma inverse_on_update_with_list {X} `{OrderedType X} {Y} `{OrderedType Y}
  (ϱ:XY) (ϱ´:YX) 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 ϱ´).
Proof.
  intros.
  hnf; intros.
  decide (x of_list Z). clear H4.
  induction Z. exfalso. simpl in i. eapply not_in_empty in i; eauto.
  simpl. lud. eapply H3; eauto. simpl. eapply union_3. intuition.
  eapply union_2; eauto. eapply IHZ. eapply injective_on_incl; eauto.
  eapply incl_union_lr; eauto. simpl. intuition. simpl in i.
  eapply add_3; eauto. decide (a === x); eauto. exfalso. eapply H4.
  rewrite e; reflexivity.

  assert (ϱ x of_list(lookup_list ϱ Z)).
  rewrite of_list_lookup_list; eauto. rewrite lookup_set_spec; eauto.
  intro; dcr.
  eapply H3 in H9; eauto; cset_tac; intuition.
  erewrite update_with_list_no_update; eauto. eapply H4; eauto using in_in_minus.
Qed.

Lemma inverse_on_union {X} `{OrderedType X} {Y} (f:XY) (g:YX) D
  : inverse_on D f g
  → inverse_on f g
  → inverse_on (D ) f g.
Proof.
  intros. hnf; intros. cset_tac. destruct H2; eauto.
Qed.

Lemma lookup_list_inverse_on {X} `{OrderedType X} {Y} `{OrderedType Y} f g
  `{Proper _ (_eq ==> _eq) f} `{Proper _ (_eq ==> _eq) g} L
  : lookup_list f L ===
  → lookup_list g === L
  → inverse_on (of_list L) f g.
Proof.
  intros. general induction L; simpl in ×.
  hnf; intros. exfalso; cset_tac; eauto.
  hnf; intros. eapply add_iff in H5. destruct H5.
  destruct ; simpl in *; inv H3; inv H4.
  rewrite <- H5. rewrite H9. eauto.
  inv H3; eauto; inv H4; eapply IHL; try eassumption.
Qed.

Lemma update_with_list_inverse_on {X} `{OrderedType X} {Y} `{OrderedType Y} (f:XY) (g:YX) D Z
  : length Z = length
  → inverse_on D (update_with_list Z f) (update_with_list Z g)
  → inverse_on (D \ of_list Z) f g.
Proof.
  intros.
  hnf; intros. cset_tac.
  pose proof (H2 _ H4).
  erewrite update_with_list_no_update in H3; eauto.
  erewrite update_with_list_no_update in H3; eauto.
  intro. erewrite update_with_list_no_update in H6; eauto.
  rewrite (update_with_list_no_update _ _ _ H5) in H3; eauto.
  eapply H5. rewrite <- H3. eapply update_with_list_lookup_in; eauto using length_eq_sym.
Qed.

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.
Proof.
  intros; hnf; intros.
  eapply lookup_set_spec in H3. destruct H3; dcr.
  rewrite H5. eapply H0. eapply H2. eauto. eauto.
Qed.

Lemma inverse_on_agree_on_2 {X} `{OrderedType X} {Y} `{OrderedType Y}
  D (f : XY) (g : YX) `{Proper _ (_eq ==> _eq) f} `{Proper _ (_eq ==> _eq) g}
`{Proper _ (_eq ==> _eq) } `{Proper _ (_eq ==> _eq) }
 : inverse_on D f g
   → inverse_on D
   → agree_on _eq D f
   → agree_on _eq (lookup_set f D) g .
Proof.
  intros. unfold agree_on. intros.
  eapply lookup_set_spec in H8; eauto. destruct H8; dcr.
  rewrite H10 at 1. assert (f x0 === x0). eapply H7; eauto.
  rewrite H8 in H10.
  rewrite H10. rewrite H5; eauto. rewrite H6; eauto.
Qed.

Lemma inverse_on_agree_on {X} `{OrderedType X} {Y} `{OrderedType Y}
      (f : XY) (g : YX) (G:set X)
 `{Proper _ (_eq ==> _eq) f}
 `{Proper _ (_eq ==> _eq) }
  : inverse_on G f g
    → agree_on _eq G f
    → agree_on _eq (lookup_set f G) g
    → inverse_on G .
Proof.
  intros; hnf; intros.
  hnf in H4. rewrite <- H4; eauto.
  hnf in H5. rewrite <- H5; eauto.
  eapply lookup_set_spec; eauto.
Qed.

Lemma inverse_on_injective_on {X} `{OrderedType X} {Y} `{OrderedType Y}
      (f: XY) (g: YX) `{Proper _ (_eq ==> _eq) g} G
  : inverse_on G f ginjective_on G f.
Proof.
  intros; hnf; intros. hnf in H1. rewrite <- H2.
  rewrite H1; eauto. eauto.
Qed.

Lemma inverse_on_id {X} `{OrderedType X} (G:set X)
  : inverse_on G id id.
Proof.
  intros. hnf; intros. reflexivity.
Qed.

Lemma inverse_on_update_fresh X `{OrderedType X} (D:set X) (Z :list X) (ϱ ϱ´ : XX) `{Proper _ (_eq ==> _eq) ϱ}
 : inverse_on (D \ of_list Z) ϱ ϱ´
  → unique
  → length Z = length
  → disj (of_list ) (lookup_set ϱ (D \ of_list Z))
  → inverse_on D (update_with_list Z ϱ)
                 (update_with_list Z ϱ´).
Proof.
  intros. eapply length_length_eq in H3.
  hnf; intros. lud. decide(x of_list Z).
  general induction H3; simpl in *; eauto; dcr. cset_tac; exfalso; eauto.
  lud. eapply add_iff in i. destruct i; eauto.
  assert (y of_list YL). rewrite e.
  eapply update_with_list_lookup_in; eauto using length_eq_length.
  exfalso. eapply (fresh_of_list H6 H11).
  exfalso; eauto.
  eapply add_iff in i; destruct i; isabsurd.
  eapply IHlength_eq; try eassumption.
  hnf; intros. exfalso; cset_tac; eauto.
  hnf; intros. split; intros. cset_tac. eapply lookup_set_spec in H14; dcr.
  cset_tac; intuition. intuition. cset_tac; intuition.

  erewrite update_with_list_no_update; eauto.
  erewrite update_with_list_no_update; eauto.
  eapply H1; eauto. cset_tac ; eauto.
  erewrite update_with_list_no_update; eauto. intro.
  specialize (H4 (ϱ x)). cset_tac; intuition; eauto.
  eapply H7.
  eapply lookup_set_spec; cset_tac; intuition.
  eexists x; eauto.
Qed.

Lemma inverse_on_dead_update X `{OrderedType X} Y `{OrderedType Y} (ra:XY) ira (x:X) (y:Y) s
: inverse_on s (update ra x y) (update ira y x)
  → inverse_on (s \ {{x}}) ra ira.
Proof.
  intros. hnf; intros. cset_tac; dcr.
  specialize (H1 _ H3). lud; intuition.
Qed.