Library Common
Require Import OrderedType.
Require Import DigraphInterface.
Require Import Labels.
Module eqlistAFacts (M : OrderedType).
Lemma eqlistA_refl : forall l,
eqlistA M.eq l l.
Proof.
induction l. constructor.
constructor. apply M.eq_refl. auto.
Qed.
Lemma eqlistA_trans : forall l l' l'',
eqlistA M.eq l l' ->
eqlistA M.eq l' l'' ->
eqlistA M.eq l l''.
Proof.
induction l; intros.
inversion H. subst. auto.
inversion H. subst. destruct l''.
inversion H0. constructor. inversion H. inversion H0. subst.
eapply M.eq_trans. eauto. eauto.
inversion H0. subst. eapply IHl. eauto. eauto.
Qed.
Lemma eqlistA_sym : forall l l',
eqlistA M.eq l l' ->
eqlistA M.eq l' l.
Proof.
induction l; intros.
inversion H; auto.
inversion H. subst. inversion H. constructor. subst. apply M.eq_sym. auto. auto.
Qed.
End eqlistAFacts.
Module Eadd (Vertex : OrderedType) (Lab : Labels) (G : Directed_Graph Vertex Lab).
Import G Edge.
Ltac eq_key_simpl :=
unfold VertexMap.eq_key, VertexMap.Raw.Proofs.PX.eqk in *; simpl in *; auto.
Ltac eq_key_elt_simpl :=
unfold VertexMap.eq_key_elt, VertexMap.Raw.Proofs.PX.eqke in *; simpl in *; auto.
Ltac eq_key_solve := eq_key_simpl; eq_key_elt_simpl.
Lemma NoDup_sorted_equiv_eq : forall (A : Type) l l',
NoDupA (@VertexMap.eq_key A) l ->
NoDupA (@VertexMap.eq_key A) l' ->
Sorted (@VertexMap.lt_key A) l ->
Sorted (@VertexMap.lt_key A) l' ->
(forall x, InA (@VertexMap.eq_key_elt A) x l <-> InA (@VertexMap.eq_key_elt A) x l') ->
eqlistA (@VertexMap.eq_key_elt A) l l'.
Proof.
intros.
assert (eqlistA (@VertexMap.eq_key_elt A) l l').
apply SortA_equivlistA_eqlistA with (ltA := @VertexMap.lt_key A); intuition.
auto.
Qed.
Lemma NoDup_sorted_add_cons : forall (A : Type) l l' (x : VertexMap.key) (dx newdx : A),
(forall y z, InA (@VertexMap.eq_key_elt A) (y,z) l ->
InA (@VertexMap.eq_key_elt A) (y,z) l' \/ (@VertexMap.eq_key_elt A) (y,z) (x,dx)) ->
(forall y z, InA (@VertexMap.eq_key_elt A) (y,z) l' ->
InA (@VertexMap.eq_key_elt A) (y,z) l \/ (@VertexMap.eq_key_elt A) (y,z) (x,newdx)) ->
InA (@VertexMap.eq_key_elt A) (x,dx) l ->
InA (@VertexMap.eq_key_elt A) (x,newdx) l' ->
Sorted (@VertexMap.lt_key A) l ->
Sorted (@VertexMap.lt_key A) l' ->
NoDupA (@VertexMap.eq_key A) l ->
NoDupA (@VertexMap.eq_key A) l' ->
exists l1, exists l2, eqlistA (@VertexMap.eq_key_elt A) l (l1 ++ (x,dx) :: l2) /\ eqlistA (@VertexMap.eq_key_elt A) l' (l1 ++ (x,newdx) :: l2).
Proof.
induction l; intros.
inversion H1.
destruct l'; intros.
inversion H2.
destruct a as [a a']. destruct p as [p p'].
inversion H1. inversion H8. simpl in *. subst.
inversion H2. inversion H9. simpl in *. subst.
exists nil. exists l. simpl.
constructor. constructor. intuition. intuition.
constructor. intuition.
assert (eqlistA (@VertexMap.eq_key_elt A) l l').
apply NoDup_sorted_equiv_eq.
inversion H5; auto.
inversion H6; auto.
inversion H3; auto.
inversion H4; auto.
split; intros; destruct x0.
assert (InA (@VertexMap.eq_key_elt A) (k,a0) ((p,p') :: l') \/
(@VertexMap.eq_key_elt A) (k,a0) (p,a')).
assert (InA (@VertexMap.eq_key_elt A) (k, a0) ((p, p') :: l') \/
(@VertexMap.eq_key_elt A) (k, a0) (x, a')).
apply H. right. auto.
destruct H11. left. auto. right. inversion H11. simpl in *. subst.
eq_key_solve. split. rewrite H13. auto. auto.
destruct H11. inversion H11; subst.
inversion H5. elim H16. subst. rewrite InA_alt. rewrite InA_alt in H7. do 2 destruct H7.
exists x0. split. inversion H14. simpl in *. subst. eq_key_solve. destruct H8.
rewrite <-H8. destruct H9. rewrite H9. destruct H14. rewrite <-H14. destruct H7. auto.
auto.
auto.
inversion H5. elim H15. subst. rewrite InA_alt. rewrite InA_alt in H7. do 2 destruct H7.
exists x0. split. inversion H11. simpl in *. subst. eq_key_solve. destruct H11.
destruct H7. destruct H8. rewrite <-H8. destruct H9. rewrite H9. rewrite <-H11. auto.
auto.
auto.
assert (InA (@VertexMap.eq_key_elt A) (k,a0) ((a,a') :: l) \/
(@VertexMap.eq_key_elt A) (k,a0) (x,p')).
assert (InA (@VertexMap.eq_key_elt A) (k, a0) ((a, a') :: l) \/
(@VertexMap.eq_key_elt A) (k, a0) (x, p')).
apply H0. right. auto.
destruct H11. left. auto. right. inversion H11. simpl in *. subst.
eq_key_solve.
destruct H11. inversion H11; subst.
inversion H6. elim H16. subst. rewrite InA_alt. rewrite InA_alt in H7. do 2 destruct H7.
exists x0. split. inversion H14. simpl in *. subst. eq_key_solve. destruct H9.
rewrite <-H9. destruct H8. rewrite H8. destruct H14. rewrite <-H14. destruct H7. auto.
auto.
auto.
inversion H6. elim H15. subst. rewrite InA_alt. rewrite InA_alt in H7. do 2 destruct H7.
exists x0. split. inversion H11. simpl in *. subst. eq_key_solve. destruct H11.
destruct H7. destruct H8. destruct H9. rewrite <-H9. rewrite <-H11. auto.
auto.
intuition.
subst. exists nil. exists l.
split. simpl. intuition.
simpl. clear H1 H2 H8.
inversion H4. subst.
inversion H8; subst. inversion H9.
assert (InA (@VertexMap.eq_key_elt A) (p,p') ((a, a') :: l) \/
(@VertexMap.eq_key_elt A) (p, p') (a, newdx)).
assert(InA (@VertexMap.eq_key_elt A) (p,p') ((a, a') :: l) \/
(@VertexMap.eq_key_elt A) (p,p') (x, newdx)).
apply H0. left. intuition.
destruct H2. left. auto.
right. eq_key_solve. destruct H2; split. rewrite H2. auto. auto.
destruct H2. inversion H2. subst.
assert ((@VertexMap.lt_key A) (p,p') (a,newdx)).
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key_elt A) (l := b :: l0); intuition.
inversion H9; [left|right]; subst. eq_key_solve.
destruct H13; split. rewrite <-H11. auto. auto.
rewrite InA_alt. rewrite InA_alt in H13. destruct H13. destruct H11.
exists x0. split. eq_key_solve. destruct H11. rewrite <-H11. split; auto.
auto.
inversion H12. simpl in *. subst.
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in H11. simpl in H11.
elim (Vertex.lt_not_eq H11). auto.
subst.
assert (Vertex.lt p (fst b)).
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in H1. auto.
assert (Vertex.eq (fst b) a \/ Vertex.lt (fst b) a).
inversion H9; subst.
left. rewrite <-H10. eq_key_solve. destruct H14. auto.
right. inversion H7; subst.
assert (VertexMap.lt_key b (x,newdx)).
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key_elt A) (l := l0); intuition.
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in H13.
simpl in H13. rewrite <-H10. auto.
assert (Vertex.lt a p).
assert ((@VertexMap.lt_key A (a,a') (p,p'))).
inversion H3. subst.
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key A) (l := l); intuition.
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in H14. auto.
assert (Vertex.lt p p).
apply Vertex.lt_trans with (y := (fst b)). auto.
destruct H13. rewrite H13. auto. apply Vertex.lt_trans with (y := a). auto. auto.
elim (Vertex.lt_not_eq H15). auto.
simpl. constructor. eq_key_solve. destruct H2. rewrite H10. auto. set (l' := b :: l0) in *.
assert (eqlistA (@VertexMap.eq_key_elt A) l l').
apply NoDup_sorted_equiv_eq.
inversion H5; auto.
inversion H6; auto.
inversion H3; auto.
inversion H4; auto.
inversion H2; subst.
split; intros; destruct x0.
assert (InA (@VertexMap.eq_key_elt A) (k,a0) ((p,p') :: l') \/
(@VertexMap.eq_key_elt A) (k,a0) (p,a')).
assert (InA (@VertexMap.eq_key_elt A) (k, a0) ((p, p') :: l') \/
(@VertexMap.eq_key_elt A) (k, a0) (x, a')).
apply H. right. auto.
destruct H14. left. auto. right. inversion H14. simpl in *. subst.
eq_key_solve. split. destruct H2. rewrite H2. rewrite <-H10. auto. auto.
destruct H14. inversion H14; subst.
inversion H5. elim H18. subst. rewrite InA_alt. rewrite InA_alt in H13. do 2 destruct H13.
exists x0. split. inversion H16. simpl in *. subst. eq_key_solve. destruct H16.
rewrite <-H11. rewrite <-H12. destruct H13. auto.
auto.
auto.
inversion H5. elim H17. subst. rewrite InA_alt. rewrite InA_alt in H13. do 2 destruct H13.
exists x0. split. inversion H14. simpl in *. subst. eq_key_solve. rewrite <-H11.
destruct H13. destruct H14. rewrite <-H16. auto.
auto.
simpl in *. rewrite <-H12 in *.
assert (InA (@VertexMap.eq_key_elt A) (k,a0) ((a,a') :: l) \/
(@VertexMap.eq_key_elt A) (k,a0) (x,p')).
assert (InA (@VertexMap.eq_key_elt A) (k, a0) ((a, a') :: l) \/
(@VertexMap.eq_key_elt A) (k, a0) (x, p')).
apply H0. right. auto.
destruct H14. left. auto. right. inversion H14. simpl in *. subst. auto.
destruct H14. inversion H14; subst.
inversion H6. elim H17. subst. rewrite InA_alt. rewrite InA_alt in H9. do 2 destruct H9.
exists x0. split. inversion H9. simpl in *. subst. eq_key_solve. destruct H9.
rewrite <-H9. rewrite H10. auto.
auto.
auto.
inversion H6. elim H17. subst. rewrite InA_alt. rewrite InA_alt in H9. do 2 destruct H9.
exists x0. split. inversion H9. simpl in *. subst. eq_key_solve. destruct H9.
rewrite <-H9. rewrite H10. auto.
auto.
intuition.
subst. inversion H2. subst.
inversion H9. simpl in *. subst. clear H9.
assert (Vertex.lt a p).
assert ((@VertexMap.lt_key A) (a,a') (p,dx)).
inversion H3.
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key A) (l := l); intuition.
subst. rewrite InA_alt in H8. rewrite InA_alt. destruct H8. destruct H8.
exists x0. split. eq_key_solve. rewrite <-H7. destruct H8. auto.
auto.
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in H9. auto.
assert (Vertex.lt p a).
assert ((@VertexMap.lt_key A (p,p') (a,a'))).
inversion H4.
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key A) (l := l'); intuition.
assert (InA (@VertexMap.eq_key_elt A) (a, a') ((p, p') :: l') \/
(@VertexMap.eq_key_elt A) (a, a') (x, dx)).
apply H. left. intuition. destruct H14.
inversion H14; subst.
elim (Vertex.lt_not_eq H9). eq_key_solve. destruct H16. auto. auto.
elim (Vertex.lt_not_eq H9). rewrite <-H7. eq_key_solve. intuition.
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in H10. auto.
elim (Vertex.lt_not_eq (Vertex.lt_trans H9 H10)). auto.
subst.
assert ((@VertexMap.eq_key_elt A) (a,a') (p,p')).
assert (InA (@VertexMap.eq_key_elt A) (a,a') ((p,p') :: l') \/
(@VertexMap.eq_key_elt A) (a,a') (x,dx)).
apply H. left. intuition.
destruct H7. inversion H7; subst. auto.
assert (InA (@VertexMap.eq_key_elt A) (p,p') ((a,a') :: l) \/
(@VertexMap.eq_key_elt A) (p,p') (x,newdx)).
apply H0. left. intuition.
destruct H10. inversion H10. subst. intuition.
subst.
assert ((@VertexMap.lt_key A) (a,a') (p,p')).
inversion H3.
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key A) (l := l); intuition.
assert ((@VertexMap.lt_key A) (p,p') (a,a')).
inversion H4.
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key A) (l := l'); intuition.
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in *. simpl in *.
elim (Vertex.lt_not_eq (Vertex.lt_trans H12 H14)). auto.
inversion H6. subst. elim H14.
rewrite InA_alt. rewrite InA_alt in H9. destruct H9. destruct H9.
exists x0. split. inversion H9; inversion H10; eq_key_solve. rewrite H17. auto.
auto.
inversion H5. subst. elim H12.
rewrite InA_alt. rewrite InA_alt in H8. destruct H8. destruct H8.
exists x0. split. inversion H7; inversion H8; eq_key_solve. rewrite H11. auto.
auto.
inversion H7. simpl in *. subst.
assert (exists l1 : list (VertexMap.key * A),
exists l2 : list (VertexMap.key * A),
eqlistA (@VertexMap.eq_key_elt A) l (l1 ++ (x, dx) :: l2) /\ eqlistA (@VertexMap.eq_key_elt A) l' (l1 ++ (x, newdx) :: l2)).
apply IHl.
intros.
assert (InA (@VertexMap.eq_key_elt A) (y,z) ((p,p') :: l') \/
(@VertexMap.eq_key_elt A) (y,z) (x,dx)).
apply H. right. auto.
destruct H12. inversion H12; subst.
inversion H14. simpl in *. subst. inversion H5. subst. elim H17.
rewrite InA_alt. rewrite InA_alt in H11. destruct H11. destruct H11.
exists x0. split. inversion H11; inversion H14; eq_key_solve.
destruct H7. rewrite H7. destruct H11. rewrite <-H11. auto.
auto.
left. auto. right. auto.
intros.
assert (InA (@VertexMap.eq_key_elt A) (y,z) ((a,p') :: l) \/
(@VertexMap.eq_key_elt A) (y,z) (x,newdx)).
apply H0. right. auto.
destruct H12. inversion H12. subst.
inversion H14. simpl in *. subst. inversion H6. subst. elim H17.
rewrite InA_alt. rewrite InA_alt in H11. destruct H11. destruct H11.
exists x0. split. inversion H11; inversion H14; eq_key_solve.
destruct H11. rewrite <-H11. rewrite H20. auto.
auto.
subst. left. auto. right. auto.
auto.
auto.
inversion H3; auto.
inversion H4; auto.
inversion H5; auto.
inversion H6; auto.
do 2 destruct H11. destruct H11.
exists ((p,p') :: x0). exists x1. split.
constructor. intuition. intuition.
constructor. intuition. intuition.
Qed.
Lemma add_elements_cons : forall (A : Type) d x (dx newdx : A),
VertexMap.find x d = Some dx ->
exists l1, exists l2,
eqlistA (@VertexMap.eq_key_elt A)
(VertexMap.elements d) (l1 ++ (x,dx) :: l2) /\
eqlistA (@VertexMap.eq_key_elt A) (
VertexMap.elements (VertexMap.add x newdx d)) (l1 ++ (x,newdx) :: l2).
Proof.
intros. apply NoDup_sorted_add_cons.
intros.
generalize VertexMap.elements_2. intro.
destruct (Vertex.eq_dec x y).
right.
generalize (H1 _ _ _ _ H0). intro.
generalize (VertexMap.find_2 H). intro.
rewrite e in H3. rewrite (MapsTo_fun H2 H3). eq_key_solve.
left.
apply VertexMap.elements_1.
apply VertexMap.add_2. auto.
apply H1. auto.
intros.
generalize VertexMap.elements_2. intro.
destruct (Vertex.eq_dec x y). subst.
right.
generalize (H1 _ _ _ _ H0). intro.
generalize (VertexMap.add_1 d newdx (Vertex.eq_refl y)). intro.
rewrite MapFacts.add_mapsto_iff in H2. rewrite MapFacts.add_mapsto_iff in H3.
destruct H2. destruct H2. destruct H3. destruct H3. subst. eq_key_solve.
destruct H3. elim H3. auto.
destruct H2. elim H2. auto.
left.
apply VertexMap.elements_1.
eapply VertexMap.add_3. eauto. eapply H1. eauto.
apply VertexMap.elements_1.
apply VertexMap.find_2. auto.
apply VertexMap.elements_1.
apply VertexMap.add_1. auto.
apply VertexMap.elements_3.
apply VertexMap.elements_3.
apply VertexMap.elements_3w.
apply VertexMap.elements_3w.
Qed.
Lemma eqlistA_fold : forall (A : Type) (B : Type) l1 l2 (a : B) f,
eqlistA (@VertexMap.eq_key_elt A) l1 l2 ->
(forall x y z, (@VertexMap.eq_key_elt A) x y -> f z x = f z y) ->
fold_left f l1 a = fold_left f l2 a.
Proof.
induction l1; intros.
inversion H. auto.
induction l2. inversion H.
inversion H; subst. simpl. rewrite (H0 _ _ _ H4).
apply IHl1. auto. auto.
Qed.
End Eadd.
Require Import DigraphInterface.
Require Import Labels.
Module eqlistAFacts (M : OrderedType).
Lemma eqlistA_refl : forall l,
eqlistA M.eq l l.
Proof.
induction l. constructor.
constructor. apply M.eq_refl. auto.
Qed.
Lemma eqlistA_trans : forall l l' l'',
eqlistA M.eq l l' ->
eqlistA M.eq l' l'' ->
eqlistA M.eq l l''.
Proof.
induction l; intros.
inversion H. subst. auto.
inversion H. subst. destruct l''.
inversion H0. constructor. inversion H. inversion H0. subst.
eapply M.eq_trans. eauto. eauto.
inversion H0. subst. eapply IHl. eauto. eauto.
Qed.
Lemma eqlistA_sym : forall l l',
eqlistA M.eq l l' ->
eqlistA M.eq l' l.
Proof.
induction l; intros.
inversion H; auto.
inversion H. subst. inversion H. constructor. subst. apply M.eq_sym. auto. auto.
Qed.
End eqlistAFacts.
Module Eadd (Vertex : OrderedType) (Lab : Labels) (G : Directed_Graph Vertex Lab).
Import G Edge.
Ltac eq_key_simpl :=
unfold VertexMap.eq_key, VertexMap.Raw.Proofs.PX.eqk in *; simpl in *; auto.
Ltac eq_key_elt_simpl :=
unfold VertexMap.eq_key_elt, VertexMap.Raw.Proofs.PX.eqke in *; simpl in *; auto.
Ltac eq_key_solve := eq_key_simpl; eq_key_elt_simpl.
Lemma NoDup_sorted_equiv_eq : forall (A : Type) l l',
NoDupA (@VertexMap.eq_key A) l ->
NoDupA (@VertexMap.eq_key A) l' ->
Sorted (@VertexMap.lt_key A) l ->
Sorted (@VertexMap.lt_key A) l' ->
(forall x, InA (@VertexMap.eq_key_elt A) x l <-> InA (@VertexMap.eq_key_elt A) x l') ->
eqlistA (@VertexMap.eq_key_elt A) l l'.
Proof.
intros.
assert (eqlistA (@VertexMap.eq_key_elt A) l l').
apply SortA_equivlistA_eqlistA with (ltA := @VertexMap.lt_key A); intuition.
auto.
Qed.
Lemma NoDup_sorted_add_cons : forall (A : Type) l l' (x : VertexMap.key) (dx newdx : A),
(forall y z, InA (@VertexMap.eq_key_elt A) (y,z) l ->
InA (@VertexMap.eq_key_elt A) (y,z) l' \/ (@VertexMap.eq_key_elt A) (y,z) (x,dx)) ->
(forall y z, InA (@VertexMap.eq_key_elt A) (y,z) l' ->
InA (@VertexMap.eq_key_elt A) (y,z) l \/ (@VertexMap.eq_key_elt A) (y,z) (x,newdx)) ->
InA (@VertexMap.eq_key_elt A) (x,dx) l ->
InA (@VertexMap.eq_key_elt A) (x,newdx) l' ->
Sorted (@VertexMap.lt_key A) l ->
Sorted (@VertexMap.lt_key A) l' ->
NoDupA (@VertexMap.eq_key A) l ->
NoDupA (@VertexMap.eq_key A) l' ->
exists l1, exists l2, eqlistA (@VertexMap.eq_key_elt A) l (l1 ++ (x,dx) :: l2) /\ eqlistA (@VertexMap.eq_key_elt A) l' (l1 ++ (x,newdx) :: l2).
Proof.
induction l; intros.
inversion H1.
destruct l'; intros.
inversion H2.
destruct a as [a a']. destruct p as [p p'].
inversion H1. inversion H8. simpl in *. subst.
inversion H2. inversion H9. simpl in *. subst.
exists nil. exists l. simpl.
constructor. constructor. intuition. intuition.
constructor. intuition.
assert (eqlistA (@VertexMap.eq_key_elt A) l l').
apply NoDup_sorted_equiv_eq.
inversion H5; auto.
inversion H6; auto.
inversion H3; auto.
inversion H4; auto.
split; intros; destruct x0.
assert (InA (@VertexMap.eq_key_elt A) (k,a0) ((p,p') :: l') \/
(@VertexMap.eq_key_elt A) (k,a0) (p,a')).
assert (InA (@VertexMap.eq_key_elt A) (k, a0) ((p, p') :: l') \/
(@VertexMap.eq_key_elt A) (k, a0) (x, a')).
apply H. right. auto.
destruct H11. left. auto. right. inversion H11. simpl in *. subst.
eq_key_solve. split. rewrite H13. auto. auto.
destruct H11. inversion H11; subst.
inversion H5. elim H16. subst. rewrite InA_alt. rewrite InA_alt in H7. do 2 destruct H7.
exists x0. split. inversion H14. simpl in *. subst. eq_key_solve. destruct H8.
rewrite <-H8. destruct H9. rewrite H9. destruct H14. rewrite <-H14. destruct H7. auto.
auto.
auto.
inversion H5. elim H15. subst. rewrite InA_alt. rewrite InA_alt in H7. do 2 destruct H7.
exists x0. split. inversion H11. simpl in *. subst. eq_key_solve. destruct H11.
destruct H7. destruct H8. rewrite <-H8. destruct H9. rewrite H9. rewrite <-H11. auto.
auto.
auto.
assert (InA (@VertexMap.eq_key_elt A) (k,a0) ((a,a') :: l) \/
(@VertexMap.eq_key_elt A) (k,a0) (x,p')).
assert (InA (@VertexMap.eq_key_elt A) (k, a0) ((a, a') :: l) \/
(@VertexMap.eq_key_elt A) (k, a0) (x, p')).
apply H0. right. auto.
destruct H11. left. auto. right. inversion H11. simpl in *. subst.
eq_key_solve.
destruct H11. inversion H11; subst.
inversion H6. elim H16. subst. rewrite InA_alt. rewrite InA_alt in H7. do 2 destruct H7.
exists x0. split. inversion H14. simpl in *. subst. eq_key_solve. destruct H9.
rewrite <-H9. destruct H8. rewrite H8. destruct H14. rewrite <-H14. destruct H7. auto.
auto.
auto.
inversion H6. elim H15. subst. rewrite InA_alt. rewrite InA_alt in H7. do 2 destruct H7.
exists x0. split. inversion H11. simpl in *. subst. eq_key_solve. destruct H11.
destruct H7. destruct H8. destruct H9. rewrite <-H9. rewrite <-H11. auto.
auto.
intuition.
subst. exists nil. exists l.
split. simpl. intuition.
simpl. clear H1 H2 H8.
inversion H4. subst.
inversion H8; subst. inversion H9.
assert (InA (@VertexMap.eq_key_elt A) (p,p') ((a, a') :: l) \/
(@VertexMap.eq_key_elt A) (p, p') (a, newdx)).
assert(InA (@VertexMap.eq_key_elt A) (p,p') ((a, a') :: l) \/
(@VertexMap.eq_key_elt A) (p,p') (x, newdx)).
apply H0. left. intuition.
destruct H2. left. auto.
right. eq_key_solve. destruct H2; split. rewrite H2. auto. auto.
destruct H2. inversion H2. subst.
assert ((@VertexMap.lt_key A) (p,p') (a,newdx)).
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key_elt A) (l := b :: l0); intuition.
inversion H9; [left|right]; subst. eq_key_solve.
destruct H13; split. rewrite <-H11. auto. auto.
rewrite InA_alt. rewrite InA_alt in H13. destruct H13. destruct H11.
exists x0. split. eq_key_solve. destruct H11. rewrite <-H11. split; auto.
auto.
inversion H12. simpl in *. subst.
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in H11. simpl in H11.
elim (Vertex.lt_not_eq H11). auto.
subst.
assert (Vertex.lt p (fst b)).
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in H1. auto.
assert (Vertex.eq (fst b) a \/ Vertex.lt (fst b) a).
inversion H9; subst.
left. rewrite <-H10. eq_key_solve. destruct H14. auto.
right. inversion H7; subst.
assert (VertexMap.lt_key b (x,newdx)).
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key_elt A) (l := l0); intuition.
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in H13.
simpl in H13. rewrite <-H10. auto.
assert (Vertex.lt a p).
assert ((@VertexMap.lt_key A (a,a') (p,p'))).
inversion H3. subst.
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key A) (l := l); intuition.
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in H14. auto.
assert (Vertex.lt p p).
apply Vertex.lt_trans with (y := (fst b)). auto.
destruct H13. rewrite H13. auto. apply Vertex.lt_trans with (y := a). auto. auto.
elim (Vertex.lt_not_eq H15). auto.
simpl. constructor. eq_key_solve. destruct H2. rewrite H10. auto. set (l' := b :: l0) in *.
assert (eqlistA (@VertexMap.eq_key_elt A) l l').
apply NoDup_sorted_equiv_eq.
inversion H5; auto.
inversion H6; auto.
inversion H3; auto.
inversion H4; auto.
inversion H2; subst.
split; intros; destruct x0.
assert (InA (@VertexMap.eq_key_elt A) (k,a0) ((p,p') :: l') \/
(@VertexMap.eq_key_elt A) (k,a0) (p,a')).
assert (InA (@VertexMap.eq_key_elt A) (k, a0) ((p, p') :: l') \/
(@VertexMap.eq_key_elt A) (k, a0) (x, a')).
apply H. right. auto.
destruct H14. left. auto. right. inversion H14. simpl in *. subst.
eq_key_solve. split. destruct H2. rewrite H2. rewrite <-H10. auto. auto.
destruct H14. inversion H14; subst.
inversion H5. elim H18. subst. rewrite InA_alt. rewrite InA_alt in H13. do 2 destruct H13.
exists x0. split. inversion H16. simpl in *. subst. eq_key_solve. destruct H16.
rewrite <-H11. rewrite <-H12. destruct H13. auto.
auto.
auto.
inversion H5. elim H17. subst. rewrite InA_alt. rewrite InA_alt in H13. do 2 destruct H13.
exists x0. split. inversion H14. simpl in *. subst. eq_key_solve. rewrite <-H11.
destruct H13. destruct H14. rewrite <-H16. auto.
auto.
simpl in *. rewrite <-H12 in *.
assert (InA (@VertexMap.eq_key_elt A) (k,a0) ((a,a') :: l) \/
(@VertexMap.eq_key_elt A) (k,a0) (x,p')).
assert (InA (@VertexMap.eq_key_elt A) (k, a0) ((a, a') :: l) \/
(@VertexMap.eq_key_elt A) (k, a0) (x, p')).
apply H0. right. auto.
destruct H14. left. auto. right. inversion H14. simpl in *. subst. auto.
destruct H14. inversion H14; subst.
inversion H6. elim H17. subst. rewrite InA_alt. rewrite InA_alt in H9. do 2 destruct H9.
exists x0. split. inversion H9. simpl in *. subst. eq_key_solve. destruct H9.
rewrite <-H9. rewrite H10. auto.
auto.
auto.
inversion H6. elim H17. subst. rewrite InA_alt. rewrite InA_alt in H9. do 2 destruct H9.
exists x0. split. inversion H9. simpl in *. subst. eq_key_solve. destruct H9.
rewrite <-H9. rewrite H10. auto.
auto.
intuition.
subst. inversion H2. subst.
inversion H9. simpl in *. subst. clear H9.
assert (Vertex.lt a p).
assert ((@VertexMap.lt_key A) (a,a') (p,dx)).
inversion H3.
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key A) (l := l); intuition.
subst. rewrite InA_alt in H8. rewrite InA_alt. destruct H8. destruct H8.
exists x0. split. eq_key_solve. rewrite <-H7. destruct H8. auto.
auto.
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in H9. auto.
assert (Vertex.lt p a).
assert ((@VertexMap.lt_key A (p,p') (a,a'))).
inversion H4.
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key A) (l := l'); intuition.
assert (InA (@VertexMap.eq_key_elt A) (a, a') ((p, p') :: l') \/
(@VertexMap.eq_key_elt A) (a, a') (x, dx)).
apply H. left. intuition. destruct H14.
inversion H14; subst.
elim (Vertex.lt_not_eq H9). eq_key_solve. destruct H16. auto. auto.
elim (Vertex.lt_not_eq H9). rewrite <-H7. eq_key_solve. intuition.
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in H10. auto.
elim (Vertex.lt_not_eq (Vertex.lt_trans H9 H10)). auto.
subst.
assert ((@VertexMap.eq_key_elt A) (a,a') (p,p')).
assert (InA (@VertexMap.eq_key_elt A) (a,a') ((p,p') :: l') \/
(@VertexMap.eq_key_elt A) (a,a') (x,dx)).
apply H. left. intuition.
destruct H7. inversion H7; subst. auto.
assert (InA (@VertexMap.eq_key_elt A) (p,p') ((a,a') :: l) \/
(@VertexMap.eq_key_elt A) (p,p') (x,newdx)).
apply H0. left. intuition.
destruct H10. inversion H10. subst. intuition.
subst.
assert ((@VertexMap.lt_key A) (a,a') (p,p')).
inversion H3.
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key A) (l := l); intuition.
assert ((@VertexMap.lt_key A) (p,p') (a,a')).
inversion H4.
apply SortA_InfA_InA with (eqA := @VertexMap.eq_key A) (l := l'); intuition.
unfold VertexMap.lt_key, VertexMap.Raw.Proofs.PX.ltk in *. simpl in *.
elim (Vertex.lt_not_eq (Vertex.lt_trans H12 H14)). auto.
inversion H6. subst. elim H14.
rewrite InA_alt. rewrite InA_alt in H9. destruct H9. destruct H9.
exists x0. split. inversion H9; inversion H10; eq_key_solve. rewrite H17. auto.
auto.
inversion H5. subst. elim H12.
rewrite InA_alt. rewrite InA_alt in H8. destruct H8. destruct H8.
exists x0. split. inversion H7; inversion H8; eq_key_solve. rewrite H11. auto.
auto.
inversion H7. simpl in *. subst.
assert (exists l1 : list (VertexMap.key * A),
exists l2 : list (VertexMap.key * A),
eqlistA (@VertexMap.eq_key_elt A) l (l1 ++ (x, dx) :: l2) /\ eqlistA (@VertexMap.eq_key_elt A) l' (l1 ++ (x, newdx) :: l2)).
apply IHl.
intros.
assert (InA (@VertexMap.eq_key_elt A) (y,z) ((p,p') :: l') \/
(@VertexMap.eq_key_elt A) (y,z) (x,dx)).
apply H. right. auto.
destruct H12. inversion H12; subst.
inversion H14. simpl in *. subst. inversion H5. subst. elim H17.
rewrite InA_alt. rewrite InA_alt in H11. destruct H11. destruct H11.
exists x0. split. inversion H11; inversion H14; eq_key_solve.
destruct H7. rewrite H7. destruct H11. rewrite <-H11. auto.
auto.
left. auto. right. auto.
intros.
assert (InA (@VertexMap.eq_key_elt A) (y,z) ((a,p') :: l) \/
(@VertexMap.eq_key_elt A) (y,z) (x,newdx)).
apply H0. right. auto.
destruct H12. inversion H12. subst.
inversion H14. simpl in *. subst. inversion H6. subst. elim H17.
rewrite InA_alt. rewrite InA_alt in H11. destruct H11. destruct H11.
exists x0. split. inversion H11; inversion H14; eq_key_solve.
destruct H11. rewrite <-H11. rewrite H20. auto.
auto.
subst. left. auto. right. auto.
auto.
auto.
inversion H3; auto.
inversion H4; auto.
inversion H5; auto.
inversion H6; auto.
do 2 destruct H11. destruct H11.
exists ((p,p') :: x0). exists x1. split.
constructor. intuition. intuition.
constructor. intuition. intuition.
Qed.
Lemma add_elements_cons : forall (A : Type) d x (dx newdx : A),
VertexMap.find x d = Some dx ->
exists l1, exists l2,
eqlistA (@VertexMap.eq_key_elt A)
(VertexMap.elements d) (l1 ++ (x,dx) :: l2) /\
eqlistA (@VertexMap.eq_key_elt A) (
VertexMap.elements (VertexMap.add x newdx d)) (l1 ++ (x,newdx) :: l2).
Proof.
intros. apply NoDup_sorted_add_cons.
intros.
generalize VertexMap.elements_2. intro.
destruct (Vertex.eq_dec x y).
right.
generalize (H1 _ _ _ _ H0). intro.
generalize (VertexMap.find_2 H). intro.
rewrite e in H3. rewrite (MapsTo_fun H2 H3). eq_key_solve.
left.
apply VertexMap.elements_1.
apply VertexMap.add_2. auto.
apply H1. auto.
intros.
generalize VertexMap.elements_2. intro.
destruct (Vertex.eq_dec x y). subst.
right.
generalize (H1 _ _ _ _ H0). intro.
generalize (VertexMap.add_1 d newdx (Vertex.eq_refl y)). intro.
rewrite MapFacts.add_mapsto_iff in H2. rewrite MapFacts.add_mapsto_iff in H3.
destruct H2. destruct H2. destruct H3. destruct H3. subst. eq_key_solve.
destruct H3. elim H3. auto.
destruct H2. elim H2. auto.
left.
apply VertexMap.elements_1.
eapply VertexMap.add_3. eauto. eapply H1. eauto.
apply VertexMap.elements_1.
apply VertexMap.find_2. auto.
apply VertexMap.elements_1.
apply VertexMap.add_1. auto.
apply VertexMap.elements_3.
apply VertexMap.elements_3.
apply VertexMap.elements_3w.
apply VertexMap.elements_3w.
Qed.
Lemma eqlistA_fold : forall (A : Type) (B : Type) l1 l2 (a : B) f,
eqlistA (@VertexMap.eq_key_elt A) l1 l2 ->
(forall x y z, (@VertexMap.eq_key_elt A) x y -> f z x = f z y) ->
fold_left f l1 a = fold_left f l2 a.
Proof.
induction l1; intros.
inversion H. auto.
induction l2. inversion H.
inversion H; subst. simpl. rewrite (H0 _ _ _ H4).
apply IHl1. auto. auto.
Qed.
End Eadd.