Skip to content

Commit

Permalink
Started adapting SimpleIntegration.v to metric.v instead of Classified.v
Browse files Browse the repository at this point in the history
EvgenyMakarov committed Nov 7, 2012
1 parent f15aec7 commit a9aeb4f
Showing 3 changed files with 159 additions and 117 deletions.
121 changes: 61 additions & 60 deletions broken/AbstractIntegration.v
Original file line number Diff line number Diff line change
@@ -585,6 +585,66 @@ Proof with auto.
apply (integral_wd f)...
Qed.

(** Finally, we offer a smart constructor for implementations that would need to recognize and
treat the zero-width case specially anyway (which is the case for the implementation
with Riemann sums, because there, a positive width is needed to divide the error by). *)

Section extension_to_nn_width.

Context
(f: Q → CR)
(pre_integral: Q → Qpos → CR) (* Note the Qpos instead of QnonNeg. *)
(* The three properties limited to pre_integral: *)
(pre_additive: forall (a: Q) (b c: Qpos),
pre_integral a b + pre_integral (a + `b)%Q c[=]pre_integral a (b + c)%Qpos)
(pre_bounded: forall (from: Q) (width: Qpos) (mid: Q) (r: Qpos),
(forall x: Q, from <= x <= from + width -> ball r (f x) (' mid)) ->
ball (width * r) (pre_integral from width) (' (width * mid)%Q))
{pre_wd: Proper (Qeq ==> QposEq ==> @st_eq _) pre_integral}.

Instance integral_extended_to_nn_width: Integral f :=
fun from => QnonNeg.rect (fun _ => CR)
(fun _ _ => '0%Q)
(fun n d _ => pre_integral from (QposMake n d)).

Let proper: Proper (Qeq ==> QnonNeg.eq ==> @st_eq _) (∫ f).
Proof with auto.
intros ?????.
induction x0 using QnonNeg.rect;
induction y0 using QnonNeg.rect.
reflexivity.
discriminate.
discriminate.
intros. apply pre_wd...
Qed.

Let bounded (from: Q) (width: Qpos) (mid: Q) (r: Qpos):
(forall x, from <= x <= from + width -> ball r (f x) (' mid)) ->
ball (width * r) (∫ f from width) (' (width * mid)%Q).
Proof.
induction width using Qpos_positive_numerator_rect.
apply (pre_bounded from (a#b) mid r).
Qed.

Let additive (a: Q) (b c: QnonNeg): ∫ f a b + ∫ f (a + `b)%Q c == ∫ f a (b + c)%Qnn.
Proof.
unfold integrate.
induction b using QnonNeg.rect;
induction c using QnonNeg.rect; simpl integral_extended_to_nn_width; intros.
ring.
rewrite CRplus_0_l.
apply pre_wd; unfold QposEq, Qeq; simpl; repeat rewrite Zpos_mult_morphism; ring.
rewrite CRplus_0_r.
apply pre_wd; unfold QposEq, Qeq; simpl; repeat rewrite Zpos_mult_morphism; ring.
rewrite (pre_additive a (QposMake n d) (QposMake n0 d0)).
apply pre_wd; reflexivity.
Qed.

Lemma integral_extended_to_nn_width_correct: Integrable f.
Proof. constructor; auto. Qed.

End extension_to_nn_width.

Import abstract_algebra.

Lemma mult_comm `{SemiRing R} : Commutative (.*.).
@@ -779,64 +839,5 @@ Proof with try assumption.
apply (unique g)...
apply (Integrable_proper_l f)...
Qed.
(** Finally, we offer a smart constructor for implementations that would need to recognize and
treat the zero-width case specially anyway (which is the case for the implementation
with Riemann sums, because there, a positive width is needed to divide the error by). *)
Section extension_to_nn_width.
Context
(f: Q → CR)
(pre_integral: Q → Qpos → CR) (* Note the Qpos instead of QnonNeg. *)
(* The three properties limited to pre_integral: *)
(pre_additive: forall (a: Q) (b c: Qpos),
pre_integral a b + pre_integral (a + `b)%Q c[=]pre_integral a (b + c)%Qpos)
(pre_bounded: forall (from: Q) (width: Qpos) (mid: Q) (r: Qpos),
(forall x: Q, from <= x <= from + width -> ball r (f x) (' mid)) ->
ball (width * r) (pre_integral from width) (' (width * mid)))
{pre_wd: Proper (Qeq ==> QposEq ==> @st_eq _) pre_integral}.
Instance integral_extended_to_nn_width: Integral f :=
fun from => QnonNeg.rect (fun _ => CR)
(fun _ _ => '0)
(fun n d _ => pre_integral from (QposMake n d)).
Let proper: Proper (Qeq ==> QnonNeg.eq ==> @st_eq _) (∫ f).
Proof with auto.
intros ?????.
induction x0 using QnonNeg.rect;
induction y0 using QnonNeg.rect.
reflexivity.
discriminate.
discriminate.
intros. apply pre_wd...
Qed.
Let bounded (from: Q) (width: Qpos) (mid: Q) (r: Qpos):
(forall x, from <= x <= from + width -> ball r (f x) (' mid)) ->
ball (width * r) (∫ f from width) (' (width * mid)).
Proof.
induction width using Qpos_positive_numerator_rect.
apply (pre_bounded from (a#b) mid r).
Qed.
Let additive (a: Q) (b c: QnonNeg): ∫ f a b + ∫ f (a + `b)%Q c == ∫ f a (b + c)%Qnn.
Proof.
unfold integrate.
induction b using QnonNeg.rect;
induction c using QnonNeg.rect; simpl integral_extended_to_nn_width; intros.
ring.
rewrite CRplus_0_l.
apply pre_wd; unfold QposEq, Qeq; simpl; repeat rewrite Zpos_mult_morphism; ring.
rewrite CRplus_0_r.
apply pre_wd; unfold QposEq, Qeq; simpl; repeat rewrite Zpos_mult_morphism; ring.
rewrite (pre_additive a (QposMake n d) (QposMake n0 d0)).
apply pre_wd; reflexivity.
Qed.
Lemma integral_extended_to_nn_width_correct: Integrable f.
Proof. constructor; auto. Qed.
End extension_to_nn_width.
*)

56 changes: 41 additions & 15 deletions broken/SimpleIntegration.v
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
(*
(** A straightforward implementation of the abstract integration interface
in AbstractionIntegration using Riemann sums. The sole product of
this module are the Integrate and Integrable type class instances.
@@ -11,17 +9,39 @@
Require Import
List NPeano Unicode.Utf8
QArith Qabs Qpossec Qsums
Qmetric
Qmetric Qsetoid (* Needs imported for Q_is_Setoid to be a canonical structure *)
CRArith AbstractIntegration
util.Qgcd
Program
uneven_CRplus
stdlib_omissions.P
stdlib_omissions.Z
stdlib_omissions.Q
metric2.Classified
metric FromMetric2
Qauto
implementations.stdlib_rationals.

Open Scope Q_scope.

Lemma Qplus_pos_compat (x y : Q) : 0 < x -> 0 < y -> 0 < x + y.
Proof. intros; apply Qplus_lt_le_0_compat; [| apply Qlt_le_weak]; trivial. Qed.

Ltac Qauto_pos :=
repeat (first [ assumption
| constructor
| apply Qplus_pos_compat
| apply Qmult_lt_0_compat
| apply Qinv_lt_0_compat]);
auto with *.

Lemma gball_mspc_ball {X : MetricSpace} (r : Q) (x y : X) :
gball r x y <-> mspc_ball r x y.
Proof. reflexivity. Qed.

Lemma ball_mspc_ball {X : MetricSpace} (r : Qpos) (x y : X) :
ball r x y <-> mspc_ball r x y.
Proof. rewrite <- ball_gball; reflexivity. Qed.

Open Scope uc_scope.

Hint Resolve Qpos_nonzero.
@@ -47,21 +67,26 @@ Definition plus_half_times (x y: Q): Q := x * y + (1#2)*y.

Section definition.

Context (f: Q -> CR) `{!LocallyUniformlyContinuous_mu f} `{!LocallyUniformlyContinuous f}.
Context (f: Q -> CR) `{UC : !IsLocallyUniformlyContinuous f lmu}.

(** Note that in what follows we don't specialize for [0,1] or [0,w] ranges first. While this
would make the definition marginally cleaner, the resulting definition is harder to prove
correct. Part of the reason for this is that key primitives (such as mu and approximate)
don't come with Proper proofs, which means that common sense reasoning about
those operations with their arguments transformed doesn't work well. *)

Definition intervals (from: Q) (w: Qpos) (error: Qpos): positive :=
match luc_mu f from w (error / w) with
Program Definition intervals (from: Q) (w: Qpos) (error: Qpos): positive :=
match lmu from w (error / w) with
(* Todo: This is nice and simple, but suboptimal. Better would be to take the luc_mu
around the midpoint and with radius (w/2). *)
| QposInfinity => 1%positive
| Qpos2QposInf mue => QposCeiling ((1#2) * w / mue)%Qpos
| Qinf.infinite => 1%positive
| Qinf.finite mue => QposCeiling ((1#2) * w / mue)%Qpos
end.
Next Obligation.
change (Qinf.lt 0 mue). rewrite Heq_anonymous.
(*unfold IsLocallyUniformlyContinuous in *.*)
apply (uc_pos (restrict f from w)); [apply UC | Qauto_pos].
Qed.

Definition approx (from: Q) (w: Qpos) (e: Qpos): Q :=
let halferror := (e * (1#2))%Qpos in
@@ -83,6 +108,8 @@ Section definition.
Proof with auto.
unfold plus_half_times.
apply ball_sym.
unfold IsLocallyUniformlyContinuous in UC.
apply ball_mspc_ball. admit. (*apply (uc_prf _ (lmu fr wb)).
apply (locallyUniformlyContinuous f fr wb (he / wb)).
unfold mspc_ball.
unfold CRGroupOps.MetricSpaceBall_instance_0.
@@ -148,14 +175,14 @@ Section definition.
rewrite inject_nat_convert.
apply Qfloor_ball.
unfold QposEq. simpl.
field. split; try discriminate...
field. split; try discriminate...*)
Qed.

(** To construct a CR, we'll need to prove that approx is a regular function.
However, that property is essentially a specialization of a more general
well-definedness property that we'll need anyway, so we prove that one first. *)

Let hint := luc_Proper f.
(*Let hint := luc_Proper f.*)

Lemma wd
(from1 from2: Q) (w: bool -> Qpos) (e: bool -> Qpos)
@@ -229,7 +256,7 @@ End definition.

Section implements_abstract_interface.

Context (f: Q → CR) `{!LocallyUniformlyContinuous_mu f} `{!LocallyUniformlyContinuous f}.
Context (f: Q → CR) `{!IsLocallyUniformlyContinuous f lmu}.

Section additivity.

@@ -251,7 +278,7 @@ Section implements_abstract_interface.
Let approx01 (i: nat) :=
approximate (f (a + plus_half_times i (totalw / w01ints))) (e * (1 # 2) / totalw)%Qpos.

Let hint := luc_Proper f.
(*Let hint := luc_Proper f.*)

Lemma added_summations: Qball (e + e)
(Σ (wbints true) approx0 * (ww true / wbints true) +
@@ -431,7 +458,7 @@ Section implements_abstract_interface.

Let bounded (from: Q) (width: Qpos) (mid: Q) (r: Qpos):
(forall x, from <= x <= from + width -> ball r (f x) ('mid)%CR) ->
ball (width * r) (pre_result f from width) (' (width * mid))%CR.
ball (width * r) (pre_result f from width) (' (width * mid)%Q)%CR.
Proof with auto.
intros. apply (@regFunBall_Cunit Q_as_MetricSpace).
intro. unfold pre_result. simpl approximate.
@@ -463,4 +490,3 @@ Section implements_abstract_interface.
Qed.

End implements_abstract_interface.
*)
99 changes: 57 additions & 42 deletions broken/metric.v
Original file line number Diff line number Diff line change
@@ -215,6 +215,10 @@ try (unfold Qinf.eq, equiv in *; contradiction).
now apply mspc_triangle with (b := y2); [rewrite Ee1e2 | apply mspc_symm].
Qed.

(*Check _ : Le Qinf.T.
Lemma mspc_refl ∀ e : Q, 0 ≤ e → Reflexive (ball e);*)


Lemma mspc_triangle' :
∀ (q1 q2 : Q) (x2 x1 x3 : X) (q : Q),
q1 + q2 = q → ball q1 x1 x2 → ball q2 x2 x3 → ball q x1 x3.
@@ -288,6 +292,59 @@ End UniformContinuity.

Global Arguments UniformlyContinuous X {_} Y {_}.

Section SubMetricSpace.

Context `{ExtMetricSpaceClass X} (P : X -> Prop).

Global Instance sig_mspc_ball : MetricSpaceBall (sig P) := λ e x y, ball e (` x) (` y).

Global Instance sig_mspc : ExtMetricSpaceClass (sig P).
Proof.
constructor.
+ repeat intro; rapply mspc_radius_proper; congruence.
+ repeat intro; rapply mspc_inf.
+ intros; now rapply mspc_negative.
+ repeat intro; now rapply mspc_refl.
+ repeat intro; now rapply mspc_symm.
+ repeat intro; rapply mspc_triangle; eauto.
+ repeat intro; now rapply mspc_closed.
Qed.

End SubMetricSpace.

Section LocalUniformContinuity.

Context `{ExtMetricSpaceClass X, ExtMetricSpaceClass Y}.

Definition restrict (f : X -> Y) (x : X) (r : Q) : sig (ball r x) -> Y :=
f ∘ @proj1_sig _ _.

Class IsLocallyUniformlyContinuous (f : X -> Y) (lmu : X -> Q -> Q -> Qinf) :=
luc_prf : forall (x : X) (r : Q), IsUniformlyContinuous (restrict f x r) (lmu x r).

Global Arguments luc_prf f lmu {_} x r.

Global Instance uc_ulc (f : X -> Y) `{!IsUniformlyContinuous f mu} :
IsLocallyUniformlyContinuous f (λ _ _, mu).
Proof.
intros x r. constructor; [now apply (uc_pos f) |].
intros e [x1 A1] [x2 A2] e_pos A. now apply (uc_prf f mu).
Qed.

Global Instance luc_proper `{IsLocallyUniformlyContinuous f lmu} : Proper ((=) ==> (=)) f.
Proof.
intros x1 x2 A. apply -> mspc_eq. intros e e_pos.
assert (A1 : ball 1%Q x1 x1) by (apply mspc_refl; Qauto_nonneg).
assert (A2 : ball 1%Q x1 x2) by (rewrite A; apply mspc_refl; Qauto_nonneg).
change (ball e (restrict f x1 1 (exist _ x1 A1)) (restrict f x1 1 (exist _ x2 A2))).
unfold IsLocallyUniformlyContinuous in *. apply (uc_prf _ (lmu x1 1)); [easy |].
change (ball (lmu x1 1 e) x1 x2).
rewrite <- A. assert (0 < lmu x1 1 e) by now apply (uc_pos (restrict f x1 1)).
destruct (lmu x1 1 e) as [q |]; [apply mspc_refl; solve_propholds | apply mspc_inf].
Qed.

End LocalUniformContinuity.

Section Contractions.

Context `{MetricSpaceClass X, ExtMetricSpaceClass Y}.
@@ -650,48 +707,6 @@ Qed.

End CompleteSpaceSequenceLimits.

Section SubMetricSpace.

Context `{ExtMetricSpaceClass X} (P : X -> Prop).

Global Instance sig_mspc_ball : MetricSpaceBall (sig P) := λ e x y, ball e (` x) (` y).

Global Instance sig_mspc : ExtMetricSpaceClass (sig P).
Proof.
constructor.
+ repeat intro; rapply mspc_radius_proper; congruence.
+ repeat intro; rapply mspc_inf.
+ intros; now rapply mspc_negative.
+ repeat intro; now rapply mspc_refl.
+ repeat intro; now rapply mspc_symm.
+ repeat intro; rapply mspc_triangle; eauto.
+ repeat intro; now rapply mspc_closed.
Qed.

End SubMetricSpace.

Section LocalUniformContinuity.

Context `{ExtMetricSpaceClass X, ExtMetricSpaceClass Y}.

Definition restrict (f : X -> Y) (x : X) (r : Q) : sig (ball r x) -> Y :=
f ∘ @proj1_sig _ _.

Class IsLocallyUniformlyContinuous (f : X -> Y) (lmu : X -> Q -> Q -> Qinf) :=
luc_prf : forall (x : X) (r : Q), IsUniformlyContinuous (restrict f x r) (lmu x r).

Global Arguments luc_prf f lmu {_} x r.

Global Instance uc_ulc (f : X -> Y) `{!IsUniformlyContinuous f mu} :
IsLocallyUniformlyContinuous f (λ _ _, mu).
Proof.
intros x r. constructor; [now apply (uc_pos f) |].
intros e [x1 A1] [x2 A2] e_pos A. now apply (uc_prf f mu).
Qed.

End LocalUniformContinuity.


(*Section ClosedSegmentComplete.
Context `{CompleteMetricSpaceClass X, Le X, @PartialOrder X _ _}.

0 comments on commit a9aeb4f

Please sign in to comment.