A series of notation allows rasters to be rendered (and to a certain
extent parsed) in Coq
Notation "'⎥' a b" := (Vcons (vector bool _) a _ b)
(format "'[v' '⎥' a '/' b ']'", at level 0, a, b at level 0) : raster.
Notation "'⎥' a" := (Vcons (vector bool _) a _ (Vnil _))
(format "'⎥' a", at level 0, a, b at level 0) : raster.
Notation "█ a" := (Vcons bool true _ a) (at level 0, right associativity) : raster.
Notation "⎢" := (@Vnil bool) (at level 0, right associativity) : raster.
Notation "' ' a" := (Vcons bool false _ a) (at level 0, right associativity) : raster.
Notation "░ a" := (Vcons bool false _ a) (at level 0, right associativity, only parsing) : raster_parsing.
(format "'[v' '⎥' a '/' b ']'", at level 0, a, b at level 0) : raster.
Notation "'⎥' a" := (Vcons (vector bool _) a _ (Vnil _))
(format "'⎥' a", at level 0, a, b at level 0) : raster.
Notation "█ a" := (Vcons bool true _ a) (at level 0, right associativity) : raster.
Notation "⎢" := (@Vnil bool) (at level 0, right associativity) : raster.
Notation "' ' a" := (Vcons bool false _ a) (at level 0, right associativity) : raster.
Notation "░ a" := (Vcons bool false _ a) (at level 0, right associativity, only parsing) : raster_parsing.
Standard rasters.
Definition emptyRaster n m : raster n m :=
Vconst _ (Vconst _ false _) _.
Definition fullRaster n m : raster n m :=
Vconst _ (Vconst _ false _) _.
Definition vectorAsList A n (v:vector A n) : list A :=
vector_rect A (fun (n0 : N) (_ : vector A n0) => list A) nil
(fun (a : A) (n0 : N) (_ : vector A n0) (IHv : list A) => a :: IHv) n v.
Coercion vectorAsList : vector>->list.
Lemma length_vectorAsList : forall A n (v:vector A n), (length v) = n.
Vconst _ (Vconst _ false _) _.
Definition fullRaster n m : raster n m :=
Vconst _ (Vconst _ false _) _.
Definition vectorAsList A n (v:vector A n) : list A :=
vector_rect A (fun (n0 : N) (_ : vector A n0) => list A) nil
(fun (a : A) (n0 : N) (_ : vector A n0) (IHv : list A) => a :: IHv) n v.
Coercion vectorAsList : vector>->list.
Lemma length_vectorAsList : forall A n (v:vector A n), (length v) = n.
Indexing into a raster
Definition RasterIndex n m (r:raster n m) i j :=
nth j (nth i (map (@vectorAsList _ _) r) nil) false.
nth j (nth i (map (@vectorAsList _ _) r) nil) false.
Indexing into an empty raster is alway empty
setRaster transforms a raster by setting (or reseting) the (i,j)th
pixel.
Definition updateVector A n (v:vector A n) (f:A->A) : N -> vector A n :=
vector_rect A (fun (n0 : N) (_ : vector A n0) => N -> vector A n0)
(fun (_ : N) => Vnil A)
(fun (a : A) (n0 : N) (v0 : vector A n0) (IHv : N -> vector A n0)
(i : N) =>
match i with
| 0 => Vcons A (f a) n0 v0
| S i0 => Vcons A a n0 (IHv i0)
end) n v.
Definition setRaster n m (r:raster n m) (x:bool) (i j:nat) :=
updateVector r (fun row => updateVector row (fun _ => x) j) i.
Lemma updateVector_correct1 : forall A n (v:vector A n) f i d1 d2,
i < n -> nth i (updateVector v f i) d1 = f (nth i v d2).
Lemma updateVector_correct2 : forall A n (v:vector A n) f d1 i j,
i <> j ->
nth i (updateVector v f j) d1 = nth i v d1.
Lemma setRaster_correct1 : forall n m (r:raster n m) x i j,
(i < m) -> (j < n) ->
RasterIndex (setRaster r x i j) i j = x.
Lemma setRaster_overflow : forall n m (r:raster n m) x i j,
(m <= i) \/ (n <= j) ->
(setRaster r x i j) = r.
Lemma setRaster_correct2 : forall n m (r:raster n m) x i j i0 j0,
(i <> i0) \/ (j <> j0) ->
RasterIndex (setRaster r x i0 j0) i j = RasterIndex r i j.
vector_rect A (fun (n0 : N) (_ : vector A n0) => N -> vector A n0)
(fun (_ : N) => Vnil A)
(fun (a : A) (n0 : N) (v0 : vector A n0) (IHv : N -> vector A n0)
(i : N) =>
match i with
| 0 => Vcons A (f a) n0 v0
| S i0 => Vcons A a n0 (IHv i0)
end) n v.
Definition setRaster n m (r:raster n m) (x:bool) (i j:nat) :=
updateVector r (fun row => updateVector row (fun _ => x) j) i.
Lemma updateVector_correct1 : forall A n (v:vector A n) f i d1 d2,
i < n -> nth i (updateVector v f i) d1 = f (nth i v d2).
Lemma updateVector_correct2 : forall A n (v:vector A n) f d1 i j,
i <> j ->
nth i (updateVector v f j) d1 = nth i v d1.
Lemma setRaster_correct1 : forall n m (r:raster n m) x i j,
(i < m) -> (j < n) ->
RasterIndex (setRaster r x i j) i j = x.
Lemma setRaster_overflow : forall n m (r:raster n m) x i j,
(m <= i) \/ (n <= j) ->
(setRaster r x i j) = r.
Lemma setRaster_correct2 : forall n m (r:raster n m) x i j i0 j0,
(i <> i0) \/ (j <> j0) ->
RasterIndex (setRaster r x i0 j0) i j = RasterIndex r i j.