Mercurial > cpdt > repo

comparison src/MoreDep.v @ 443:97c60ffdb998

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Vertical spacing pass for MoreDep and DataStruct
author Adam Chlipala <adam@chlipala.net>
date Wed, 01 Aug 2012 16:32:04 -0400
parents 8077352044b2
children 2740b8a23cce
comparison
equal deleted inserted replaced
442:89c67796754e 443:97c60ffdb998
85 (* end thide *) 85 (* end thide *)
86 86
87 (* EX: Implement statically checked "car"/"hd" *) 87 (* EX: Implement statically checked "car"/"hd" *)
88 88
89 (** Now let us attempt a function that is surprisingly tricky to write. In ML, the list head function raises an exception when passed an empty list. With length-indexed lists, we can rule out such invalid calls statically, and here is a first attempt at doing so. We write [???] as a placeholder for a term that we do not know how to write, not for any real Coq notation like those introduced two chapters ago. 89 (** Now let us attempt a function that is surprisingly tricky to write. In ML, the list head function raises an exception when passed an empty list. With length-indexed lists, we can rule out such invalid calls statically, and here is a first attempt at doing so. We write [???] as a placeholder for a term that we do not know how to write, not for any real Coq notation like those introduced two chapters ago.
90
91 [[ 90 [[
92 Definition hd n (ls : ilist (S n)) : A := 91 Definition hd n (ls : ilist (S n)) : A :=
93 match ls with 92 match ls with
94 | Nil => ??? 93 | Nil => ???
95 | Cons _ h _ => h 94 | Cons _ h _ => h
96 end. 95 end.
97
98 ]] 96 ]]
99
100 It is not clear what to write for the [Nil] case, so we are stuck before we even turn our function over to the type checker. We could try omitting the [Nil] case: 97 It is not clear what to write for the [Nil] case, so we are stuck before we even turn our function over to the type checker. We could try omitting the [Nil] case:
101
102 [[ 98 [[
103 Definition hd n (ls : ilist (S n)) : A := 99 Definition hd n (ls : ilist (S n)) : A :=
104 match ls with 100 match ls with
105 | Cons _ h _ => h 101 | Cons _ h _ => h
106 end. 102 end.
139 hd' 135 hd'
140 : forall n : nat, ilist n -> match n with 136 : forall n : nat, ilist n -> match n with
141 | 0 => unit 137 | 0 => unit
142 | S _ => A 138 | S _ => A
143 end 139 end
144
145 ]] 140 ]]
146 *) 141 *)
147 142
148 Definition hd n (ls : ilist (S n)) : A := hd' ls. 143 Definition hd n (ls : ilist (S n)) : A := hd' ls.
149 (* end thide *) 144 (* end thide *)
241 (* end hide *) 236 (* end hide *)
242 237
243 (** Despite the fancy type, the function definition is routine. In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype. The only unusual thing is the use of an expression of the form [if E then true else false] in the [Eq] case. Remember that [eq_nat_dec] has a rich dependent type, rather than a simple boolean type. Coq's native [if] is overloaded to work on a test of any two-constructor type, so we can use [if] to build a simple boolean from the [sumbool] that [eq_nat_dec] returns. 238 (** Despite the fancy type, the function definition is routine. In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype. The only unusual thing is the use of an expression of the form [if E then true else false] in the [Eq] case. Remember that [eq_nat_dec] has a rich dependent type, rather than a simple boolean type. Coq's native [if] is overloaded to work on a test of any two-constructor type, so we can use [if] to build a simple boolean from the [sumbool] that [eq_nat_dec] returns.
244 239
245 We can implement our old favorite, a constant folding function, and prove it correct. It will be useful to write a function [pairOut] that checks if an [exp] of [Prod] type is a pair, returning its two components if so. Unsurprisingly, a first attempt leads to a type error. 240 We can implement our old favorite, a constant folding function, and prove it correct. It will be useful to write a function [pairOut] that checks if an [exp] of [Prod] type is a pair, returning its two components if so. Unsurprisingly, a first attempt leads to a type error.
246
247 [[ 241 [[
248 Definition pairOut t1 t2 (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) := 242 Definition pairOut t1 t2 (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) :=
249 match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with 243 match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with
250 | Pair _ _ e1 e2 => Some (e1, e2) 244 | Pair _ _ e1 e2 => Some (e1, e2)
251 | _ => None 245 | _ => None
372 end 366 end
373 367
374 ]] 368 ]]
375 369
376 We would like to do a case analysis on [cfold e1], and we attempt that in the way that has worked so far. 370 We would like to do a case analysis on [cfold e1], and we attempt that in the way that has worked so far.
377
378 [[ 371 [[
379 destruct (cfold e1). 372 destruct (cfold e1).
380 ]] 373 ]]
381 374
382 << 375 <<
535 End present. 528 End present.
536 529
537 (** Insertion relies on two balancing operations. It will be useful to give types to these operations using a relative of the subset types from last chapter. While subset types let us pair a value with a proof about that value, here we want to pair a value with another non-proof dependently typed value. The %\index{Gallina terms!sigT}%[sigT] type fills this role. *) 530 (** Insertion relies on two balancing operations. It will be useful to give types to these operations using a relative of the subset types from last chapter. While subset types let us pair a value with a proof about that value, here we want to pair a value with another non-proof dependently typed value. The %\index{Gallina terms!sigT}%[sigT] type fills this role. *)
538 531
539 Locate "{ _ : _ & _ }". 532 Locate "{ _ : _ & _ }".
540 (** [[ 533 (** %\vspace{-.15in}%[[
541 Notation Scope 534 Notation Scope
542 "{ x : A & P }" := sigT (fun x : A => P) 535 "{ x : A & P }" := sigT (fun x : A => P)
543 ]] 536 ]]
544 *) 537 *)
545 538
546 Print sigT. 539 Print sigT.
547 (** [[ 540 (** %\vspace{-.15in}%[[
548 Inductive sigT (A : Type) (P : A -> Type) : Type := 541 Inductive sigT (A : Type) (P : A -> Type) : Type :=
549 existT : forall x : A, P x -> sigT P 542 existT : forall x : A, P x -> sigT P
550 ]] 543 ]]
551 *) 544 *)
552 545