Require Import EqDec Computable Util AutoIndTac LengthEq.
Require Export CSet Containers.SetDecide.
Require Export MapBasics MapUpdate MapLookup OrderedTypeEx.

Set Implicit Arguments.

Hint Extern 5 ⇒
match goal with
| [ H : ?s === ?f ?y, H' : ?x === ?y |- ?f ?x === ?s ] ⇒ rewrite H'; symmetry; eapply H
| [ H : ?s === ?f ?y, H' : ?x === ?y |- ?s === ?f ?x ] ⇒ rewrite H'; eapply H
| [ H : ?f ?y === ?s, H' : ?x === ?y |- ?f ?x === ?s ] ⇒ rewrite H'; eapply H
| [ H : ?f ?y === ?s, H' : ?y === ?x |- ?f ?x === ?s ] ⇒ rewrite <- H'; eapply H
| [ H : ?x === ?y, H' : ?y === ?z |- ?x === ?z ] ⇒ transitivity y; [eapply H | eapply H']

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

  Definition injective_on D (f:XY) :=
     x y, x D y D f x === f y x === y.

  Lemma injective_on_incl (D D':set X) (f:X Y)
    : injective_on D f D' D injective_on D' f.

  Lemma injective_on_dead lv (f:X Y) x v `{Proper _ (respectful _eq _eq) f}
  : injective_on (lv\ singleton x) f
     injective_on (lv\ singleton x) (f[x<-v]).
    intros; hnf; intros. lud; eauto.
    + exfalso; cset_tac.
    + exfalso; cset_tac.

  Lemma injective_on_fresh lv (f:X Y) x xr `{Proper _ (_eq ==> _eq) f}
    : injective_on (lv\ singleton x) f
       ¬xr lookup_set f (lv\ singleton x)
       injective_on {x; lv} (f[x <- xr]).
    intros. hnf; intros. lud.
    + exfalso; lset_tac.
    + exfalso; lset_tac.
    + eapply H2; cset_tac.

  Lemma injective_on_forget s (f:X Y) y `{Proper _ (_eq ==> _eq) f}
  : injective_on s f
     injective_on (s\ singleton y) f.
    intros. hnf; intros.

  Lemma lookup_set_minus_incl_inj s t (m:X Y) `{Proper _ (_eq ==> _eq) m}
  : injective_on (s t) m
     lookup_set m (s \ t) lookup_set m s \ (lookup_set m t).
    intros; hnf; intros. lset_tac.
    eapply H4. rewrite H2; cset_tac. eqs.

End MapInjectivity.

Global Instance injective_on_morphism {X} `{OrderedType X} {Y} {HY:OrderedType Y}
  : Proper (Equal ==> (@feq X Y (@_eq Y HY)) ==> iff) (@injective_on X H Y HY).
  unfold Proper, respectful; intros.
  split; intros; hnf; intros.
  + eapply H2; try rewrite H0 ; eauto.
    hnf in H1. repeat rewrite H1. eauto.
  + rewrite H0 in ×. eapply H2; cset_tac; eauto.
    hnf in H1. repeat rewrite <- H1. eauto.

Lemma injective_on_update_not_in {X} `{OrderedType X} {Y} `{OrderedType Y}
  D x (f:X Y) `{Proper _ (_eq ==> _eq) f}
: injective_on (D \ singleton x) f
   f x lookup_set f (D \ singleton x)
   injective_on D f.
  intros; hnf; intros.
  decide(x0 === x); decide (x0 === y); eauto.
  - exfalso. lset_tac. eapply H3.
    eexists y. cset_tac; eauto.
  - eapply H2; lset_tac; eauto.
    eapply H3; eauto.

Lemma injective_on_update_fresh {X} `{OrderedType X} {Y} `{OrderedType Y}
  D x y f `{Proper _ (_eq ==> _eq) f}
: injective_on (D \ singleton x) f
   y lookup_set f (D \ singleton x)
   injective_on D (update f x y).
  intros; hnf; intros. lset_tac. lud.
  - exfalso; eauto.
  - exfalso; eauto.
  - eapply H2; cset_tac; eauto.

Lemma injective_on_not_in_lookup_set {X} `{OrderedType X} {Y} `{OrderedType Y} f D D' x
    `{Proper _ (_eq ==> _eq) f}
    : injective_on D f
       D' D\ singleton x x D
       f x lookup_set f D'.
  intros. lset_tac. specialize (H3 _ H7). cset_tac.

Lemma lookup_set_not_in {X} `{OrderedType X} {Y} `{OrderedType Y} f D x
    `{Proper _ (_eq ==> _eq) f}
  : f x lookup_set f D
     lookup_set f D \ singleton (f x) [=] lookup_set f (D\ singleton x).
  intros. lset_tac.

Definition injective_on_step {X} {Y} `{OrderedType Y}
f (x : X) (p : set Y × bool) :=
      ({f x; fst p}, if snd p then
        negb (sumbool_bool (@decision_procedure (f x fst p) _))
       else false).

Lemma injective_on_step_transpose {X} {Y} `{OrderedType Y}
  : transpose _eq (@injective_on_step X Y _ f).
  hnf; intros.
  unfold injective_on_step. econstructor.
  - destruct z; simpl. econstructor; cset_tac; intuition.
  - destruct z. unfold snd. destruct b; eauto.
    unfold fst, snd.
    decide (f y s); decide (f x s); simpl; try reflexivity;
      decide (f x {f y; s}); decide (f y {f x; s}); simpl; try reflexivity;
        exfalso; cset_tac.

Lemma injective_on_step_spec {X} `{OrderedType X} {Y} `{OrderedType Y}
f (x : X) (p : set Y × bool) (s:set Y) b
: snd (injective_on_step f x (s,b))
    {f x; s} [=] fst (injective_on_step f x (s,b)).
  intros. unfold injective_on_step in ×.
  destruct b. unfold snd in ×. unfold fst; reflexivity.

Instance injective_on_step_proper
  {X} `{OrderedType X} {Y} `{OrderedType Y} (f:XY)
  `{Proper _ (_eq ==> _eq) f}
 : Proper (_eq ==> _eq ==> _eq) (injective_on_step f).
  unfold Proper, respectful; intros.
  inv H3. econstructor.
  - simpl. rewrite H4.
    eapply add_m; eauto.
  - inv H5; simpl. cases; trivial.
    decide (f x a); decide (f y c); simpl; trivial.
    exfalso; eapply n; rewrite <- H2, <- H4; eauto.
    exfalso; eapply n; rewrite H2, H4; eauto.

Instance injective_on_step_proper'
  {X} `{OrderedType X} {Y} `{OrderedType Y} (f:XY)
  `{Proper _ (_eq ==> eq) f}
 : Proper (_eq ==> eq ==> eq) (injective_on_step f).
  unfold Proper, respectful; intros; subst.
  destruct y0; unfold injective_on_step; simpl.
  rewrite (H1 _ _ H2).
  decide (f x s); decide (f y s); simpl; trivial.

Definition injective_on_compute {X} `{OrderedType X} {Y} `{OrderedType Y}
  (D:set X) (f: X Y) `{Proper _ (_eq ==> _eq) f} : bool
  := snd (fold (injective_on_step f) D (, true)).

Lemma injective_on_compute_lookup_set {X} `{OrderedType X} {Y} `{OrderedType Y}
   (f: X Y) `{Proper _ (_eq ==> _eq) f}
   D LD',
    lookup_set f D LD' [=] fst (fold (injective_on_step f) D (LD', true)).
  eapply (@fold_rec _ _ _ _ _ (fun (D:set X) (fld:set Y × bool) ⇒
          lookup_set f D LD' [=] fst fld
         ) _ (LD', true)); intros; simpl.

  - eapply empty_is_empty_1 in H2.
    exfalso; eauto.
  - destruct a; simpl in ×.
    rewrite <- H5; clear H5. eapply Add_Equal in H4.
    rewrite H4; clear H4.

Definition injective_on_iff {X} `{OrderedType X} {Y} `{OrderedType Y}
   (f: X Y) `{Proper _ (_eq ==> _eq) f} D
: D' LD',
    D' D [=]
     lookup_set f D' [=] LD'
     injective_on D' f
     (snd (fold (injective_on_step f) D (LD', true)) (injective_on (D D') f)).
  pattern D. eapply set_induction; intros.
  - eapply empty_is_empty_1 in H2. intuition. eapply injective_on_incl; eauto.
    rewrite H2. cset_tac; intuition.
    pose proof (@fold_equal X _ _ _ _ _ _ (injective_on_step f) _ (injective_on_step_transpose f) (LD', true) _ _ H2).
    rewrite fold_empty in H7.
    destruct (fold (injective_on_step f) s (LD', true)).
    inv H7. inv H13. eapply I.
  - pose proof H4 as FOO. eapply Add_Equal in H4.
     pose proof (@fold_equal X _ _ _ _ _ _ (injective_on_step f) _ (injective_on_step_transpose f) (LD', true) _ _ H4).
     destruct (fold (injective_on_step f) s' (LD', true)).
     rewrite (@fold_add X _ _ _ _ _ _ (injective_on_step f) (injective_on_step_proper f) (injective_on_step_transpose f) (LD', true) _ _ H3) in H8.

     decide (x D'). exfalso. destruct (FOO x).
     cset_tac; intuition.
     assert (D' s [=] ).
     revert H5. rewrite H4. clear_all; cset_tac; intuition.

  specialize (H2 D' _ H9 H6 H7).
  case_eq (fold (injective_on_step f) s (LD', true)); intros; rewrite H10 in ×.
  unfold injective_on_step in H8. unfold fst in H8.
  decide (f x s1).
  destruct b. try now (destruct b0; simpl in *; inv H8; isabsurd).
  simpl; split; intros; isabsurd.

  pose proof (injective_on_compute_lookup_set s LD').
  rewrite H12 in H10. clear H8.
  rewrite <- H10 in i. rewrite <- H6 in i. rewrite <- lookup_set_union in i.
  eapply lookup_set_spec in i. destruct i; dcr.
  eapply H11 in H15. cset_tac.
  rewrite H4; revert H14 H9; clear_all; intros. cset_tac; intuition.
  rewrite H4.
  revert H14 H9; clear_all; intros.
  cset_tac; intuition. eassumption. eassumption.

  destruct b, b0; try now (simpl in *; inv H8; isabsurd).
  simpl; split; intros; eauto.
  destruct H2. specialize (H2 I).
  pose proof (injective_on_compute_lookup_set s LD'). simpl.
  rewrite H13 in H10.
  clear H8.
  rewrite <- H10 in n0.
  rewrite <- H6 in n0. rewrite <- lookup_set_union in n0; eauto.
  assert (s D' [=] (s' D') \ singleton x).
  rewrite H4. clear H1 H2 H4 H6 H7 H10 H11 H12 H13 H14 n0 s0 FOO.
  cset_tac; intuition.
  rewrite H8 in n0. rewrite H8 in H2.
  pose proof (injective_on_update_not_in H2 n0); eauto.
  simpl in ×. split; [isabsurd|]; intros.
  eapply H2. eapply injective_on_incl; eauto.
  rewrite H4. eauto with cset.

Global Instance injective_on_computable {X} `{OrderedType X} {Y} `{OrderedType Y}
  (D:set X) (f: X Y) `{Proper _ (_eq ==> _eq) f} `{Proper _ (_eq ==> eq) f}
: Computable (injective_on D f).
  case_eq (@injective_on_compute X _ Y _ D f _); eauto; intros.
  left. pose proof (@injective_on_iff X _ Y _ f _ D ).
  destruct H4; eauto. cset_tac; intuition. isabsurd.
  unfold injective_on_compute in H3.
  rewrite H3 in H4. specialize (H4 I). eapply injective_on_incl ;eauto.
  cset_tac; eauto.
  right. intro.
  pose proof (@injective_on_iff X _ Y _ f _ D ).
  edestruct H5. cset_tac; intuition. cset_tac; intuition.
  change False with (Is_true false). rewrite <- H3.
  unfold injective_on_compute in H3. rewrite H3 in H7.
  unfold injective_on_compute. rewrite H3. eapply H7.
  eapply injective_on_incl; eauto with cset.

Lemma lookup_set_minus_eq X `{OrderedType X} Y `{OrderedType Y} s t (m:X Y) `{Proper _ (_eq ==> _eq) m}
: injective_on (s t) m
   lookup_set m (s \ t) [=] lookup_set m s \ (lookup_set m t).
  split; intros. eapply lookup_set_minus_incl_inj; eauto.
  apply lookup_set_minus_incl; eauto.

Lemma injective_on_agree X `{OrderedType X} Y `{OrderedType Y} D (ϱ ϱ': X Y)
: injective_on D ϱ
   agree_on _eq D ϱ ϱ'
   injective_on D ϱ'.
  intros. hnf; intros. eapply H1; eauto.
  exploit H2; eauto. rewrite H6.
  exploit H2; try eapply H3. rewrite H7. eauto.

Lemma injective_on_fresh_list X `{OrderedType X} Y `{OrderedType Y} XL YL (ϱ: X Y) `{Proper _ (_eq ==> _eq) ϱ} lv
: injective_on lv ϱ
   length XL = length YL
   (of_list YL) (lookup_set ϱ lv) [=]
   unique XL
   unique YL
   injective_on (lv of_list XL) (ϱ [XL <-- YL]).
  intros. eapply length_length_eq in H3.
  general induction H3; simpl in × |- × ; eauto.
  - eapply injective_on_incl; eauto with cset.
  - eapply injective_on_agree. instantiate (1:=ϱ [x <- y] [XL <-- YL]).
    + assert (lv { x; of_list XL} [=] {x; lv} of_list XL) by (cset_tac; eauto).
      rewrite H7. dcr.
      eapply IHlength_eq; eauto.
      × eapply injective_on_fresh; eauto.
        eapply injective_on_incl; eauto.
        lset_tac. eapply (H4 y). lset_tac.
      × rewrite lookup_set_add; eauto. lud; eauto.
        split; [| clear_all; cset_tac].
        rewrite <- H4. lset_tac.
        lud; eauto.
    + eapply update_unique_commute; eauto using length_eq_length.