Finmap.v 42.9 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472
Require Import MetricCore.
Require Import PreoMet.
Require Import Arith Min Max List.

Module BoolDec.
  Definition U := bool.
  Definition eq_dec (x y : U) : { x = y } + {x <> y}.
  Proof.
    decide equality.
  Defined.
End BoolDec.

Module D := Coq.Logic.Eqdep_dec.DecidableEqDep(BoolDec).

Module CompDec.
  Definition U := comparison.
  Definition eq_dec (x y : U) : { x = y } + {x <> y}.
  Proof.
    decide equality.
  Defined.
End CompDec.

Module DC := Coq.Logic.Eqdep_dec.DecidableEqDep(CompDec).

Class Comparer (T : Type) := comp : T -> T -> comparison.
Class Order (T :Type) := leq : relation T.

Class comparable (T : Type) {cT : Comparer T} {ord : Order T} `{ord_part : PartialOrder _ (@eq T) leq} :=
  compat_compare : forall x y, match comp x y with
                                 | Lt => leq x y /\ x <> y
                                 | Eq => x = y
                                 | Gt => leq y x /\ x <> y
                               end.

Instance Comp_nat : Comparer nat := nat_compare.
Instance PreOrd_le : PreOrder le.
Proof.
  split.
  - intros x; auto.
  - intros x y z Hxy Hxz; eapply le_trans; eassumption.
Qed.
Instance PartOrd_nat : PartialOrder (@eq nat) le.
Proof.
  split; [intros; subst; split; reflexivity |].
  unfold Basics.flip; intros [HLe HLe']; auto with arith.
Qed.
Instance ord_nat : Order nat := le.
Instance comp_nat : comparable nat.
Proof.
  intros x y; remember (comp x y) as C; symmetry in HeqC; destruct C; unfold comp, Comp_nat in *.
  - apply nat_compare_eq; assumption.
  - rewrite <- nat_compare_lt in HeqC; split; unfold leq, ord_nat; omega.
  - rewrite <- nat_compare_gt in HeqC; split; unfold leq, ord_nat; omega.
Qed.

Infix "∈" := In (at level 40, no associativity).

Section Sortedness.
  Context {T} `{compT : comparable T}.

  Lemma comp_self_Eq k : comp k k = Eq.
  Proof.
    assert (HT := compat_compare k k); destruct (comp k k); intuition.
  Qed.

  Lemma comp_gt_Gt m k (HGt : leq m k /\ k <> m) : comp k m = Gt.
  Proof.
    assert (HT := compat_compare k m); destruct (comp k m); intuition.
    contradiction H2; assert (HT := ord_part k m); simpl in HT.
    apply <- HT; clear HT; split; assumption.
  Qed.

  Lemma comp_lt_Lt m k (HLt : leq k m /\ k <> m) : comp k m = Lt.
  Proof.
    assert (HT := compat_compare k m); destruct (comp k m); intuition.
    contradiction H2; assert (HT := ord_part k m); simpl in HT.
    apply <- HT; clear HT; split; assumption.
  Qed.

  Definition iseq (k1 k2 : T) : bool := match comp k1 k2 with Eq => true | _ => false end.
  Lemma iseq_eq k1 k2 : iseq k1 k2 = true <-> k1 = k2.
  Proof.
    unfold iseq; assert (HT := compat_compare k1 k2); destruct (comp k1 k2); intuition discriminate.
  Qed.

  Fixpoint inlst k xs :=
    match xs with
      | nil => false
      | x :: xs => (iseq k x || inlst k xs)%bool
    end.

  Lemma In_inlst k xs : inlst k xs = true <-> k  xs.
  Proof.
    induction xs; simpl; [intuition discriminate |].
    rewrite Bool.orb_true_iff, IHxs; clear IHxs; intuition.
    - rewrite iseq_eq in H0; subst; tauto.
    - subst; unfold iseq; rewrite comp_self_Eq; auto.
  Qed.

  Lemma eq_sym_iff : forall T (x y : T), x = y <-> y = x.
  Proof.
    split; apply eq_sym; assumption.
  Qed.

  Lemma NIn_inlst k xs : inlst k xs = false <-> ~ (k  xs).
    induction xs; simpl; [tauto |].
    rewrite Bool.orb_false_iff, IHxs, (eq_sym_iff _ a), <- iseq_eq; clear IHxs.
    destruct (iseq k a); intuition congruence.
  Qed.

  Inductive StrictSorted : list T -> Prop :=
  | SS_nil : StrictSorted nil
  | SS_sing : forall x, StrictSorted (x :: nil)
  | SS_cons : forall x x' xs (HS : StrictSorted (x' :: xs)) (HLt : comp x x' = Lt),
    StrictSorted (x :: x' :: xs).

  Lemma SS_tail x xs (HSS : StrictSorted (x :: xs)) : StrictSorted xs.
  Proof.
    inversion HSS; subst; assumption || apply SS_nil.
  Qed.

  Lemma comp_Lt_lt: forall m k, comp k m = Lt -> leq k m /\ k <> m. 
  Proof.
    intros m k H; assert (HT := compat_compare k m); rewrite H in HT; assumption.
  Qed.

  Lemma comp_Gt_gt: forall m k, comp k m = Gt -> leq m k /\ k <> m. 
  Proof.
    intros m k H; assert (HT := compat_compare k m); rewrite H in HT; assumption.
  Qed.

  Lemma Lt_trans: forall x y z, comp x y = Lt -> comp y z = Lt -> comp x z = Lt.
  Proof.
    intros; apply comp_lt_Lt; apply comp_Lt_lt in H; apply comp_Lt_lt in H0.
    split; [etransitivity; intuition eassumption |].
    intros abs; subst; contradiction (proj2 H); apply ord_part; split; tauto.
  Qed.
  
  Lemma Gt_trans: forall x y z, comp x y = Gt -> comp y z = Gt -> comp x z = Gt.
  Proof.
    intros; apply comp_gt_Gt; apply comp_Gt_gt in H; apply comp_Gt_gt in H0.
    split; [etransitivity; intuition eassumption |].
    intros abs; subst; contradiction (proj2 H); apply ord_part; split; tauto.
  Qed.

  Lemma StrictSorted_lt_notin k x xs (HLt : leq k x /\ k <> x)
        (HSS : StrictSorted (x :: xs)) : ~ (k  (x :: xs)).
  Proof.
    induction xs; [simpl; intros [HEq | HC]; [subst |]; tauto |].
    inversion HSS; subst; simpl; intros HIn; apply IHxs; clear HSS IHxs; [| simpl; intuition].
    - clear HIn; inversion HS; subst; [apply SS_sing | apply SS_cons; [assumption |]].
      apply comp_lt_Lt; apply comp_Lt_lt in HLt0; apply comp_Lt_lt in HLt1. 
      split; [etransitivity; intuition eassumption |].
      intros HEq; subst; contradiction (proj2 HLt1); apply ord_part; split; tauto.
    - subst; apply comp_Lt_lt in HLt0; destruct HLt0; contradiction H0; apply ord_part; split; assumption.
  Qed.

  Lemma StrictSorted_lt_notin' k x xs (HLt : comp k x = Lt)
        (HSS : StrictSorted (x :: xs)) : ~ (k  (x :: xs)).
  Proof.
    apply comp_Lt_lt in HLt; apply StrictSorted_lt_notin; assumption.
  Qed.
  
  Lemma StrictSorted_notin x xs (HSS : StrictSorted (x :: xs)) : ~ (x  xs).
  Proof.
    destruct xs as [| y ys]; [tauto |]; apply StrictSorted_lt_notin'; [| eapply SS_tail; eassumption].
    inversion HSS; subst; assumption.
  Qed.

  Lemma last_cons (x y : T) xs : last (x :: xs) y = last xs x.
  Proof.
    revert x y; induction xs; intros; [reflexivity |].
    etransitivity; [apply IHxs |]; symmetry; apply IHxs.
  Qed.

  Lemma SS_last_le y x xs (HSS : StrictSorted (x :: xs)) (HIn : y  (x :: xs)) :
    leq y (last xs x).
  Proof.
    revert x y HSS HIn; induction xs; intros.
    - destruct HIn; [subst; reflexivity | contradiction].
    - rewrite last_cons; inversion_clear HSS; apply comp_Lt_lt in HLt.
      simpl in HIn; destruct HIn as [HEq | HIn]; [subst |].
      + transitivity a; [tauto |].
        apply IHxs; [assumption | simpl; tauto].
      + apply IHxs; assumption.
  Qed.

End Sortedness.

Section Def.
  Context (K V : Type).

  Record FinDom `{compK : comparable K} :=
    mkFD {findom_t : list (K * V);
          findom_P : StrictSorted (map (@fst _ _) findom_t)}.

  Context `{compK : comparable K}.

  Fixpoint findom_lu f x : option V :=
    match f with
      | nil => None
      | (k, v) :: f =>
        match comp x k with
          | Lt => None
          | Eq => Some v
          | Gt => findom_lu f x
        end
    end.

  Definition findom_f f := findom_lu (findom_t f).
  Definition dom f := map (@fst _ _) (findom_t f).
  Definition codom f := map (@snd _ _) (findom_t f).
End Def.

Arguments mkFD [K V] {cT ord equ preo ord_part compK} _ _.
Arguments findom_t [K V] {cT ord equ preo ord_part compK} _.
Arguments findom_lu [K V] {cT} _ _.
Arguments dom [K V] {cT ord equ preo ord_part compK} f.
Arguments codom [K V] {cT ord equ preo ord_part compK} f.
Arguments findom_f [K V] {cT ord equ preo ord_part compK} f x.
Notation "K '-f>' V" := (FinDom K V) (at level 45).

Section FinDom.
  Context {K} `{compK : comparable K}.

  Coercion findom_f : FinDom >-> Funclass.

  Section Props.
    Context {V : Type} `{ev : Setoid V}.

    Program Definition fdEmpty : K -f> V := mkFD nil SS_nil.

    Lemma fdLookup_notin_strong k (f : K -f> V) : (~ (k  dom f)) <-> f k = None.
    Proof.
      destruct f as [fs fP]; unfold findom_f, dom in *; simpl in *; induction fs; [firstorder |].
      destruct a as [m v]; assert (HT := compat_compare k m); simpl in *; destruct (comp k m); subst.
      - split; [intros HNIn; contradiction HNIn; tauto | inversion 1].
      - split; [reflexivity | intros _]; apply (StrictSorted_lt_notin _ _ _ HT fP).
      - apply SS_tail in fP; rewrite <- IHfs; [| assumption]; intuition.
    Qed.

    Lemma option_dec {A} (v : option A): {v = None} + {exists a, v = Some a}.
      destruct v ; eauto.
    Qed.
      
    Lemma option_None_eq (v : option V) : v == None -> v = None.
    Proof.
      assert (d := option_dec v) ; destruct d as [l | r]; [auto | destruct r as [x Hx] ; rewrite Hx ; inversion 1].
    Qed.

    Lemma fdLookup_notin k (f : K -f> V) : (~ (k  dom f)) <-> f k == None.
    Proof.
      split ; intro H.
      + apply fdLookup_notin_strong in H ; rewrite H ; reflexivity.
      + apply option_None_eq in H ; apply fdLookup_notin_strong ; auto.
    Qed.
    
    Lemma fdLookup_in_strong : forall (f : K -f> V) k, k  dom f <-> exists v, f k = Some v.
    Proof.
      destruct f as [fs fP]; unfold findom_f, dom; simpl; induction fs; intros; simpl.
      - intuition; destruct H as [x Hx]; inversion Hx.
      - destruct a as [kf vf]; assert (HT := compat_compare k kf); unfold findom_f in *; simpl in *; split; intros.
        + destruct (comp k kf); [exists vf ; reflexivity |..].
          * destruct H; [subst; firstorder |]; contradiction (StrictSorted_lt_notin _ _ _ HT fP); simpl; tauto.
          * apply -> IHfs; [| eapply SS_tail; eassumption]; destruct H; [subst; tauto | assumption].
        + destruct H as [v HEqv]; destruct (comp k kf); [subst; tauto | inversion HEqv |].
          right; apply <- IHfs; eauto using @SS_tail.
    Qed.    

    Lemma fdLookup_in : forall (f : K -f> V) k, k  dom f <-> exists v, f k == Some v.
    Proof.
      destruct f as [fs fP]; unfold findom_f, dom; simpl map; simpl findom_t.
      induction fs; intros.
      - intuition; destruct H as [x Hx]; inversion Hx.
      - destruct a as [kf vf]; assert (HT := compat_compare k kf); unfold findom_f in *; simpl findom_lu in *; split; intros.
        + destruct (comp k kf); [exists vf ; reflexivity |..].
          * destruct H; [subst; firstorder |]; contradiction (StrictSorted_lt_notin _ _ _ HT fP); simpl; tauto.
          * apply -> IHfs; [| eapply SS_tail; eassumption]; destruct H; [subst; tauto | assumption].
        + destruct H as [v HEqv]; destruct (comp k kf); [simpl; subst; tauto | inversion HEqv |].
          right; apply <- IHfs; eauto using @SS_tail.
    Qed.    

    Fixpoint pre_upd (x : K * V) ys :=
      match ys with
        | nil => x :: nil
        | y :: ys' => match comp (fst x) (fst y) with
                        | Lt => x :: ys
                        | Eq => x :: ys'
                        | Gt => y :: pre_upd x ys'
                      end
      end.

    Program Definition fdUpdate k v (f : K -f> V) : K -f> V := mkFD (pre_upd (k, v) (findom_t f)) _.
    Next Obligation.
      destruct f as [fs fSS]; induction fs; simpl in *; [apply SS_sing |].
      destruct a as [kf vf]; simpl in *; assert (HT := compat_compare k kf); destruct (comp k kf);
        subst; simpl; [assumption | apply SS_cons; [assumption|apply comp_lt_Lt; assumption] |]. 
      assert (HR : match map (@fst _ _) (pre_upd (k, v) fs)
                     with nil => True | kn :: _ => leq kf kn /\ kf <> kn end).
      - assert (HNEq' : kf <> k) by (intros HEq; subst; tauto).
        destruct fs as [| [kn vn] fs']; inversion fSS; clear fSS IHfs; subst; simpl; [tauto |].
        destruct (comp k kn); simpl; apply comp_Lt_lt in HLt; tauto.
      - destruct (pre_upd (k, v) fs) as [| [kn vn] fs']; [apply SS_sing |]; simpl in *.
        apply comp_lt_Lt in HR; apply SS_cons; eauto using @SS_tail.
    Qed.
      
    Lemma fdUpdate_eq k v f : fdUpdate k v f k = Some v.
    Proof.
      destruct f as [fs fP]; unfold findom_f; simpl in *; clear fP;
        induction fs; simpl; [rewrite comp_self_Eq; reflexivity |].
      destruct a as [kf vf]; assert (HT := compat_compare k kf); simpl; destruct (comp k kf); simpl;
        try (rewrite comp_self_Eq; reflexivity).
      rewrite comp_gt_Gt; assumption.
    Qed.

    Lemma fdUpdate_neq k k' v f (Hneq : k <> k') : fdUpdate k v f k' = f k'.
    Proof.
      destruct f as [fs fP]; unfold findom_f; simpl in *; clear fP; induction fs; simpl.
        assert (HT := compat_compare k' k); destruct (comp k' k); subst; tauto.
      destruct a as [kf vf]; assert (HT := compat_compare k kf); simpl; destruct (comp k kf); simpl;
        [..| rewrite IHfs; reflexivity].
        subst; assert (HT := compat_compare k' kf); destruct (comp k' kf); subst; tauto.
      assert (HR := compat_compare k' k); destruct (comp k' k); subst; try tauto.
      assert (HQ := compat_compare k' kf); destruct (comp k' kf); try reflexivity; clear IHfs.
        subst; contradiction Hneq; apply ord_part; split; tauto.
      contradiction Hneq; apply ord_part; split; [etransitivity |]; intuition eassumption.
    Qed.

    Fixpoint pre_rem x (ys : list (K * V)) :=
      match ys with
        | nil => nil
        | y :: ys' => match comp x (fst y) with
                        | Eq => ys'
                        | Lt => ys
                        | Gt => y :: pre_rem x ys'
                      end
      end.

    Program Definition fdRemove k (f : K -f> V) : K -f> V := mkFD (pre_rem k (findom_t f)) _.
    Next Obligation.
      destruct f as [fs fP]; simpl; induction fs; simpl; [assumption |].
      destruct a as [kf vf]; assert (HT := compat_compare k kf); simpl; destruct (comp k kf); eauto using @SS_tail.
      specialize (IHfs (SS_tail _ _ fP)); simpl; clear HT.
      assert (HR : match map (@fst _ _) (pre_rem k fs)
                     with nil => True | kn :: _ => leq kf kn /\ kf <> kn end).
      - destruct fs as [| [kn vn] fs']; simpl in *; [trivial |].
        destruct (comp k kn); simpl; inversion fP; subst; apply comp_Lt_lt in HLt; try tauto.
        clear fP; destruct fs' as [| [km vm] fs']; simpl in *; [trivial |].
        inversion HS; subst; split; apply comp_Lt_lt in HLt0; [etransitivity; intuition eassumption | intros HEq; subst].
        contradiction (proj2 HLt); apply ord_part; split; tauto.
      - destruct (map (@fst _ _) (pre_rem k fs)) as [| kn fs']; [apply SS_sing | apply comp_lt_Lt in HR; apply SS_cons; assumption].
    Qed.

    Lemma fdRemove_eq t f : fdRemove t f t = None.
    Proof.
      destruct f as [fs fP]; simpl; induction fs; [reflexivity |].
      destruct a as [k v]; assert (HT := compat_compare t k); simpl in *; destruct (comp t k).
      - apply fdLookup_notin_strong, StrictSorted_notin; subst; unfold dom; simpl; rewrite comp_self_Eq; apply fP.
      - apply fdLookup_notin_strong; unfold findom_f, dom in *; simpl in *; rewrite comp_lt_Lt; [| assumption].
        apply StrictSorted_lt_notin; assumption.
      - unfold findom_f in *; simpl in *; rewrite comp_gt_Gt; [| assumption].
        simpl; rewrite comp_gt_Gt; [| assumption].
        eapply IHfs, SS_tail; eassumption.
    Qed.

    Lemma fdRemove_neq t t' f (Hneq : t <> t') : fdRemove t f t' = f t'.
    Proof.
      destruct f as [fs fP]; unfold findom_f; simpl; induction fs; [reflexivity |].
      destruct a as [k v]; assert (HT := compat_compare t k); simpl; destruct (comp t k); [| reflexivity |].
      - subst; assert (HQ := compat_compare t' k); destruct (comp t' k); subst; try tauto.
        apply (fdLookup_notin_strong _ (mkFD fs (SS_tail _ _ fP))); unfold dom; simpl in *.
        intros HT; eapply StrictSorted_lt_notin; eassumption || (simpl; tauto).
      - simpl; rewrite IHfs; [reflexivity |]; eapply SS_tail; eassumption.
    Qed.

    Program Fixpoint Indom_lookup k (f : list (K * V)) (HIn : inlst k (map (@fst _ _) f) = true) : V :=
      match f as f' return inlst k (map (@fst _ _) f') = true -> V with
        | nil => fun F => False_rect _ _
        | (k', v') :: fr => fun P =>
          match iseq k k' as b return (b || inlst k (map (@fst _ _) fr) = true)%bool -> V with
            | true => fun _ => v'
            | false => fun P => Indom_lookup k fr P
          end P
      end HIn.

    Lemma Indom_lookup_find k (f : K -f> V) (HIn : inlst k (dom f) = true) : Some (Indom_lookup _ _ HIn) = f k.
    Proof.
      destruct f as [fs fP]; unfold dom, findom_f in *; simpl in *; induction fs; [discriminate |].
      revert HIn; destruct a as [kf vf]; simpl in *; unfold iseq.
      assert (HT := compat_compare k kf); revert HT; destruct (comp k kf); intros; [subst; reflexivity |..].
      - contradict HIn; simpl; rewrite In_inlst.
        intros HIn; eapply StrictSorted_lt_notin; eassumption || (simpl; tauto).
      - eapply IHfs, SS_tail; eassumption.
    Qed.

    Lemma orb_right_intro a b (HT : b = true) : (a || b = true)%bool.
    Proof. subst b; apply Bool.orb_true_r. Qed.

    Fixpoint ind_app_map U (xs : list K)
      (I : forall x (HIn : inlst x xs = true), U) :=
      match xs as lst return (forall x (HIn : inlst x lst = true), U) -> list (K * U) with
        | nil => fun _ => nil
        | x :: xs => fun R => (x, R x (proj2 (In_inlst _ _) (in_eq x xs))) ::
                               ind_app_map U xs (fun y Y => R _ (orb_right_intro _ _ Y))
      end I.

    Lemma list_fst_map U xs I : map (@fst _ _) (ind_app_map U xs I) = xs.
    Proof. induction xs; [reflexivity |]; simpl; f_equal; apply IHxs. Qed.

    Program Definition findom_map U W (m : K -f> U) (f : forall x (HIn : inlst x (dom m) = true), W) : K -f> W :=
      mkFD (ind_app_map _ (dom m) f) _.
    Next Obligation.
      rewrite list_fst_map; apply m.
    Qed.

    Lemma ff (P : K -> nat -> Prop) (A : forall x n m, n <= m -> P x n -> P x m) (xs : list K) :
      (forall x, inlst x xs = true -> exists m, P x m) -> exists m, forall x, inlst x xs = true -> P x m.
    Proof.
      induction xs; intros; [exists 0; intros; discriminate |].
      specialize (IHxs (fun k HIn => H k (orb_right_intro _ _ HIn))); destruct IHxs as [m IH].
      specialize (H a (proj2 (In_inlst (compT := compK) _ _) (in_eq a xs))); destruct H as [k Hk].
      exists (max m k); intros t HIn; rewrite In_inlst in HIn; simpl in HIn; destruct HIn as [HEq | HIn];
        [subst | rewrite <- In_inlst in HIn]; eapply A; [| eassumption |..]; eauto using le_max_r, le_max_l.
    Qed.

    Lemma findom_fun_map U xs (I : forall x, inlst x xs = true -> U) x
      (HIn : inlst x xs = true) (HSS : StrictSorted xs) :
      findom_lu (ind_app_map _ xs I) x = Some (I _ HIn).
    Proof.
      induction xs; [discriminate |].
      simpl; assert (HT := compat_compare x a); destruct (comp x a).
      - subst; rewrite (D.UIP _ _ _ HIn); reflexivity.
      - contradiction (StrictSorted_lt_notin _ _ xs HT).
        rewrite <- In_inlst; assumption.
      - simpl in *; specialize (IHxs (fun y Y => I _ (orb_right_intro _ _ Y))).
        assert (HInT : inlst x xs = true) by (unfold iseq in HIn; rewrite comp_gt_Gt in HIn; assumption).
        specialize (IHxs HInT (SS_tail _ _ HSS)); simpl in IHxs; rewrite (D.UIP _ _ _ HIn) in IHxs; apply IHxs.
    Qed.

    Lemma findom_map_app U W (m : K -f> U) x (HIn : inlst x (dom m) = true)
      (f : forall x, (inlst x (dom m) = true) -> W) :
      findom_map _ _ m f x = Some (f x HIn).
    Proof.
      destruct m as [ms mP]; unfold findom_f; simpl; unfold dom in *; simpl in *.
      apply (findom_fun_map _ _ f); assumption.
    Qed.

    Lemma findom_fun_map_nf U xs (I : forall x, inlst x xs = true -> U) x
      (HNIn : inlst x xs = false) (HSS : StrictSorted xs) :
      findom_lu (ind_app_map _ xs I) x = None.
    Proof.
      induction xs; [reflexivity |].
      simpl; assert (HT := compat_compare x a); destruct (comp x a); [| reflexivity |].
      - simpl in HNIn; rewrite <- iseq_eq in HT; rewrite HT in HNIn; discriminate.
      - simpl in *; apply IHxs; [| eapply SS_tail; eassumption].
        destruct (iseq x a); [discriminate | apply HNIn].
    Qed.

    Lemma findom_map_app_nf U W (m : K -f> U) x (HNIn : inlst x (dom m) = false)
      (f : forall x, (inlst x (dom m) = true) -> W) :
      findom_map _ _ m f x = None.
    Proof.
      destruct m as [ms mP]; unfold findom_f; simpl; unfold dom in *; simpl in *.
      apply (findom_fun_map_nf _ _ f); assumption.
    Qed.

  End Props.

  Section Instances.
    Context {V} `{cV : pcmType V}.

    Definition equiv_fd (f1 f2 : K -f> V) := forall k, f1 k == f2 k.
473
    Global Program Instance type_findom : Setoid (K -f> V) | 5:= mkType equiv_fd.
474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491
    Next Obligation.
      split.
      - intros m k; reflexivity.
      - intros m1 m2 HS k; symmetry; apply HS.
      - intros m1 m2 m3 H12 H23 k; etransitivity; [apply H12 | apply H23].
    Qed.

    Global Instance lookup_proper : Proper (equiv ==> eq ==> equiv) (findom_f (V := V)).
    Proof.
      intros f1 f2 HEqf k1 k2 HEqk; subst; apply HEqf.
    Qed.

    Definition dist_fd n (f1 f2 : K -f> V) :=
      match n with
        | O => True
        | S _ => forall k, f1 k = n = f2 k
      end.

492
    Global Program Instance metric_findom : metric (K -f> V) | 5 := mkMetr dist_fd.
493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554
    Next Obligation.
      revert n; intros [| n] f1 f2 EQf g1 g2 EQg; [reflexivity |]; split;
      intros EQ k; [symmetry in EQf, EQg |]; rewrite EQf, EQg; apply EQ.
    Qed.
    Next Obligation.
      split; intros HEq.
      - intros k; rewrite <- dist_refl; intros [| n]; [reflexivity; exact None | apply (HEq (S n) k) ].
      - intros [| n]; [reflexivity |]; intros k; generalize (S n); rewrite dist_refl; apply HEq.
    Qed.
    Next Obligation.
      revert n; intros [| n] x y HS; [reflexivity |]; intros k; symmetry; apply HS.
    Qed.
    Next Obligation.
      revert n; intros [| n] x y z Hxy Hyz; [reflexivity |]; intros k; etransitivity; [apply Hxy | apply Hyz].
    Qed.
    Next Obligation.
      destruct n as [| n]; [reflexivity |]; intros k; eapply dist_mono, H.
    Qed.

    Lemma domeq (m1 m2 : K -f> V) n (HEq : m1 = S n = m2) : dom m1 = dom m2.
    Proof.
      destruct m1 as [ms1 mP1]; destruct m2 as [ms2 mP2]; revert ms2 mP2 HEq; induction ms1; intros.
      { destruct ms2 as [| [kf vf] ms2]; [reflexivity |]; specialize (HEq kf); unfold findom_f in *; simpl in *.
        rewrite comp_self_Eq in HEq; contradiction HEq.
      }
      destruct a as [k1 v1]; destruct ms2 as [| [k2 v2] ms2].
      { specialize (HEq k1); unfold findom_f in *; simpl in *; rewrite comp_self_Eq in HEq; contradiction HEq.
      }
      assert (HEqk : k1 = k2).
      { assert (HT := compat_compare k1 k2); assert (HLt := HEq k1); assert (HGt := HEq k2);
          unfold findom_f in *; simpl in *; clear IHms1 HEq.
        rewrite comp_self_Eq in HLt; destruct (comp k1 k2); [assumption | contradiction HLt |].
        rewrite comp_lt_Lt, comp_self_Eq in HGt; [contradiction HGt | intuition].
      }
      subst; unfold dom; simpl; f_equal; simpl in *.
      apply IHms1 with (mP1 := SS_tail _ _ mP1) (mP2 := SS_tail _ _ mP2); intros k; clear IHms1.
      specialize (HEq k); unfold findom_f in *; simpl in *.
      assert (HT : mkFD ms1 (SS_tail _ _ mP1) k = S n = mkFD ms2 (SS_tail _ _ mP2) k); [| apply HT].
      assert (HT := compat_compare k k2); destruct (comp k k2); [subst | | assumption].
      { rewrite !(proj1 (fdLookup_notin_strong _ _)); [reflexivity |..]; unfold dom; simpl; apply StrictSorted_notin; assumption.
      }
      rewrite !(proj1 (fdLookup_notin_strong _ _)); [reflexivity |..]; unfold dom; simpl; intros HIn.
      { apply (StrictSorted_lt_notin _ _ _ HT mP2); simpl; tauto.
      }
      apply (StrictSorted_lt_notin _ _ _ HT mP1); simpl; tauto.
    Qed.

    Lemma finmap_chain_dom x n (σ : chain (K -f> V)) {σc : cchain σ} (HIn : In x (dom (σ 1))) : In x (dom (σ (S n))).
    Proof.
      revert σ σc HIn; induction n; intros; [assumption |].
      apply (IHn (cutn σ 1)); simpl; clear IHn; [apply _ |].
      rewrite fdLookup_in in HIn; destruct HIn as [v HLU].
      remember ((σ 2) x) as ov; symmetry in Heqov; destruct ov.
      - rewrite fdLookup_in; eexists; setoid_rewrite Heqov; reflexivity.
      - assert (HT := chain_cauchy σ _ 1 1 2 x).
        rewrite Heqov, HLU in HT; contradiction HT.
    Qed.

    Definition finmap_chainx (σ : chain (K -f> V)) {σc : cchain σ} x (HIn : x  dom (σ 1)) :=
      fun n => Indom_lookup x (findom_t (σ (S n))) (proj2 (In_inlst _ _) (finmap_chain_dom _ _ _ HIn)).

    Program Instance finmap_chainx_cauchy (σ : chain (K -f> V)) {σc : cchain σ} x (HIn : x  dom (σ 1)) :
555
      cchain (finmap_chainx σ x HIn) | 5.
556 557 558 559 560 561 562 563 564
    Next Obligation.
      unfold cchain; intros.
      assert (HT : Some (finmap_chainx σ x HIn i) = S n = Some (finmap_chainx σ x HIn j)); [| apply dist_mono, HT].
      unfold finmap_chainx; rewrite !Indom_lookup_find; apply (chain_cauchy σ σc (S n)); auto with arith.
    Qed.

    Definition findom_lub (σ : chain (K -f> V)) (σc : cchain σ) : K -f> V :=
      findom_map _ _ (σ 1) (fun x HLu => compl (finmap_chainx σ x (proj1 (In_inlst _ _) HLu))).

565
    Global Program Instance findom_cmetric : cmetric (K -f> V) | 5 := mkCMetr findom_lub.
566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959
    Next Obligation.
      intros [| n]; [exists 0; intros; exact I |].
      assert (HT : exists m, forall x, inlst x (dom (σ 1)) = true -> forall (X : inlst x (dom (σ 1)) = true) i,
        m < i -> σ i x = S n = Some (compl (finmap_chainx _ _ (proj1 (In_inlst _ _) X)))).
      { apply ff; intros; [apply H0; omega |].
        destruct (conv_cauchy (finmap_chainx _ _ (proj1 (In_inlst _ _) H)) (S n)) as [m P]; exists m;
          intros HIn [| i] HLe; [inversion HLe |].
        apply lt_n_Sm_le in HLe; specialize (P _ HLe); unfold finmap_chainx at 2 in P; simpl in P.
        erewrite <- Indom_lookup_find; unfold dist; simpl; rewrite <- P; apply umet_complete_extn; intros k; clear P; simpl.
        change (Some (finmap_chainx σ x (proj1 (In_inlst _ _) H) k) = S n = Some (finmap_chainx σ x (proj1 (In_inlst _ _) HIn) k)).
        unfold finmap_chainx; rewrite !Indom_lookup_find; reflexivity.
      }
      destruct HT as [m HT]; exists (S m); intros [| i] HLe k; [inversion HLe |].
      destruct (inlst k (dom (σ 1))) eqn: HIn.
      - specialize (HT _ HIn HIn (S i)); rewrite HT; [| auto with arith].
        unfold findom_lub; rewrite findom_map_app with (HIn := HIn); reflexivity.
      - assert (HInS := HIn); rewrite domeq with (n := 0) (m2 := σ (S i)) in HInS;
        [| eapply chain_cauchy; auto with arith].
        rewrite !(proj1 (fdLookup_notin _ _)); [reflexivity | rewrite <- In_inlst; congruence |].
        unfold findom_lub, dom; simpl; rewrite list_fst_map, <- In_inlst; congruence.
    Qed.

    Local Existing Instance option_preo_bot.
    Local Existing Instance option_pcm_bot.

    Definition extOrd (m1 m2 : K -f> V) := forall k, m1 k  m2 k.

    Global Program Instance extOrd_preo : preoType (K -f> V) := mkPOType extOrd.
    Next Obligation.
      split.
      - intros m k; reflexivity.
      - intros m1 m2 m3 S12 S23 k; etransitivity; [apply (S12 k) | apply (S23 k) ].
    Qed.

    Definition chain_fin_app (σ : chain (K -f> V)) k : chain (option V) :=
      fun i => σ i k.
    Instance cchain_fin_app (σ : chain (K -f> V)) {σc : cchain σ} k : cchain (chain_fin_app σ k).
    Proof.
      intros n i j LEi LEj; unfold chain_fin_app.
      specialize (σc n i j LEi LEj).
      destruct n as [| n]; [apply dist_bound |].
      specialize (σc k); assumption.
    Qed.

    Lemma foo (σ : chain (K -f> V)) (σc : cchain σ) k :
      compl σ k == compl (chain_fin_app σ k).
    Proof.
      unfold compl, option_cmt, option_compl, chain_fin_app; simpl.
      generalize (@eq_refl _ (σ 1 k)) as EQs; pattern (σ 1 k) at 1 3; destruct (σ 1 k) as [vs |]; intros.
      - unfold findom_lub.
        assert (HIn : inlst k (dom (σ 1)) = true).
        { rewrite In_inlst, fdLookup_in_strong; exists vs; congruence. }
        rewrite findom_map_app with (HIn := HIn).
        unfold equiv; simpl; apply umet_complete_ext; intros.
        unfold unSome, finmap_chainx.
        generalize (@eq_refl _ (σ (S i) k)) as EQsi.
        pattern (σ (S i) k) at 1 3; destruct (σ (S i) k) as [vsi |]; intros; [| exfalso].
        + erewrite <- (Indom_lookup_find _ (σ (S i))) in EQsi.
          inversion EQsi; reflexivity.
        + assert (LEi : 1 <= S i) by auto with arith.
          specialize (σc 1 1 (S i) (le_n _) LEi k).
          rewrite <- EQs, <- EQsi in σc; contradiction σc.
      - unfold findom_lub.
        rewrite findom_map_app_nf; [reflexivity |].
        rewrite NIn_inlst, fdLookup_notin_strong; congruence.
    Qed.

    Global Instance findom_pcmType : pcmType (K -f> V).
    Proof.
      split.
      - intros s s' HEqs t t' HEqt; split; intros HSub k.
        + rewrite <- (HEqs k), <- (HEqt k); apply (HSub k).
        + rewrite (HEqs k), (HEqt k); apply (HSub k).
      - intros σ ρ σc ρc HSub k; rewrite !foo.
        eapply pcm_respC; [now auto with typeclass_instances | intros].
        unfold chain_fin_app; eapply HSub.
    Qed.

    Lemma dom_ext (m1 m2 : K -f> V) k (HSub : m1  m2) (HIn : k  dom m1) : k  dom m2.
    Proof.
      destruct m1 as [ms1 mP1]; destruct m2 as [ms2 mP2]; specialize (HSub k); simpl in *.
      unfold findom_f, dom in *; simpl in *.
      induction ms1; simpl in *; [contradiction | destruct a as [k0 v0]; simpl in * ].
      assert (HT := compat_compare k k0); destruct (comp k k0); [subst k0 | |].
      - destruct (findom_lu ms2 k) as [v1 |] eqn: HFnd; [| contradiction HSub].
        clear -HFnd mP2 compK.
        assert (HT := fdLookup_in_strong (mkFD ms2 mP2) k); unfold dom, findom_f in HT; simpl in HT.
        rewrite HT; exists v1; assumption.
      - assert (HNIn := (StrictSorted_lt_notin _ _ _ HT mP1) HIn); contradiction.
      - destruct HIn as [HEq | HIn]; [destruct HT; congruence | apply SS_tail in mP1].
        apply IHms1; assumption.
    Qed.

  End Instances.

  Section Map.
    Context U V `{pcmU : pcmType U} `{cmV : pcmType V}.

    Program Definition pre_fdMap (f : U -> V) (m : K -f> U) : (K -f> V) :=
      mkFD (map (fun (a : K * U) => let (k, v) := a in (k, f v)) (findom_t m)) _.
    Next Obligation.
      destruct m as [ms mP]; simpl; induction ms as [| [k u]]; [apply SS_nil | simpl in *].
      destruct ms as [| [k' u'] ms]; [apply SS_sing | simpl in *].
      inversion mP; subst; apply SS_tail in mP; apply SS_cons; [apply IHms |]; assumption.
    Qed.

    Lemma pre_fdMap_dom_same f m : dom m = dom (pre_fdMap f m).
    Proof.
      destruct m as [ms mP]; unfold dom; simpl; clear mP; induction ms as [| [k u]]; [reflexivity |].
      simpl; f_equal; apply IHms.
    Qed.

    Lemma pre_fdMap_lookup f (m : K -f> U) k u (HFnd : m k = Some u) : (pre_fdMap f m) k = Some (f u).
    Proof.
      destruct m as [ms mP]; unfold findom_f in *; simpl in *; clear mP.
      induction ms as [| [k' u']]; [discriminate | simpl in *].
      assert (HT := compat_compare k k'); destruct (comp k k'); [subst k' | discriminate |].
      - inversion HFnd; subst u'; reflexivity.
      - apply IHms; assumption.
    Qed.

    Lemma pre_fdMap_lookup_nf f (m : K -f> U) k (HFnd : m k = None) : (pre_fdMap f m) k = None.
    Proof.
      apply fdLookup_notin_strong; rewrite <- pre_fdMap_dom_same; apply fdLookup_notin_strong; assumption.
    Qed.

    Program Definition fdMap (f : U -m> V) : (K -f> U) -m> (K -f> V) :=
      m[(pre_fdMap f)].
    Next Obligation.
      intros m1 m2 HEq; destruct n as [| n]; [apply dist_bound |]; intros k; simpl; specialize (HEq k).
      destruct (m1 k) as [u1 |] eqn: HFnd1; destruct (m2 k) as [u2 |] eqn: HFnd2; try contradiction HEq; [|].
      - rewrite pre_fdMap_lookup with (u := u1), pre_fdMap_lookup with (u := u2);
        [apply met_morph_nonexp |..]; assumption.
      - rewrite !pre_fdMap_lookup_nf; assumption.
    Qed.
    Next Obligation.
      intros m1 m2 Subm k; specialize (Subm k); destruct (m1 k) as [u1 |] eqn: HFnd1.
      - erewrite pre_fdMap_lookup by eassumption.
        destruct (m2 k) as [u2 |] eqn: HFnd2; [| contradiction Subm].
        erewrite pre_fdMap_lookup by eassumption.
        unfold pord in *; simpl in *.
        rewrite Subm; reflexivity.
      - rewrite pre_fdMap_lookup_nf by assumption; exact I.
    Qed.

    Global Instance fdMap_resp : Proper (equiv ==> equiv) fdMap.
    Proof.
      intros f1 f2 EQf m k; destruct (m k) as [u |] eqn: HFnd; simpl morph.
      - rewrite !pre_fdMap_lookup with (u := u) by assumption.
        rewrite EQf; apply morph_resp; reflexivity.
      - rewrite !pre_fdMap_lookup_nf by assumption; reflexivity.
    Qed.

    Global Instance fdMap_nonexp n : Proper (dist n ==> dist n) fdMap.
    Proof.
      intros f1 f2 EQf m; destruct n as [| n]; [apply dist_bound |]; intros k.
      simpl morph; destruct (m k) as [u |] eqn: HFnd.
      - rewrite !pre_fdMap_lookup with (u := u) by assumption.
        unfold dist; simpl; rewrite EQf; apply met_morph_nonexp; reflexivity.
      - rewrite !pre_fdMap_lookup_nf by assumption; reflexivity.
    Qed.

    Global Instance fdMap_monic : Proper (pord ==> pord) fdMap.
    Proof.
      intros f1 f2 Subf m k; simpl morph.
      destruct (m k) as [u |] eqn: HFnd.
      - erewrite !pre_fdMap_lookup by eassumption.
        unfold pord; simpl; apply (Subf u).
      - rewrite !pre_fdMap_lookup_nf by assumption.
        reflexivity.
    Qed.

    Notation "fd [ x -> v ]" := (fdUpdate x v fd) (at level 50, x at next level).
    Notation "fd \ x" := (fdRemove x fd) (at level 50).
    
    Lemma eq_SS : forall ks (fP fP' : StrictSorted ks), fP = fP'.
    Proof.
      clear -compK; induction ks; intros.
      + refine (match fP as fP in StrictSorted xs return
                      match xs return StrictSorted xs -> Prop with
                        | nil => fun fP => fP = fP'
                        | _ => fun _ => True
                      end fP with
                  | SS_nil => match fP' as gP in StrictSorted xs return
                                   match xs return StrictSorted xs -> Prop with
                                     | nil => fun gP => SS_nil = gP
                                     | _ => fun _ => True
                                   end gP with
                               | SS_nil => eq_refl
                               | _ => I
                             end
                  | _ => I
                end).
      + refine (match fP as fP in StrictSorted xs return
                      match xs return StrictSorted xs -> Prop with
                        | nil => fun _ => True
                        | k :: ks => fun fP =>
                                      forall fP' (IHks : forall fP fP' : StrictSorted ks, fP = fP'), fP = fP'
                      end fP with
                  | SS_nil => I
                  | SS_sing x => _
                  | SS_cons x x' xs HSS HLt => _
                end fP' IHks); clear -compK; intros.
        * refine (match fP' as fP in StrictSorted xs return
                        match xs return StrictSorted xs -> Prop with
                          | k :: nil => fun fP => SS_sing k = fP
                          | _ => fun _ => True
                        end fP with
                    | SS_sing x => eq_refl
                    | _ => I
                  end).
        * refine (match fP' as fP in StrictSorted xs return
                        match xs return StrictSorted xs -> Prop with
                          | x :: x' :: xs => fun fP => forall HSS HLt (IHks : forall fP fP' : StrictSorted (x' :: xs), fP = fP'), SS_cons x x' xs HSS HLt = fP
                          | _ => fun _ => True
                        end fP with
                    | SS_cons x x' xs HSS HLt => _
                    | _ => I
                  end HSS HLt IHks); clear -compK.
          intros; f_equal; [apply IHks | clear -compK].
          apply DC.UIP.
    Qed.          

    Lemma eq_fd (f g : K -f> V) (HEq : findom_t f = findom_t g) : f = g.
    Proof.
      destruct f; destruct g; simpl in *; subst; f_equal; apply eq_SS.
    Qed.

    Lemma fin_Ind : forall (P : (K -f> V) -> Prop)
                      (HNil : P fdEmpty)
                      (HExt : forall k v f, P f -> P (fdUpdate k v f)),
                    forall f, P f.
    Proof.
      clear dependent U.
      intros.
      destruct f as [fs fP].
      induction fs; simpl in *. 
      - assert ({| findom_t := nil; findom_P := fP |} = fdEmpty (V := V)) by (apply eq_fd; reflexivity); rewrite H; assumption.
      - destruct a as [k v]; simpl in *.
        inversion fP; subst; [destruct fs;[|discriminate]|].
        + specialize (HExt k v fdEmpty HNil). 
          unfold fdUpdate in HExt.
          unfold pre_upd in HExt. simpl in HExt.
          assert ({| findom_t := (k, v) :: nil; findom_P := fdUpdate_obligation_1 k v fdEmpty |} = {| findom_t := (k, v) :: nil; findom_P := fP |}) by (apply eq_fd; reflexivity). rewrite <- H; assumption.        
        + rewrite H1 in HS. specialize (HExt k v ({|findom_t := fs; findom_P := HS |}) (IHfs HS)).
          assert (findom_t (fdUpdate k v {| findom_t := fs; findom_P := HS |}) = (k,v)::fs).
          {
          unfold fdUpdate; simpl. 
          unfold pre_upd.          
          destruct fs; [discriminate|]. 
          inversion H1; subst; simpl (fst (k,v)).
          rewrite HLt; reflexivity.
          }
          assert ( fdUpdate k v {| findom_t := fs; findom_P := HS |} =
                   {| findom_t := (k, v) :: fs; findom_P := fP |}) by (apply eq_fd; assumption).
          rewrite <- H0; assumption.
Qed.

  End Map.

  Section Filter.
    Context V `{cmV : cmetric V}.

    Lemma filter_split A (p : A -> bool) x xs ys (HEq : x :: xs = filter p ys) :
      exists ysf, exists yst, ys = ysf ++ x :: yst /\ xs = filter p yst /\ filter p ysf = nil.
    Proof.
      induction ys; simpl in *; [discriminate |].
      destruct (p a) eqn: PA; [inversion HEq; subst | specialize (IHys HEq) ].
      + eexists nil; exists ys; tauto.
      + destruct IHys as [ysf [yst [EQ1 [EQ2 EQ3]]]]; exists (a :: ysf); exists yst.
        simpl; subst; rewrite PA; tauto.
    Qed.

    Lemma SS_app xs ys (HSS : StrictSorted (xs ++ ys)) :
      StrictSorted xs /\ StrictSorted ys.
    Proof.
      induction xs; simpl in *; [split; [apply SS_nil | assumption] |].
      assert (HSS' : StrictSorted xs /\ StrictSorted ys) by (eapply IHxs, SS_tail, HSS).
      clear IHxs; destruct HSS' as [HSSxs HSSys]; split; [| assumption]; clear HSSys.
      destruct xs; [apply SS_sing | apply SS_cons; [assumption |]].
      inversion HSS; subst; assumption.
    Qed.

    Program Definition fdFilter (p : V -> bool) (m : K -f> V) : K -f> V :=
      mkFD (filter (fun a : K * V => p (snd a)) (findom_t m)) _.
    Next Obligation.
      destruct m as [ms mP]; unfold findom_f in *; simpl in *.
      remember (filter (fun a => p (snd a)) ms) as ns.
      generalize dependent ms; induction ns; intros; [apply SS_nil |].
      apply filter_split in Heqns; destruct Heqns as [msf [mst [EQ1 [EQ2 _]]]]; subst.
      rewrite map_app in mP; apply SS_app in mP; destruct mP as [_ mP].
      specialize (IHns mst (SS_tail _ _ mP) (eq_refl _)).
      remember (filter (fun a => p (snd a)) mst) as ns; destruct ns; [apply SS_sing |].
      apply SS_cons; [assumption |]; clear IHns.
      apply filter_split in Heqns; destruct Heqns as [nsf [nst [EQ1 [EQ2 EQ3]]]]; subst.
      clear - mP compK; induction nsf; [simpl; inversion mP; subst; assumption |].
      apply IHnsf; clear IHnsf.
      destruct nsf; simpl in *.
      + inversion mP; subst; clear mP.
        inversion HS; subst; clear HS.
        apply comp_Lt_lt in HLt; apply comp_Lt_lt in HLt0; destruct HLt, HLt0.
        apply SS_cons; [assumption | apply comp_lt_Lt; split; [etransitivity; eassumption | ]].
        intros EQ; rewrite EQ in H.
        apply H2, ord_part; split; assumption.
      + inversion mP; subst; clear mP.
        inversion HS; subst; clear HS.
        apply comp_Lt_lt in HLt; apply comp_Lt_lt in HLt0; destruct HLt, HLt0.
        apply SS_cons; [assumption | apply comp_lt_Lt; split; [etransitivity; eassumption | ]].
        intros EQ; rewrite EQ in H.
        apply H2, ord_part; split; assumption.
    Qed.

  End Filter.

  Section MapProps.

    Context U V W `{pcmU : pcmType U} `{cmV : pcmType V} `{cmW : pcmType W}.

    Lemma fdMap_comp (f : U -m> V) (g : V -m> W) :
      (fdMap _ _ g  fdMap _ _ f == fdMap _ _ (g  f))%pm.
    Proof.
      intros m k; simpl morph.
      destruct (m k) as [u |] eqn: HFnd.
      - rewrite pre_fdMap_lookup with (u := u) by assumption.
        rewrite pre_fdMap_lookup with (u := f u); [reflexivity |].
        rewrite pre_fdMap_lookup with (u := u) by assumption; reflexivity.
      - rewrite !pre_fdMap_lookup_nf; [reflexivity |..]; try assumption; [].
        rewrite pre_fdMap_lookup_nf; reflexivity || assumption.
    Qed.

    Lemma fdMap_id : fdMap _ _ (pid U) == (pid (K -f> U)).
    Proof.
      intros w k; simpl morph.
      destruct (w k) as [v |] eqn: HFnd.
      - rewrite pre_fdMap_lookup with (u := v) by assumption; reflexivity.
      - rewrite pre_fdMap_lookup_nf by assumption; reflexivity.
    Qed.

    Context {extV : extensible V}.

    Definition Extend_fd (me md : K -f> V) :=
      findom_map _ _ me
                 (fun x (HIn : inlst x (dom me) = true) =>
                    let b := inlst x (dom md) in
                    let ve := Indom_lookup x (findom_t me) HIn in
                    match b as b return inlst x (dom md) = b -> V with
                      | true => fun eq => extend ve (Indom_lookup x (findom_t md) eq)
                      | false => fun _ => ve
                    end eq_refl).
    Local Obligation Tactic := idtac.

    Global Program Instance extensible_fd : extensible (K -f> V) := mkExtend Extend_fd.
    Next Obligation.
      clear dependent U; clear dependent W; intros; intros k; unfold Extend_fd.
      destruct (inlst k (dom ve)) eqn: HIne.
      - rewrite findom_map_app with (HIn := HIne).
        generalize (@eq_refl _ (inlst k (dom vd))) as HInd.
        pattern (inlst k (dom vd)) at 2 3; destruct (inlst k (dom vd)); intros.
        + specialize (HD k); specialize (HS k).
          rewrite <- Indom_lookup_find with (HIn := HIne).
          rewrite <- Indom_lookup_find with (HIn := HIne) in HS.
          rewrite <- Indom_lookup_find with (HIn := HInd) in HD.
          destruct (v k) as [vv |]; [| contradiction HD].
          unfold dist, pord in *; simpl in *.
          eapply extend_dist; eassumption.
        + rewrite Indom_lookup_find; reflexivity.
      - rewrite findom_map_app_nf by assumption.
        rewrite NIn_inlst, fdLookup_notin in HIne.
        rewrite HIne; reflexivity.
    Qed.
    Next Obligation.
      clear dependent U; clear dependent W; intros; intros k.
      specialize (HD k); destruct (vd k) as [v1 |] eqn: HFnd1; [| exact I].
      specialize (HS k); destruct (v k) as [v2 |]; [| contradiction HD].
      destruct (ve k) as [v3 |] eqn: HFnd2; [| contradiction HS].
      assert (HInd : inlst k (dom vd) = true) by (rewrite In_inlst, fdLookup_in_strong; eauto).
      assert (HIne : inlst k (dom ve) = true) by (rewrite In_inlst, fdLookup_in_strong; eauto).
      unfold extend, Extend_fd.
      rewrite findom_map_app with (HIn := HIne).
      generalize (@eq_refl _ (inlst k (dom vd))).
      pattern (inlst k (dom vd)) at 2 3; rewrite HInd; clear HInd; intros HInd.
      unfold dist, pord in *; simpl in *.
      rewrite <- Indom_lookup_find with (HIn := HInd) in HFnd1.
      inversion HFnd1; subst v1; clear HFnd1.
      rewrite <- Indom_lookup_find with (HIn := HIne) in HFnd2.
      inversion HFnd2; subst v3; clear HFnd2.
      eapply extend_sub; eassumption.
    Qed.

  End MapProps.

End FinDom.

Arguments fdMap {K cT ord equ preo ord_part compK U V eqT mT cmT pTA pcmU eqT0 mT0 cmT0 pTA0 cmV} _.