CoRN.examples.Circle
Require Import Plot RasterQ Qmetric.
Plotting graphs in the plane
Notation Q:=Q_as_MetricSpace.
Notation R2:=(Complete Q2).
Lemma stableComplete(X:MetricSpace):stableMetric X → stableMetric (Complete X).
Proof.
unfold stableMetric. simpl. unfold regFunBall. intuition.
Qed.
Definition stableR2:=(stableComplete Q2 stableQ2).
Open Local Scope uc_scope.
Require Import metric2.Classified.
Section diag.
Variable X:MetricSpace.
Definition diag_raw:X->(ProductMS X X):=fun x=>(x,x).
Lemma diag_uc:(is_UniformlyContinuousFunction diag_raw (fun e ⇒ e)%Qpos).
Proof.
unfold diag_raw, is_UniformlyContinuousFunction. simpl. unfold prod_ball. intuition.
Qed.
Definition diag:X-->(ProductMS X X):=Build_UniformlyContinuousFunction diag_uc.
End diag.
Require Import Interval.
Open Local Scope uc_scope.
Section PathImage.
Variable path:Q-->R2.
Variable CompleteMult:(Complete R2 -->R2).
Variable (l r:Q).
Hypothesis Hlr : l < r.
The image of a path as a Compact subset of the plane.
Definition PathImage:=(CompactImage (1#1)%Qpos stableR2 plFEQ path
(CompactIntervalQ (Qlt_le_weak _ _ Hlr))).
End PathImage.
Section PlotPath.
Variable (from to:Q).
Hypothesis Hfromto:from<to.
Variable (l r:Q).
Hypothesis Hlr : l < r.
Variable (b t:Q).
Hypothesis Hbt : b < t.
Variable n m : nat.
Let w := proj1_sigT _ _ (Qpos_lt_plus Hlr).
Let h := proj1_sigT _ _ (Qpos_lt_plus Hbt).
(CompactIntervalQ (Qlt_le_weak _ _ Hlr))).
End PathImage.
Section PlotPath.
Variable (from to:Q).
Hypothesis Hfromto:from<to.
Variable (l r:Q).
Hypothesis Hlr : l < r.
Variable (b t:Q).
Hypothesis Hbt : b < t.
Variable n m : nat.
Let w := proj1_sigT _ _ (Qpos_lt_plus Hlr).
Let h := proj1_sigT _ _ (Qpos_lt_plus Hbt).
Half the error in the Plot example, since we need to approximate twice.
Let err := Qpos_max ((1 # 8 × P_of_succ_nat (pred n)) × w)
((1 # 8 × P_of_succ_nat (pred m)) × h).
Variable path:Q-->R2.
((1 # 8 × P_of_succ_nat (pred m)) × h).
Variable path:Q-->R2.
The actual plot function
Definition PlotPath := (n, m, 2, (RasterizeQ2
(approximate
(FinCompact stableQ2 stableR2 (approximate (PathImage path from to Hfromto) err))
err) n m t l b r )).
End PlotPath.
Section PlotCirclePath.
Require Import CRtrans.
Require Import Vector.
Export Vector.VectorNotations.
Definition CircleFunction_aux:=(together cos_uc sin_uc).
Definition CirclePath:Q --> R2:=
(Couple ∘ CircleFunction_aux ∘ (diag Q)).
Notation star := (@refl_equal _ Lt).
Notation "∗" := star.
Local Open Scope raster.
Notation "'Vcons'" := Vector.cons.
Notation "'Vnil'" := Vector.nil.
Notation "# a b" := (Vcons (Vector.t bool _) a _ b)
(at level 0, a, b at level 0) : raster.
Notation "'#' a" := (Vcons (Vector.t bool _) a _ (Vnil _))
(at level 0, a, b at level 0) : raster.
Notation "0 # a" := (Vcons bool true _ a) (at level 0, right associativity) : raster.
Notation " # " := (Vnil bool) (at level 0, right associativity) : raster.
Notation "1 # a" := (Vcons bool false _ a) (at level 0, right associativity) : raster.
Definition Circle:=Eval vm_compute in (PlotPath 0 7 star (-(1)) 1 star (-(1)) 1 star 40 40 CirclePath).
Add ML Path "dump".
Declare ML Module "dump".
Dump Circle.
End PlotCirclePath.
(approximate
(FinCompact stableQ2 stableR2 (approximate (PathImage path from to Hfromto) err))
err) n m t l b r )).
End PlotPath.
Section PlotCirclePath.
Require Import CRtrans.
Require Import Vector.
Export Vector.VectorNotations.
Definition CircleFunction_aux:=(together cos_uc sin_uc).
Definition CirclePath:Q --> R2:=
(Couple ∘ CircleFunction_aux ∘ (diag Q)).
Notation star := (@refl_equal _ Lt).
Notation "∗" := star.
Local Open Scope raster.
Notation "'Vcons'" := Vector.cons.
Notation "'Vnil'" := Vector.nil.
Notation "# a b" := (Vcons (Vector.t bool _) a _ b)
(at level 0, a, b at level 0) : raster.
Notation "'#' a" := (Vcons (Vector.t bool _) a _ (Vnil _))
(at level 0, a, b at level 0) : raster.
Notation "0 # a" := (Vcons bool true _ a) (at level 0, right associativity) : raster.
Notation " # " := (Vnil bool) (at level 0, right associativity) : raster.
Notation "1 # a" := (Vcons bool false _ a) (at level 0, right associativity) : raster.
Definition Circle:=Eval vm_compute in (PlotPath 0 7 star (-(1)) 1 star (-(1)) 1 star 40 40 CirclePath).
Add ML Path "dump".
Declare ML Module "dump".
Dump Circle.
End PlotCirclePath.