Library vector


Require Export Arith.



Section le_pirr.
  Axiom le_pirr: forall i j (h h': i<=j), h=h'.
  Theorem lt_pirr: forall i j (h h': i<j), h=h'.
  Hint Immediate lt_pirr le_pirr.
End le_pirr.

Ltac lt_eq_lt x y H := destruct (lt_eq_lt_dec x y) as [H|H]; [ destruct H as [H|H] | idtac ].

Ltac gclear x := generalize x; clear x.
Ltac gclear2 x y := generalize x y; clear x y.
Ltac gclear3 x y z := generalize x y z; clear x y z.
Ltac gclear4 x y z t := generalize x y z t; clear x y z t.


Ltac vauto := autorewrite with vector; auto with arith.

Section Vector.

  Variable A: Set.

  Inductive vector: nat -> Set :=
    | nnil: vector 0
    | ncons: forall (n: nat) (a: A), vector n -> vector (S n).

  Definition head (n: nat) (l: vector (S n)): A :=
    match l in vector k return 0<k -> A with
    | nnil => fun h => False_rec A (lt_n_O _ h)
    | ncons _ a _ => fun _ => a
    end (lt_O_Sn n).

  Definition tail (n: nat) (l: vector (S n)): vector n :=
    match l in vector k return 0<k -> vector (pred k) with
    | nnil => fun h => False_rec (vector (pred 0)) (lt_n_O _ h)
    | ncons _ _ q => fun _ => q
    end (lt_O_Sn n).

  Fixpoint get (n: nat) (l: vector n) (k: nat) {struct l}: k<n -> A :=
    match l in vector n return k < n -> A with
    | nnil => fun h => False_rec _ (lt_n_O _ h)
    | ncons n a q =>
        match k return k < S n -> A with
        | 0 => fun _ => a
        | S k => fun h => get q (lt_S_n _ _ h)
        end
    end.
  Implicit Arguments get [n].

  Fixpoint append (n: nat) (l: vector n) {struct l}: forall m: nat, vector m -> vector (n+m) :=
    match l in vector n return forall m: nat, vector m -> vector (n+m) with
    | nnil => fun _ l' => l'
    | ncons _ a q => fun _ l => ncons a (append q l)
    end.

  Fixpoint split1 (n: nat): forall (k: nat) (l: vector (n+k)), vector n :=
    match n return forall k (l: vector (n+k)), vector n with
    | 0 => fun k l => nnil
    | S n => fun k l => ncons (head l) (split1 n k (tail l))
    end.

  Fixpoint split2 (n: nat): forall (k: nat) (l: vector (n+k)), vector k :=
    match n return forall k (l: vector (n+k)), vector k with
    | 0 => fun k l => l
    | S n => fun k l => split2 n k (tail l)
    end.

  Fixpoint overwrite (k n: nat) (l: vector k) (l': vector n) {struct l}: vector n :=
    match l, l' with
    | nnil, l' => l'
    | ncons _ _ _, nnil => nnil
    | ncons _ a q, ncons _ a' q' => ncons a (overwrite q q')
    end.

  Fixpoint truncate (k: nat): forall n, vector n -> k<=n -> vector k :=
    match k return forall n, vector n -> k<=n -> vector k with
    | 0 => fun n l h => nnil
    | S k => fun n l =>
      match l in vector n return S k<=n -> vector (S k) with
      | nnil => fun h => False_rec _ (le_Sn_O _ h)
      | ncons _ a q => fun h => ncons a (truncate q (le_S_n _ _ h))
      end
    end.

  Fixpoint rev_init (n: nat) (f: nat -> A) {struct n}: vector n :=
    match n return vector n with
    | 0 => nnil
    | S m => ncons (f n) (rev_init m f)
    end.

  Definition init (n: nat) (f: nat -> A) := rev_init n (fun m => f (n-m)).


  Definition fill(k n: nat) (l: vector k) (a: A) :=
    init n (fun i => match le_lt_dec k i with
                     | right h => get l i h
                     | _ => a
                     end).

  Fixpoint change (n: nat) (l: vector n) (i: nat) (a: A) {struct l}: vector n :=
    match l in vector n, i return vector n with
    | nnil, _ => nnil
    | ncons _ a' q, 0 => ncons a q
    | ncons _ a' q, S i => ncons a' (change q i a)
    end.

  Lemma empty_nnil: forall l: vector 0, l=nnil.

  Lemma nempty_ncons: forall n (l: vector (S n)), exists x, exists q, l=ncons x q.

  Theorem head_tail: forall (n: nat) (l: vector (S n)), l = ncons (head l) (tail l).


  Theorem vector_eq: forall (n: nat) (l l': vector n),
        (forall (i: nat) (h: i<n), get l i h = get l' i h) -> l=l'.

  Lemma get_cons: forall (n: nat) (a: A) (l: vector n) (i : nat) (h: i<n),
                   get (ncons a l) (S i) (lt_n_S _ _ h) = get l i h.

  Lemma head_get: forall (n: nat) (l: vector (S n)), head l = get l 0 (lt_O_Sn n).

  Definition eq_from(k n: nat) (l l': vector n): Prop := forall i (h h': i<n), k<=i -> get l i h = get l' i h'.
  Definition eq_until(k n: nat) (l l': vector n): Prop := forall i (h h': i<n), i<k -> get l i h = get l' i h'.
  Definition eq_between(k k' n: nat) (l l': vector n): Prop := forall i (h h': i<n), k<=i -> i<k' -> get l i h = get l' i h'.

  Theorem eq_from_sym: forall k n (l l': vector n), eq_from k l l' -> eq_from k l' l.

  Theorem eq_until_sym: forall k n (l l': vector n), eq_until k l l' -> eq_until k l' l.

  Theorem eq_between_sym: forall k k' n (l l': vector n), eq_between k k' l l' -> eq_between k k' l' l.

End Vector.

Implicit Arguments get [A n].
Implicit Arguments truncate [A n].

Lemma get_pirr: forall i n (h h': i<n) A (l: vector A n), get l i h = get l i h'.
Hint Immediate get_pirr.

Lemma get_pirr': forall i j n (h: i<n) (h': j<n) A (l: vector A n), i=j -> get l i h = get l j h'.

Theorem get_tail: forall A (n: nat) (l: vector A (S n)) (i : nat) (h: i<n), get (tail l) i h = get l (S i) (lt_n_S _ _ h).

Theorem get_append_1: forall i n (h: i<n) A (l: vector A n) m (l': vector A m) (h': i<n+m),
                get (append l l') i h' = get l i h.

Lemma lt_minus: forall i j k (ij: i<=j) (jik: j<i+k), j-i<k.

Theorem get_append_2: forall i n (h: i>=n) A (l: vector A n) m (l': vector A m) (h': i<n+m),
              get (append l l') i h' = get l' (i-n) (lt_minus m h h').

Theorem get_append_2': forall i m n (h: m+i<m+n) A (l: vector A m) (l': vector A n),
              get (append l l') (m+i) h = get l' i (plus_lt_reg_l _ _ _ h).
Hint Rewrite get_append_2': vector.

Theorem get_split1: forall n k i (h: i<n) A (l: vector A (n+k)), get (split1 n k l) i h = get l i (lt_plus_trans _ _ _ h).
Hint Rewrite get_split1: vector.

Theorem get_split2: forall n k i (h: i<k) A (l: vector A (n+k)), get (split2 n k l) i h = get l (n+i) (plus_lt_compat_l _ _ _ h).
Hint Rewrite get_split2: vector.

Theorem split: forall A n k (l: vector A (n+k)), l = append (split1 n k l) (split2 n k l).
Hint Immediate split.

Theorem split1_append: forall m n A (l: vector A m) (l': vector A n), split1 m n (append l l') = l.
Hint Rewrite split1_append: vector.

Theorem split2_append: forall m n A (l: vector A m) (l': vector A n), split2 m n (append l l') = l'.
Hint Rewrite split2_append: vector.

Theorem split_eq: forall m n A (l l': vector A (m+n)), split1 m n l = split1 m n l' -> split2 m n l = split2 m n l' -> l = l'.
Ltac split_eq m n := match goal with |- ?l = ?l' => rewrite (split m n l); rewrite (split m n l'); apply split_eq end.

Theorem get_overwrite_1: forall i k (h': i<k) n (h: i<n) A (l : vector A k) (l': vector A n), get (overwrite l l') i h = get l i h'.

Theorem get_overwrite_2: forall i k (h': k<=i) n (h: i<n) A (l : vector A k) (l': vector A n), get (overwrite l l') i h = get l' i h.

Theorem split1_overwrite: forall m n A (l: vector A m) (l': vector A (m+n)), split1 m n (overwrite l l') = l.
Hint Rewrite split1_overwrite: vector.

Theorem split1_overwrite': forall k m n A (l: vector A k) (l': vector A (m+n)), split1 m n (overwrite l l') = (overwrite l (split1 _ _ l')).
Hint Rewrite split1_overwrite: vector.

Theorem split2_overwrite: forall m n A (l: vector A m) (l': vector A (m+n)), split2 m n (overwrite l l') = split2 m n l'.
Hint Rewrite split2_overwrite: vector.

Theorem split2_overwrite': forall k m n A (l: vector A (m+k)) (l': vector A (m+n)), split2 m n (overwrite l l') = (overwrite (split2 m k l) (split2 m n l')).
Hint Rewrite split2_overwrite': vector.

Theorem overwrite_nothing: forall n A (l: vector A 0) (l': vector A n), overwrite l l' = l'.
Hint Rewrite overwrite_nothing: vector.

Theorem overwrite_full: forall n A (l l': vector A n), overwrite l l' = l.
Hint Rewrite overwrite_full: vector.

Theorem overwrite_empty: forall n A (l: vector A n) (l': vector A 0), overwrite l l' = nnil _.
Hint Rewrite overwrite_empty: vector.

Theorem get_truncate: forall A k i n (l: vector A n) (h: k<=n) (h': i<k), get (truncate k l h) i h' = get l i (lt_le_trans _ _ _ h' h).
Hint Rewrite get_truncate: vector.

Theorem truncate_id: forall A n (l: vector A n) (h: n<=n), truncate n l h = l.
Hint Rewrite truncate_id: vector.

Theorem truncate_overwrite_id: forall A k n (l': vector A k) (l: vector A n) (h: k<=n), truncate k (overwrite l' l) h = l'.
Hint Rewrite truncate_overwrite_id: vector.

Theorem change_append_1: forall A m n (l: vector A m) (l': vector A n) i a, i<m -> change (append l l') i a = append (change l i a) l'.

Theorem change_append_2: forall A m n (l: vector A m) (l': vector A n) i a, change (append l l') (m+i) a = append l (change l' i a).
Hint Rewrite change_append_2: vector.

Theorem get_change_ii: forall i n (h: i<n) A (l: vector A n) a,
                         get (change l i a) i h = a.
Hint Rewrite get_change_ii: vector.

Theorem get_change_ij: forall i j (d: i<>j) A n (h: j<n) (l: vector A n) a,
                         get (change l i a) j h = get l j h.

Theorem change_ii_invol: forall A i a a' n (l: vector A n),
                         change (change l i a') i a = change l i a.
Hint Rewrite change_ii_invol: vector.

Theorem change_ij_comm: forall i j (d: i<>j) A ai aj n (l: vector A n),
                         change (change l i ai) j aj = change (change l j aj) i ai.

Theorem change_id: forall i n (h: i<n) A (l: vector A n) a, a=get l i h -> change l i a = l.

Theorem change_id': forall i j n (hj: j<n) A (l: vector A n) a, i=j -> a=get l j hj -> change l i a = l.

Theorem change_id_out: forall i n A (l: vector A n) a, change l (n+i) a = l.
Hint Rewrite change_id_out: vector.

Theorem head_change_O: forall A n (l: vector A (S n)) a, head (change l 0 a) = a.
Hint Rewrite head_change_O: vector.

Theorem head_change_S: forall A n (l: vector A (S n)) i a, head (change l (S i) a) = head l.
Hint Rewrite head_change_S: vector.

Theorem split1_change: forall m n A (l: vector A (m+n)) i a, split1 m n (change l i a) = change (split1 m n l) i a.
Hint Rewrite split1_change: vector.

Theorem split1_change': forall m n A (l: vector A (m+n)) i a, split1 m n (change l (m+i) a) = split1 m n l.
Hint Rewrite split1_change': vector.

Theorem split2_change: forall m n A (l: vector A (m+n)) i a, split2 m n (change l (m+i) a) = change (split2 m n l) i a.
Hint Rewrite split2_change: vector.

Theorem split2_change': forall m n A (l: vector A (m+n)) i a, i<m -> split2 m n (change l i a) = split2 m n l.

Lemma get_rev_init: forall i n (h: i<n) (A: Set) (f: nat -> A),
                     get (rev_init n f) i h = f (n-i).
Hint Rewrite get_rev_init: vector.

Theorem get_init: forall i n (h: i<n) (A: Set) (f: nat -> A),
                     get (init n f) i h = f i.
Hint Rewrite get_init: vector.

Theorem get_fill_1: forall i k (h': i<k) A n (h: i<n) (l: vector A k) a, get (fill n l a) i h = get l i h'.

Theorem get_fill_2: forall A i k n (h: i<n) (l: vector A k) a, k<=i -> get (fill n l a) i h = a.

Theorem change_fill: forall A i k (h: i<k) n (l: vector A k) a a', change (fill n l a) i a' = fill n (change l i a') a.

Theorem append_fill_O: forall A (l l': vector A 0) m n a, append (fill m l a) (fill n l' a) = fill (m+n) (nnil _) a.
Hint Rewrite append_fill_O: vector.

Theorem split1_fill: forall A k (l: vector A k) m n a, split1 m n (fill (m+n) l a) = fill m l a.
Hint Rewrite split1_fill: vector.

Theorem split2_fill: forall A k (l: vector A k) m n a, k<=m -> split2 m n (fill (m+n) l a) = fill n (nnil _) a.

Theorem fill_overwrite: forall m n (h: m<=n) k A (l: vector A m) (l': vector A n) a, fill k (overwrite l l') a = overwrite l (fill k l' a).

Theorem overwrite_invol: forall A m (l: vector A m) n (l': vector A n), overwrite l (overwrite l l') = overwrite l l'.
Hint Rewrite overwrite_invol: vector.

Theorem change_overwrite_1: forall i k (h: i<k) A n (l: vector A k) (l': vector A n) a, change (overwrite l l') i a = overwrite (change l i a) l'.

Theorem overwrite_append_1: forall m k (h: k<=m) A n (l: vector A k) (l1: vector A m) (l2: vector A n), overwrite l (append l1 l2) = append (overwrite l l1) l2.
Hint Rewrite overwrite_append_1: vector.

Theorem change_overwrite_2: forall i k (h: k<=i) A n (l: vector A k) (l': vector A n) a, change (overwrite l l') i a = overwrite l (change l' i a).

Theorem truncate_append: forall A m n (l: vector A m) (l': vector A n) (h: m<=m+n), truncate m (append l l') h = l.
Hint Rewrite truncate_append: vector.

Theorem truncate_change: forall A n (l: vector A n) i k a (h: k<=n), truncate k (change l i a) h = change (truncate k l h) i a.
Hint Rewrite truncate_change: vector.

Theorem truncate_overwrite: forall A m (l: vector A m) n (l': vector A n) k (h:k<=n), truncate k (overwrite l l') h = overwrite l (truncate k l' h).
Hint Rewrite truncate_overwrite: vector.

Theorem truncate_eq_from_eq: forall k m (h: k<=m) A (l l': vector A m), truncate k l h = truncate k l' h -> eq_from k l l' -> l = l'.

Theorem eq_from_change: forall k m (h: k<=m) A i (l l': vector A m) a, i<k -> eq_from k l l' -> eq_from k (change l i a) l'.

Theorem eq_from_overwrite': forall A m n (l: vector A m) (l': vector A n), eq_from m (overwrite l l') l'.
Hint Immediate eq_from_overwrite'.

Theorem eq_from_overwrite: forall A m n (l: vector A m) (l1 l2: vector A n), eq_from m l1 l2 -> eq_from m (overwrite l l1) l2.

Theorem eq_from_append: forall A m n (l1 l2: vector A m) (l: vector A n), eq_from m (append l1 l) (append l2 l).
Hint Immediate eq_from_append.

Lemma nki_n: forall i k n, k<=n -> i < k -> n-k+i < n.

Definition etruncate k n (l: vector nat n) (h: k<=n): vector nat k :=
  init k (fun i => match le_lt_dec k i with left _ => 0 | right h' => get l (n-k+i) (nki_n h h') end).
Implicit Arguments etruncate [n].

Theorem get_etruncate: forall k n (l: vector nat n) (h: k<=n) i (h': i<k), get (etruncate k l h) i h' = get l (n-k+i) (nki_n h h').
Hint Rewrite get_etruncate: vector.

Theorem etruncate_change: forall n (l: vector nat n) i k a (h: k<=n), etruncate k (change l ((n-k)+i) a) h = change (etruncate k l h) i a.
Hint Rewrite etruncate_change: vector.

Theorem etruncate_append: forall m n (l: vector nat m) (l': vector nat n) (h: n<=m+n), etruncate n (append l l') h = l'.
Hint Rewrite etruncate_append: vector.

Theorem etruncate_append_cons: forall m n (l: vector nat m) (l': vector nat n) a (h: n<=m+S n), etruncate n (append l (ncons a l')) h = l'.
Hint Rewrite etruncate_append_cons: vector.

Theorem etruncate_eq_until_eq: forall k m (h: k<=m) (l l': vector nat m), etruncate k l h = etruncate k l' h -> eq_until (m-k) l l' -> l = l'.

Theorem eq_until_change: forall k m (h: k<=m) A i (l l': vector A m) a, k<=i -> eq_until k l l' -> eq_until k (change l i a) l'.

Lemma eq_le: forall m n, m=n -> m<=n.
Definition coerce m n (h: n=m) (l: vector nat m) := etruncate n l (eq_le h).
Implicit Arguments coerce [m].

Theorem get_coerce: forall m n (h: n=m) (l: vector nat m) i (h': i<n), get (coerce n h l) i h' = get l i (lt_le_trans _ _ _ h' (eq_le h)).
Hint Rewrite get_coerce: vector.

Section Map.

  Variables A B: Set.
  Variable f: A -> B.

  Fixpoint map(n: nat) (l: vector A n) {struct l}: vector B n :=
  match l in vector _ n return vector B n with
  | nnil => nnil B
  | ncons _ a q => ncons (f a) (map q)
  end.

  Theorem get_map: forall (n: nat) (l: vector A n) (i: nat) (h: i<n), get (map l) i h = f (get l i h).
  Hint Rewrite get_map: vector.

End Map.


Infix "::" := ncons (at level 60, right associativity).
Infix "@" := append (at level 61, left associativity).


Ltac finite_list l := rewrite (empty_nnil l) || ( rewrite (head_tail l); finite_list (tail l) ).
Ltac get_change := rewrite get_change_ii || (rewrite get_change_ij; [ get_change | assumption || auto with arith ]).