Lvc.Constr.MapInjectivity
Require Import EqDec Computable Util AutoIndTac LengthEq.
Require Export CSet Containers.SetDecide.
Require Export MapBasics MapUpdate MapLookup OrderedTypeEx.
Set Implicit Arguments.
Section MapInjectivity.
Open Scope fmap_scope.
Variable X : Type.
Context `{OrderedType X}.
Variable Y : Type.
Context `{OrderedType Y}.
Definition injective_on D (f:X→Y) :=
∀ 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\{{x}}) f
→ injective_on (lv\{{x}}) (f[x<-v]).
Proof.
intros; hnf; intros. lud; eauto.
+ exfalso; cset_tac; eauto.
+ exfalso; cset_tac; eauto.
Qed.
Lemma injective_on_fresh lv (f:X → Y) x xr `{Proper _ (_eq ==> _eq) f}
: injective_on (lv\{{x}}) f
→ ¬xr ∈ lookup_set f (lv\{{x}})
→ injective_on ({{x}} ∪ lv) (f[x <- xr]).
Proof.
intros. hnf; intros. lud.
+ exfalso. eapply H3. eapply lookup_set_spec; eauto.
∃ x0. split.
- cset_tac; intuition.
- eqs.
+ exfalso. eapply H3. eapply lookup_set_spec; eauto.
eexists y. split; cset_tac; intuition; eauto.
+ eapply H2; eauto. cset_tac; intuition.
cset_tac; intuition.
Qed.
Lemma injective_on_forget s (f:X → Y) y `{Proper _ (_eq ==> _eq) f}
: injective_on s f
→ injective_on (s\{{y}}) f.
Proof.
intros. hnf; intros.
assert (y =/= y0). intro; cset_tac; firstorder.
assert (x =/= y). intro; cset_tac; firstorder.
eapply H. cset_tac; firstorder.
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.
eapply lookup_set_spec in H3; decompose records; eauto.
edestruct (minus_in_in _ _ _ _ H5); eauto.
eapply in_in_minus; eauto. eapply lookup_set_spec; eauto.
intro. eapply lookup_set_spec in H7; decompose records; eauto.
subst. eapply H4. rewrite H2; eauto. eapply union_left; eauto.
eapply union_right; eauto. rewrite <- H6. rewrite <- H10. reflexivity.
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.
+ eapply H2; cset_tac; eauto; firstorder.
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 \ {{x}}) f
→ f x ∉ lookup_set f (D \ {{x}})
→ injective_on D f.
Proof.
intros; hnf; intros.
decide(x0 === x); decide (x0 === y); eauto.
- exfalso. eapply H3. eapply lookup_set_spec. eauto.
eexists y. cset_tac; eqs; eauto. rewrite e in H6; eauto.
- eapply H2; cset_tac; eauto.
intro. eapply H3.
eapply lookup_set_spec; intuition.
cset_tac.
intuition.
eexists x0; eauto. intuition.
rewrite H6, H7; eauto.
Qed.
Lemma injective_on_update_fresh {X} `{OrderedType X} {Y} `{OrderedType Y}
D x y f `{Proper _ (_eq ==> _eq) f}
: injective_on (D \ {{x}}) f
→ y ∉ lookup_set f (D \ {{x}})
→ injective_on D (update f x y).
Proof.
intros; hnf; intros. lud.
exfalso. eapply H3. eapply lookup_set_spec; eauto.
eexists x0. cset_tac; eauto.
exfalso. eapply H3. eapply lookup_set_spec; eauto.
eexists y0. cset_tac; 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\{{x}} → x ∈ D
→ f x ∉ lookup_set f D´.
Proof.
intros. intro. eapply lookup_set_spec in H5; eauto. destruct H5; dcr.
specialize (H3 _ H6). cset_tac; eauto.
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 \ {{f x}} [=] lookup_set f (D\{{x}}).
Proof.
intros. cset_tac; split; intros; dcr. eapply lookup_set_spec; eauto.
+ eapply lookup_set_spec in H4. destruct H4; dcr; eauto.
eexists x0; cset_tac; intuition.
eapply H2. eapply lookup_set_spec; eauto.
eexists x. rewrite <- H3 in H4; eauto.
eauto.
+ eapply lookup_set_spec in H3; eauto. destruct H3; dcr. cset_tac.
eapply lookup_set_spec; eauto.
intro. eapply H2. eapply lookup_set_spec; eauto. eexists x0; split; eqs; eauto.
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.
unfold fst, snd;
decide (f y ∈ s); decide (f x ∈ {f y; s});
decide (f x ∈ s); decide (f y ∈ {f x; s}); simpl;
eauto; cset_tac; intuition.
econstructor.
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.
Global Instance injective_on_step_proper
{X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
`{Proper _ (_eq ==> _eq) f}
: Proper (_eq ==> _eq ==> _eq) (injective_on_step f).
Proof.
unfold Proper, respectful; intros.
destruct x0, y0. unfold injective_on_step. unfold snd.
destruct b, b0. unfold fst. econstructor.
inv H3. rewrite H7. rewrite H2. reflexivity.
decide (f x ∈ s); decide (f y ∈ s0).
econstructor. exfalso. eapply n. rewrite <- H2.
inv H3. rewrite <- H7. eauto.
exfalso. eapply n. rewrite H2.
inv H3. rewrite H7. eauto. econstructor.
inv H3. inv H9. inv H3. inv H9.
econstructor. simpl. rewrite H2.
inv H3. rewrite H7. econstructor; eauto. econstructor.
Qed.
Global Instance injective_on_step_proper´
{X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
`{Proper _ (_eq ==> eq) f}
: Proper (_eq ==> eq ==> eq) (injective_on_step f).
Proof.
unfold Proper, respectful; intros.
destruct x0, y0. unfold injective_on_step. unfold snd.
destruct b, b0. unfold fst. f_equal.
inv H3. rewrite H2. reflexivity.
decide (f x ∈ s); decide (f y ∈ s0).
econstructor. exfalso. eapply n. rewrite <- H2.
inv H3. eauto.
exfalso. eapply n. rewrite H2.
inv H3. eauto.
inv H3. econstructor. inv H3. inv H3.
inv H3. f_equal. simpl. rewrite H2. reflexivity.
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.
set_tac; intuition. destruct H4; cset_tac.
eapply H2 in H4. cset_tac; intuition.
+ cset_tac.
split; intros. destruct H6. set_tac. destruct H6; dcr.
eapply H4 in H7. destruct H7. rewrite <- H6 in H8; eauto.
right. eapply H5. cset_tac. left. set_tac. eexists x0; intuition.
eauto. eauto. right. eapply H5. cset_tac. right; eauto.
destruct H6. left. set_tac. eexists x; intuition.
eapply H4. eauto. intuition.
eapply H5 in H6. cset_tac; intuition.
left. set_tac; intuition. set_tac; intuition.
eexists x0; eauto. split; eauto. eapply H4. right; eauto.
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. eapply (H5 x). intuition cset_tac.
eapply H11; reflexivity.
assert (D´ ∩ s [=] ∅). cset_tac; intuition. destruct (FOO a).
eapply H5; split; eauto.
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 H15 in n,H3. destruct H14; eauto.
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.
assert (s ∪ D´ [=] (s´ ∪ D´) \ {{x}}).
rewrite H4; cset_tac; intuition.
rewrite H8 in n0. rewrite H8 in H2.
pose proof (injective_on_update_not_in H2 n0); eauto. intuition.
simpl. split; intros; isabsurd.
simpl in H2. eapply H2. eapply (injective_on_incl H11).
rewrite H4. cset_tac; intuition.
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.
assert (a ∈ lookup_set f D).
set_tac; eauto. set_tac; eauto. eexists x. intuition.
set_tac; eauto. set_tac. destruct H6; cset_tac. eauto.
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. cset_tac; intuition.
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 X0.
exploit H2; try eapply H3. rewrite X1. 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. cset_tac; intuition.
- eapply injective_on_agree.
assert (lv ∪ { x; of_list XL} [=] {{x}} ∪ lv ∪ of_list XL) by (cset_tac; intuition; eauto).
rewrite H7. eapply IHlength_eq; auto.
Focus 2.
eapply injective_on_fresh. instantiate (1:=ϱ); eauto.
eapply injective_on_incl; eauto. instantiate (1:=y).
intro. eapply lookup_set_spec in H8. dcr.
eapply (not_in_empty (ϱ x0)). rewrite <- H4. cset_tac; intuition.
eapply lookup_set_spec; eauto. eapply H1.
hnf; intros. lud; eauto; try now exfalso; eauto.
dcr. cset_tac; intuition.
eapply lookup_set_spec in H12; dcr. lud.
eapply H8. rewrite <- H14; eauto. eapply InA_in; eauto.
cset_tac; intuition.
eapply H4. split. right; eauto.
eapply lookup_set_spec. eauto. eexists; eauto.
hnf; intros. lud; eauto; try now exfalso; eauto.
eapply update_unique_commute; eauto using length_eq_length.
Qed.
Require Export CSet Containers.SetDecide.
Require Export MapBasics MapUpdate MapLookup OrderedTypeEx.
Set Implicit Arguments.
Section MapInjectivity.
Open Scope fmap_scope.
Variable X : Type.
Context `{OrderedType X}.
Variable Y : Type.
Context `{OrderedType Y}.
Definition injective_on D (f:X→Y) :=
∀ 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\{{x}}) f
→ injective_on (lv\{{x}}) (f[x<-v]).
Proof.
intros; hnf; intros. lud; eauto.
+ exfalso; cset_tac; eauto.
+ exfalso; cset_tac; eauto.
Qed.
Lemma injective_on_fresh lv (f:X → Y) x xr `{Proper _ (_eq ==> _eq) f}
: injective_on (lv\{{x}}) f
→ ¬xr ∈ lookup_set f (lv\{{x}})
→ injective_on ({{x}} ∪ lv) (f[x <- xr]).
Proof.
intros. hnf; intros. lud.
+ exfalso. eapply H3. eapply lookup_set_spec; eauto.
∃ x0. split.
- cset_tac; intuition.
- eqs.
+ exfalso. eapply H3. eapply lookup_set_spec; eauto.
eexists y. split; cset_tac; intuition; eauto.
+ eapply H2; eauto. cset_tac; intuition.
cset_tac; intuition.
Qed.
Lemma injective_on_forget s (f:X → Y) y `{Proper _ (_eq ==> _eq) f}
: injective_on s f
→ injective_on (s\{{y}}) f.
Proof.
intros. hnf; intros.
assert (y =/= y0). intro; cset_tac; firstorder.
assert (x =/= y). intro; cset_tac; firstorder.
eapply H. cset_tac; firstorder.
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.
eapply lookup_set_spec in H3; decompose records; eauto.
edestruct (minus_in_in _ _ _ _ H5); eauto.
eapply in_in_minus; eauto. eapply lookup_set_spec; eauto.
intro. eapply lookup_set_spec in H7; decompose records; eauto.
subst. eapply H4. rewrite H2; eauto. eapply union_left; eauto.
eapply union_right; eauto. rewrite <- H6. rewrite <- H10. reflexivity.
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.
+ eapply H2; cset_tac; eauto; firstorder.
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 \ {{x}}) f
→ f x ∉ lookup_set f (D \ {{x}})
→ injective_on D f.
Proof.
intros; hnf; intros.
decide(x0 === x); decide (x0 === y); eauto.
- exfalso. eapply H3. eapply lookup_set_spec. eauto.
eexists y. cset_tac; eqs; eauto. rewrite e in H6; eauto.
- eapply H2; cset_tac; eauto.
intro. eapply H3.
eapply lookup_set_spec; intuition.
cset_tac.
intuition.
eexists x0; eauto. intuition.
rewrite H6, H7; eauto.
Qed.
Lemma injective_on_update_fresh {X} `{OrderedType X} {Y} `{OrderedType Y}
D x y f `{Proper _ (_eq ==> _eq) f}
: injective_on (D \ {{x}}) f
→ y ∉ lookup_set f (D \ {{x}})
→ injective_on D (update f x y).
Proof.
intros; hnf; intros. lud.
exfalso. eapply H3. eapply lookup_set_spec; eauto.
eexists x0. cset_tac; eauto.
exfalso. eapply H3. eapply lookup_set_spec; eauto.
eexists y0. cset_tac; 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\{{x}} → x ∈ D
→ f x ∉ lookup_set f D´.
Proof.
intros. intro. eapply lookup_set_spec in H5; eauto. destruct H5; dcr.
specialize (H3 _ H6). cset_tac; eauto.
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 \ {{f x}} [=] lookup_set f (D\{{x}}).
Proof.
intros. cset_tac; split; intros; dcr. eapply lookup_set_spec; eauto.
+ eapply lookup_set_spec in H4. destruct H4; dcr; eauto.
eexists x0; cset_tac; intuition.
eapply H2. eapply lookup_set_spec; eauto.
eexists x. rewrite <- H3 in H4; eauto.
eauto.
+ eapply lookup_set_spec in H3; eauto. destruct H3; dcr. cset_tac.
eapply lookup_set_spec; eauto.
intro. eapply H2. eapply lookup_set_spec; eauto. eexists x0; split; eqs; eauto.
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.
unfold fst, snd;
decide (f y ∈ s); decide (f x ∈ {f y; s});
decide (f x ∈ s); decide (f y ∈ {f x; s}); simpl;
eauto; cset_tac; intuition.
econstructor.
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.
Global Instance injective_on_step_proper
{X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
`{Proper _ (_eq ==> _eq) f}
: Proper (_eq ==> _eq ==> _eq) (injective_on_step f).
Proof.
unfold Proper, respectful; intros.
destruct x0, y0. unfold injective_on_step. unfold snd.
destruct b, b0. unfold fst. econstructor.
inv H3. rewrite H7. rewrite H2. reflexivity.
decide (f x ∈ s); decide (f y ∈ s0).
econstructor. exfalso. eapply n. rewrite <- H2.
inv H3. rewrite <- H7. eauto.
exfalso. eapply n. rewrite H2.
inv H3. rewrite H7. eauto. econstructor.
inv H3. inv H9. inv H3. inv H9.
econstructor. simpl. rewrite H2.
inv H3. rewrite H7. econstructor; eauto. econstructor.
Qed.
Global Instance injective_on_step_proper´
{X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
`{Proper _ (_eq ==> eq) f}
: Proper (_eq ==> eq ==> eq) (injective_on_step f).
Proof.
unfold Proper, respectful; intros.
destruct x0, y0. unfold injective_on_step. unfold snd.
destruct b, b0. unfold fst. f_equal.
inv H3. rewrite H2. reflexivity.
decide (f x ∈ s); decide (f y ∈ s0).
econstructor. exfalso. eapply n. rewrite <- H2.
inv H3. eauto.
exfalso. eapply n. rewrite H2.
inv H3. eauto.
inv H3. econstructor. inv H3. inv H3.
inv H3. f_equal. simpl. rewrite H2. reflexivity.
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.
set_tac; intuition. destruct H4; cset_tac.
eapply H2 in H4. cset_tac; intuition.
+ cset_tac.
split; intros. destruct H6. set_tac. destruct H6; dcr.
eapply H4 in H7. destruct H7. rewrite <- H6 in H8; eauto.
right. eapply H5. cset_tac. left. set_tac. eexists x0; intuition.
eauto. eauto. right. eapply H5. cset_tac. right; eauto.
destruct H6. left. set_tac. eexists x; intuition.
eapply H4. eauto. intuition.
eapply H5 in H6. cset_tac; intuition.
left. set_tac; intuition. set_tac; intuition.
eexists x0; eauto. split; eauto. eapply H4. right; eauto.
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. eapply (H5 x). intuition cset_tac.
eapply H11; reflexivity.
assert (D´ ∩ s [=] ∅). cset_tac; intuition. destruct (FOO a).
eapply H5; split; eauto.
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 H15 in n,H3. destruct H14; eauto.
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.
assert (s ∪ D´ [=] (s´ ∪ D´) \ {{x}}).
rewrite H4; cset_tac; intuition.
rewrite H8 in n0. rewrite H8 in H2.
pose proof (injective_on_update_not_in H2 n0); eauto. intuition.
simpl. split; intros; isabsurd.
simpl in H2. eapply H2. eapply (injective_on_incl H11).
rewrite H4. cset_tac; intuition.
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.
assert (a ∈ lookup_set f D).
set_tac; eauto. set_tac; eauto. eexists x. intuition.
set_tac; eauto. set_tac. destruct H6; cset_tac. eauto.
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. cset_tac; intuition.
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 X0.
exploit H2; try eapply H3. rewrite X1. 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. cset_tac; intuition.
- eapply injective_on_agree.
assert (lv ∪ { x; of_list XL} [=] {{x}} ∪ lv ∪ of_list XL) by (cset_tac; intuition; eauto).
rewrite H7. eapply IHlength_eq; auto.
Focus 2.
eapply injective_on_fresh. instantiate (1:=ϱ); eauto.
eapply injective_on_incl; eauto. instantiate (1:=y).
intro. eapply lookup_set_spec in H8. dcr.
eapply (not_in_empty (ϱ x0)). rewrite <- H4. cset_tac; intuition.
eapply lookup_set_spec; eauto. eapply H1.
hnf; intros. lud; eauto; try now exfalso; eauto.
dcr. cset_tac; intuition.
eapply lookup_set_spec in H12; dcr. lud.
eapply H8. rewrite <- H14; eauto. eapply InA_in; eauto.
cset_tac; intuition.
eapply H4. split. right; eauto.
eapply lookup_set_spec. eauto. eexists; eauto.
hnf; intros. lud; eauto; try now exfalso; eauto.
eapply update_unique_commute; eauto using length_eq_length.
Qed.