Require Export CReals1.

Section CMetric_Fields.

Record is_CMetricField (F : CField) (abs : CSetoid_fun F IR) : Prop :=
  {ax_abs_gt_zero : ∀ x : F, [0] [<=] abs x;
   ax_abs_resp_mult : ∀ x y : F, abs (x[*]y) [=] abs x[*]abs y;
   ax_abs_triangle : ∀ x y : F, abs (x[+]y) [<=] abs x[+]abs y}.

Record CMetricField : Type :=
  {cmf_crr :> CField;
   cmf_abs : CSetoid_fun cmf_crr IR;
   cmf_proof : is_CMetricField cmf_crr cmf_abs}.

End CMetric_Fields.

Notation MAbs := (cmf_abs _).
Section basics.

Lemma MAbs_one : ∀ F : CMetricField,
 {MAbs ([1]:F) [=] [0]} + {MAbs ([1]:F) [=] [1]}.
Proof.
 intro F.
 apply square_id.
 astepl (cmf_abs F [1][*]cmf_abs F [1]).
 astepl (cmf_abs F ([1][*][1])).
  astepl (cmf_abs F [1]).
  apply eq_reflexive.
 apply ax_abs_resp_mult.
 apply cmf_proof.
Qed.

Lemma MAbs_one_recip_one : ∀ F : CMetricField,
 MAbs ([1]:F) [=] MAbs ( [--][1]:F).
Proof.
 intro F.
 cut ({cmf_abs F ([1]:F) [=] [0]} + {cmf_abs F ([1]:F) [=] [1]}).
  intro H.
  elim H.
   intro H2.
   astepl ZeroR.
   astepr (cmf_abs F ( [--][1][*][1])).
   astepr (cmf_abs F [--][1][*]cmf_abs F [1]).
    astepr (cmf_abs F [--][1][*][0]).
    astepr ZeroR.
    apply eq_reflexive_unfolded.
   apply eq_symmetric_unfolded.
   apply ax_abs_resp_mult.
   apply cmf_proof.
  intro H1.
  cut (cmf_abs F [--][1] [=] cmf_abs F [1] or cmf_abs F [--][1] [=] [--] (cmf_abs F [1])).
   intro H2.
   elim H2.
    intro H3.
    apply eq_symmetric_unfolded.
    exact H3.
   intro H3.

End basics.
Section CMetric_Field_Cauchy.
Variable F : CMetricField.

Definition MCauchy_prop (g : nat → F) : CProp := ∀ e : IR,
  [0] [<] e → {N : nat | ∀ m, N ≤ m → MAbs (g m[-]g N) [<=] e}.

Record MCauchySeq : Type :=
 {MCS_seq :> nat → F;
  MCS_proof : MCauchy_prop MCS_seq}.

Definition MseqLimit (seq : nat → F) (lim : F) : CProp := ∀ e : IR,
  [0] [<] e → {N : nat | ∀ m, N ≤ m → MAbs (seq m[-]lim) [<=] e}.

Definition is_MCauchyCompl (lim : MCauchySeq → F) : CProp :=
  ∀ (s : MCauchySeq), MseqLimit s (lim s).

End CMetric_Field_Cauchy.

Implicit Arguments MseqLimit [F].