adamc@114
|
1 (* Copyright (c) 2008, Adam Chlipala
|
adamc@114
|
2 *
|
adamc@114
|
3 * This work is licensed under a
|
adamc@114
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
adamc@114
|
5 * Unported License.
|
adamc@114
|
6 * The license text is available at:
|
adamc@114
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
adamc@114
|
8 *)
|
adamc@114
|
9
|
adamc@114
|
10 (* Dependent list types presented in Chapter 8 *)
|
adamc@114
|
11
|
adamc@179
|
12 Require Import Arith List Tactics.
|
adamc@114
|
13
|
adamc@114
|
14 Set Implicit Arguments.
|
adamc@114
|
15
|
adamc@114
|
16
|
adamc@114
|
17 Section ilist.
|
adamc@123
|
18 Variable A : Type.
|
adamc@114
|
19
|
adamc@123
|
20 Fixpoint ilist (n : nat) : Type :=
|
adamc@114
|
21 match n with
|
adamc@114
|
22 | O => unit
|
adamc@114
|
23 | S n' => A * ilist n'
|
adamc@114
|
24 end%type.
|
adamc@114
|
25
|
adamc@149
|
26 Definition inil : ilist O := tt.
|
adamc@149
|
27 Definition icons n x (ls : ilist n) : ilist (S n) := (x, ls).
|
adamc@149
|
28
|
adamc@149
|
29 Definition hd n (ls : ilist (S n)) : A := fst ls.
|
adamc@149
|
30 Definition tl n (ls : ilist (S n)) : ilist n := snd ls.
|
adamc@149
|
31
|
adamc@149
|
32 Implicit Arguments icons [n].
|
adamc@149
|
33
|
adamc@123
|
34 Fixpoint index (n : nat) : Type :=
|
adamc@114
|
35 match n with
|
adamc@114
|
36 | O => Empty_set
|
adamc@114
|
37 | S n' => option (index n')
|
adamc@114
|
38 end.
|
adamc@114
|
39
|
adamc@114
|
40 Fixpoint get (n : nat) : ilist n -> index n -> A :=
|
adamc@114
|
41 match n return ilist n -> index n -> A with
|
adamc@114
|
42 | O => fun _ idx => match idx with end
|
adamc@114
|
43 | S n' => fun ls idx =>
|
adamc@114
|
44 match idx with
|
adamc@114
|
45 | None => fst ls
|
adamc@114
|
46 | Some idx' => get n' (snd ls) idx'
|
adamc@114
|
47 end
|
adamc@114
|
48 end.
|
adamc@149
|
49
|
adamc@149
|
50 Section everywhere.
|
adamc@149
|
51 Variable x : A.
|
adamc@149
|
52
|
adamc@149
|
53 Fixpoint everywhere (n : nat) : ilist n :=
|
adamc@149
|
54 match n return ilist n with
|
adamc@149
|
55 | O => inil
|
adamc@149
|
56 | S n' => icons x (everywhere n')
|
adamc@149
|
57 end.
|
adamc@149
|
58 End everywhere.
|
adamc@149
|
59
|
adamc@149
|
60 Section singleton.
|
adamc@149
|
61 Variables x default : A.
|
adamc@149
|
62
|
adamc@149
|
63 Fixpoint singleton (n m : nat) {struct n} : ilist n :=
|
adamc@149
|
64 match n return ilist n with
|
adamc@149
|
65 | O => inil
|
adamc@149
|
66 | S n' =>
|
adamc@149
|
67 match m with
|
adamc@149
|
68 | O => icons x (everywhere default n')
|
adamc@149
|
69 | S m' => icons default (singleton n' m')
|
adamc@149
|
70 end
|
adamc@149
|
71 end.
|
adamc@149
|
72 End singleton.
|
adamc@149
|
73
|
adamc@149
|
74 Section map2.
|
adamc@149
|
75 Variable f : A -> A -> A.
|
adamc@149
|
76
|
adamc@149
|
77 Fixpoint map2 (n : nat) : ilist n -> ilist n -> ilist n :=
|
adamc@149
|
78 match n return ilist n -> ilist n -> ilist n with
|
adamc@149
|
79 | O => fun _ _ => inil
|
adamc@149
|
80 | S n' => fun ls1 ls2 => icons (f (hd ls1) (hd ls2)) (map2 _ (tl ls1) (tl ls2))
|
adamc@149
|
81 end.
|
adamc@149
|
82 End map2.
|
adamc@194
|
83
|
adamc@194
|
84 Section fold.
|
adamc@194
|
85 Variable B : Type.
|
adamc@194
|
86 Variable f : A -> B -> B.
|
adamc@194
|
87 Variable i : B.
|
adamc@194
|
88
|
adamc@194
|
89 Fixpoint foldr (n : nat) : ilist n -> B :=
|
adamc@194
|
90 match n return ilist n -> B with
|
adamc@194
|
91 | O => fun _ => i
|
adamc@194
|
92 | S n' => fun ils => f (hd ils) (foldr n' (tl ils))
|
adamc@194
|
93 end.
|
adamc@194
|
94 End fold.
|
adamc@114
|
95 End ilist.
|
adamc@114
|
96
|
adamc@194
|
97 Implicit Arguments inil [A].
|
adamc@194
|
98 Implicit Arguments icons [A n].
|
adamc@194
|
99
|
adamc@149
|
100 Implicit Arguments icons [A n].
|
adamc@114
|
101 Implicit Arguments get [A n].
|
adamc@149
|
102 Implicit Arguments map2 [A n].
|
adamc@194
|
103 Implicit Arguments foldr [A B n].
|
adamc@114
|
104
|
adamc@196
|
105 Section imap.
|
adamc@196
|
106 Variables A B : Type.
|
adamc@196
|
107 Variable f : A -> B.
|
adamc@196
|
108
|
adamc@196
|
109 Fixpoint imap (n : nat) : ilist A n -> ilist B n :=
|
adamc@196
|
110 match n return ilist A n -> ilist B n with
|
adamc@196
|
111 | O => fun _ => inil
|
adamc@196
|
112 | S n' => fun ls => icons (f (hd ls)) (imap _ (tl ls))
|
adamc@196
|
113 end.
|
adamc@196
|
114 End imap.
|
adamc@196
|
115
|
adamc@196
|
116 Implicit Arguments imap [A B n].
|
adamc@196
|
117
|
adamc@114
|
118 Section hlist.
|
adamc@114
|
119 Variable A : Type.
|
adamc@114
|
120 Variable B : A -> Type.
|
adamc@114
|
121
|
adamc@114
|
122 Fixpoint hlist (ls : list A) : Type :=
|
adamc@114
|
123 match ls with
|
adamc@114
|
124 | nil => unit
|
adamc@114
|
125 | x :: ls' => B x * hlist ls'
|
adamc@114
|
126 end%type.
|
adamc@114
|
127
|
adamc@125
|
128 Definition hnil : hlist nil := tt.
|
adamc@125
|
129 Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) :=
|
adamc@125
|
130 (v, hls).
|
adamc@125
|
131
|
adamc@114
|
132 Variable elm : A.
|
adamc@114
|
133
|
adamc@114
|
134 Fixpoint member (ls : list A) : Type :=
|
adamc@114
|
135 match ls with
|
adamc@114
|
136 | nil => Empty_set
|
adamc@114
|
137 | x :: ls' => (x = elm) + member ls'
|
adamc@114
|
138 end%type.
|
adamc@114
|
139
|
adamc@126
|
140 Definition hfirst (x : A) (ls : list A) (pf : x = elm) : member (x :: ls) :=
|
adamc@126
|
141 inl _ pf.
|
adamc@126
|
142 Definition hnext (x : A) (ls : list A) (m : member ls) : member (x :: ls) :=
|
adamc@126
|
143 inr _ m.
|
adamc@126
|
144
|
adamc@114
|
145 Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
|
adamc@114
|
146 match ls return hlist ls -> member ls -> B elm with
|
adamc@114
|
147 | nil => fun _ idx => match idx with end
|
adamc@114
|
148 | _ :: ls' => fun mls idx =>
|
adamc@114
|
149 match idx with
|
adamc@114
|
150 | inl pf => match pf with
|
adamc@114
|
151 | refl_equal => fst mls
|
adamc@114
|
152 end
|
adamc@114
|
153 | inr idx' => hget ls' (snd mls) idx'
|
adamc@114
|
154 end
|
adamc@114
|
155 end.
|
adamc@125
|
156
|
adamc@125
|
157 Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) :=
|
adamc@125
|
158 match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with
|
adamc@125
|
159 | nil => fun _ hls2 => hls2
|
adamc@125
|
160 | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
|
adamc@125
|
161 end.
|
adamc@194
|
162
|
adamc@194
|
163 Variable f : forall x, B x.
|
adamc@194
|
164
|
adamc@194
|
165 Fixpoint hmake (ls : list A) : hlist ls :=
|
adamc@194
|
166 match ls return hlist ls with
|
adamc@194
|
167 | nil => hnil
|
adamc@194
|
168 | x :: ls' => hcons _ (f x) (hmake ls')
|
adamc@194
|
169 end.
|
adamc@196
|
170
|
adamc@196
|
171 Implicit Arguments hget [ls].
|
adamc@196
|
172
|
adamc@196
|
173 Theorem hget_hmake : forall ls (m : member ls),
|
adamc@196
|
174 hget (hmake ls) m = f elm.
|
adamc@196
|
175 induction ls; crush.
|
adamc@196
|
176 case a0; reflexivity.
|
adamc@196
|
177 Qed.
|
adamc@114
|
178 End hlist.
|
adamc@114
|
179
|
adamc@125
|
180 Implicit Arguments hnil [A B].
|
adamc@125
|
181 Implicit Arguments hcons [A B x ls].
|
adamc@114
|
182 Implicit Arguments hget [A B elm ls].
|
adamc@125
|
183 Implicit Arguments happ [A B ls1 ls2].
|
adamc@194
|
184 Implicit Arguments hmake [A B].
|
adamc@125
|
185
|
adamc@126
|
186 Implicit Arguments hfirst [A elm x ls].
|
adamc@126
|
187 Implicit Arguments hnext [A elm x ls].
|
adamc@126
|
188
|
adamc@125
|
189 Infix ":::" := hcons (right associativity, at level 60).
|
adamc@125
|
190 Infix "+++" := happ (right associativity, at level 60).
|
adamc@163
|
191
|
adamc@163
|
192 Section hmap.
|
adamc@163
|
193 Variable A : Type.
|
adamc@163
|
194 Variables B1 B2 : A -> Type.
|
adamc@163
|
195
|
adamc@163
|
196 Variable f : forall x, B1 x -> B2 x.
|
adamc@163
|
197
|
adamc@163
|
198 Fixpoint hmap (ls : list A) : hlist B1 ls -> hlist B2 ls :=
|
adamc@163
|
199 match ls return hlist B1 ls -> hlist B2 ls with
|
adamc@163
|
200 | nil => fun _ => hnil
|
adamc@163
|
201 | _ :: _ => fun hl => f (fst hl) ::: hmap _ (snd hl)
|
adamc@163
|
202 end.
|
adamc@179
|
203
|
adamc@179
|
204 Implicit Arguments hmap [ls].
|
adamc@179
|
205
|
adamc@179
|
206 Theorem hmap_happ : forall ls2 (h2 : hlist B1 ls2) ls1 (h1 : hlist B1 ls1),
|
adamc@179
|
207 hmap h1 +++ hmap h2 = hmap (h1 +++ h2).
|
adamc@179
|
208 induction ls1; crush.
|
adamc@179
|
209 Qed.
|
adamc@163
|
210 End hmap.
|
adamc@163
|
211
|
adamc@163
|
212 Implicit Arguments hmap [A B1 B2 ls].
|