proposition: Lemma bindings_Add : forall m m' x e, ~In x m -> Add x e m m' -> eqlistA eqke (bindings m') (bindings_lt (x,e) m ++ (x,e):: bindings_ge (x,e) m).
proof: Proof. intros; unfold bindings_lt, bindings_ge. apply sort_equivlistA_eqlistA; auto with *. - apply (@SortA_app _ eqke); auto with *. + apply (@filter_sort _ eqke); auto with *; keauto. + constructor; auto with map. * apply (@filter_sort _ eqke); auto with *; keauto. * rewrite (@InfA_alt _ eqke); auto with *; try (keauto; fail). { intros. rewrite filter_InA in H1; auto with *; destruct H1. rewrite leb_1 in H2. destruct y; klean. rewrite <- bindings_mapsto_iff in H1. assert (~K.eq x t0). { contradict H. exists e0; apply MapsTo_1 with t0; auto. F.order. } F.order. } { apply (@filter_sort _ eqke); auto with *; keauto. } + intros. rewrite filter_InA in H1; auto with *; destruct H1. rewrite gtb_1 in H3. destruct y; destruct x0; klean. inversion_clear H2. * red in H4. klean; destruct H4; simpl in *. F.order. * rewrite filter_InA in H4; auto with *; destruct H4. rewrite leb_1 in H4. klean; F.order. - intros (k,e'). rewrite InA_app_iff, InA_cons, 2 filter_InA, <-2 bindings_mapsto_iff, leb_1, gtb_1, find_mapsto_iff, (H0 k), <- find_mapsto_iff, add_mapsto_iff by (auto with * ). change (eqke (k,e') (x,e)) with (K.eq k x /\ e' = e). klean. split. + intros [(->,->)|(Hk,Hm)]. * right; now left. * destruct (lt_dec k x); intuition. + intros [(Hm,LT)|[(->,->)|(Hm,EQ)]]. * right; split; trivial; F.order. * now left. * destruct (eq_dec x k) as [Hk|Hk]. elim H. exists e'. now rewrite Hk. right; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)