Rasterization

Rasterization takes finite enumeration of points in Q2 and moves them around a little so that they lie on a raster. Thus rasterization produces a raster object that when interpreted as a finite enumeration of Q2 is close to the original enumeration of points. How close depends on how fine a raster is chosen.

There is a choice as to how to treat points that lie outside of the bound of a chosen rectangle for rasterization. In this implemenation I choose to push all points inside the raster. In typical applications a rectangle is chosen that contains all the points, so that this doesn't matter.

Rasterize Point adds a single point p into a raster.
Definition RasterizePoint n m (bm:raster n m) (t l b r:Q) (p:Q*Q) : raster n m :=
let i := min (pred n) (Z_to_nat (Zle_max_l 0 (rasterize1 l r n (fst p)))) in
let j := min (pred m) (Z_to_nat (Zle_max_l 0 (rasterize1 b t m (snd p)))) in
setRaster bm true (pred m - j) i.
Lemma RasterizePoint_carry : forall t l b r n m (bm:raster n m) p i j,
 Is_true (RasterIndex bm i j) -> Is_true (RasterIndex (RasterizePoint bm t l b r p) i j).

Rasterization is done by rasterizing each point, and composing the resulting raster transfomers. A fold_left is done for efficency. (It is translated to a fold_right when we reason about it).
Definition RasterizeQ2 (f:FinEnum stableQ2) n m (t l b r:Q) : raster n m :=
fold_left (fun x y => @RasterizePoint n m x t l b r y) f (emptyRaster _ _).
Section RasterizeCorrect.

Let C := fun l r (n:nat) (i:Z) => l + (r - l) * (2 * i + 1 # 1) / (2 * n # 1).

Lemma rasterization_error : forall l (w:Qpos) n x,
(l <= x <= l + w) ->
ball (m:=Q_as_MetricSpace) ((1 #2*P_of_succ_nat n) * w) (C l (l + w) (S n) (min n
             (Z_to_nat
                (Zle_max_l 0 (rasterize1 l (l+w) (S n) x))))) x.

Lemma switch_line_interp : forall t b m j, (j <= m)%nat -> C t b (S m) (m - j)%nat == C b t (S m) j.

Variable b l:Q.
Variable w h:Qpos.

Let r:=l+w.
Let t:=b+h.

Variable f:FinEnum stableQ2.

Variable n m : N.

Let errX : Q+ := ((1#2*P_of_succ_nat n)*w)%Qpos.
Let errY : Q+ := ((1#2*P_of_succ_nat m)*h)%Qpos.
Let err : Q+ := Qpos_max errX errY.

Hypothesis Hf:forall x y, InFinEnumC ((x,y):ProductMS _ _) f ->
 (l<= x <= r) /\ (b <= y <= t).

The Rasterization is close to the original enumeration.
Lemma RasterizeQ2_correct1 : forall x y,
 InFinEnumC ((x,y):ProductMS _ _) f ->
 existsC (ProductMS _ _)
  (fun p => InFinEnumC p (InterpRaster (RasterizeQ2 f (S n) (S m) t l b r) (l,t) (r,b))
            /\ ball err p (x,y)).

Lemma RasterizeQ2_correct2 : forall x y,
 InFinEnumC ((x,y):ProductMS _ _) (InterpRaster (RasterizeQ2 f (S n) (S m) t l b r) (l,t) (r,b))
 -> (existsC (ProductMS _ _)
  (fun p => InFinEnumC p f/\ ball err p (x,y))).

Lemma RasterizeQ2_correct :
 ball err
  (InterpRaster (RasterizeQ2 f (S n) (S m) t l b r) (l,t) (r,b))
  f.

End RasterizeCorrect.