Mercurial > cpdt > repo

comparison src/DepList.v @ 216:d1464997078d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Switch DepList to inductive, not recursive, types
author Adam Chlipala <adamc@hcoop.net>
date Wed, 11 Nov 2009 14:28:47 -0500
parents f8bcd33bdd91
children d5787b70cf48
comparison
equal deleted inserted replaced
215:f8bcd33bdd91 216:d1464997078d
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008-2009, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
15 15
16 16
17 Section ilist. 17 Section ilist.
18 Variable A : Type. 18 Variable A : Type.
19 19
20 Fixpoint ilist (n : nat) : Type := 20 Inductive ilist : nat -> Type :=
21 match n with 21 | INil : ilist O
22 | O => unit 22 | ICons : forall n, A -> ilist n -> ilist (S n).
23 | S n' => A * ilist n' 23
24 end%type. 24 Definition hd n (ls : ilist (S n)) :=
25 25 match ls in ilist n' return match n' with
26 Definition inil : ilist O := tt. 26 | O => unit
27 Definition icons n x (ls : ilist n) : ilist (S n) := (x, ls). 27 | S _ => A
28 28 end with
29 Definition hd n (ls : ilist (S n)) : A := fst ls. 29 | INil => tt
30 Definition tl n (ls : ilist (S n)) : ilist n := snd ls. 30 | ICons _ x _ => x
31 31 end.
32 Implicit Arguments icons [n]. 32 Definition tl n (ls : ilist (S n)) :=
33 33 match ls in ilist n' return match n' with
34 Fixpoint fin (n : nat) : Type := 34 | O => unit
35 match n with 35 | S n => ilist n
36 | O => Empty_set 36 end with
37 | S n' => option (fin n') 37 | INil => tt
38 end. 38 | ICons _ _ ls' => ls'
39 39 end.
40 Fixpoint get (n : nat) : ilist n -> fin n -> A := 40
41 match n return ilist n -> fin n -> A with 41 Inductive fin : nat -> Set :=
42 | O => fun _ idx => match idx with end 42 | First : forall n, fin (S n)
43 | S n' => fun ls idx => 43 | Next : forall n, fin n -> fin (S n).
44 match idx with 44
45 | None => fst ls 45 Fixpoint get n (ls : ilist n) : fin n -> A :=
46 | Some idx' => get n' (snd ls) idx' 46 match ls with
47 | INil => fun idx =>
48 match idx in fin n' return (match n' with
49 | O => A
50 | S _ => unit
51 end) with
52 | First _ => tt
53 | Next _ _ => tt
47 end 54 end
55 | ICons _ x ls' => fun idx =>
56 match idx in fin n' return (fin (pred n') -> A) -> A with
57 | First _ => fun _ => x
58 | Next _ idx' => fun get_ls' => get_ls' idx'
59 end (get ls')
48 end. 60 end.
49 61
50 Section everywhere. 62 Section everywhere.
51 Variable x : A. 63 Variable x : A.
52 64
53 Fixpoint everywhere (n : nat) : ilist n := 65 Fixpoint everywhere (n : nat) : ilist n :=
54 match n return ilist n with 66 match n with
55 | O => inil 67 | O => INil
56 | S n' => icons x (everywhere n') 68 | S n' => ICons x (everywhere n')
57 end. 69 end.
58 End everywhere. 70 End everywhere.
59 71
60 Section singleton. 72 Section singleton.
61 Variables x default : A. 73 Variables x default : A.
62 74
63 Fixpoint singleton (n m : nat) {struct n} : ilist n := 75 Fixpoint singleton (n m : nat) : ilist n :=
64 match n return ilist n with 76 match n with
65 | O => inil 77 | O => INil
66 | S n' => 78 | S n' =>
67 match m with 79 match m with
68 | O => icons x (everywhere default n') 80 | O => ICons x (everywhere default n')
69 | S m' => icons default (singleton n' m') 81 | S m' => ICons default (singleton n' m')
70 end 82 end
71 end. 83 end.
72 End singleton. 84 End singleton.
73 85
74 Section map2. 86 Section map2.
75 Variable f : A -> A -> A. 87 Variable f : A -> A -> A.
76 88
77 Fixpoint map2 (n : nat) : ilist n -> ilist n -> ilist n := 89 Fixpoint map2 n (il1 : ilist n) : ilist n -> ilist n :=
78 match n return ilist n -> ilist n -> ilist n with 90 match il1 in ilist n return ilist n -> ilist n with
79 | O => fun _ _ => inil 91 | INil => fun _ => INil
80 | S n' => fun ls1 ls2 => icons (f (hd ls1) (hd ls2)) (map2 _ (tl ls1) (tl ls2)) 92 | ICons _ x il1' => fun il2 => ICons (f x (hd il2)) (map2 il1' (tl il2))
81 end. 93 end.
82 End map2. 94 End map2.
83 95
84 Section fold. 96 Section fold.
85 Variable B : Type. 97 Variable B : Type.
86 Variable f : A -> B -> B. 98 Variable f : A -> B -> B.
87 Variable i : B. 99 Variable i : B.
88 100
89 Fixpoint foldr (n : nat) : ilist n -> B := 101 Fixpoint foldr n (il : ilist n) : B :=
90 match n return ilist n -> B with 102 match il with
91 | O => fun _ => i 103 | INil => i
92 | S n' => fun ils => f (hd ils) (foldr n' (tl ils)) 104 | ICons _ x il' => f x (foldr il')
93 end. 105 end.
94 End fold. 106 End fold.
95 End ilist. 107 End ilist.
96 108
97 Implicit Arguments inil [A]. 109 Implicit Arguments INil [A].
98 Implicit Arguments icons [A n]. 110 Implicit Arguments First [n].
99
100 Implicit Arguments icons [A n].
101 Implicit Arguments get [A n].
102 Implicit Arguments map2 [A n].
103 Implicit Arguments foldr [A B n].
104 111
105 Section imap. 112 Section imap.
106 Variables A B : Type. 113 Variables A B : Type.
107 Variable f : A -> B. 114 Variable f : A -> B.
108 115
109 Fixpoint imap (n : nat) : ilist A n -> ilist B n := 116 Fixpoint imap n (il : ilist A n) : ilist B n :=
110 match n return ilist A n -> ilist B n with 117 match il with
111 | O => fun _ => inil 118 | INil => INil
112 | S n' => fun ls => icons (f (hd ls)) (imap _ (tl ls)) 119 | ICons _ x il' => ICons (f x) (imap il')
113 end. 120 end.
114 End imap. 121 End imap.
115
116 Implicit Arguments imap [A B n].
117 122
118 Section hlist. 123 Section hlist.
119 Variable A : Type. 124 Variable A : Type.
120 Variable B : A -> Type. 125 Variable B : A -> Type.
121 126
122 Fixpoint hlist (ls : list A) : Type := 127 Inductive hlist : list A -> Type :=
128 | HNil : hlist nil
129 | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
130
131 Definition hhd ls (hl : hlist ls) :=
132 match hl in hlist ls return match ls with
133 | nil => unit
134 | x :: _ => B x
135 end with
136 | HNil => tt
137 | HCons _ _ v _ => v
138 end.
139
140 Definition htl ls (hl : hlist ls) :=
141 match hl in hlist ls return match ls with
142 | nil => unit
143 | _ :: ls' => hlist ls'
144 end with
145 | HNil => tt
146 | HCons _ _ _ hl' => hl'
147 end.
148
149 Variable elm : A.
150
151 Inductive member : list A -> Type :=
152 | HFirst : forall ls, member (elm :: ls)
153 | HNext : forall x ls, member ls -> member (x :: ls).
154
155 Fixpoint hget ls (mls : hlist ls) : member ls -> B elm :=
156 match mls with
157 | HNil => fun mem =>
158 match mem in member ls' return (match ls' with
159 | nil => B elm
160 | _ :: _ => unit
161 end) with
162 | HFirst _ => tt
163 | HNext _ _ _ => tt
164 end
165 | HCons _ _ x mls' => fun mem =>
166 match mem in member ls' return (match ls' with
167 | nil => Empty_set
168 | x' :: ls'' =>
169 B x' -> (member ls'' -> B elm) -> B elm
170 end) with
171 | HFirst _ => fun x _ => x
172 | HNext _ _ mem' => fun _ get_mls' => get_mls' mem'
173 end x (hget mls')
174 end.
175
176 Fixpoint happ (ls1 : list A) (hl1 : hlist ls1) : forall ls2, hlist ls2 -> hlist (ls1 ++ ls2) :=
177 match hl1 in hlist ls1 return forall ls2, hlist ls2 -> hlist (ls1 ++ ls2) with
178 | HNil => fun _ hl2 => hl2
179 | HCons _ _ x hl1' => fun _ hl2 => HCons x (happ hl1' hl2)
180 end.
181
182 Variable f : forall x, B x.
183
184 Fixpoint hmake (ls : list A) : hlist ls :=
123 match ls with 185 match ls with
124 | nil => unit 186 | nil => HNil
125 | x :: ls' => B x * hlist ls' 187 | x :: ls' => HCons (f x) (hmake ls')
126 end%type. 188 end.
127
128 Definition hnil : hlist nil := tt.
129 Definition hcons (x : A) (ls : list A) (v : B x) (hls : hlist ls) : hlist (x :: ls) :=
130 (v, hls).
131
132 Variable elm : A.
133
134 Fixpoint member (ls : list A) : Type :=
135 match ls with
136 | nil => Empty_set
137 | x :: ls' => (x = elm) + member ls'
138 end%type.
139
140 Definition hfirst (x : A) (ls : list A) (pf : x = elm) : member (x :: ls) :=
141 inl _ pf.
142 Definition hnext (x : A) (ls : list A) (m : member ls) : member (x :: ls) :=
143 inr _ m.
144
145 Fixpoint hget (ls : list A) : hlist ls -> member ls -> B elm :=
146 match ls return hlist ls -> member ls -> B elm with
147 | nil => fun _ idx => match idx with end
148 | _ :: ls' => fun mls idx =>
149 match idx with
150 | inl pf => match pf with
151 | refl_equal => fst mls
152 end
153 | inr idx' => hget ls' (snd mls) idx'
154 end
155 end.
156
157 Fixpoint happ (ls1 ls2 : list A) {struct ls1} : hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) :=
158 match ls1 return hlist ls1 -> hlist ls2 -> hlist (ls1 ++ ls2) with
159 | nil => fun _ hls2 => hls2
160 | _ :: _ => fun hls1 hls2 => (fst hls1, happ _ _ (snd hls1) hls2)
161 end.
162
163 Variable f : forall x, B x.
164
165 Fixpoint hmake (ls : list A) : hlist ls :=
166 match ls return hlist ls with
167 | nil => hnil
168 | x :: ls' => hcons _ (f x) (hmake ls')
169 end.
170
171 Implicit Arguments hget [ls].
172 189
173 Theorem hget_hmake : forall ls (m : member ls), 190 Theorem hget_hmake : forall ls (m : member ls),
174 hget (hmake ls) m = f elm. 191 hget (hmake ls) m = f elm.
175 induction ls; crush. 192 induction ls; crush;
176 case a0; reflexivity. 193 match goal with
194 | [ |- context[match ?E with HFirst _ => _ | HNext _ _ _ => _ end] ] => dep_destruct E
195 end; crush.
177 Qed. 196 Qed.
178 End hlist. 197 End hlist.
179 198
180 Implicit Arguments hnil [A B]. 199 Implicit Arguments HNil [A B].
181 Implicit Arguments hcons [A B x ls]. 200 Implicit Arguments HCons [A B x ls].
182 Implicit Arguments hget [A B elm ls].
183 Implicit Arguments happ [A B ls1 ls2].
184 Implicit Arguments hmake [A B]. 201 Implicit Arguments hmake [A B].
185 202
186 Implicit Arguments hfirst [A elm x ls]. 203 Implicit Arguments HFirst [A elm ls].
187 Implicit Arguments hnext [A elm x ls]. 204 Implicit Arguments HNext [A elm x ls].
188 205
189 Infix ":::" := hcons (right associativity, at level 60). 206 Infix ":::" := HCons (right associativity, at level 60).
190 Infix "+++" := happ (right associativity, at level 60). 207 Infix "+++" := happ (right associativity, at level 60).
191 208
192 Section hmap. 209 Section hmap.
193 Variable A : Type. 210 Variable A : Type.
194 Variables B1 B2 : A -> Type. 211 Variables B1 B2 : A -> Type.
195 212
196 Variable f : forall x, B1 x -> B2 x. 213 Variable f : forall x, B1 x -> B2 x.
197 214
198 Fixpoint hmap (ls : list A) : hlist B1 ls -> hlist B2 ls := 215 Fixpoint hmap (ls : list A) (hl : hlist B1 ls) : hlist B2 ls :=
199 match ls return hlist B1 ls -> hlist B2 ls with 216 match hl with
200 | nil => fun _ => hnil 217 | HNil => HNil
201 | _ :: _ => fun hl => f (fst hl) ::: hmap _ (snd hl) 218 | HCons _ _ x hl' => f x ::: hmap hl'
202 end. 219 end.
203
204 Implicit Arguments hmap [ls].
205 220
206 Theorem hmap_happ : forall ls2 (h2 : hlist B1 ls2) ls1 (h1 : hlist B1 ls1), 221 Theorem hmap_happ : forall ls2 (h2 : hlist B1 ls2) ls1 (h1 : hlist B1 ls1),
207 hmap h1 +++ hmap h2 = hmap (h1 +++ h2). 222 hmap h1 +++ hmap h2 = hmap (h1 +++ h2).
208 induction ls1; crush. 223 induction h1; crush.
209 Qed. 224 Qed.
210 225
211 Theorem hget_hmap : forall elm ls (hls : hlist B1 ls) (m : member elm ls), 226 Theorem hget_hmap : forall elm ls (hls : hlist B1 ls) (m : member elm ls),
212 hget (hmap hls) m = f (hget hls m). 227 hget (hmap hls) m = f (hget hls m).
213 induction ls; crush. 228 induction hls; crush;
214 case a1; crush. 229 match goal with
230 | [ |- context[match ?E with HFirst _ => _ | HNext _ _ _ => _ end] ] => dep_destruct E
231 end; crush.
215 Qed. 232 Qed.
216 End hmap. 233 End hmap.
217 234
218 Implicit Arguments hmap [A B1 B2 ls]. 235 Implicit Arguments hmap [A B1 B2 ls].