CoRN.ode.Picard

Require Import
 Unicode.Utf8 Program
 CRArith CRabs
 Qauto Qround Qmetric.

Require Qinf QnonNeg QnnInf CRball.
Import
  QnonNeg Qinf.notations QnonNeg.notations QnnInf.notations CRball.notations
  Qabs propholds.

Require Import stdlib_rationals theory.rationals.
Require Import metric FromMetric2 AbstractIntegration SimpleIntegration BanachFixpoint.
Require Import canonical_names decision setoid_tactics util.

Close Scope uc_scope. Open Scope signature_scope.
Bind Scope mc_scope with Q.

Local Notation ball := mspc_ball.

Lemma Qinf_lt_le (x y : Qinf) : x < y → x ≤ y.
Proof.
destruct x as [x |]; destruct y as [y |]; [| easy..].
change (x < y → x ≤ y). intros; solve_propholds.
Qed.

Instance Q_nonneg (rx : QnonNeg) : PropHolds (@le Q _ 0 rx).
Proof. apply (proj2_sig rx). Qed.

Instance Q_nonempty : NonEmpty Q := inhabits 0.

Program Instance sig_nonempty `{ExtMetricSpaceClass X}
  (r : QnonNeg) (x : X) : NonEmpty (sig (ball r x)) := inhabits x.
Next Obligation. apply mspc_refl; solve_propholds. Qed.

Instance prod_nonempty `{NonEmpty X, NonEmpty Y} : NonEmpty (X × Y).
Proof.
match goal with H : NonEmpty X |- _ ⇒ destruct H as [x] end.
match goal with H : NonEmpty Y |- _ ⇒ destruct H as [y] end.
exact (inhabits (x, y)).
Qed.

Global Instance Qmsd : MetricSpaceDistance Q := λ x y, abs (x - y).

Global Instance Qmsc : MetricSpaceClass Q.
Proof. intros x1 x2; apply gball_Qabs; reflexivity. Qed.


Section Extend.

Context `{ExtMetricSpaceClass Y} (a : Q) (r : QnonNeg).


Lemma mspc_ball_edge_l : ball r a (a - `r).
Proof.
destruct r as [e ?]; simpl.
apply gball_Qabs. mc_setoid_replace (a - (a - e)) with e by ring.
change (abs e ≤ e). rewrite abs.abs_nonneg; [reflexivity | trivial].
Qed.

Lemma mspc_ball_edge_r : ball r a (a + `r).
Proof.
destruct r as [e ?]; simpl.
apply Qmetric.gball_Qabs. mc_setoid_replace (a - (a + e)) with (-e) by ring.
change (abs (-e) ≤ e). rewrite abs.abs_negate, abs.abs_nonneg; [reflexivity | trivial].
Qed.

Context (f : sig (ball r a) → Y).
Global Existing Instance Q_lt.

End Extend.