Mercurial > cpdt > repo

comparison src/DataStruct.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents 559ec7328410
children d5787b70cf48
comparison
equal deleted inserted replaced
301:f4768d5a75eb 302:7b38729be069
134 134
135 Check Cons 0 (Cons 1 (Cons 2 Nil)). 135 Check Cons 0 (Cons 1 (Cons 2 Nil)).
136 (** %\vspace{-.15in}% [[ 136 (** %\vspace{-.15in}% [[
137 Cons 0 (Cons 1 (Cons 2 Nil)) 137 Cons 0 (Cons 1 (Cons 2 Nil))
138 : ilist nat 3 138 : ilist nat 3
139 ]] *) 139 ]]
140 *)
140 141
141 (* begin thide *) 142 (* begin thide *)
142 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) First. 143 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) First.
143 (** %\vspace{-.15in}% [[ 144 (** %\vspace{-.15in}% [[
144 = 0 145 = 0
145 : nat 146 : nat
146 ]] *) 147 ]]
148 *)
147 149
148 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next First). 150 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next First).
149 (** %\vspace{-.15in}% [[ 151 (** %\vspace{-.15in}% [[
150 = 1 152 = 1
151 : nat 153 : nat
152 ]] *) 154 ]]
155 *)
153 156
154 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next (Next First)). 157 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next (Next First)).
155 (** %\vspace{-.15in}% [[ 158 (** %\vspace{-.15in}% [[
156 = 2 159 = 2
157 : nat 160 : nat
158 ]] *) 161 ]]
162 *)
159 (* end thide *) 163 (* end thide *)
160 164
161 (** Our [get] function is also quite easy to reason about. We show how with a short example about an analogue to the list [map] function. *) 165 (** Our [get] function is also quite easy to reason about. We show how with a short example about an analogue to the list [map] function. *)
162 166
163 Section ilist_map. 167 Section ilist_map.
256 260
257 Eval simpl in hget someValues MFirst. 261 Eval simpl in hget someValues MFirst.
258 (** %\vspace{-.15in}% [[ 262 (** %\vspace{-.15in}% [[
259 = 5 263 = 5
260 : (fun T : Set => T) nat 264 : (fun T : Set => T) nat
261 ]] *) 265 ]]
266 *)
262 267
263 Eval simpl in hget someValues (MNext MFirst). 268 Eval simpl in hget someValues (MNext MFirst).
264 (** %\vspace{-.15in}% [[ 269 (** %\vspace{-.15in}% [[
265 = true 270 = true
266 : (fun T : Set => T) bool 271 : (fun T : Set => T) bool
267 ]] *) 272 ]]
273 *)
268 274
269 (** We can also build indexed lists of pairs in this way. *) 275 (** We can also build indexed lists of pairs in this way. *)
270 276
271 Example somePairs : hlist (fun T : Set => T * T)%type someTypes := 277 Example somePairs : hlist (fun T : Set => T * T)%type someTypes :=
272 MCons (1, 2) (MCons (true, false) MNil). 278 MCons (1, 2) (MCons (true, false) MNil).
322 328
323 Eval simpl in expDenote Const MNil. 329 Eval simpl in expDenote Const MNil.
324 (** %\vspace{-.15in}% [[ 330 (** %\vspace{-.15in}% [[
325 = tt 331 = tt
326 : typeDenote Unit 332 : typeDenote Unit
327 ]] *) 333 ]]
334 *)
328 335
329 Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) MNil. 336 Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) MNil.
330 (** %\vspace{-.15in}% [[ 337 (** %\vspace{-.15in}% [[
331 = fun x : unit => x 338 = fun x : unit => x
332 : typeDenote (Arrow Unit Unit) 339 : typeDenote (Arrow Unit Unit)
333 ]] *) 340 ]]
341 *)
334 342
335 Eval simpl in expDenote (Abs (dom := Unit) 343 Eval simpl in expDenote (Abs (dom := Unit)
336 (Abs (dom := Unit) (Var (MNext MFirst)))) MNil. 344 (Abs (dom := Unit) (Var (MNext MFirst)))) MNil.
337 (** %\vspace{-.15in}% [[ 345 (** %\vspace{-.15in}% [[
338 = fun x _ : unit => x 346 = fun x _ : unit => x
339 : typeDenote (Arrow Unit (Arrow Unit Unit)) 347 : typeDenote (Arrow Unit (Arrow Unit Unit))
340 ]] *) 348 ]]
349 *)
341 350
342 Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) MNil. 351 Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) MNil.
343 (** %\vspace{-.15in}% [[ 352 (** %\vspace{-.15in}% [[
344 = fun _ x0 : unit => x0 353 = fun _ x0 : unit => x0
345 : typeDenote (Arrow Unit (Arrow Unit Unit)) 354 : typeDenote (Arrow Unit (Arrow Unit Unit))
346 ]] *) 355 ]]
356 *)
347 357
348 Eval simpl in expDenote (App (Abs (Var MFirst)) Const) MNil. 358 Eval simpl in expDenote (App (Abs (Var MFirst)) Const) MNil.
349 (** %\vspace{-.15in}% [[ 359 (** %\vspace{-.15in}% [[
350 = tt 360 = tt
351 : typeDenote Unit 361 : typeDenote Unit
352 ]] *) 362 ]]
363 *)
353 364
354 (* end thide *) 365 (* end thide *)
355 366
356 (** We are starting to develop the tools behind dependent typing's amazing advantage over alternative approaches in several important areas. Here, we have implemented complete syntax, typing rules, and evaluation semantics for simply-typed lambda calculus without even needing to define a syntactic substitution operation. We did it all without a single line of proof, and our implementation is manifestly executable. In a later chapter, we will meet other, more common approaches to language formalization. Such approaches often state and prove explicit theorems about type safety of languages. In the above example, we got type safety, termination, and other meta-theorems for free, by reduction to CIC, which we know has those properties. *) 367 (** We are starting to develop the tools behind dependent typing's amazing advantage over alternative approaches in several important areas. Here, we have implemented complete syntax, typing rules, and evaluation semantics for simply-typed lambda calculus without even needing to define a syntactic substitution operation. We did it all without a single line of proof, and our implementation is manifestly executable. In a later chapter, we will meet other, more common approaches to language formalization. Such approaches often state and prove explicit theorems about type safety of languages. In the above example, we got type safety, termination, and other meta-theorems for free, by reduction to CIC, which we know has those properties. *)
357 368