# Library Kildall.lists.vector

Section Vector.

Require Export Eqdep.
Require Export Arith.
Require Export semilattices.

Variable A : Set.

Inductive vector : natSet:=
| vector_nil : (vector 0)
| vector_cons : (n:nat), Avector n->(vector (S n)).

Definition eq_list:=(eq_dep nat vector).

fun (n:nat) (v:(vector n)) ⇒
match v in (vector x) return (lt 0 x)-> A with
vector_nilfun h:(lt O O) ⇒ (False_rec A (lt_irrefl O h)) |
(vector_cons n' h _) ⇒ fun H : (lt 0 (S n')) ⇒ h
end.

fun (n:nat)(v:(vector (S n))) ⇒ (head' (S n) v (lt_O_Sn n)).

Definition tail:=
fun (n:nat)(v:vector n) ⇒
match v in (vector x) return (vector (pred x)) with
vector_nilvector_nil|
(vector_cons n' h v')=> v' end.

Lemma empty_dep: (n:nat)(v:(vector n)), n=O->(eq_list O vector_nil n v).
Proof.
unfold eq_list; intros n v.
dependent inversion v; auto.
intro h; absurd ((S n0)=0); auto.
Save.

Hint Resolve empty_dep.

Lemma empty: (v:(vector O)), vector_nil=v.
Proof.
intro v.
apply (eq_dep_eq nat vector O).
apply empty_dep; auto.
Save.

Hint Resolve empty.

Remark non_empty_dep:
(n m : nat), m=(S n) (v:(vector (S n))),
{h:A & {t:(vector n) | (eq_list (S n) v (S n) (vector_cons n h t))}}.
Proof.
intros.
generalize H.
dependent inversion_clear v with
(fun (n':nat)(v:(vector n')) ⇒
m=n'{a:A & {v':(vector n)|(eq_list n' v (S n) (vector_cons n a v'))}}).
unfold eq_list.
intro H'.
a.
v0.
constructor.
Qed.

Lemma non_empty: (n:nat)(v:(vector (S n))),
{a:A &{t:(vector n)|v=(vector_cons n a t)}}.
Proof.
intros n v.
cut (sigS (fun a:A
(sig (fun t:(vector n)=>(eq_list (S n) v (S n) (vector_cons n a t)))))).
intros H; elim H; clear H.
intros a H; elim H; clear H.
intros t H.
a; t.
apply (eq_dep_eq nat vector (S n)) .
unfold eq_list in H; auto.
apply (non_empty_dep n (S n)); auto.
Defined.

Lemma split_vector : (n:nat)(v:(vector (S n))),
v=(vector_cons n (head n v) (tail (S n) v)).
Proof.
intros n v.
elim (non_empty n v).
intros h H; elim H; clear H.
intros t e.
rewrite e; simpl.
auto.
Save.

Definition hd' := fun (n:nat)(v:(vector (S n))) ⇒
let (a, H):= (non_empty n v) in a.

Lemma Non_empty_Hd :
(n:nat)(a:A)(v:(vector n)), (hd' n (vector_cons n a v))=a.
Proof.
intros n a v; unfold hd'.
elim (non_empty n (vector_cons n a v)).
intros x H; elim H.
clear H; intros X H.
injection H; auto.
Save.

Inductive vector_pointwise (r:relation A):
n:nat, (vector n)->(vector n) → Prop :=
| le_nil: vector_pointwise r 0 vector_nil vector_nil
| le_cons: (a a' : A) (n : nat) (v v' : (vector n)),
(r a a')->vector_pointwise r n v v'vector_pointwise r (S n) (vector_cons n a v) (vector_cons n a' v').

Definition Vector_pointwise (r:relation A) (n:nat) : relation (vector n) :=
vector_pointwise r n.
Definition SI_vector_pointwise (r:relation A) (n:nat) : relation (vector n) :=
strict (inv (vector_pointwise r n)).

Fixpoint vector_replace (n:nat) (v:vector n) (i:nat) (a:A) {struct v}:
(vector n) :=
match v in vector n return vector n with
| vector_nilvector_nil
| vector_cons n' h t
match i with
| 0 ⇒ vector_cons n' a t
| (S i') ⇒ vector_cons n' h (vector_replace n' t i' a)
end
end.

Fixpoint belong_element_vector (n:nat) (l : vector n) (a:A) {struct l} : Prop :=
match l in vector n return Prop with
| vector_nilFalse
| vector_cons n' h th=a belong_element_vector n' t a
end.

Fixpoint element_at (n:nat) (v : vector n) (i:nat) {struct v} :
(lt i n)->A :=
match v in vector n, i return (lt i n)->A with
| vector_nil, _fun x : (lt i 0) ⇒ (False_rec A (lt_n_O i x))
| (vector_cons p h t), 0 ⇒ fun (x : (lt 0 (S p)))=> h
| (vector_cons p h t), (S i') ⇒
fun (x : (lt (S i') (S p))) ⇒ (element_at p t i') (lt_S_n i' p x)
end.

Fixpoint element_at_unsafe (n : nat) (v : vector n) (i : nat) {struct v} : option A :=
match v with
| vector_nilNone
| vector_cons p h t
match i with
| 0 ⇒ Some h
| S i'element_at_unsafe p t i'
end
end.

Fixpoint constant_list (n : nat) (a : A) {struct n} : vector n :=
match n return vector n with
| 0 ⇒ vector_nil
| (S p) ⇒ vector_cons p a (constant_list p a)
end.

End Vector.

Fixpoint vector_map (A B:Set) (g:AB) (n:nat) (v:vector A n) {struct v} :
vector B n :=
match v in (vector _ n) return (vector _ n) with
| vector_nilvector_nil B
| vector_cons p h tvector_cons B p (g h) (vector_map A B g p t)
end.

Fixpoint map2 (A B C : Set) (f : ABC) (n : nat) {struct n}:
(vector A n)->(vector B n)-> (vector C n):=
match n return (vector _ n)->(vector _ n)-> (vector _ n) with
| 0 ⇒ (fun (v:(vector _ 0))(v':(vector _ 0)) ⇒ (vector_nil _))
| (S p)=> (fun (v:(vector _ (S p))) (v':(vector _ (S p))) ⇒
(vector_cons _ p (f (head A p v) (head B p v'))
(map2 _ _ _ f _ (tail _ _ v) (tail _ _ v'))))
end.

Definition Map2 (A : Set) (f : binop A) (n:nat):= map2 A A A f n.

Implicit Arguments vector_cons [A n].
Implicit Arguments vector_nil [A].
Implicit Arguments tail [A n].
Implicit Arguments empty [A].
Implicit Arguments split_vector [A n].
Implicit Arguments vector_replace [A n].
Implicit Arguments belong_element_vector [A n].
Implicit Arguments element_at [A n].
Implicit Arguments vector_map [A B n].
Implicit Arguments map2 [A B C n].
Implicit Arguments Map2 [A].
Implicit Arguments constant_list [A].
Implicit Arguments element_at_unsafe [A n].

Ltac Split x:= replace x with (vector_cons (head x) (tail x));
[trivial | symmetry; exact (split_vector x)].

Ltac CaseEq f:=generalize (refl_equal f); pattern f at -1 in |- *; case f.

Notation "v '[' p '<-' e ']'" := (vector_replace v p e) (at level 50).
Notation "e 'INv' v" := (belong_element_vector v e) (at level 50).
Notation "v '[' p '|' C ']'" := (element_at v p C) (at level 50).
Notation "v '[' p '|_]'" := (element_at_unsafe v p) (at level 50).