1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
Require Import ExtLib.Data.Fin.
Set Implicit Arguments.
Set Strict Implicit.
Set Asymmetric Patterns.
Fixpoint vector (T : Type) (n : nat) : Type :=
match n with
| 0 => unit
| S n => prod T (vector T n)
end.
Fixpoint get {T} {n : nat} (f : fin n) : vector T n -> T :=
match f in fin n return vector T n -> T with
| F0 n => fun v : T * vector T n => fst v
| FS n f => fun v : T * vector T n => get f (snd v)
end.
Fixpoint put {T} {n : nat} (f : fin n) (t : T) : vector T n -> vector T n :=
match f in fin n return vector T n -> vector T n with
| F0 _ => fun v => (t, snd v)
| FS _ f => fun v => (fst v, put f t (snd v))
end.
Theorem get_put_eq : forall {T n} (v : vector T n) (f : fin n) val,
get f (put f val v) = val.
Proof.
induction n.
{ inversion f. }
{ remember (S n). destruct f.
inversion Heqn0; subst; intros; reflexivity.
inversion Heqn0; subst; simpl; auto. }
Qed.
Theorem get_put_neq : forall {T n} (v : vector T n) (f f' : fin n) val,
f <> f' ->
get f (put f' val v) = get f v.
Proof.
induction n.
{ inversion f. }
{ remember (S n); destruct f.
{ inversion Heqn0; clear Heqn0; subst; intros.
destruct (fin_case f'); try congruence.
destruct H0; subst. auto. }
{ inversion Heqn0; clear Heqn0; subst; intros.
destruct (fin_case f').
subst; auto.
destruct H0; subst. simpl.
eapply IHn. congruence. } }
Qed.
Definition vector_tl {T : Type} {n : nat} (v : vector T (S n)) : vector T n :=
snd v.
Definition vector_hd {T : Type} {n : nat} (v : vector T (S n)) : T :=
fst v.
|
