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@114
|
105 Section hlist.
|
adamc@114
|
106 Variable A : Type.
|
adamc@114
|
107 Variable B : A -> Type.
|
adamc@114
|
108
|
adamc@114
|
109 Fixpoint hlist (ls : list A) : Type :=
|
adamc@114
|
110 match ls with
|
adamc@114
|
111 | nil => unit
|
adamc@114
|
112 | x :: ls' => B x * hlist ls'
|
adamc@114
|
113 end%type.
|
adamc@114
|
114
|
adamc@125
|
115 Definition hnil : hlist nil := tt.
|
adamc@125
|
116 Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) :=
|
adamc@125
|
117 (v, hls).
|
adamc@125
|
118
|
adamc@114
|
119 Variable elm : A.
|
adamc@114
|
120
|
adamc@114
|
121 Fixpoint member (ls : list A) : Type :=
|
adamc@114
|
122 match ls with
|
adamc@114
|
123 | nil => Empty_set
|
adamc@114
|
124 | x :: ls' => (x = elm) + member ls'
|
adamc@114
|
125 end%type.
|
adamc@114
|
126
|
adamc@126
|
127 Definition hfirst (x : A) (ls : list A) (pf : x = elm) : member (x :: ls) :=
|
adamc@126
|
128 inl _ pf.
|
adamc@126
|
129 Definition hnext (x : A) (ls : list A) (m : member ls) : member (x :: ls) :=
|
adamc@126
|
130 inr _ m.
|
adamc@126
|
131
|
adamc@114
|
132 Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
|
adamc@114
|
133 match ls return hlist ls -> member ls -> B elm with
|
adamc@114
|
134 | nil => fun _ idx => match idx with end
|
adamc@114
|
135 | _ :: ls' => fun mls idx =>
|
adamc@114
|
136 match idx with
|
adamc@114
|
137 | inl pf => match pf with
|
adamc@114
|
138 | refl_equal => fst mls
|
adamc@114
|
139 end
|
adamc@114
|
140 | inr idx' => hget ls' (snd mls) idx'
|
adamc@114
|
141 end
|
adamc@114
|
142 end.
|
adamc@125
|
143
|
adamc@125
|
144 Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) :=
|
adamc@125
|
145 match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with
|
adamc@125
|
146 | nil => fun _ hls2 => hls2
|
adamc@125
|
147 | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
|
adamc@125
|
148 end.
|
adamc@194
|
149
|
adamc@194
|
150 Variable f : forall x, B x.
|
adamc@194
|
151
|
adamc@194
|
152 Fixpoint hmake (ls : list A) : hlist ls :=
|
adamc@194
|
153 match ls return hlist ls with
|
adamc@194
|
154 | nil => hnil
|
adamc@194
|
155 | x :: ls' => hcons _ (f x) (hmake ls')
|
adamc@194
|
156 end.
|
adamc@114
|
157 End hlist.
|
adamc@114
|
158
|
adamc@125
|
159 Implicit Arguments hnil [A B].
|
adamc@125
|
160 Implicit Arguments hcons [A B x ls].
|
adamc@114
|
161 Implicit Arguments hget [A B elm ls].
|
adamc@125
|
162 Implicit Arguments happ [A B ls1 ls2].
|
adamc@194
|
163 Implicit Arguments hmake [A B].
|
adamc@125
|
164
|
adamc@126
|
165 Implicit Arguments hfirst [A elm x ls].
|
adamc@126
|
166 Implicit Arguments hnext [A elm x ls].
|
adamc@126
|
167
|
adamc@125
|
168 Infix ":::" := hcons (right associativity, at level 60).
|
adamc@125
|
169 Infix "+++" := happ (right associativity, at level 60).
|
adamc@163
|
170
|
adamc@163
|
171 Section hmap.
|
adamc@163
|
172 Variable A : Type.
|
adamc@163
|
173 Variables B1 B2 : A -> Type.
|
adamc@163
|
174
|
adamc@163
|
175 Variable f : forall x, B1 x -> B2 x.
|
adamc@163
|
176
|
adamc@163
|
177 Fixpoint hmap (ls : list A) : hlist B1 ls -> hlist B2 ls :=
|
adamc@163
|
178 match ls return hlist B1 ls -> hlist B2 ls with
|
adamc@163
|
179 | nil => fun _ => hnil
|
adamc@163
|
180 | _ :: _ => fun hl => f (fst hl) ::: hmap _ (snd hl)
|
adamc@163
|
181 end.
|
adamc@179
|
182
|
adamc@179
|
183 Implicit Arguments hmap [ls].
|
adamc@179
|
184
|
adamc@179
|
185 Theorem hmap_happ : forall ls2 (h2 : hlist B1 ls2) ls1 (h1 : hlist B1 ls1),
|
adamc@179
|
186 hmap h1 +++ hmap h2 = hmap (h1 +++ h2).
|
adamc@179
|
187 induction ls1; crush.
|
adamc@179
|
188 Qed.
|
adamc@163
|
189 End hmap.
|
adamc@163
|
190
|
adamc@163
|
191 Implicit Arguments hmap [A B1 B2 ls].
|