Rasters on Planes
By attaching coordinates to the top-left and bottom-right corners of a raster, it can be interpreted as a finite set in Q^2.
For Q2, classical membership in a finite enumeration is the
same as a constructive membership.
Lemma InStrengthen : forall x (l:FinEnum stableQ2),
InFinEnumC x l -> exists y : ProductMS _ _, In y l /\ st_eq x y.
Definition InterpRow (up : list Q) n (v:Bvector n) : FinEnum stableQ:=
map (@fst _ _ ) (filter (@snd _ _) (combine up v)).
Definition InterpRaster n m (bitmap : raster n m) (tl br:(ProductMS Q_as_MetricSpace Q_as_MetricSpace)) : FinEnum stableQ2 :=
let (l,t) := tl in
let (r,b) := br in
let up := (UniformPartition l r n) in
flat_map (fun (p:Q*Bvector _) => let (y,r):=p in map (fun x => (x,y)) (InterpRow up r)) (combine (UniformPartition t b m) bitmap).
InFinEnumC x l -> exists y : ProductMS _ _, In y l /\ st_eq x y.
Definition InterpRow (up : list Q) n (v:Bvector n) : FinEnum stableQ:=
map (@fst _ _ ) (filter (@snd _ _) (combine up v)).
Definition InterpRaster n m (bitmap : raster n m) (tl br:(ProductMS Q_as_MetricSpace Q_as_MetricSpace)) : FinEnum stableQ2 :=
let (l,t) := tl in
let (r,b) := br in
let up := (UniformPartition l r n) in
flat_map (fun (p:Q*Bvector _) => let (y,r):=p in map (fun x => (x,y)) (InterpRow up r)) (combine (UniformPartition t b m) bitmap).
Notation for the interpretation of a raster.
Notation "a ⇱ b ⇲ c" := (InterpRaster b a c) (at level 1,
format "a ⇱ '[v' '/' b ']' '[v' '/' ⇲ c ']'") : raster.
format "a ⇱ '[v' '/' b ']' '[v' '/' ⇲ c ']'") : raster.
Correctness properties of our interpretation.
Section InterpRasterCorrect.
Let f := fun l r (n:nat) (i:Z) => l + (r - l) * (2 * i + 1 # 1) / (2 * n # 1).
Lemma InterpRaster_correct1 : forall n m (t l b r:Q) (bitmap: raster n m) i j,
Is_true (RasterIndex bitmap i j) -> In (f l r n j,f t b m i) (InterpRaster bitmap (l,t) (r,b)).
Lemma InterpRaster_correct2 : forall n m (t l b r:Q) x y (bitmap: raster n m),
In (x,y) (InterpRaster bitmap (l,t) (r,b)) ->
exists p, Is_true (RasterIndex bitmap (fst p) (snd p)) /\ x=f l r n (snd p) /\ y=f t b m (fst p).
End InterpRasterCorrect.
Let f := fun l r (n:nat) (i:Z) => l + (r - l) * (2 * i + 1 # 1) / (2 * n # 1).
Lemma InterpRaster_correct1 : forall n m (t l b r:Q) (bitmap: raster n m) i j,
Is_true (RasterIndex bitmap i j) -> In (f l r n j,f t b m i) (InterpRaster bitmap (l,t) (r,b)).
Lemma InterpRaster_correct2 : forall n m (t l b r:Q) x y (bitmap: raster n m),
In (x,y) (InterpRaster bitmap (l,t) (r,b)) ->
exists p, Is_true (RasterIndex bitmap (fst p) (snd p)) /\ x=f l r n (snd p) /\ y=f t b m (fst p).
End InterpRasterCorrect.