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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
Set Implicit Arguments.
Require Import Lia.
Require Import Coquplib.
From Coq Require Import Lists.List Datatypes.
Import ListNotations.
Local Open Scope nat_scope.
Record Array (A : Type) : Type :=
mk_array
{ arr_contents : list A
; arr_length : nat
; arr_wf : length arr_contents = arr_length
}.
Definition make_array {A : Type} (l : list A) : Array A :=
@mk_array A l (length l) eq_refl.
Fixpoint list_set {A : Type} (i : nat) (x : A) (l : list A) {struct l} : list A :=
match i, l with
| _, nil => nil
| S n, h :: t => h :: list_set n x t
| O, h :: t => x :: t
end.
Lemma list_set_spec1 {A : Type} :
forall l i (x : A),
i < length l -> nth_error (list_set i x l) i = Some x.
Proof.
induction l; intros; destruct i; simplify; try lia; try reflexivity; firstorder.
Qed.
Hint Resolve list_set_spec1 : array.
Lemma list_set_spec2 {A : Type} :
forall l i (x : A) d,
i < length l -> nth i (list_set i x l) d = x.
Proof.
induction l; intros; destruct i; simplify; try lia; try reflexivity; firstorder.
Qed.
Hint Resolve list_set_spec2 : array.
Lemma array_set_wf {A : Type} :
forall l ln i (x : A),
length l = ln -> length (list_set i x l) = ln.
Proof.
induction l; intros; destruct i; auto.
invert H; simplify; auto.
Qed.
Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) :=
let l := a.(arr_contents) in
let ln := a.(arr_length) in
let WF := a.(arr_wf) in
@mk_array A (list_set i x l) ln (@array_set_wf A l ln i x WF).
Lemma array_set_spec1 {A : Type} :
forall a i (x : A),
i < a.(arr_length) -> nth_error ((array_set i x a).(arr_contents)) i = Some x.
Proof.
intros.
rewrite <- a.(arr_wf) in H.
unfold array_set. simplify.
eauto with array.
Qed.
Hint Resolve array_set_spec1 : array.
Lemma array_set_spec2 {A : Type} :
forall a i (x : A) d,
i < a.(arr_length) -> nth i ((array_set i x a).(arr_contents)) d = x.
Proof.
intros.
rewrite <- a.(arr_wf) in H.
unfold array_set. simplify.
eauto with array.
Qed.
Hint Resolve array_set_spec2 : array.
Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A :=
nth_error a.(arr_contents) i.
Lemma array_get_error_bound {A : Type} :
forall (a : Array A) i,
i < a.(arr_length) -> exists x, array_get_error i a = Some x.
Proof.
intros.
rewrite <- a.(arr_wf) in H.
assert (~ length (arr_contents a) <= i) by lia.
pose proof (nth_error_None a.(arr_contents) i).
apply not_iff_compat in H1.
apply <- H1 in H0.
destruct (nth_error (arr_contents a) i ) eqn:EQ; try contradiction; eauto.
Qed.
Lemma array_get_error_set_bound {A : Type} :
forall (a : Array A) i x,
i < a.(arr_length) -> array_get_error i (array_set i x a) = Some x.
Proof.
intros.
unfold array_get_error.
eauto with array.
Qed.
Definition array_get {A : Type} (i : nat) (x : A) (a : Array A) : A :=
nth i a.(arr_contents) x.
Lemma array_get_set_bound {A : Type} :
forall (a : Array A) i x d,
i < a.(arr_length) -> array_get i d (array_set i x a) = x.
Proof.
intros.
unfold array_get.
info_eauto with array.
Qed.
Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A :=
match n with
| O => acc
| S n => list_repeat' (a::acc) a n
end.
Lemma list_repeat'_len : forall {A : Type} (a : A) n l,
Datatypes.length (list_repeat' l a n) = (n + Datatypes.length l)%nat.
Proof.
induction n; intros; simplify; try reflexivity.
specialize (IHn (a :: l)).
rewrite IHn.
simplify.
lia.
Qed.
Definition list_repeat {A : Type} : A -> nat -> list A := list_repeat' nil.
Lemma list_repeat_len {A : Type} : forall n (a : A), Datatypes.length (list_repeat a n) = n.
Proof.
intros.
unfold list_repeat.
rewrite list_repeat'_len.
simplify. lia.
Qed.
Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n).
Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C :=
match x, y with
| a :: t, b :: t' => f a b :: list_combine f t t'
| _, _ => nil
end.
Definition combine {A B C : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C :=
make_array (list_combine f x.(arr_contents) y.(arr_contents)).
|
