MetricCore.v 34.1 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 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 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 555 556 557 558 559 560 561 562 563 564 565 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 960 961 962 963 964 965 966 967 968 969 970
(** This module implements the core theory of complete bisected ultrametric
    spaces. It starts with their definition and simple properties. In the last part
    the standard constructions are defined, the same as in CSetoids.

    The distance function is really defined as picking out equivalence classes
    directly, instead of the usual definition with a map into reals. The approaches
    are equivalent for bisected metric spaces. *)

Require Export CSetoid.
Require Import Omega.
Require Import Min Max.

Open Scope nat_scope.

Generalizable Variables T U V W.

(** ** 1-Bounded bisected Ultra Metric type
    d_n(x,y) <-> |x - y| <= 1/2^n *)

(** Metric on the [type] M with requirements. Note that this only covers bisected metric spaces. *)
Class metric (T : Type) {eqT : Setoid T} :=
  { dist         :  nat -> T -> T -> Prop;
    dist_morph n :> Proper (equiv ==> equiv ==> iff) (dist n);
    dist_refl    :  forall x y, (forall n, dist n x y) <-> x == y;
    dist_sym   n :> Symmetric (dist n);
    dist_trans n :> Transitive (dist n);
    dist_mono    :  forall n x y, dist (S n) x y -> dist n x y;
    dist_bound   :  forall x y, dist 0 x y}.

Notation "'mkMetr' D" := (Build_metric _ _ D _ _ _ _ _ _) (at level 10).

Record Mtyp :=
  { mtyp  :> eqType;
    mmetr : metric mtyp}.
Instance mtyp_proj_metr {M : Mtyp} : metric M := mmetr M.
Definition mfromType (T : Type) `{mT : metric T} := Build_Mtyp (fromType T) _.

Section DistProps.
  Context `{mT : metric T}.

  Lemma mono_dist x y m n (HLe : m <= n) : dist n x y -> dist m x y.
  Proof.
    induction HLe; [tauto |].
    intros HS; apply IHHLe, dist_mono; assumption.
  Qed.

  (** The spaces are ultrametric spaces. *)
  Lemma tai_dist x y z n m (HL : dist n x y) (HR : dist m y z) :
    dist (min m n) x z.
  Proof.
    etransitivity; eapply mono_dist; try eassumption; eauto using le_min_r, le_min_l.
  Qed.

  Global Instance Reflexive_dist n : Reflexive (dist n).
  Proof. intros x; revert n; rewrite dist_refl; reflexivity. Qed.

End DistProps.

Notation "x '=' n '=' y" := (dist n x y).

Instance dist_iff `{metric T} n : Proper (dist n ==> dist n ==> iff) (dist n).
Proof.
  intros x y EQxy u v EQuv; split; intros EQ; [symmetry in EQxy, EQuv |];
  rewrite EQxy, EQuv; assumption.
Qed.

Existing Class le.

Existing Instance le_plus_trans.
Instance le_plus_trans' n m p {HLe : n <= p} : n <= m + p.
Proof.
  rewrite plus_comm; apply _.
Qed.
Existing Instance le_S.
Existing Instance le_n.
Instance max_le_tr_l n m p {HLe : n <= m} : n <= max m p.
Proof.
  rewrite HLe; apply le_max_l.
Qed.
Instance max_le_tr_r n m p {HLe : n <= p} : n <= max m p.
Proof.
  rewrite HLe; apply le_max_r.
Qed.

Instance mono_proper `{metric T} m n {HLe : n <= m} :
  Proper (dist m ==> dist m ==> iff) (dist n).
Proof.
  intros m1 m2 EQm m3 m4 EQm'.
  eapply mono_dist in EQm; [| eassumption].
  eapply mono_dist in EQm'; [| eassumption].
  rewrite EQm, EQm'; reflexivity.
Qed.

(** Cauchy chains of elements of a metric spaces. This is a very strong form of
convergence, since we require than all elements after the n-th are closer than 2⁻ⁿ.*)
Definition chain (T : Type) := nat -> T.
Class cchain `{mT : metric T} (σ : chain T) :=
  chain_cauchy : forall n i j {HLei : n <= i} {HLej : n <= j}, (σ i) = n = (σ j).

Arguments cchain [T eqT mT] σ.
Arguments chain_cauchy [T eqT mT] _ _ n i j {HLei HLej}.

Section Chains.
  Context `(σ : chain T) `{σc : cchain _ σ}.

  (** n-th tail of the sequence *)
  Definition cutn (n : nat) : chain T := fun i => σ (n + i).
  Global Instance cutn_cauchy (n : nat) : cchain (cutn n).
  Proof.
    intros k i j HLei HLej.
    unfold cutn.
    apply mono_dist with (n + k); [apply _ |].
    apply σc; now apply plus_le_compat_l.
  Qed.

  (** Constant chains are chains. *)
  Global Instance const_chain m : cchain (fun _ => m).
  Proof. unfold cchain; reflexivity. Qed.

  (** Chain [c] converges to [x].
      NOTE: Interesting that here you require an existence of [m] and not that every element after n-th is closer than 2⁻ⁿ. *)
  Definition mconverge (m : T) :=
    forall n, exists k, forall i {HLe : k <= i}, m = n = (σ i).

End Chains.

Class cmetric T `{mT : metric T} :=
  { compl       : forall σ {σc : cchain σ}, T;
    conv_cauchy : forall σ {σc : cchain σ}, mconverge σ (compl σ)}.

