Require Vector.
Export Vector.VectorNotations.
Require Export List.
Require Import Arith.

Set Implicit Arguments.

Definition raster n m := Vector.t (Vector.t bool n) m.

Notation "'⎥' a b" := (Vector.cons _ a _ b)
  (format "'[v' '⎥' a '/' b ']'", at level 0, a, b at level 0) : raster.
Notation "'⎥' a" := (Vector.cons _ a _ Vector.nil)
  (format "'⎥' a", at level 0, a, b at level 0) : raster.
Notation "█ a" := (Vector.cons bool true _ a) (at level 0, right associativity) : raster.
Notation "⎢" := (@Vector.nil bool) (at level 0, right associativity) : raster.
Notation "' ' a" := (Vector.cons bool false _ a) (at level 0, right associativity) : raster.
Notation "░ a" := (Vector.cons bool false _ a) (at level 0, right associativity, only parsing) : raster_parsing.

Definition emptyRaster n m : raster n m := Vector.const (Vector.const false _) _.

Coercion Vector.to_list : Vector.t>->list.

Lemma length_vectorAsList : ∀ A n (v: Vector.t A n), (length v) = n.
Proof.
 induction v.
  reflexivity.
 simpl.
 auto with ×.
Qed.

Definition RasterIndex n m (r:raster n m) i j :=
 nth j (nth i (map (@Vector.to_list _ _) r) nil) false.

Lemma emptyRasterEmpty : ∀ n m i j,
RasterIndex (emptyRaster n m) i j = false.
Proof.
 intros n m.
 induction m.
  intros [|i] [|j]; constructor.
 intros i j.
 simpl.
 destruct i.
  unfold RasterIndex.
  simpl.
  clear IHm.
  revert j.
  induction n.
   destruct j; auto.
  destruct j; auto.
  simpl.
  apply IHn.
 unfold RasterIndex in ×.
 simpl.
 apply IHm.
Qed.

Fixpoint updateVector A n (v : Vector.t A n) (f : A→A) : nat → Vector.t A n :=
  match v with
  | Vector.nil ⇒ fun _ ⇒ Vector.nil A
  | Vector.cons a' n' v' ⇒ fun i ⇒
    match i with
    | 0 ⇒ Vector.cons A (f a') n' v'
    | S i' ⇒ Vector.cons A a' n' (updateVector v' f i')
    end
  end.

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 : ∀ A n (v: Vector.t A n) f i d1 d2,
i < n → nth i (updateVector v f i) d1 = f (nth i v d2).
Proof.
 induction v.
  intros.
  absurd (i < 0); auto with ×.
 intros f [|i] d1 d2 H.
  reflexivity.
 simpl.
 apply IHv.
 auto with ×.
Qed.

Lemma updateVector_correct2 : ∀ A n (v: Vector.t A n) f d1 i j,
i ≠ j →
nth i (updateVector v f j) d1 = nth i v d1.
Proof.
 induction v.
  reflexivity.
 intros f d1 i [|j] H; destruct i as [|i]; try reflexivity.
  elim H; auto.
 simpl.
 apply IHv.
 auto.
Qed.

Lemma setRaster_correct1 : ∀ n m (r:raster n m) x i j,
 (i < m) → (j < n) →
 RasterIndex (setRaster r x i j) i j = x.
Proof.
 intros n m r x i j Hi Hj.
 unfold RasterIndex.
 replace (nth i (map (@Vector.to_list _ _) (setRaster r x i j)) nil)
   with (nth i (map (@Vector.to_list _ _) (setRaster r x i j)) (Vector.const false n)).
  rewrite map_nth.
  unfold setRaster.
  rewrite (updateVector_correct1 r (fun row ⇒ updateVector row (fun _ : bool ⇒ x) j) (Vector.const false n) (Vector.const false n) Hi).
  rewrite updateVector_correct1; auto.
 apply nth_indep.
 rewrite map_length.
 rewrite length_vectorAsList.
 auto.
Qed.

Lemma updateVector_overflow : ∀ A n (v : Vector.t A n) f i, n ≤ i → updateVector v f i = v.
Proof with try reflexivity; auto with arith.
 induction v...
 intros f [|i] E.
  inversion E.
 simpl. rewrite IHv...
Qed.

Lemma setRaster_overflow : ∀ n m (r:raster n m) x i j,
 (m ≤ i) ∨ (n ≤ j) →
 (setRaster r x i j) = r.
Proof with try reflexivity; auto.
 unfold setRaster.
 intros n m r x i j [Hi | Hj].
  apply updateVector_overflow...
 revert i j Hj. induction r...
 intros [|i] j Hj; simpl; f_equal...
 apply updateVector_overflow...
Qed.

Lemma setRaster_correct2 : ∀ 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.
Proof.
 intros n m r x i j i0 j0 H.
 destruct (le_lt_dec m i0) as [Hm | Hm].
  rewrite setRaster_overflow; auto with ×.
 destruct (le_lt_dec n j0) as [Hn | Hn].
  rewrite setRaster_overflow; auto with ×.
 unfold RasterIndex.
 assert (L:∀ v : Vector.t (Vector.t bool n) m, nth j (nth i (map (@Vector.to_list _ _) v) nil) false =
   nth j (nth i (map (@Vector.to_list _ _) v) (Vector.const false n)) false).
  intros v.
  destruct (le_lt_dec m i) as [Hi | Hi].
   transitivity false.
    rewrite (nth_overflow (map (@Vector.to_list _ _) v)).
     destruct j; reflexivity.
    rewrite map_length.
    rewrite length_vectorAsList.
    auto.
   rewrite map_nth.
   rewrite (nth_overflow v).
    clear - j.
    revert j.
    induction n.
     destruct j; reflexivity.
    intros [|j].
     reflexivity.
    simpl.
    apply IHn.
   rewrite length_vectorAsList.
   auto.
  f_equal.
  apply nth_indep.
  rewrite map_length, length_vectorAsList.
  auto.
 transitivity (nth j (nth i (map (@Vector.to_list _ _) (setRaster r x i0 j0)) (Vector.const false n)) false).
  apply L.
 transitivity (nth j (nth i (map (@Vector.to_list _ _) r) (Vector.const false n)) false);[|symmetry;apply L].
 do 2 rewrite map_nth.
 destruct (eq_nat_dec i i0).
  destruct H as [Hi | Hj].
   elim Hi; auto.
  rewrite <- e in *; clear e.
  unfold setRaster.
  rewrite (updateVector_correct1 r (fun row ⇒ updateVector row (fun _ : bool ⇒ x) j0) (Vector.const false n) (Vector.const false n) Hm).
  rewrite updateVector_correct2; auto.
 unfold setRaster.
 rewrite updateVector_correct2; auto.
Qed.