# Lvc.Constr.MapInjectivity

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']
end.

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.
Proof.
firstorder.
Qed.

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]).
Proof.
intros; hnf; intros. lud; eauto.
+ exfalso; cset_tac.
+ exfalso; cset_tac.
Qed.

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]).
Proof.
intros. hnf; intros. lud.
+ exfalso; lset_tac.
+ exfalso; lset_tac.
+ eapply H2; cset_tac.
Qed.

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

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).
Proof.
intros; hnf; intros. lset_tac.
eapply H4. rewrite H2; cset_tac. eqs.
Qed.

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).
Proof.
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.
Qed.

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.
Proof.
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.
Qed.

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).
Proof.
intros; hnf; intros. lset_tac. lud.
- exfalso; eauto.
- exfalso; eauto.
- eapply H2; cset_tac; eauto.
Qed.

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'.
Proof.
intros. lset_tac. specialize (H3 _ H7). cset_tac.
Qed.

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).
Proof.
intros. lset_tac.
Qed.

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}
f
: transpose _eq (@injective_on_step X Y _ f).
Proof.
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.
Qed.

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)).
Proof.
intros. unfold injective_on_step in ×.
destruct b. unfold snd in ×. unfold fst; reflexivity.
reflexivity.
Qed.

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).
Proof.
unfold Proper, respectful; intros.
inv H3. econstructor.
- simpl. rewrite H4.
- inv H5; simpl. cases; trivial.
f_equal.
decide (f x a); decide (f y c); simpl; trivial.
exfalso; eapply n; rewrite <- H2, <- H4; eauto.
exfalso; eapply n; rewrite H2, H4; eauto.
Qed.

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).
Proof.
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.
Qed.

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)).
Proof.
intros.
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.
lset_tac.
exfalso; eauto.
- destruct a; simpl in ×.
rewrite <- H5; clear H5. eapply Add_Equal in H4.
rewrite H4; clear H4.
lset_tac.
Qed.

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)).
Proof.
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.

simpl_pair_eqs.
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).
simpl_pair_eqs.
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.
Qed.

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).
Proof.
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.
isabsurd.
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.
Defined.

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).
Proof.
split; intros. eapply lookup_set_minus_incl_inj; eauto.
apply lookup_set_minus_incl; eauto.
Qed.

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

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]).
Proof.
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.
Qed.