Notation "'mkCMetr' C" := (Build_cmetric _ _ _ C _) (at level 10).

(*(** Completion assigns to each Cauchy chain an element of M, such that the chain
converges to that element, i.e. it assigns it an actual limit. *)
Class Completion M `{mM : metric M} := mcompl : forall (σ : chain M) (σc : cchain σ), M.
Arguments mcompl {M e eqM D mM Completion} σ {σc}.

Class cmetric M `{mM : metric M} {cM : Completion M} :=
  conv_cauchy : forall σ {σc : cchain σ}, mconverge σ (mcompl σ).
*)

Record cmtyp :=
  { cmm  :> Mtyp;
    iscm :  cmetric cmm}.
Instance cmtyp_cmetric {M : cmtyp} : cmetric M := iscm M.
Definition cmfromType (T : Type) `{cT : cmetric T} := Build_cmtyp (mfromType T) _.

Section ChainCompl.
  Context `{cT : cmetric T} (σ ρ : chain T) {σc : cchain σ} {ρc : cchain ρ}.

  Lemma umet_complete_extn n (HEq : forall i, σ i = n = ρ i) :
    compl σ = n = compl ρ.
  Proof.
    destruct (conv_cauchy σ n) as [m Hm]; destruct (conv_cauchy ρ n) as [k Hk].
    rewrite Hm, Hk; eauto using le_max_l, le_max_r.
  Qed.

  Lemma umet_complete_ext :
    (forall i, σ i == ρ i) -> compl σ == compl ρ.
  Proof.
    intros HEq; rewrite <- dist_refl; intros n; apply umet_complete_extn.
    intros i; revert n; rewrite dist_refl; apply HEq.
  Qed.

  Lemma umet_complete_const m : compl (fun _ => m) == m.
  Proof.
    symmetry; rewrite <- dist_refl; intros n.
    destruct (conv_cauchy (fun _ => m) n) as [k Hk]; rewrite Hk; eauto || reflexivity.
  Qed.

  (** Limits don't depend on prefixes of sequences. *)
  Lemma cut_complete_eq n :
    compl σ == compl (cutn σ n).
  Proof.
    rewrite <- dist_refl; intros m; destruct (conv_cauchy σ m) as [k Hk].
    destruct (conv_cauchy (cutn σ n) m) as [j Hj]; simpl in *.
    unfold cutn in *; rewrite Hj, Hk; [reflexivity | | apply le_max_l]; clear Hk Hj.
    apply _.
  Qed.

End ChainCompl.

(** Morphisms of metric spaces — non-expansive functions. *)
Record metric_morphism T U `{mT : metric T} `{mU : metric U} :=
  mkUMorph
    { met_morph :> T -=> U;
      met_morph_nonexp n : Proper (dist n ==> dist n) met_morph}.

Arguments mkUMorph [T U eqT mT eqT0 mU] _ _.
Arguments met_morph [T U] {eqT mT eqT0 mU} _.
Infix "-n>" := metric_morphism (at level 45, right associativity).
Notation "'n[(' f ')]'" := (mkUMorph s[(f)] _).

Instance subrel_dist `{mT : metric T} n : subrelation equiv (dist n).
Proof.
  intros x y HEq; revert n; rewrite dist_refl; assumption.
Qed.

Section MMInst.
  Context `{mT : metric T} `{mU : metric U}.

  Global Program Instance nonexp_type : Setoid (T -n> U) :=
    mkType (fun f g => met_morph f == g).
  Next Obligation.
    split.
    + intros f x; reflexivity.
    + intros f g HS x; symmetry; apply HS.
    + intros f g h Hfg Hgh x; etransitivity; [apply Hfg | apply Hgh].
  Qed.

  Global Program Instance nonexp_metric : metric (T -n> U) :=
    mkMetr (fun n f g => forall x, f x = n = g x).
  Next Obligation.
    intros f1 f2 EQf g1 g2 EQg; split; intros EQfg x; [symmetry in EQf, EQg |];
    rewrite (EQf x), (EQg x); apply EQfg.
  Qed.
  Next Obligation.
    split; [intros HEq t | intros HEq n].
    - rewrite <- dist_refl; intros n; apply HEq.
    - intros t; revert n; rewrite dist_refl; apply HEq.
  Qed.
  Next Obligation.
    intros f g HS x; symmetry; apply HS.
  Qed.
  Next Obligation.
    intros f g h Hfg Hgh x; etransitivity; [apply Hfg | apply Hgh].
  Qed.
  Next Obligation.
    eauto using mono_dist.
  Qed.
  Next Obligation.
    apply dist_bound.
  Qed.

(*
  (** Note the set of morphisms, not the set of non-expansive maps. The distance is the supremum of pointwise distances. *)
  Global Program Instance fundistS : Dist (M -s> N) :=
    fun n f g => forall x, f x = n = g x.

  (** Note the set of non-expansive maps with the point-wise distance. *)
  Global Program Instance fundist : Dist (M -n> N) :=
    fun n f g => met_morph f = n = met_morph g.

  (** The hom-set (i.e. the set of non-expansive maps) is again a bisected ultrametic spaces. *)
  Global Instance MMmetric : metric (M -n> N) (D := fundist).
  Proof.
    split.
    + split; [intros HEq t | intros HEq n].
      * rewrite <- dist_refl; intros n; apply HEq.
      * intros t; revert n; rewrite dist_refl; apply HEq.
    + intros n f g HS x; symmetry; apply HS.
    +intros n f g h Hfg Hgh x; etransitivity; [apply Hfg | apply Hgh].
    + intros n f g HS x; simpl in *; eapply mono_dist; [| apply HS]; omega.
    + intros f g x; apply dist_bound.
    + intros n f1 f2 EQf g1 g2 EQg; split; intros EQfg x; [symmetry in EQf, EQg |];
      rewrite (EQf x), (EQg x); apply EQfg.
  Qed.
*)

End MMInst.

(** The next ones just seem to be "lemmas" stating that metric morphisms and morphisms preserve suitable equalities. *)
Instance mmorph_proper n `{mT : metric T} `{mU : metric U} :
  Proper (dist n ==> dist n ==> dist n) (met_morph (T := T) (U := U)).
Proof.
  intros f g HEq x y HEq'; etransitivity; [apply HEq | apply g, HEq'].
Qed.

Definition distS `{eqT : Setoid T} `{mU : metric U} n (f g : T -=> U) :=
  forall x, f x = n = g x.

Instance mmorph_properS n `{mT : metric T} `{mU : metric U} :
  Proper (distS n ==> equiv ==> dist n) (morph T U).
Proof.
  intros f g HEq x y HEq'; rewrite HEq'; apply HEq.
Qed.

Instance mmorph_inherit `{mT : metric T} `{mU : metric U} :
  Proper (equiv ==> equiv) (met_morph (T := T) (U := U)).
Proof. intros f g HEq; apply HEq. Qed.

Instance mmorph_extend `{mT : metric T} `{mU : metric U} n :
  Proper (dist n ==> distS n) (met_morph (T := T) (U := U)).
Proof. intros f g HEq x; rewrite (HEq x); reflexivity. Qed.

Instance morph_proper' n `{mT : metric T} `{mU : metric U} (f : T -n> U) :
  Proper (dist n ==> dist n) f := met_morph_nonexp _ _ _ _.

Ltac resp_dist := intros n; resp_set.

Section MCont.
  Context `{cT : cmetric T} `{cU : cmetric U} `{cV : cmetric V}.

  (** Definition of contractive functions. This works since the spaces are bisected. *)
  Class contractive (f : T -n> U) := contr n : Proper (dist n ==> dist (S n)) f.

  (** Image of a Cauchy chain by a non-expansive function is another Cauchy sequence. *)
  Definition liftc (f : T -> U) (σ : chain T) : chain U := fun i => f (σ i).
  Arguments liftc f σ i / .
  Global Instance liftc_cauchy (f : T -n> U) (σ : chain T) {σc : cchain σ} :
    cchain (liftc f σ).
  Proof.
    intros n i j HLei HLej; simpl.
    rewrite (chain_cauchy σ); reflexivity || assumption.
  Qed.

  (** The same as before, only for two-argument functions. *)
  Definition binaryLimit (f : T -n> U -n> V) (σ : chain T) (ρ : chain U) : chain V :=
    fun i => f (σ i) (ρ i).
  Arguments binaryLimit f σ ρ i / .
  Global Instance binLim_cauchy (f : T -n> U -n> V) (σ : chain T) (ρ : chain U) {σc : cchain σ} {ρc : cchain ρ} : cchain (binaryLimit f σ ρ).
  Proof.
    intros n i j HLei HLej; simpl.
    rewrite (chain_cauchy σ), (chain_cauchy ρ); reflexivity || assumption.
  Qed.

  (** Non-expansive functions preserve limits, i.e. are continuous. *)
  Lemma nonexp_continuous (f : T -n> U) (σ : chain T) (σc : cchain σ) :
    f (compl σ) == compl (liftc f σ).
  Proof.
    rewrite <- dist_refl; intros n; destruct (conv_cauchy σ n) as [k B].
    destruct (conv_cauchy (liftc f σ) n) as [m A]; simpl in *.
    specialize (B (max m k) _); specialize (A (max m k) _).
    rewrite B, A; reflexivity.
  Qed.

  Local Obligation Tactic := intros; resp_set || program_simpl.

  (** Composition of non-expansive maps is non-expansive. *)
  Program Definition umcomp (f : U -n> V) (g : T -n> U) : T -n> V :=
    n[(f << g)].

  Program Definition lift2m (f : T -=> U -=> V) p q : (T -n> U -n> V) :=
    mkUMorph s[(fun x => mkUMorph (f x) (p x))] q.

End MCont.

Infix "<M<" := umcomp (at level 35).

Section MCompP.
  Context `{cT : cmetric T} `{cU : cmetric U} `{cV : cmetric V} `{cW : cmetric W}.
  
  (** Composition preserves distances. *)
  Global Instance ndist_umcomp n :
    Proper (dist n (T := U -n> V) ==> dist n ==> dist n) umcomp.
  Proof. intros f f' HEq g g' HEq' x; simpl; rewrite HEq, HEq'; reflexivity. Qed.

  Lemma lift_comp (f : U -n> V) (g : T -n> U) (σ : chain T) {σc : cchain σ} :
    compl (liftc f (liftc g σ)) == compl (liftc (f <M< g) σ).
  Proof.
    apply umet_complete_ext; try apply _; intros i; reflexivity.
  Qed.

  Lemma mcomp_assoc (f : V -n> W) (g : U -n> V) (h : T -n> U) :
    f <M< (g <M< h) == (f <M< g) <M< h.
  Proof. intros x; reflexivity. Qed.

  Local Obligation Tactic := intros; resp_set || program_simpl.

  (** Composition as a _non-expansive_ morphism itself. This then shows that the
  category of bisected spaces is enriched in itself. *)
  Program Definition comp : (U -n> V) -n> (T -n> U) -n> T -n> V :=
    lift2m (lift2s (fun f g => f <M< g) _ _) _ _.

  Program Definition umid : T -n> T := n[(mid _)].

  Program Definition umconst x : T -n> U := n[(mconst x)].

  Global Program Instance umconst_contractive m : contractive (umconst m).

  Program Definition precomp_ne (f : T -n> U) : (U -n> V) -n> (T -n> V) :=
    n[(fun g => g <M< f)].

  Program Definition postcomp_ne (f : T -n> U) : (V -n> T) -n> (V -n> U) :=
    n[(fun g => f <M< g)].

End MCompP.

Arguments umid T {eqT mT}.

(** Single element space and the distance on it. *)
Program Instance unit_metric : metric unit :=
  mkMetr (fun _ _ _ => True).
Next Obligation. tauto. Qed.

(** The unit space is complete. *)
Program Instance unit_cmetric : cmetric unit :=
  mkCMetr (fun _ _ => tt).
Next Obligation.
  intros n; exists 0; intros k HLe; destruct (σ k); reflexivity.
Qed.

Section Iteration.
  Context `{mT : metric T}.

  Fixpoint iter n (f : T -> T) :=
    match n with
      | O => id
      | S n => fun x => f (iter n f x)
    end.

  (** Iteration of a non-expansive function again gives a non-expansive function. *)

  Program Definition itern n (f : T -n> T) : T -n> T :=
    n[(iter n f)].
  Next Obligation.
    induction n; simpl; [apply _ | resp_set].
  Qed.
  Next Obligation.
    induction n; simpl; [apply _ | resp_set].
  Qed.

  Lemma iter_plus f m n x : iter m f (iter n f x) = iter (m + n) f x.
  Proof. induction m; simpl; [reflexivity | f_equal; assumption]. Qed.

  (** If a function is contractive then after sufficiently many iterations it
  maps all elements closer than 2⁻ⁿ. *)
  Lemma bounded_contractive_n f {HC : contractive f} n m x y (HLe : n <= m) :
    iter m f x = n = iter m f y.
  Proof.
    revert m x y HLe; induction n; intros; [apply dist_bound |].
    destruct m; [inversion HLe |]; simpl; apply HC, IHn; omega.
  Qed.

  Global Instance cfix f {HC : contractive f} x : cchain (fun n => iter n f x).
  Proof.
    unfold cchain; intros.
    cutrewrite (i = n + (i - n)); [rewrite <- iter_plus | omega].
    cutrewrite (j = n + (j - n)); [rewrite <- iter_plus | omega].
    apply bounded_contractive_n; [assumption | auto].
  Qed.

End Iteration.

Section Fixpoints.
  Context `{cT : cmetric T}.

  (** A fixed point of a contractive f is the limit of the iterations of the
  function. This seemingly depends on the starting point x. *)
  Definition fixp f {HC : contractive f} x := compl (fun n => iter n f x).

  (** Stating that the proposed fixed point is in fact a fixed point. *)
  Lemma fixp_eq f x {HC : contractive f} : fixp f x == f (fixp f x).
  Proof.
    rewrite <- dist_refl; intros n; unfold fixp.
    destruct (conv_cauchy (fun n => iter n f x) n) as [m Hm].
    rewrite (Hm (S (max n m))), (Hm (max n m)) at 1; simpl; reflexivity || apply _.
  Qed.

  Lemma fixp_iter f x i {HC : contractive f} : fixp f x == iter i f (fixp f x).
  Proof.
    induction i; [reflexivity |].
    simpl; rewrite fixp_eq, IHi at 1; reflexivity.
  Qed.

  (** Fixed points are unique, i.e. the fixp does not depend on the starting point of the iteration. *)
  Lemma fixp_unique f x y {HC : contractive f} : fixp f x == fixp f y.
  Proof.
    rewrite <- dist_refl; intros n; unfold fixp.
    destruct (conv_cauchy (fun n => iter n f x) n) as [mx Hmx].
    destruct (conv_cauchy (fun n => iter n f y) n) as [my Hmy].
    rewrite (Hmx (max n (max mx my))), Hmy;
      [ rewrite bounded_contractive_n | ..]; reflexivity || apply _.
  Qed.

  (** This lemma states that fixp is non-expansive in f. *)
  Lemma fixp_ne (f f' : T -n> T) {HC : contractive f} (HC' : contractive f') x x' n  (HEq : f = n = f') :
    fixp f x = n = fixp f' x'.
  Proof.
    rewrite fixp_unique with (x := x') (y := x).
    clear x'; unfold fixp; destruct (conv_cauchy (fun n => iter n f x) n) as [m Hm].
    destruct (conv_cauchy (fun n => iter n f' x) n) as [k Hk].
    rewrite (Hm (max m k)), (Hk (max m k)); try apply _; [].
    clear Hm Hk; induction (max m k); simpl; [reflexivity |].
    rewrite IHn0; apply HEq.
  Qed.

  (** From the non-expansiveness it also follows that fixp preserves equality of f. *)
  Lemma fixp_equiv (f f' : T -n> T) {HC : contractive f} (HC' : contractive f') x x' (HEq : f == f') :
    fixp f x == fixp f' x'.
  Proof.
    rewrite <- dist_refl; intros n; apply fixp_ne.
    rewrite HEq; reflexivity.
  Qed.

  (** The above properties should be enough to reason about fixpoints, so we make the definition opaque *)
  Global Opaque fixp.

End Fixpoints.

Section ChainApps.
  Context `{cT : cmetric T} `{cU : cmetric U} (σ : chain (T -n> U)) {σc : cchain σ}.

  (** A cauchy chain applied to an element gives another Cauchy chain. *)
  Global Instance chain_app x : cchain (fun i => σ i x).
  Proof. unfold cchain; intros; rewrite (chain_cauchy σ); reflexivity || assumption. Qed.

  Instance nonexp_lub n : Proper (dist n ==> dist n) (fun x => compl (fun i => σ i x)).
  Proof.
    intros x y HEq; destruct (conv_cauchy (fun i => σ i x) n) as [mx Hmx].
    destruct (conv_cauchy (fun i => σ i y) n) as [my Hmy].
    rewrite Hmx, Hmy; simpl; [rewrite HEq; reflexivity | ..]; auto using le_max_r, le_max_l.
  Qed.

  (** Given a Cauchy chain of functions we get a non-expansive function by
  taking limits starting at different points. Used to show that the hom-set is a
  complete metric space. *)
  Program Definition fun_lub : T -n> U :=
    n[(fun x => compl (fun i => σ i x))].
  Next Obligation.
    intros x y HEq; rewrite <- dist_refl; intros n.
    rewrite (nonexp_lub n); [| rewrite HEq]; reflexivity.
  Qed.
  Next Obligation. exact (nonexp_lub n). Qed.

End ChainApps.

Section NonexpCMetric.
  Context `{cT : cmetric T} `{cU : cmetric U}.

  (** THe set of non-expansive morphisms between two complete metric spaces is again a complete metric space. *)
  Global Program Instance nonexp_cmetric : cmetric (T -n> U) :=
    mkCMetr fun_lub.
  Next Obligation.
    intros n; exists n; intros m HLe x.
    destruct (conv_cauchy (fun i => σ i x) n) as [k Hk].
    rewrite (Hk (max m k)), (chain_cauchy σ); [reflexivity |..]; apply _.
  Qed.

End NonexpCMetric.

(** Product of two complete metric spaces. *)
Section MetricProducts.
  Context `{cT : cmetric T} `{cU : cmetric U} `{cV : cmetric V}.

  Local Obligation Tactic := intros; apply _ || resp_set || program_simpl.

  Definition prod_dist n (p1 p2 : U * V) :=
    fst p1 = n = fst p2 /\ snd p1 = n = snd p2.
  Global Arguments prod_dist n p1 p2 /.

  Global Program Instance prod_metric : metric (U * V) := mkMetr prod_dist.
  Next Obligation.
    intros [a1 b1] [a2 b2] [Ha Hb] [a3 b3] [a4 b4] [Ha' Hb']; simpl in *.
    rewrite Ha, Hb, Ha', Hb'; reflexivity.
  Qed.
  Next Obligation.
    split; intros HEq.
    + split; rewrite <- dist_refl; intros n; destruct (HEq n); assumption.
    + intros n; split; revert n; rewrite dist_refl; destruct HEq; assumption.
  Qed.
  Next Obligation.
    intros [a1 b1] [a2 b2] [Ha Hb]; split; symmetry; assumption.
  Qed.
  Next Obligation.
    intros [a1 b1] [a2 b2] [a3 b3] [Ha12 Hb12] [Ha23 Hb23]; split; etransitivity; eassumption.
  Qed.
  Next Obligation.
    destruct H; split; eapply mono_dist; try eassumption; auto.
  Qed.
  Next Obligation.
    split; apply dist_bound.
  Qed.

  Global Instance prod_proper_n n : Proper (dist n ==> dist n ==> dist n) (@pair U V).
  Proof. intros a a' Ha b b' Hb; split; assumption. Qed.

  Global Instance mfst_proper_n n : Proper (dist n ==> dist n) (@fst U V).
  Proof. intros [a1 b1] [a2 b2] [Ha Hb]; assumption. Qed.

  Global Instance msnd_proper_n n : Proper (dist n ==> dist n) (@snd U V).
  Proof. intros [a1 b1] [a2 b2] [Ha Hb]; assumption. Qed.

  Definition Mfst : U * V -n> U := n[(mfst)].
  Definition Msnd : U * V -n> V := n[(msnd)].

  Program Definition Mprod (f : T -n> U) (g : T -n> V) : T -n> U * V :=
    n[(mprod f g)].
  Next Obligation.
    intros x y HEq; simpl; rewrite HEq; split; reflexivity.
  Qed.

  Lemma Mprod_fst f g : Mfst <M< Mprod f g == f.
  Proof. intros x; reflexivity. Qed.

  Lemma Mprod_snd f g : Msnd <M< Mprod f g == g.
  Proof. intros x; reflexivity. Qed.

  Lemma Mprod_unique (f : T -n> U) (g : T -n> V) (h : T -n> U * V) :
    Mfst <M< h == f -> Msnd <M< h == g -> h == Mprod f g.
  Proof. intros HL HR; apply (mprod_unique HL HR). Qed.

  (** Product of complete spaces is again a complete space. *)
  Definition prod_compl (σ : chain (U * V)) (σc : cchain σ) :=
    (compl (liftc Mfst σ), compl (liftc Msnd σ)).
  Arguments prod_compl σ σc /.

  Global Program Instance prod_cmetric : cmetric (U * V) :=
    mkCMetr prod_compl.
  Next Obligation.
    intros n; destruct (conv_cauchy (liftc Mfst σ) n) as [mfst Hfst].
    destruct (conv_cauchy (liftc Msnd σ) n) as [msnd Hsnd].
    exists (max mfst msnd); intros k HLe; split; simpl in *;
      [apply Hfst | apply Hsnd]; eauto using le_max_l, le_max_r, le_trans.
  Qed.

End MetricProducts.

(** Indexed product, very similar to binary product. The metric is pointwise, the supremum. *)
Section MetricIndexed.
  Context {I : Type} {P : I -> Mtyp}.

  Local Obligation Tactic := intros; apply _ || resp_set || program_simpl.

  Definition distI n (a b : forall i, P i) := forall i, mprojI i a = n = mprojI i b.
  Global Arguments distI n a b /.

  Global Program Instance prodI_metr : metric (forall i, P i) :=
    mkMetr distI.
  Next Obligation.
    intros x y EQxy u v EQuv; split; intros EQ i; [symmetry in EQxy, EQuv |]; rewrite (EQxy i), (EQuv i); apply EQ.
  Qed.
  Next Obligation.
    split; intros HEq n.
    + rewrite <- dist_refl; intros m; apply (HEq m).
    + intros i; revert n; rewrite dist_refl; apply HEq.
  Qed.
  (*Next Obligation.
    intros x y HS i; symmetry; apply HS.
  Qed.*)
  Next Obligation.
    intros x y z Hxy Hyz i; etransitivity; [apply Hxy | apply Hyz].
  Qed.
  Next Obligation.
    eapply mono_dist, H; auto.
  Qed.
  Next Obligation.
    apply dist_bound.
  Qed.

  Program Definition MprojI (i : I) : (forall i, P i) -n> P i :=
    n[(mprojI i)].

  Context `{mT : metric T}.
  Program Definition MprodI (f : forall i, T -n> P i) : T -n> forall i, P i :=
    n[(mprodI f)].

  Lemma MprodI_proj f i : MprojI i <M< MprodI f == f i.
  Proof. intros x; reflexivity. Qed.

  Lemma MprodI_unique f g (HEq : forall i, MprojI i <M< g == f i) : g == MprodI f.
  Proof. apply (mprodI_unique f g HEq). Qed.

End MetricIndexed.

(** Indexed product of complete spaces is again a complete space. *)
Section CompleteIndexed.
  Context {I : Type} {P : I -> cmtyp}.

  Definition prodI_compl (σ : chain (forall i, P i)) (σc : cchain σ) (i : I) :=
    compl (liftc (MprojI i) σ).
  Arguments prodI_compl σ σc i /.
  Global Program Instance prodI_cmetric : cmetric (forall i, P i) :=
    mkCMetr prodI_compl.
  Next Obligation.
    intros n; exists n; intros m HLe i.
    destruct (conv_cauchy (liftc (MprojI i) σ) n) as [k Hk]; simpl in *.
    rewrite  Hk; [| apply le_max_r]; clear Hk.
    unfold liftc; apply σc; eauto using le_trans, le_max_l.
  Qed.

End CompleteIndexed.

Section Chains_of_IProds.
  Context {I : Type} {P : I -> cmtyp} (σ : chain (forall i, P i)) {σc : cchain σ}.

  Global Instance dep_chain_app (x : I) : cchain (fun n => σ n x).
  Proof.
    unfold cchain; intros; apply σc; assumption.
  Qed.

  Lemma dep_chain_compl (x : I) :
    compl σ x == compl (fun n => σ n x).
  Proof.
    apply umet_complete_ext; intros n; reflexivity.
  Qed.

End Chains_of_IProds.

Section ComplSetup.
  Context `{cT : cmetric T} `{cU : cmetric U} (σ : chain T) (ρ : chain U) {σc : cchain σ} {ρc : cchain ρ}.

  Definition chain_pair n := (σ n, ρ n).
  Global Instance cchain_pair : cchain chain_pair.
  Proof. split; simpl; eapply chain_cauchy; assumption. Qed.

  (** The limit in the product is computed pointwise, i.e. the limit is the pair
  of limits computed in original spaces. *)
  Lemma pair_limit : compl (chain_pair) == (compl σ, compl ρ).
  Proof. split; simpl; apply umet_complete_ext; intros i; reflexivity. Qed.

End ComplSetup.

(** The subspace defined by P is chain complete. *)
Class LimitPreserving `{cT : cmetric T} (P : T -> Prop) :=
  lim_pres : forall (σ : chain T) (σc : cchain σ), (forall i, P (σ i)) -> P (compl σ).

(** The set of contractive functions is complete in the set of non-expansive ones. *)
Instance contractive_complete `{cT : cmetric T} `{cU : cmetric U} :
  LimitPreserving (fun f : T -n> U => contractive f).
Proof.
  intros σ σc HC n x y HEq; destruct (conv_cauchy σ (S n)) as [m Hm].
  rewrite (Hm m); [apply HC |]; trivial.
Qed.

Section OptM.
  Context `{mT : metric T}.

  Definition option_dist n (x y : option T) :=
    match n with
      | O => True
      | S _ => match x, y with
                 | Some x, Some y => x = n = y
                 | None, None => True
                 | Some _, None => False
                 | None, Some _ => False
               end
      end.

  Global Program Instance option_metric : metric (option T) :=
    mkMetr option_dist.
  Next Obligation.
    destruct n as [| n]; intros [x |] [y |] EQxy [u |] [v |] EQuv; simpl in *; try (contradiction || reflexivity); [].
    unfold equiv in EQxy, EQuv; simpl in *; rewrite EQxy, EQuv; reflexivity.
  Qed.
  Next Obligation.
    split; intros HEq.
    - destruct x; destruct y; try (contradiction (HEq 1) || reflexivity); [].
      unfold equiv; simpl; rewrite <- dist_refl; intros n.
      specialize (HEq (S n)); eapply mono_dist, HEq; auto.
    - intros [| n]; [reflexivity |].
      destruct x; destruct y; try (contradiction HEq || reflexivity); simpl in *.
      generalize (S n); rewrite dist_refl; assumption.
  Qed.
  Next Obligation.
    destruct n as [| n]; intros [x |] [y |] HS; try (contradiction HS || reflexivity);
    simpl; symmetry; assumption.
  Qed.
  Next Obligation.
    revert n; intros [| n] [x |] [y |] [z |] Hxy Hyz; try (contradiction || reflexivity);
    simpl; etransitivity; [apply Hxy | apply Hyz].
  Qed.
  Next Obligation.
    destruct n as [n |]; destruct x as [x |]; destruct y as [y |]; try (contradiction H || reflexivity);
    simpl; eapply mono_dist, H; auto.
  Qed.

End OptM.

(** Subspaces. *)
Section Submetric.
  Context `{mT : metric T} {P : T -> Prop}.
  Local Obligation Tactic := intros; apply _ || resp_set || program_simpl.

  Definition subset_Dist n (x y : {e : T | P e}) := proj1_sig x = n = proj1_sig y.
  Global Arguments subset_Dist n x y /.

  Global Program Instance sub_metric : metric {e : T | P e} :=
    mkMetr subset_Dist.
  Next Obligation.
    intros [x Hx] [y Hy] EQxy [u Hu] [v Hv] EQuv; unfold equiv in EQxy, EQuv; simpl in *.
    rewrite EQxy, EQuv; reflexivity.
  Qed.
  Next Obligation.
    apply dist_refl.
  Qed.
  Next Obligation.
    intros [x Hx] [y Hy] [z Hz] Hxy Hyz; simpl in *; etransitivity; eassumption.
  Qed.
  Next Obligation.
    eapply mono_dist, H; auto.
  Qed.
  Next Obligation.
    apply dist_bound.
  Qed.

  Program Definition inclM : {e : T | P e} -n> T :=
    n[(mincl)].

  Context {U} `{mU : metric U}.

  Program Definition inheritM (f : U -n> T) (HAll : forall n, P (f n)) :=
    n[(minherit f HAll)].

  Lemma forgetM_mono f g (HF : inclM <M< f == inclM <M< g) : f == g.
  Proof. apply mforget_mono, HF. Qed.

End Submetric.

Section SubCMetric.
  Context `{cT : cmetric T} {P : T -> Prop} {C : LimitPreserving P}.

  (** If a space defined by P is complete (assumption [ccomplete P]) then it
  already contains the limits of its Cauchy chains. *)
  Lemma subchainlubP (σ : chain {x : T | P x}) {σc : cchain σ} :
    P (compl (liftc inclM σ)).
  Proof. apply C; intros i; unfold liftc; destruct (σ i); simpl; assumption. Qed.

  Definition sub_compl (σ : chain {x : T | P x}) {σc : cchain σ} :=
    exist P (compl (liftc inclM σ)) (subchainlubP σ).
  Global Program Instance sub_cmetric : cmetric {x : T | P x} :=
    mkCMetr sub_compl.
  Next Obligation.
    intros n; simpl; destruct (conv_cauchy (liftc inclM σ) n) as [m Hm].
    exists m; intros k HLe; apply (Hm _ HLe).
  Qed.

End SubCMetric.

Section Exponentials.
  Context `{mT : metric T} `{mU : metric U} `{mV : metric V}.
  Local Obligation Tactic := intros; apply _ || resp_set || program_simpl.

  Program Definition uncurry (f : T -n> U -n> V) : (T * U -n> V) :=
    n[(fun p => f (fst p) (snd p))].
  Next Obligation.
    intros [a1 b1] [a2 b2] [Ha Hb]; simpl in *.
    rewrite Ha, Hb; reflexivity.
  Qed.
  Next Obligation.
    intros [a1 b1] [a2 b2] [Ha Hb]; simpl in *.
    rewrite Ha, Hb; reflexivity.
  Qed.  

  Program Definition curryM (f : T * U -n> V) : T -n> U -n> V := lift2m (mcurry f) _ _.

  Context `{mW : metric W}.

  Definition prodM_map (f : T -n> U) (g : V -n> W) := Mprod (f <M< Mfst) (g <M< Msnd).

  Program Definition evalM : (T -n> U) * T -n> U :=
    n[(meval << mprod_map s[(met_morph (U := U))] (mid _))].
  Next Obligation.
    intros f g HEq; simpl; rewrite !HEq at 1; reflexivity.
  Qed.

End Exponentials.

Section ExponentialProps.
  Context `{mT : metric T} `{mU : metric U} `{mV : metric V}.

  Lemma curryMCom (f : T * U -n> V) : f == evalM <M< prodM_map (curryM f) (umid _).
  Proof. intros [a b]; reflexivity. Qed.

  Lemma curryM_unique (f : T * U -n> V) g (HEq : f == evalM <M< prodM_map g (umid _)) :
    g == curryM f.
  Proof. intros a b; simpl; rewrite HEq; reflexivity. Qed.

End ExponentialProps.

Lemma nonexp_cont2 `{cT : cmetric T} `{cU : cmetric U} `{cV : cmetric V} (f : T -n> U -n> V) (σ : chain T) (ρ : chain U) {σc : cchain σ} {ρc : cchain ρ} :
  f (compl σ) (compl ρ) == compl (binaryLimit f σ ρ).
Proof.
  assert (HT := nonexp_continuous (uncurry f) (chain_pair σ ρ) _).
  rewrite pair_limit in HT at 1; simpl in HT; rewrite HT; apply umet_complete_ext; intros i; clear HT.
  reflexivity.
Qed.

(** Discrete spaces are proper metric spaces (discrete meaning that the distance
    is 1 if elements are diffent and 0 for equal elements. Equality here is
    propositional Coq equality. *)
Section Discrete.
  Context {T : Type}.

  Program Instance discreteType : Setoid T := mkType (@eq T).

  Definition discreteDist n (x y : T) :=
    match n with
        O => True
      | _ => x = y
    end.
  Global Arguments discreteDist n x y / .

  Program Instance discreteMetric : metric T := mkMetr discreteDist.
  Next Obligation.
    split; intros HEq; [specialize (HEq 1) | intros [ | n] ];
    inversion HEq; subst; simpl; reflexivity.
  Qed.
  Next Obligation.
    destruct n as [| n]; intros x y HS; simpl in *; [| symmetry]; tauto.
  Qed.
  Next Obligation.
    destruct n as [| n]; intros x y z Hxy Hyz; simpl in *; [| etransitivity]; eauto.
  Qed.
  Next Obligation.
    destruct n; tauto.
  Qed.

  Definition discreteCompl (σ : chain T) {σc : cchain σ} := σ 1.

  Program Instance discreteCMetric : cmetric T := mkCMetr discreteCompl.
  Next Obligation.
    intros n; exists 1; simpl; intros [| i] HLe; [inversion HLe |].
    destruct n as [| n]; [exact I |].
    assert (HT := chain_cauchy σ _ 1 (S i) 1); inversion HT.
    rewrite H0; reflexivity.
  Qed.

End Discrete.

Section Option.
  Context `{cT : cmetric T}.

  Program Definition unSome (σ : chain (option T)) {σc : cchain σ} (HNE : σ 1 <> None) : chain T :=
    fun i => match σ (S i) with
               | None => False_rect _ _
               | Some v => v
             end.
  Next Obligation.
    specialize (σc 1 1 (S i)); rewrite <- Heq_anonymous in σc.
    destruct (σ 1) as [v |]; [contradiction σc; auto with arith | contradiction HNE; reflexivity].
  Qed.

  Instance unSome_c (σ : chain (option T)) {σc : cchain σ} HNE : cchain (unSome σ HNE).
  Proof.
    intros [| k] n m HLE1 HLE2; [apply dist_bound |]; unfold unSome.
    generalize (@eq_refl _ (σ (S n))); pattern (σ (S n)) at 1 3.
    destruct (σ (S n)) as [v |]; simpl; intros EQn.
    - generalize (@eq_refl _ (σ (S m))); pattern (σ (S m)) at 1 3.
      destruct (σ (S m)) as [v' |]; simpl; intros EQm.
      + specialize (σc (S k) (S n) (S m)); rewrite <- EQm, <- EQn in σc.
        apply σc; auto with arith.
      + exfalso; specialize (σc 1 1 (S m)); rewrite <- EQm in σc.
        destruct (σ 1) as [v' |]; [contradiction σc; auto with arith | contradiction HNE; reflexivity].
    - exfalso; specialize (σc 1 1 (S n)); rewrite <- EQn in σc.
      destruct (σ 1) as [v |]; [contradiction σc; auto with arith | contradiction HNE; reflexivity].
  Qed.

  Program Definition option_compl (σ : chain (option T)) {σc : cchain σ} :=
    match σ 1 with
      | None => None
      | Some v => Some (compl (unSome σ _))
    end.

  Global Program Instance option_cmt : cmetric (option T) := mkCMetr option_compl.
  Next Obligation.
    intros [| n]; [exists 0; intros; apply dist_bound | unfold option_compl].
    generalize (@eq_refl _ (σ 1)) as EQ1; pattern (σ 1) at 1 3; destruct (σ 1) as [v |]; intros.
    - assert (HT := conv_cauchy (unSome σ (option_compl_obligation_1 _ _ _ EQ1)) (S n)).
      destruct HT as [k HT]; exists (max k (S n)); intros.
      destruct (σ i) as [vi |] eqn: EQi; [unfold dist; simpl; rewrite (HT i) by eauto with arith | exfalso].
      + unfold unSome; generalize (@eq_refl _ (σ (S i))); pattern (σ (S i)) at 1 3.
        destruct (σ (S i)) as [vsi |]; intros EQsi; clear HT; [| exfalso].
        * assert (HT : S n <= i) by eauto with arith.
          specialize (σc (S n) (S i) i); rewrite EQi, <- EQsi in σc.
          apply σc; auto with arith.
        * specialize (σc 1 1 (S i)); rewrite <- EQ1, <- EQsi in σc.
          apply σc; auto with arith.
      + clear HT; specialize (σc 1 1 i); rewrite <- EQ1, EQi in σc.
        apply σc; auto with arith.
        rewrite <- HLe, <- Max.le_max_r; auto with arith.
    - exists 1; intros.
      destruct (σ i) as [vi |] eqn: EQi; [| reflexivity].
      specialize (σc 1 1 i); rewrite <- EQ1, EQi in σc.
      apply σc; auto with arith.
  Qed.

End Option.

Arguments dist {_ _ _} _ _ _ /.