Mercurial > cpdt > repo

annotate src/MoreDep.v @ 367:b809d3a8a5b1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass over old Large material; index fixes
author Adam Chlipala <adam@chlipala.net>
date Tue, 08 Nov 2011 11:54:09 -0500
parents ad315efc3b6b
children 549d604c3d16
rev   line source
adam@297 1 (* Copyright (c) 2008-2011, Adam Chlipala
adamc@83 2 *
adamc@83 3 * This work is licensed under a
adamc@83 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@83 5 * Unported License.
adamc@83 6 * The license text is available at:
adamc@83 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@83 8 *)
adamc@83 9
adamc@83 10 (* begin hide *)
adamc@85 11 Require Import Arith Bool List.
adamc@83 12
adam@314 13 Require Import CpdtTactics MoreSpecif.
adamc@83 14
adamc@83 15 Set Implicit Arguments.
adamc@83 16 (* end hide *)
adamc@83 17
adamc@83 18
adamc@83 19 (** %\chapter{More Dependent Types}% *)
adamc@83 20
adam@292 21 (** Subset types and their relatives help us integrate verification with programming. Though they reorganize the certified programmer's workflow, they tend not to have deep effects on proofs. We write largely the same proofs as we would for classical verification, with some of the structure moved into the programs themselves. It turns out that, when we use dependent types to their full potential, we warp the development and proving process even more than that, picking up %``%#"#free theorems#"#%''% to the extent that often a certified program is hardly more complex than its uncertified counterpart in Haskell or ML.
adamc@83 22
adam@338 23 In particular, we have only scratched the tip of the iceberg that is Coq's inductive definition mechanism. The inductive types we have seen so far have their counterparts in the other proof assistants that we surveyed in Chapter 1. This chapter explores the strange new world of dependent inductive datatypes (that is, dependent inductive types outside [Prop]), a possibility that sets Coq apart from all of the competition not based on type theory. *)
adamc@83 24
adamc@84 25
adamc@84 26 (** * Length-Indexed Lists *)
adamc@84 27
adam@338 28 (** Many introductions to dependent types start out by showing how to use them to eliminate array bounds checks%\index{array bounds checks}%. When the type of an array tells you how many elements it has, your compiler can detect out-of-bounds dereferences statically. Since we are working in a pure functional language, the next best thing is length-indexed lists%\index{length-indexed lists}%, which the following code defines. *)
adamc@84 29
adamc@84 30 Section ilist.
adamc@84 31 Variable A : Set.
adamc@84 32
adamc@84 33 Inductive ilist : nat -> Set :=
adamc@84 34 | Nil : ilist O
adamc@84 35 | Cons : forall n, A -> ilist n -> ilist (S n).
adamc@84 36
adamc@84 37 (** We see that, within its section, [ilist] is given type [nat -> Set]. Previously, every inductive type we have seen has either had plain [Set] as its type or has been a predicate with some type ending in [Prop]. The full generality of inductive definitions lets us integrate the expressivity of predicates directly into our normal programming.
adamc@84 38
adam@338 39 The [nat] argument to [ilist] tells us the length of the list. The types of [ilist]'s constructors tell us that a [Nil] list has length [O] and that a [Cons] list has length one greater than the length of its tail. We may apply [ilist] to any natural number, even natural numbers that are only known at runtime. It is this breaking of the %\index{phase distinction}\textit{%#<i>#phase distinction#</i>#%}% that characterizes [ilist] as %\textit{%#<i>#dependently typed#</i>#%}%.
adamc@84 40
adamc@213 41 In expositions of list types, we usually see the length function defined first, but here that would not be a very productive function to code. Instead, let us implement list concatenation. *)
adamc@84 42
adamc@213 43 Fixpoint app n1 (ls1 : ilist n1) n2 (ls2 : ilist n2) : ilist (n1 + n2) :=
adamc@213 44 match ls1 with
adamc@213 45 | Nil => ls2
adamc@213 46 | Cons _ x ls1' => Cons x (app ls1' ls2)
adamc@213 47 end.
adamc@84 48
adam@338 49 (** Past Coq versions signalled an error for this definition. The code is still invalid within Coq's core language, but current Coq versions automatically add annotations to the original program, producing a valid core program. These are the annotations on [match] discriminees that we began to study in the previous chapter. We can rewrite [app] to give the annotations explicitly. *)
adamc@100 50
adamc@100 51 (* begin thide *)
adam@338 52 Fixpoint app' n1 (ls1 : ilist n1) n2 (ls2 : ilist n2) : ilist (n1 + n2) :=
adam@338 53 match ls1 in (ilist n1) return (ilist (n1 + n2)) with
adam@338 54 | Nil => ls2
adam@338 55 | Cons _ x ls1' => Cons x (app' ls1' ls2)
adam@338 56 end.
adamc@100 57 (* end thide *)
adamc@84 58
adam@338 59 (** Using [return] alone allowed us to express a dependency of the [match] result type on the %\textit{%#<i>#value#</i>#%}% of the discriminee. What %\index{Gallina terms!in}%[in] adds to our arsenal is a way of expressing a dependency on the %\textit{%#<i>#type#</i>#%}% of the discriminee. Specifically, the [n1] in the [in] clause above is a %\textit{%#<i>#binding occurrence#</i>#%}% whose scope is the [return] clause.
adamc@84 60
adamc@84 61 We may use [in] clauses only to bind names for the arguments of an inductive type family. That is, each [in] clause must be an inductive type family name applied to a sequence of underscores and variable names of the proper length. The positions for %\textit{%#<i>#parameters#</i>#%}% to the type family must all be underscores. Parameters are those arguments declared with section variables or with entries to the left of the first colon in an inductive definition. They cannot vary depending on which constructor was used to build the discriminee, so Coq prohibits pointless matches on them. It is those arguments defined in the type to the right of the colon that we may name with [in] clauses.
adamc@84 62
adam@338 63 Our [app] function could be typed in so-called %\index{stratified type systems}\textit{%#<i>#stratified#</i>#%}% type systems, which avoid true dependency. That is, we could consider the length indices to lists to live in a separate, compile-time-only universe from the lists themselves. This stratification between a compile-time universe and a run-time universe, with no references to the latter in the former, gives rise to the terminology %``%#"#stratified.#"#%''% Our next example would be harder to implement in a stratified system. We write an injection function from regular lists to length-indexed lists. A stratified implementation would need to duplicate the definition of lists across compile-time and run-time versions, and the run-time versions would need to be indexed by the compile-time versions. *)
adamc@84 64
adamc@100 65 (* EX: Implement injection from normal lists *)
adamc@100 66
adamc@100 67 (* begin thide *)
adamc@84 68 Fixpoint inject (ls : list A) : ilist (length ls) :=
adamc@213 69 match ls with
adamc@84 70 | nil => Nil
adamc@84 71 | h :: t => Cons h (inject t)
adamc@84 72 end.
adamc@84 73
adamc@84 74 (** We can define an inverse conversion and prove that it really is an inverse. *)
adamc@84 75
adamc@213 76 Fixpoint unject n (ls : ilist n) : list A :=
adamc@84 77 match ls with
adamc@84 78 | Nil => nil
adamc@84 79 | Cons _ h t => h :: unject t
adamc@84 80 end.
adamc@84 81
adamc@84 82 Theorem inject_inverse : forall ls, unject (inject ls) = ls.
adamc@84 83 induction ls; crush.
adamc@84 84 Qed.
adamc@100 85 (* end thide *)
adamc@100 86
adam@338 87 (* EX: Implement statically checked "car"/"hd" *)
adamc@84 88
adam@283 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 in the previous chapter.
adamc@84 90
adamc@84 91 [[
adamc@84 92 Definition hd n (ls : ilist (S n)) : A :=
adamc@84 93 match ls with
adamc@84 94 | Nil => ???
adamc@84 95 | Cons _ h _ => h
adamc@84 96 end.
adamc@213 97
adamc@213 98 ]]
adamc@84 99
adamc@84 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:
adamc@84 101
adamc@84 102 [[
adamc@84 103 Definition hd n (ls : ilist (S n)) : A :=
adamc@84 104 match ls with
adamc@84 105 | Cons _ h _ => h
adamc@84 106 end.
adam@338 107 ]]
adamc@84 108
adam@338 109 <<
adamc@84 110 Error: Non exhaustive pattern-matching: no clause found for pattern Nil
adam@338 111 >>
adamc@84 112
adam@275 113 Unlike in ML, we cannot use inexhaustive pattern matching, because there is no conception of a %\texttt{%#<tt>#Match#</tt>#%}% exception to be thrown. In fact, recent versions of Coq %\textit{%#<i>#do#</i>#%}% allow this, by implicit translation to a [match] that considers all constructors. It is educational to discover that encoding ourselves directly. We might try using an [in] clause somehow.
adamc@84 114
adamc@84 115 [[
adamc@84 116 Definition hd n (ls : ilist (S n)) : A :=
adamc@84 117 match ls in (ilist (S n)) with
adamc@84 118 | Cons _ h _ => h
adamc@84 119 end.
adamc@84 120 ]]
adamc@84 121
adam@338 122 <<
adam@338 123 Error: The reference n was not found in the current environment
adam@338 124 >>
adam@338 125
adam@338 126 In this and other cases, we feel like we want [in] clauses with type family arguments that are not variables. Unfortunately, Coq only supports variables in those positions. A completely general mechanism could only be supported with a solution to the problem of higher-order unification%~\cite{HOU}%, which is undecidable. There %\textit{%#<i>#are#</i>#%}% useful heuristics for handling non-variable indices which are gradually making their way into Coq, but we will spend some time in this and the next few chapters on effective pattern matching on dependent types using only the primitive [match] annotations.
adamc@84 127
adamc@84 128 Our final, working attempt at [hd] uses an auxiliary function and a surprising [return] annotation. *)
adamc@84 129
adamc@100 130 (* begin thide *)
adamc@84 131 Definition hd' n (ls : ilist n) :=
adamc@84 132 match ls in (ilist n) return (match n with O => unit | S _ => A end) with
adamc@84 133 | Nil => tt
adamc@84 134 | Cons _ h _ => h
adamc@84 135 end.
adamc@84 136
adam@283 137 Check hd'.
adam@283 138 (** %\vspace{-.15in}% [[
adam@283 139 hd'
adam@283 140 : forall n : nat, ilist n -> match n with
adam@283 141 | 0 => unit
adam@283 142 | S _ => A
adam@283 143 end
adam@283 144
adam@302 145 ]]
adam@302 146 *)
adam@283 147
adamc@84 148 Definition hd n (ls : ilist (S n)) : A := hd' ls.
adamc@100 149 (* end thide *)
adamc@84 150
adam@338 151 End ilist.
adam@338 152
adamc@84 153 (** We annotate our main [match] with a type that is itself a [match]. We write that the function [hd'] returns [unit] when the list is empty and returns the carried type [A] in all other cases. In the definition of [hd], we just call [hd']. Because the index of [ls] is known to be nonzero, the type checker reduces the [match] in the type of [hd'] to [A]. *)
adamc@84 154
adamc@85 155
adamc@85 156 (** * A Tagless Interpreter *)
adamc@85 157
adam@338 158 (** A favorite example for motivating the power of functional programming is implementation of a simple expression language interpreter. In ML and Haskell, such interpreters are often implemented using an algebraic datatype of values, where at many points it is checked that a value was built with the right constructor of the value type. With dependent types, we can implement a %\index{tagless interpreters}\textit{%#<i>#tagless#</i>#%}% interpreter that both removes this source of runtime inefficiency and gives us more confidence that our implementation is correct. *)
adamc@85 159
adamc@85 160 Inductive type : Set :=
adamc@85 161 | Nat : type
adamc@85 162 | Bool : type
adamc@85 163 | Prod : type -> type -> type.
adamc@85 164
adamc@85 165 Inductive exp : type -> Set :=
adamc@85 166 | NConst : nat -> exp Nat
adamc@85 167 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@85 168 | Eq : exp Nat -> exp Nat -> exp Bool
adamc@85 169
adamc@85 170 | BConst : bool -> exp Bool
adamc@85 171 | And : exp Bool -> exp Bool -> exp Bool
adamc@85 172 | If : forall t, exp Bool -> exp t -> exp t -> exp t
adamc@85 173
adamc@85 174 | Pair : forall t1 t2, exp t1 -> exp t2 -> exp (Prod t1 t2)
adamc@85 175 | Fst : forall t1 t2, exp (Prod t1 t2) -> exp t1
adamc@85 176 | Snd : forall t1 t2, exp (Prod t1 t2) -> exp t2.
adamc@85 177
adamc@85 178 (** We have a standard algebraic datatype [type], defining a type language of naturals, booleans, and product (pair) types. Then we have the indexed inductive type [exp], where the argument to [exp] tells us the encoded type of an expression. In effect, we are defining the typing rules for expressions simultaneously with the syntax.
adamc@85 179
adamc@85 180 We can give types and expressions semantics in a new style, based critically on the chance for %\textit{%#<i>#type-level computation#</i>#%}%. *)
adamc@85 181
adamc@85 182 Fixpoint typeDenote (t : type) : Set :=
adamc@85 183 match t with
adamc@85 184 | Nat => nat
adamc@85 185 | Bool => bool
adamc@85 186 | Prod t1 t2 => typeDenote t1 * typeDenote t2
adamc@85 187 end%type.
adamc@85 188
adam@338 189 (** The [typeDenote] function compiles types of our object language into %``%#"#native#"#%''% Coq types. It is deceptively easy to implement. The only new thing we see is the [%][type] annotation, which tells Coq to parse the [match] expression using the notations associated with types. Without this annotation, the [*] would be interpreted as multiplication on naturals, rather than as the product type constructor. The token [type] is one example of an identifer bound to a %\textit{%#<i>#notation scope#</i>#%}%. In this book, we will not go into more detail on notation scopes, but the Coq manual can be consulted for more information.
adamc@85 190
adamc@85 191 We can define a function [expDenote] that is typed in terms of [typeDenote]. *)
adamc@85 192
adamc@213 193 Fixpoint expDenote t (e : exp t) : typeDenote t :=
adamc@213 194 match e with
adamc@85 195 | NConst n => n
adamc@85 196 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@85 197 | Eq e1 e2 => if eq_nat_dec (expDenote e1) (expDenote e2) then true else false
adamc@85 198
adamc@85 199 | BConst b => b
adamc@85 200 | And e1 e2 => expDenote e1 && expDenote e2
adamc@85 201 | If _ e' e1 e2 => if expDenote e' then expDenote e1 else expDenote e2
adamc@85 202
adamc@85 203 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@85 204 | Fst _ _ e' => fst (expDenote e')
adamc@85 205 | Snd _ _ e' => snd (expDenote e')
adamc@85 206 end.
adamc@85 207
adamc@213 208 (** 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.
adamc@85 209
adamc@85 210 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.
adamc@85 211
adamc@85 212 [[
adamc@85 213 Definition pairOut t1 t2 (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) :=
adamc@85 214 match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with
adamc@85 215 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@85 216 | _ => None
adamc@85 217 end.
adam@338 218 ]]
adamc@85 219
adam@338 220 <<
adamc@85 221 Error: The reference t2 was not found in the current environment
adam@338 222 >>
adamc@85 223
adamc@85 224 We run again into the problem of not being able to specify non-variable arguments in [in] clauses. The problem would just be hopeless without a use of an [in] clause, though, since the result type of the [match] depends on an argument to [exp]. Our solution will be to use a more general type, as we did for [hd]. First, we define a type-valued function to use in assigning a type to [pairOut]. *)
adamc@85 225
adamc@100 226 (* EX: Define a function [pairOut : forall t1 t2, exp (Prod t1 t2) -> option (exp t1 * exp t2)] *)
adamc@100 227
adamc@100 228 (* begin thide *)
adamc@85 229 Definition pairOutType (t : type) :=
adamc@85 230 match t with
adamc@85 231 | Prod t1 t2 => option (exp t1 * exp t2)
adamc@85 232 | _ => unit
adamc@85 233 end.
adamc@85 234
adamc@85 235 (** When passed a type that is a product, [pairOutType] returns our final desired type. On any other input type, [pairOutType] returns [unit], since we do not care about extracting components of non-pairs. Now we can write another helper function to provide the default behavior of [pairOut], which we will apply for inputs that are not literal pairs. *)
adamc@85 236
adamc@85 237 Definition pairOutDefault (t : type) :=
adamc@85 238 match t return (pairOutType t) with
adamc@85 239 | Prod _ _ => None
adamc@85 240 | _ => tt
adamc@85 241 end.
adamc@85 242
adamc@85 243 (** Now [pairOut] is deceptively easy to write. *)
adamc@85 244
adamc@85 245 Definition pairOut t (e : exp t) :=
adamc@85 246 match e in (exp t) return (pairOutType t) with
adamc@85 247 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@85 248 | _ => pairOutDefault _
adamc@85 249 end.
adamc@100 250 (* end thide *)
adamc@85 251
adam@338 252 (** There is one important subtlety in this definition. Coq allows us to use convenient ML-style pattern matching notation, but, internally and in proofs, we see that patterns are expanded out completely, matching one level of inductive structure at a time. Thus, the default case in the [match] above expands out to one case for each constructor of [exp] besides [Pair], and the underscore in [pairOutDefault _] is resolved differently in each case. From an ML or Haskell programmer's perspective, what we have here is type inference determining which code is run (returning either [None] or [tt]), which goes beyond what is possible with type inference guiding parametric polymorphism in Hindley-Milner languages%\index{Hindley-Milner}%, but is similar to what goes on with Haskell type classes%\index{type classes}%.
adamc@85 253
adamc@213 254 With [pairOut] available, we can write [cfold] in a straightforward way. There are really no surprises beyond that Coq verifies that this code has such an expressive type, given the small annotation burden. In some places, we see that Coq's [match] annotation inference is too smart for its own good, and we have to turn that inference off by writing [return _]. *)
adamc@85 255
adamc@204 256 Fixpoint cfold t (e : exp t) : exp t :=
adamc@204 257 match e with
adamc@85 258 | NConst n => NConst n
adamc@85 259 | Plus e1 e2 =>
adamc@85 260 let e1' := cfold e1 in
adamc@85 261 let e2' := cfold e2 in
adamc@204 262 match e1', e2' return _ with
adamc@85 263 | NConst n1, NConst n2 => NConst (n1 + n2)
adamc@85 264 | _, _ => Plus e1' e2'
adamc@85 265 end
adamc@85 266 | Eq e1 e2 =>
adamc@85 267 let e1' := cfold e1 in
adamc@85 268 let e2' := cfold e2 in
adamc@204 269 match e1', e2' return _ with
adamc@85 270 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
adamc@85 271 | _, _ => Eq e1' e2'
adamc@85 272 end
adamc@85 273
adamc@85 274 | BConst b => BConst b
adamc@85 275 | And e1 e2 =>
adamc@85 276 let e1' := cfold e1 in
adamc@85 277 let e2' := cfold e2 in
adamc@204 278 match e1', e2' return _ with
adamc@85 279 | BConst b1, BConst b2 => BConst (b1 && b2)
adamc@85 280 | _, _ => And e1' e2'
adamc@85 281 end
adamc@85 282 | If _ e e1 e2 =>
adamc@85 283 let e' := cfold e in
adamc@85 284 match e' with
adamc@85 285 | BConst true => cfold e1
adamc@85 286 | BConst false => cfold e2
adamc@85 287 | _ => If e' (cfold e1) (cfold e2)
adamc@85 288 end
adamc@85 289
adamc@85 290 | Pair _ _ e1 e2 => Pair (cfold e1) (cfold e2)
adamc@85 291 | Fst _ _ e =>
adamc@85 292 let e' := cfold e in
adamc@85 293 match pairOut e' with
adamc@85 294 | Some p => fst p
adamc@85 295 | None => Fst e'
adamc@85 296 end
adamc@85 297 | Snd _ _ e =>
adamc@85 298 let e' := cfold e in
adamc@85 299 match pairOut e' with
adamc@85 300 | Some p => snd p
adamc@85 301 | None => Snd e'
adamc@85 302 end
adamc@85 303 end.
adamc@85 304
adamc@85 305 (** The correctness theorem for [cfold] turns out to be easy to prove, once we get over one serious hurdle. *)
adamc@85 306
adamc@85 307 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
adamc@100 308 (* begin thide *)
adamc@85 309 induction e; crush.
adamc@85 310
adamc@85 311 (** The first remaining subgoal is:
adamc@85 312
adamc@85 313 [[
adamc@85 314 expDenote (cfold e1) + expDenote (cfold e2) =
adamc@85 315 expDenote
adamc@85 316 match cfold e1 with
adamc@85 317 | NConst n1 =>
adamc@85 318 match cfold e2 with
adamc@85 319 | NConst n2 => NConst (n1 + n2)
adamc@85 320 | Plus _ _ => Plus (cfold e1) (cfold e2)
adamc@85 321 | Eq _ _ => Plus (cfold e1) (cfold e2)
adamc@85 322 | BConst _ => Plus (cfold e1) (cfold e2)
adamc@85 323 | And _ _ => Plus (cfold e1) (cfold e2)
adamc@85 324 | If _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 325 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 326 | Fst _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 327 | Snd _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 328 end
adamc@85 329 | Plus _ _ => Plus (cfold e1) (cfold e2)
adamc@85 330 | Eq _ _ => Plus (cfold e1) (cfold e2)
adamc@85 331 | BConst _ => Plus (cfold e1) (cfold e2)
adamc@85 332 | And _ _ => Plus (cfold e1) (cfold e2)
adamc@85 333 | If _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 334 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 335 | Fst _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 336 | Snd _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 337 end
adamc@213 338
adamc@85 339 ]]
adamc@85 340
adamc@85 341 We would like to do a case analysis on [cfold e1], and we attempt that in the way that has worked so far.
adamc@85 342
adamc@85 343 [[
adamc@85 344 destruct (cfold e1).
adam@338 345 ]]
adamc@85 346
adam@338 347 <<
adamc@85 348 User error: e1 is used in hypothesis e
adam@338 349 >>
adamc@85 350
adamc@85 351 Coq gives us another cryptic error message. Like so many others, this one basically means that Coq is not able to build some proof about dependent types. It is hard to generate helpful and specific error messages for problems like this, since that would require some kind of understanding of the dependency structure of a piece of code. We will encounter many examples of case-specific tricks for recovering from errors like this one.
adamc@85 352
adam@350 353 For our current proof, we can use a tactic [dep_destruct]%\index{tactics!dep\_destruct}% defined in the book [CpdtTactics] module. General elimination/inversion of dependently typed hypotheses is undecidable, since it must be implemented with [match] expressions that have the restriction on [in] clauses that we have already discussed. The tactic [dep_destruct] makes a best effort to handle some common cases, relying upon the more primitive %\index{tactics!dependent destruction}%[dependent destruction] tactic that comes with Coq. In a future chapter, we will learn about the explicit manipulation of equality proofs that is behind [dep_destruct]'s implementation in Ltac, but for now, we treat it as a useful black box. (In Chapter 12, we will also see how [dependent destruction] forces us to make a larger philosophical commitment about our logic than we might like, and we will see some workarounds.) *)
adamc@85 354
adamc@85 355 dep_destruct (cfold e1).
adamc@85 356
adamc@85 357 (** This successfully breaks the subgoal into 5 new subgoals, one for each constructor of [exp] that could produce an [exp Nat]. Note that [dep_destruct] is successful in ruling out the other cases automatically, in effect automating some of the work that we have done manually in implementing functions like [hd] and [pairOut].
adamc@85 358
adamc@213 359 This is the only new trick we need to learn to complete the proof. We can back up and give a short, automated proof. The main inconvenience in the proof is that we cannot write a pattern that matches a [match] without including a case for every constructor of the inductive type we match over. *)
adamc@85 360
adamc@85 361 Restart.
adamc@85 362
adamc@85 363 induction e; crush;
adamc@85 364 repeat (match goal with
adamc@213 365 | [ |- context[match cfold ?E with NConst _ => _ | Plus _ _ => _
adamc@213 366 | Eq _ _ => _ | BConst _ => _ | And _ _ => _
adamc@213 367 | If _ _ _ _ => _ | Pair _ _ _ _ => _
adamc@213 368 | Fst _ _ _ => _ | Snd _ _ _ => _ end] ] =>
adamc@213 369 dep_destruct (cfold E)
adamc@213 370 | [ |- context[match pairOut (cfold ?E) with Some _ => _
adamc@213 371 | None => _ end] ] =>
adamc@213 372 dep_destruct (cfold E)
adamc@85 373 | [ |- (if ?E then _ else _) = _ ] => destruct E
adamc@85 374 end; crush).
adamc@85 375 Qed.
adamc@100 376 (* end thide *)
adamc@86 377
adamc@86 378
adam@338 379 (** * Dependently Typed Red-Black Trees *)
adamc@94 380
adam@338 381 (** Red-black trees are a favorite purely functional data structure with an interesting invariant. We can use dependent types to enforce that operations on red-black trees preserve the invariant. For simplicity, we specialize our red-black trees to represent sets of [nat]s. *)
adamc@100 382
adamc@94 383 Inductive color : Set := Red | Black.
adamc@94 384
adamc@94 385 Inductive rbtree : color -> nat -> Set :=
adamc@94 386 | Leaf : rbtree Black 0
adamc@214 387 | RedNode : forall n, rbtree Black n -> nat -> rbtree Black n -> rbtree Red n
adamc@94 388 | BlackNode : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rbtree Black (S n).
adamc@94 389
adamc@214 390 (** A value of type [rbtree c d] is a red-black tree node whose root has color [c] and that has black depth [d]. The latter property means that there are no more than [d] black-colored nodes on any path from the root to a leaf. *)
adamc@214 391
adamc@214 392 (** At first, it can be unclear that this choice of type indices tracks any useful property. To convince ourselves, we will prove that every red-black tree is balanced. We will phrase our theorem in terms of a depth calculating function that ignores the extra information in the types. It will be useful to parameterize this function over a combining operation, so that we can re-use the same code to calculate the minimum or maximum height among all paths from root to leaf. *)
adamc@214 393
adamc@100 394 (* EX: Prove that every [rbtree] is balanced. *)
adamc@100 395
adamc@100 396 (* begin thide *)
adamc@95 397 Require Import Max Min.
adamc@95 398
adamc@95 399 Section depth.
adamc@95 400 Variable f : nat -> nat -> nat.
adamc@95 401
adamc@214 402 Fixpoint depth c n (t : rbtree c n) : nat :=
adamc@95 403 match t with
adamc@95 404 | Leaf => 0
adamc@95 405 | RedNode _ t1 _ t2 => S (f (depth t1) (depth t2))
adamc@95 406 | BlackNode _ _ _ t1 _ t2 => S (f (depth t1) (depth t2))
adamc@95 407 end.
adamc@95 408 End depth.
adamc@95 409
adam@338 410 (** Our proof of balanced-ness decomposes naturally into a lower bound and an upper bound. We prove the lower bound first. Unsurprisingly, a tree's black depth provides such a bound on the minimum path length. We use the richly typed procedure [min_dec] to do case analysis on whether [min X Y] equals [X] or [Y]. *)
adamc@214 411
adam@283 412 Check min_dec.
adam@283 413 (** %\vspace{-.15in}% [[
adam@283 414 min_dec
adam@283 415 : forall n m : nat, {min n m = n} + {min n m = m}
adam@302 416 ]]
adam@302 417 *)
adam@283 418
adamc@95 419 Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n.
adamc@95 420 induction t; crush;
adamc@95 421 match goal with
adamc@95 422 | [ |- context[min ?X ?Y] ] => destruct (min_dec X Y)
adamc@95 423 end; crush.
adamc@95 424 Qed.
adamc@95 425
adamc@214 426 (** There is an analogous upper-bound theorem based on black depth. Unfortunately, a symmetric proof script does not suffice to establish it. *)
adamc@214 427
adamc@214 428 Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
adamc@214 429 induction t; crush;
adamc@214 430 match goal with
adamc@214 431 | [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
adamc@214 432 end; crush.
adamc@214 433
adamc@214 434 (** Two subgoals remain. One of them is: [[
adamc@214 435 n : nat
adamc@214 436 t1 : rbtree Black n
adamc@214 437 n0 : nat
adamc@214 438 t2 : rbtree Black n
adamc@214 439 IHt1 : depth max t1 <= n + (n + 0) + 1
adamc@214 440 IHt2 : depth max t2 <= n + (n + 0) + 1
adamc@214 441 e : max (depth max t1) (depth max t2) = depth max t1
adamc@214 442 ============================
adamc@214 443 S (depth max t1) <= n + (n + 0) + 1
adamc@214 444
adamc@214 445 ]]
adamc@214 446
adamc@214 447 We see that [IHt1] is %\textit{%#<i>#almost#</i>#%}% the fact we need, but it is not quite strong enough. We will need to strengthen our induction hypothesis to get the proof to go through. *)
adamc@214 448
adamc@214 449 Abort.
adamc@214 450
adamc@214 451 (** In particular, we prove a lemma that provides a stronger upper bound for trees with black root nodes. We got stuck above in a case about a red root node. Since red nodes have only black children, our IH strengthening will enable us to finish the proof. *)
adamc@214 452
adamc@95 453 Lemma depth_max' : forall c n (t : rbtree c n), match c with
adamc@95 454 | Red => depth max t <= 2 * n + 1
adamc@95 455 | Black => depth max t <= 2 * n
adamc@95 456 end.
adamc@95 457 induction t; crush;
adamc@95 458 match goal with
adamc@95 459 | [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
adamc@100 460 end; crush;
adamc@100 461 repeat (match goal with
adamc@214 462 | [ H : context[match ?C with Red => _ | Black => _ end] |- _ ] =>
adamc@214 463 destruct C
adamc@100 464 end; crush).
adamc@95 465 Qed.
adamc@95 466
adam@338 467 (** The original theorem follows easily from the lemma. We use the tactic %\index{tactics!generalize}%[generalize pf], which, when [pf] proves the proposition [P], changes the goal from [Q] to [P -> Q]. This transformation is useful because it makes the truth of [P] manifest syntactically, so that automation machinery can rely on [P], even if that machinery is not smart enough to establish [P] on its own. *)
adamc@214 468
adamc@95 469 Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
adamc@95 470 intros; generalize (depth_max' t); destruct c; crush.
adamc@95 471 Qed.
adamc@95 472
adamc@214 473 (** The final balance theorem establishes that the minimum and maximum path lengths of any tree are within a factor of two of each other. *)
adamc@214 474
adamc@95 475 Theorem balanced : forall c n (t : rbtree c n), 2 * depth min t + 1 >= depth max t.
adamc@95 476 intros; generalize (depth_min t); generalize (depth_max t); crush.
adamc@95 477 Qed.
adamc@100 478 (* end thide *)
adamc@95 479
adamc@214 480 (** Now we are ready to implement an example operation on our trees, insertion. Insertion can be thought of as breaking the tree invariants locally but then rebalancing. In particular, in intermediate states we find red nodes that may have red children. The type [rtree] captures the idea of such a node, continuing to track black depth as a type index. *)
adamc@95 481
adamc@94 482 Inductive rtree : nat -> Set :=
adamc@94 483 | RedNode' : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rtree n.
adamc@94 484
adam@338 485 (** Before starting to define [insert], we define predicates capturing when a data value is in the set represented by a normal or possibly invalid tree. *)
adamc@214 486
adamc@96 487 Section present.
adamc@96 488 Variable x : nat.
adamc@96 489
adamc@214 490 Fixpoint present c n (t : rbtree c n) : Prop :=
adamc@96 491 match t with
adamc@96 492 | Leaf => False
adamc@96 493 | RedNode _ a y b => present a \/ x = y \/ present b
adamc@96 494 | BlackNode _ _ _ a y b => present a \/ x = y \/ present b
adamc@96 495 end.
adamc@96 496
adamc@96 497 Definition rpresent n (t : rtree n) : Prop :=
adamc@96 498 match t with
adamc@96 499 | RedNode' _ _ _ a y b => present a \/ x = y \/ present b
adamc@96 500 end.
adamc@96 501 End present.
adamc@96 502
adam@338 503 (** 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. *)
adamc@214 504
adamc@100 505 Locate "{ _ : _ & _ }".
adamc@214 506 (** [[
adamc@214 507 Notation Scope
adamc@214 508 "{ x : A & P }" := sigT (fun x : A => P)
adam@302 509 ]]
adam@302 510 *)
adamc@214 511
adamc@100 512 Print sigT.
adamc@214 513 (** [[
adamc@214 514 Inductive sigT (A : Type) (P : A -> Type) : Type :=
adamc@214 515 existT : forall x : A, P x -> sigT P
adam@302 516 ]]
adam@302 517 *)
adamc@214 518
adamc@214 519 (** It will be helpful to define a concise notation for the constructor of [sigT]. *)
adamc@100 520
adamc@94 521 Notation "{< x >}" := (existT _ _ x).
adamc@94 522
adamc@214 523 (** Each balance function is used to construct a new tree whose keys include the keys of two input trees, as well as a new key. One of the two input trees may violate the red-black alternation invariant (that is, it has an [rtree] type), while the other tree is known to be valid. Crucially, the two input trees have the same black depth.
adamc@214 524
adam@338 525 A balance operation may return a tree whose root is of either color. Thus, we use a [sigT] type to package the result tree with the color of its root. Here is the definition of the first balance operation, which applies when the possibly invalid [rtree] belongs to the left of the valid [rbtree].
adam@338 526
adam@338 527 A quick word of encouragement: After writing this code, even I do not understand the precise details of how balancing works! I consulted Chris Okasaki's paper %``%#"#Red-Black Trees in a Functional Setting#"#%''~\cite{Okasaki}% and transcribed the code to use dependent types. Luckily, the details are not so important here; types alone will tell us that insertion preserves balanced-ness, and we will prove that insertion produces trees containing the right keys.*)
adamc@214 528
adamc@94 529 Definition balance1 n (a : rtree n) (data : nat) c2 :=
adamc@214 530 match a in rtree n return rbtree c2 n
adamc@214 531 -> { c : color & rbtree c (S n) } with
adamc@94 532 | RedNode' _ _ _ t1 y t2 =>
adamc@214 533 match t1 in rbtree c n return rbtree _ n -> rbtree c2 n
adamc@214 534 -> { c : color & rbtree c (S n) } with
adamc@214 535 | RedNode _ a x b => fun c d =>
adamc@214 536 {<RedNode (BlackNode a x b) y (BlackNode c data d)>}
adamc@94 537 | t1' => fun t2 =>
adamc@214 538 match t2 in rbtree c n return rbtree _ n -> rbtree c2 n
adamc@214 539 -> { c : color & rbtree c (S n) } with
adamc@214 540 | RedNode _ b x c => fun a d =>
adamc@214 541 {<RedNode (BlackNode a y b) x (BlackNode c data d)>}
adamc@95 542 | b => fun a t => {<BlackNode (RedNode a y b) data t>}
adamc@94 543 end t1'
adamc@94 544 end t2
adamc@94 545 end.
adamc@94 546
adam@338 547 (** We apply a trick that I call the %\index{convoy pattern}\textit{%#<i>#convoy pattern#</i>#%}%. Recall that [match] annotations only make it possible to describe a dependence of a [match] %\textit{%#<i>#result type#</i>#%}% on the discriminee. There is no automatic refinement of the types of free variables. However, it is possible to effect such a refinement by finding a way to encode free variable type dependencies in the [match] result type, so that a [return] clause can express the connection.
adamc@214 548
adam@292 549 In particular, we can extend the [match] to return %\textit{%#<i>#functions over the free variables whose types we want to refine#</i>#%}%. In the case of [balance1], we only find ourselves wanting to refine the type of one tree variable at a time. We match on one subtree of a node, and we want the type of the other subtree to be refined based on what we learn. We indicate this with a [return] clause starting like [rbtree _ n -> ...], where [n] is bound in an [in] pattern. Such a [match] expression is applied immediately to the %``%#"#old version#"#%''% of the variable to be refined, and the type checker is happy.
adamc@214 550
adam@338 551 Here is the symmetric function [balance2], for cases where the possibly invalid tree appears on the right rather than on the left. *)
adamc@214 552
adamc@94 553 Definition balance2 n (a : rtree n) (data : nat) c2 :=
adamc@94 554 match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with
adamc@94 555 | RedNode' _ _ _ t1 z t2 =>
adamc@214 556 match t1 in rbtree c n return rbtree _ n -> rbtree c2 n
adamc@214 557 -> { c : color & rbtree c (S n) } with
adamc@214 558 | RedNode _ b y c => fun d a =>
adamc@214 559 {<RedNode (BlackNode a data b) y (BlackNode c z d)>}
adamc@94 560 | t1' => fun t2 =>
adamc@214 561 match t2 in rbtree c n return rbtree _ n -> rbtree c2 n
adamc@214 562 -> { c : color & rbtree c (S n) } with
adamc@214 563 | RedNode _ c z' d => fun b a =>
adamc@214 564 {<RedNode (BlackNode a data b) z (BlackNode c z' d)>}
adamc@95 565 | b => fun a t => {<BlackNode t data (RedNode a z b)>}
adamc@94 566 end t1'
adamc@94 567 end t2
adamc@94 568 end.
adamc@94 569
adamc@214 570 (** Now we are almost ready to get down to the business of writing an [insert] function. First, we enter a section that declares a variable [x], for the key we want to insert. *)
adamc@214 571
adamc@94 572 Section insert.
adamc@94 573 Variable x : nat.
adamc@94 574
adamc@214 575 (** Most of the work of insertion is done by a helper function [ins], whose return types are expressed using a type-level function [insResult]. *)
adamc@214 576
adamc@94 577 Definition insResult c n :=
adamc@94 578 match c with
adamc@94 579 | Red => rtree n
adamc@94 580 | Black => { c' : color & rbtree c' n }
adamc@94 581 end.
adamc@94 582
adam@338 583 (** That is, inserting into a tree with root color [c] and black depth [n], the variety of tree we get out depends on [c]. If we started with a red root, then we get back a possibly invalid tree of depth [n]. If we started with a black root, we get back a valid tree of depth [n] with a root node of an arbitrary color.
adamc@214 584
adamc@214 585 Here is the definition of [ins]. Again, we do not want to dwell on the functional details. *)
adamc@214 586
adamc@214 587 Fixpoint ins c n (t : rbtree c n) : insResult c n :=
adamc@214 588 match t with
adamc@94 589 | Leaf => {< RedNode Leaf x Leaf >}
adamc@94 590 | RedNode _ a y b =>
adamc@94 591 if le_lt_dec x y
adamc@94 592 then RedNode' (projT2 (ins a)) y b
adamc@94 593 else RedNode' a y (projT2 (ins b))
adamc@94 594 | BlackNode c1 c2 _ a y b =>
adamc@94 595 if le_lt_dec x y
adamc@94 596 then
adamc@94 597 match c1 return insResult c1 _ -> _ with
adamc@94 598 | Red => fun ins_a => balance1 ins_a y b
adamc@94 599 | _ => fun ins_a => {< BlackNode (projT2 ins_a) y b >}
adamc@94 600 end (ins a)
adamc@94 601 else
adamc@94 602 match c2 return insResult c2 _ -> _ with
adamc@94 603 | Red => fun ins_b => balance2 ins_b y a
adamc@94 604 | _ => fun ins_b => {< BlackNode a y (projT2 ins_b) >}
adamc@94 605 end (ins b)
adamc@94 606 end.
adamc@94 607
adam@338 608 (** The one new trick is a variation of the convoy pattern. In each of the last two pattern matches, we want to take advantage of the typing connection between the trees [a] and [b]. We might naively apply the convoy pattern directly on [a] in the first [match] and on [b] in the second. This satisfies the type checker per se, but it does not satisfy the termination checker. Inside each [match], we would be calling [ins] recursively on a locally bound variable. The termination checker is not smart enough to trace the dataflow into that variable, so the checker does not know that this recursive argument is smaller than the original argument. We make this fact clearer by applying the convoy pattern on %\textit{%#<i>#the result of a recursive call#</i>#%}%, rather than just on that call's argument.
adamc@214 609
adamc@214 610 Finally, we are in the home stretch of our effort to define [insert]. We just need a few more definitions of non-recursive functions. First, we need to give the final characterization of [insert]'s return type. Inserting into a red-rooted tree gives a black-rooted tree where black depth has increased, and inserting into a black-rooted tree gives a tree where black depth has stayed the same and where the root is an arbitrary color. *)
adamc@214 611
adamc@94 612 Definition insertResult c n :=
adamc@94 613 match c with
adamc@94 614 | Red => rbtree Black (S n)
adamc@94 615 | Black => { c' : color & rbtree c' n }
adamc@94 616 end.
adamc@94 617
adamc@214 618 (** A simple clean-up procedure translates [insResult]s into [insertResult]s. *)
adamc@214 619
adamc@97 620 Definition makeRbtree c n : insResult c n -> insertResult c n :=
adamc@214 621 match c with
adamc@94 622 | Red => fun r =>
adamc@214 623 match r with
adamc@94 624 | RedNode' _ _ _ a x b => BlackNode a x b
adamc@94 625 end
adamc@94 626 | Black => fun r => r
adamc@94 627 end.
adamc@94 628
adamc@214 629 (** We modify Coq's default choice of implicit arguments for [makeRbtree], so that we do not need to specify the [c] and [n] arguments explicitly in later calls. *)
adamc@214 630
adamc@97 631 Implicit Arguments makeRbtree [c n].
adamc@94 632
adamc@214 633 (** Finally, we define [insert] as a simple composition of [ins] and [makeRbtree]. *)
adamc@214 634
adamc@94 635 Definition insert c n (t : rbtree c n) : insertResult c n :=
adamc@97 636 makeRbtree (ins t).
adamc@94 637
adamc@214 638 (** As we noted earlier, the type of [insert] guarantees that it outputs balanced trees whose depths have not increased too much. We also want to know that [insert] operates correctly on trees interpreted as finite sets, so we finish this section with a proof of that fact. *)
adamc@214 639
adamc@95 640 Section present.
adamc@95 641 Variable z : nat.
adamc@95 642
adamc@214 643 (** The variable [z] stands for an arbitrary key. We will reason about [z]'s presence in particular trees. As usual, outside the section the theorems we prove will quantify over all possible keys, giving us the facts we wanted.
adamc@214 644
adam@367 645 We start by proving the correctness of the balance operations. It is useful to define a custom tactic [present_balance] that encapsulates the reasoning common to the two proofs. We use the keyword %\index{Vernacular commands!Ltac}%[Ltac] to assign a name to a proof script. This particular script just iterates between [crush] and identification of a tree that is being pattern-matched on and should be destructed. *)
adamc@214 646
adamc@98 647 Ltac present_balance :=
adamc@98 648 crush;
adamc@98 649 repeat (match goal with
adam@338 650 | [ _ : context[match ?T with
adamc@98 651 | Leaf => _
adamc@98 652 | RedNode _ _ _ _ => _
adamc@98 653 | BlackNode _ _ _ _ _ _ => _
adamc@98 654 end] |- _ ] => dep_destruct T
adamc@98 655 | [ |- context[match ?T with
adamc@98 656 | Leaf => _
adamc@98 657 | RedNode _ _ _ _ => _
adamc@98 658 | BlackNode _ _ _ _ _ _ => _
adamc@98 659 end] ] => dep_destruct T
adamc@98 660 end; crush).
adamc@98 661
adamc@214 662 (** The balance correctness theorems are simple first-order logic equivalences, where we use the function [projT2] to project the payload of a [sigT] value. *)
adamc@214 663
adam@294 664 Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n),
adamc@95 665 present z (projT2 (balance1 a y b))
adamc@95 666 <-> rpresent z a \/ z = y \/ present z b.
adamc@98 667 destruct a; present_balance.
adamc@95 668 Qed.
adamc@95 669
adamc@213 670 Lemma present_balance2 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n),
adamc@95 671 present z (projT2 (balance2 a y b))
adamc@95 672 <-> rpresent z a \/ z = y \/ present z b.
adamc@98 673 destruct a; present_balance.
adamc@95 674 Qed.
adamc@95 675
adamc@214 676 (** To state the theorem for [ins], it is useful to define a new type-level function, since [ins] returns different result types based on the type indices passed to it. Recall that [x] is the section variable standing for the key we are inserting. *)
adamc@214 677
adamc@95 678 Definition present_insResult c n :=
adamc@95 679 match c return (rbtree c n -> insResult c n -> Prop) with
adamc@95 680 | Red => fun t r => rpresent z r <-> z = x \/ present z t
adamc@95 681 | Black => fun t r => present z (projT2 r) <-> z = x \/ present z t
adamc@95 682 end.
adamc@95 683
adamc@214 684 (** Now the statement and proof of the [ins] correctness theorem are straightforward, if verbose. We proceed by induction on the structure of a tree, followed by finding case analysis opportunities on expressions we see being analyzed in [if] or [match] expressions. After that, we pattern-match to find opportunities to use the theorems we proved about balancing. Finally, we identify two variables that are asserted by some hypothesis to be equal, and we use that hypothesis to replace one variable with the other everywhere. *)
adamc@214 685
adamc@214 686 (** printing * $*$ *)
adamc@214 687
adamc@95 688 Theorem present_ins : forall c n (t : rbtree c n),
adamc@95 689 present_insResult t (ins t).
adamc@95 690 induction t; crush;
adamc@95 691 repeat (match goal with
adam@338 692 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
adamc@95 693 | [ |- context[if ?E then _ else _] ] => destruct E
adam@338 694 | [ _ : context[match ?C with Red => _ | Black => _ end]
adamc@214 695 |- _ ] => destruct C
adamc@95 696 end; crush);
adamc@95 697 try match goal with
adam@338 698 | [ _ : context[balance1 ?A ?B ?C] |- _ ] =>
adamc@95 699 generalize (present_balance1 A B C)
adamc@95 700 end;
adamc@95 701 try match goal with
adam@338 702 | [ _ : context[balance2 ?A ?B ?C] |- _ ] =>
adamc@95 703 generalize (present_balance2 A B C)
adamc@95 704 end;
adamc@95 705 try match goal with
adamc@95 706 | [ |- context[balance1 ?A ?B ?C] ] =>
adamc@95 707 generalize (present_balance1 A B C)
adamc@95 708 end;
adamc@95 709 try match goal with
adamc@95 710 | [ |- context[balance2 ?A ?B ?C] ] =>
adamc@95 711 generalize (present_balance2 A B C)
adamc@95 712 end;
adamc@214 713 crush;
adamc@95 714 match goal with
adamc@95 715 | [ z : nat, x : nat |- _ ] =>
adamc@95 716 match goal with
adamc@95 717 | [ H : z = x |- _ ] => rewrite H in *; clear H
adamc@95 718 end
adamc@95 719 end;
adamc@95 720 tauto.
adamc@95 721 Qed.
adamc@95 722
adamc@214 723 (** printing * $\times$ *)
adamc@214 724
adamc@214 725 (** The hard work is done. The most readable way to state correctness of [insert] involves splitting the property into two color-specific theorems. We write a tactic to encapsulate the reasoning steps that work to establish both facts. *)
adamc@214 726
adamc@213 727 Ltac present_insert :=
adamc@213 728 unfold insert; intros n t; inversion t;
adamc@97 729 generalize (present_ins t); simpl;
adamc@97 730 dep_destruct (ins t); tauto.
adamc@97 731
adamc@95 732 Theorem present_insert_Red : forall n (t : rbtree Red n),
adamc@95 733 present z (insert t)
adamc@95 734 <-> (z = x \/ present z t).
adamc@213 735 present_insert.
adamc@95 736 Qed.
adamc@95 737
adamc@95 738 Theorem present_insert_Black : forall n (t : rbtree Black n),
adamc@95 739 present z (projT2 (insert t))
adamc@95 740 <-> (z = x \/ present z t).
adamc@213 741 present_insert.
adamc@95 742 Qed.
adamc@95 743 End present.
adamc@94 744 End insert.
adamc@94 745
adam@338 746 (** We can generate executable OCaml code with the command %\index{Vernacular commands!Recursive Extraction}%[Recursive Extraction insert], which also automatically outputs the OCaml versions of all of [insert]'s dependencies. In our previous extractions, we wound up with clean OCaml code. Here, we find uses of %\index{Obj.magic}\texttt{%#<tt>#Obj.magic#</tt>#%}%, OCaml's unsafe cast operator for tweaking the apparent type of an expression in an arbitrary way. Casts appear for this example because the return type of [insert] depends on the %\textit{%#<i>#value#</i>#%}% of the function's argument, a pattern which OCaml cannot handle. Since Coq's type system is much more expressive than OCaml's, such casts are unavoidable in general. Since the OCaml type-checker is no longer checking full safety of programs, we must rely on Coq's extractor to use casts only in provably safe ways. *)
adam@338 747
adam@338 748 (* begin hide *)
adam@338 749 Recursive Extraction insert.
adam@338 750 (* end hide *)
adam@283 751
adamc@94 752
adamc@86 753 (** * A Certified Regular Expression Matcher *)
adamc@86 754
adamc@93 755 (** Another interesting example is regular expressions with dependent types that express which predicates over strings particular regexps implement. We can then assign a dependent type to a regular expression matching function, guaranteeing that it always decides the string property that we expect it to decide.
adamc@93 756
adam@338 757 Before defining the syntax of expressions, it is helpful to define an inductive type capturing the meaning of the Kleene star. That is, a string [s] matches regular expression [star e] if and only if [s] can be decomposed into a sequence of substrings that all match [e]. We use Coq's string support, which comes through a combination of the [Strings] library and some parsing notations built into Coq. Operators like [++] and functions like [length] that we know from lists are defined again for strings. Notation scopes help us control which versions we want to use in particular contexts.%\index{Vernacular commands!Open Scope}% *)
adamc@93 758
adamc@86 759 Require Import Ascii String.
adamc@86 760 Open Scope string_scope.
adamc@86 761
adamc@91 762 Section star.
adamc@91 763 Variable P : string -> Prop.
adamc@91 764
adamc@91 765 Inductive star : string -> Prop :=
adamc@91 766 | Empty : star ""
adamc@91 767 | Iter : forall s1 s2,
adamc@91 768 P s1
adamc@91 769 -> star s2
adamc@91 770 -> star (s1 ++ s2).
adamc@91 771 End star.
adamc@91 772
adam@283 773 (** Now we can make our first attempt at defining a [regexp] type that is indexed by predicates on strings. Here is a reasonable-looking definition that is restricted to constant characters and concatenation. We use the constructor [String], which is the analogue of list cons for the type [string], where [""] is like list nil.
adamc@93 774 [[
adamc@93 775 Inductive regexp : (string -> Prop) -> Set :=
adamc@93 776 | Char : forall ch : ascii,
adamc@93 777 regexp (fun s => s = String ch "")
adamc@93 778 | Concat : forall (P1 P2 : string -> Prop) (r1 : regexp P1) (r2 : regexp P2),
adamc@93 779 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2).
adamc@93 780 ]]
adamc@93 781
adam@338 782 <<
adam@338 783 User error: Large non-propositional inductive types must be in Type
adam@338 784 >>
adam@338 785
adam@338 786 What is a %\index{large inductive types}%large inductive type? In Coq, it is an inductive type that has a constructor which quantifies over some type of type [Type]. We have not worked with [Type] very much to this point. Every term of CIC has a type, including [Set] and [Prop], which are assigned type [Type]. The type [string -> Prop] from the failed definition also has type [Type].
adamc@93 787
adamc@93 788 It turns out that allowing large inductive types in [Set] leads to contradictions when combined with certain kinds of classical logic reasoning. Thus, by default, such types are ruled out. There is a simple fix for our [regexp] definition, which is to place our new type in [Type]. While fixing the problem, we also expand the list of constructors to cover the remaining regular expression operators. *)
adamc@93 789
adamc@89 790 Inductive regexp : (string -> Prop) -> Type :=
adamc@86 791 | Char : forall ch : ascii,
adamc@86 792 regexp (fun s => s = String ch "")
adamc@86 793 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
adamc@87 794 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2)
adamc@87 795 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
adamc@91 796 regexp (fun s => P1 s \/ P2 s)
adamc@91 797 | Star : forall P (r : regexp P),
adamc@91 798 regexp (star P).
adamc@86 799
adam@296 800 (** Many theorems about strings are useful for implementing a certified regexp matcher, and few of them are in the [Strings] library. The book source includes statements, proofs, and hint commands for a handful of such omitted theorems. Since they are orthogonal to our use of dependent types, we hide them in the rendered versions of this book. *)
adamc@93 801
adamc@93 802 (* begin hide *)
adamc@86 803 Open Scope specif_scope.
adamc@86 804
adamc@86 805 Lemma length_emp : length "" <= 0.
adamc@86 806 crush.
adamc@86 807 Qed.
adamc@86 808
adamc@86 809 Lemma append_emp : forall s, s = "" ++ s.
adamc@86 810 crush.
adamc@86 811 Qed.
adamc@86 812
adamc@86 813 Ltac substring :=
adamc@86 814 crush;
adamc@86 815 repeat match goal with
adamc@86 816 | [ |- context[match ?N with O => _ | S _ => _ end] ] => destruct N; crush
adamc@86 817 end.
adamc@86 818
adamc@86 819 Lemma substring_le : forall s n m,
adamc@86 820 length (substring n m s) <= m.
adamc@86 821 induction s; substring.
adamc@86 822 Qed.
adamc@86 823
adamc@86 824 Lemma substring_all : forall s,
adamc@86 825 substring 0 (length s) s = s.
adamc@86 826 induction s; substring.
adamc@86 827 Qed.
adamc@86 828
adamc@86 829 Lemma substring_none : forall s n,
adamc@93 830 substring n 0 s = "".
adamc@86 831 induction s; substring.
adamc@86 832 Qed.
adamc@86 833
adamc@86 834 Hint Rewrite substring_all substring_none : cpdt.
adamc@86 835
adamc@86 836 Lemma substring_split : forall s m,
adamc@86 837 substring 0 m s ++ substring m (length s - m) s = s.
adamc@86 838 induction s; substring.
adamc@86 839 Qed.
adamc@86 840
adamc@86 841 Lemma length_app1 : forall s1 s2,
adamc@86 842 length s1 <= length (s1 ++ s2).
adamc@86 843 induction s1; crush.
adamc@86 844 Qed.
adamc@86 845
adamc@86 846 Hint Resolve length_emp append_emp substring_le substring_split length_app1.
adamc@86 847
adamc@86 848 Lemma substring_app_fst : forall s2 s1 n,
adamc@86 849 length s1 = n
adamc@86 850 -> substring 0 n (s1 ++ s2) = s1.
adamc@86 851 induction s1; crush.
adamc@86 852 Qed.
adamc@86 853
adamc@86 854 Lemma substring_app_snd : forall s2 s1 n,
adamc@86 855 length s1 = n
adamc@86 856 -> substring n (length (s1 ++ s2) - n) (s1 ++ s2) = s2.
adamc@86 857 Hint Rewrite <- minus_n_O : cpdt.
adamc@86 858
adamc@86 859 induction s1; crush.
adamc@86 860 Qed.
adamc@86 861
adamc@214 862 Hint Rewrite substring_app_fst substring_app_snd using solve [trivial] : cpdt.
adamc@93 863 (* end hide *)
adamc@93 864
adamc@93 865 (** A few auxiliary functions help us in our final matcher definition. The function [split] will be used to implement the regexp concatenation case. *)
adamc@86 866
adamc@86 867 Section split.
adamc@86 868 Variables P1 P2 : string -> Prop.
adamc@214 869 Variable P1_dec : forall s, {P1 s} + {~ P1 s}.
adamc@214 870 Variable P2_dec : forall s, {P2 s} + {~ P2 s}.
adamc@93 871 (** We require a choice of two arbitrary string predicates and functions for deciding them. *)
adamc@86 872
adamc@86 873 Variable s : string.
adamc@93 874 (** Our computation will take place relative to a single fixed string, so it is easiest to make it a [Variable], rather than an explicit argument to our functions. *)
adamc@93 875
adam@338 876 (** The function [split'] is the workhorse behind [split]. It searches through the possible ways of splitting [s] into two pieces, checking the two predicates against each such pair. The execution of [split'] progresses right-to-left, from splitting all of [s] into the first piece to splitting all of [s] into the second piece. It takes an extra argument, [n], which specifies how far along we are in this search process. *)
adamc@86 877
adam@297 878 Definition split' : forall n : nat, n <= length s
adamc@86 879 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
adamc@214 880 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2}.
adamc@86 881 refine (fix F (n : nat) : n <= length s
adamc@86 882 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
adamc@214 883 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2} :=
adamc@214 884 match n with
adamc@86 885 | O => fun _ => Reduce (P1_dec "" && P2_dec s)
adamc@93 886 | S n' => fun _ => (P1_dec (substring 0 (S n') s)
adamc@93 887 && P2_dec (substring (S n') (length s - S n') s))
adamc@86 888 || F n' _
adamc@86 889 end); clear F; crush; eauto 7;
adamc@86 890 match goal with
adamc@86 891 | [ _ : length ?S <= 0 |- _ ] => destruct S
adam@338 892 | [ _ : length ?S' <= S ?N |- _ ] => destruct (eq_nat_dec (length S') (S N))
adamc@86 893 end; crush.
adamc@86 894 Defined.
adamc@86 895
adam@338 896 (** There is one subtle point in the [split'] code that is worth mentioning. The main body of the function is a [match] on [n]. In the case where [n] is known to be [S n'], we write [S n'] in several places where we might be tempted to write [n]. However, without further work to craft proper [match] annotations, the type-checker does not use the equality between [n] and [S n']. Thus, it is common to see patterns repeated in [match] case bodies in dependently typed Coq code. We can at least use a [let] expression to avoid copying the pattern more than once, replacing the first case body with:
adamc@93 897 [[
adamc@93 898 | S n' => fun _ => let n := S n' in
adamc@93 899 (P1_dec (substring 0 n s)
adamc@93 900 && P2_dec (substring n (length s - n) s))
adamc@93 901 || F n' _
adamc@214 902
adamc@93 903 ]]
adamc@93 904
adam@338 905 The [split] function itself is trivial to implement in terms of [split']. We just ask [split'] to begin its search with [n = length s]. *)
adamc@93 906
adamc@86 907 Definition split : {exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2}
adamc@214 908 + {forall s1 s2, s = s1 ++ s2 -> ~ P1 s1 \/ ~ P2 s2}.
adamc@86 909 refine (Reduce (split' (n := length s) _)); crush; eauto.
adamc@86 910 Defined.
adamc@86 911 End split.
adamc@86 912
adamc@86 913 Implicit Arguments split [P1 P2].
adamc@86 914
adamc@93 915 (* begin hide *)
adamc@91 916 Lemma app_empty_end : forall s, s ++ "" = s.
adamc@91 917 induction s; crush.
adamc@91 918 Qed.
adamc@91 919
adamc@91 920 Hint Rewrite app_empty_end : cpdt.
adamc@91 921
adamc@91 922 Lemma substring_self : forall s n,
adamc@91 923 n <= 0
adamc@91 924 -> substring n (length s - n) s = s.
adamc@91 925 induction s; substring.
adamc@91 926 Qed.
adamc@91 927
adamc@91 928 Lemma substring_empty : forall s n m,
adamc@91 929 m <= 0
adamc@91 930 -> substring n m s = "".
adamc@91 931 induction s; substring.
adamc@91 932 Qed.
adamc@91 933
adamc@91 934 Hint Rewrite substring_self substring_empty using omega : cpdt.
adamc@91 935
adamc@91 936 Lemma substring_split' : forall s n m,
adamc@91 937 substring n m s ++ substring (n + m) (length s - (n + m)) s
adamc@91 938 = substring n (length s - n) s.
adamc@91 939 Hint Rewrite substring_split : cpdt.
adamc@91 940
adamc@91 941 induction s; substring.
adamc@91 942 Qed.
adamc@91 943
adamc@91 944 Lemma substring_stack : forall s n2 m1 m2,
adamc@91 945 m1 <= m2
adamc@91 946 -> substring 0 m1 (substring n2 m2 s)
adamc@91 947 = substring n2 m1 s.
adamc@91 948 induction s; substring.
adamc@91 949 Qed.
adamc@91 950
adamc@91 951 Ltac substring' :=
adamc@91 952 crush;
adamc@91 953 repeat match goal with
adamc@91 954 | [ |- context[match ?N with O => _ | S _ => _ end] ] => case_eq N; crush
adamc@91 955 end.
adamc@91 956
adamc@91 957 Lemma substring_stack' : forall s n1 n2 m1 m2,
adamc@91 958 n1 + m1 <= m2
adamc@91 959 -> substring n1 m1 (substring n2 m2 s)
adamc@91 960 = substring (n1 + n2) m1 s.
adamc@91 961 induction s; substring';
adamc@91 962 match goal with
adamc@91 963 | [ |- substring ?N1 _ _ = substring ?N2 _ _ ] =>
adamc@91 964 replace N1 with N2; crush
adamc@91 965 end.
adamc@91 966 Qed.
adamc@91 967
adamc@91 968 Lemma substring_suffix : forall s n,
adamc@91 969 n <= length s
adamc@91 970 -> length (substring n (length s - n) s) = length s - n.
adamc@91 971 induction s; substring.
adamc@91 972 Qed.
adamc@91 973
adamc@91 974 Lemma substring_suffix_emp' : forall s n m,
adamc@91 975 substring n (S m) s = ""
adamc@91 976 -> n >= length s.
adamc@91 977 induction s; crush;
adamc@91 978 match goal with
adamc@91 979 | [ |- ?N >= _ ] => destruct N; crush
adamc@91 980 end;
adamc@91 981 match goal with
adamc@91 982 [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | omega ]
adamc@91 983 end.
adamc@91 984 Qed.
adamc@91 985
adamc@91 986 Lemma substring_suffix_emp : forall s n m,
adamc@92 987 substring n m s = ""
adamc@92 988 -> m > 0
adamc@91 989 -> n >= length s.
adam@335 990 destruct m as [ | m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
adamc@91 991 Qed.
adamc@91 992
adamc@91 993 Hint Rewrite substring_stack substring_stack' substring_suffix
adamc@91 994 using omega : cpdt.
adamc@91 995
adamc@91 996 Lemma minus_minus : forall n m1 m2,
adamc@91 997 m1 + m2 <= n
adamc@91 998 -> n - m1 - m2 = n - (m1 + m2).
adamc@91 999 intros; omega.
adamc@91 1000 Qed.
adamc@91 1001
adamc@91 1002 Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n.
adamc@91 1003 intros; omega.
adamc@91 1004 Qed.
adamc@91 1005
adamc@91 1006 Hint Rewrite minus_minus using omega : cpdt.
adamc@93 1007 (* end hide *)
adamc@93 1008
adamc@93 1009 (** One more helper function will come in handy: [dec_star], for implementing another linear search through ways of splitting a string, this time for implementing the Kleene star. *)
adamc@91 1010
adamc@91 1011 Section dec_star.
adamc@91 1012 Variable P : string -> Prop.
adamc@214 1013 Variable P_dec : forall s, {P s} + {~ P s}.
adamc@91 1014
adam@338 1015 (** Some new lemmas and hints about the [star] type family are useful. We omit them here; they are included in the book source at this point. *)
adamc@93 1016
adamc@93 1017 (* begin hide *)
adamc@91 1018 Hint Constructors star.
adamc@91 1019
adamc@91 1020 Lemma star_empty : forall s,
adamc@91 1021 length s = 0
adamc@91 1022 -> star P s.
adamc@91 1023 destruct s; crush.
adamc@91 1024 Qed.
adamc@91 1025
adamc@91 1026 Lemma star_singleton : forall s, P s -> star P s.
adamc@91 1027 intros; rewrite <- (app_empty_end s); auto.
adamc@91 1028 Qed.
adamc@91 1029
adamc@91 1030 Lemma star_app : forall s n m,
adamc@91 1031 P (substring n m s)
adamc@91 1032 -> star P (substring (n + m) (length s - (n + m)) s)
adamc@91 1033 -> star P (substring n (length s - n) s).
adamc@91 1034 induction n; substring;
adamc@91 1035 match goal with
adamc@91 1036 | [ H : P (substring ?N ?M ?S) |- _ ] =>
adamc@91 1037 solve [ rewrite <- (substring_split S M); auto
adamc@91 1038 | rewrite <- (substring_split' S N M); auto ]
adamc@91 1039 end.
adamc@91 1040 Qed.
adamc@91 1041
adamc@91 1042 Hint Resolve star_empty star_singleton star_app.
adamc@91 1043
adamc@91 1044 Variable s : string.
adamc@91 1045
adamc@91 1046 Lemma star_inv : forall s,
adamc@91 1047 star P s
adamc@91 1048 -> s = ""
adamc@91 1049 \/ exists i, i < length s
adamc@91 1050 /\ P (substring 0 (S i) s)
adamc@91 1051 /\ star P (substring (S i) (length s - S i) s).
adamc@91 1052 Hint Extern 1 (exists i : nat, _) =>
adamc@91 1053 match goal with
adamc@91 1054 | [ H : P (String _ ?S) |- _ ] => exists (length S); crush
adamc@91 1055 end.
adamc@91 1056
adamc@91 1057 induction 1; [
adamc@91 1058 crush
adamc@91 1059 | match goal with
adamc@91 1060 | [ _ : P ?S |- _ ] => destruct S; crush
adamc@91 1061 end
adamc@91 1062 ].
adamc@91 1063 Qed.
adamc@91 1064
adamc@91 1065 Lemma star_substring_inv : forall n,
adamc@91 1066 n <= length s
adamc@91 1067 -> star P (substring n (length s - n) s)
adamc@91 1068 -> substring n (length s - n) s = ""
adamc@91 1069 \/ exists l, l < length s - n
adamc@91 1070 /\ P (substring n (S l) s)
adamc@91 1071 /\ star P (substring (n + S l) (length s - (n + S l)) s).
adamc@91 1072 Hint Rewrite plus_n_Sm' : cpdt.
adamc@91 1073
adamc@91 1074 intros;
adamc@91 1075 match goal with
adamc@91 1076 | [ H : star _ _ |- _ ] => generalize (star_inv H); do 3 crush; eauto
adamc@91 1077 end.
adamc@91 1078 Qed.
adamc@93 1079 (* end hide *)
adamc@93 1080
adamc@93 1081 (** The function [dec_star''] implements a single iteration of the star. That is, it tries to find a string prefix matching [P], and it calls a parameter function on the remainder of the string. *)
adamc@91 1082
adamc@91 1083 Section dec_star''.
adamc@91 1084 Variable n : nat.
adamc@93 1085 (** [n] is the length of the prefix of [s] that we have already processed. *)
adamc@91 1086
adamc@91 1087 Variable P' : string -> Prop.
adamc@91 1088 Variable P'_dec : forall n' : nat, n' > n
adamc@91 1089 -> {P' (substring n' (length s - n') s)}
adamc@214 1090 + {~ P' (substring n' (length s - n') s)}.
adamc@93 1091 (** When we use [dec_star''], we will instantiate [P'_dec] with a function for continuing the search for more instances of [P] in [s]. *)
adamc@93 1092
adamc@93 1093 (** Now we come to [dec_star''] itself. It takes as an input a natural [l] that records how much of the string has been searched so far, as we did for [split']. The return type expresses that [dec_star''] is looking for an index into [s] that splits [s] into a nonempty prefix and a suffix, such that the prefix satisfies [P] and the suffix satisfies [P']. *)
adamc@91 1094
adam@297 1095 Definition dec_star'' : forall l : nat,
adam@297 1096 {exists l', S l' <= l
adamc@91 1097 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
adamc@91 1098 + {forall l', S l' <= l
adamc@214 1099 -> ~ P (substring n (S l') s)
adamc@214 1100 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)}.
adamc@91 1101 refine (fix F (l : nat) : {exists l', S l' <= l
adamc@91 1102 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
adamc@91 1103 + {forall l', S l' <= l
adamc@214 1104 -> ~ P (substring n (S l') s)
adamc@214 1105 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} :=
adamc@214 1106 match l with
adamc@91 1107 | O => _
adamc@91 1108 | S l' =>
adamc@91 1109 (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
adamc@91 1110 || F l'
adamc@91 1111 end); clear F; crush; eauto 7;
adamc@91 1112 match goal with
adamc@91 1113 | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush
adamc@91 1114 end.
adamc@91 1115 Defined.
adamc@91 1116 End dec_star''.
adamc@91 1117
adamc@93 1118 (* begin hide *)
adamc@92 1119 Lemma star_length_contra : forall n,
adamc@92 1120 length s > n
adamc@92 1121 -> n >= length s
adamc@92 1122 -> False.
adamc@92 1123 crush.
adamc@92 1124 Qed.
adamc@92 1125
adamc@92 1126 Lemma star_length_flip : forall n n',
adamc@92 1127 length s - n <= S n'
adamc@92 1128 -> length s > n
adamc@92 1129 -> length s - n > 0.
adamc@92 1130 crush.
adamc@92 1131 Qed.
adamc@92 1132
adamc@92 1133 Hint Resolve star_length_contra star_length_flip substring_suffix_emp.
adamc@93 1134 (* end hide *)
adamc@92 1135
adamc@93 1136 (** The work of [dec_star''] is nested inside another linear search by [dec_star'], which provides the final functionality we need, but for arbitrary suffixes of [s], rather than just for [s] overall. *)
adamc@93 1137
adam@297 1138 Definition dec_star' : forall n n' : nat, length s - n' <= n
adamc@91 1139 -> {star P (substring n' (length s - n') s)}
adamc@214 1140 + {~ star P (substring n' (length s - n') s)}.
adamc@214 1141 refine (fix F (n n' : nat) : length s - n' <= n
adamc@91 1142 -> {star P (substring n' (length s - n') s)}
adamc@214 1143 + {~ star P (substring n' (length s - n') s)} :=
adamc@214 1144 match n with
adamc@91 1145 | O => fun _ => Yes
adamc@91 1146 | S n'' => fun _ =>
adamc@91 1147 le_gt_dec (length s) n'
adam@338 1148 || dec_star'' (n := n') (star P)
adam@338 1149 (fun n0 _ => Reduce (F n'' n0 _)) (length s - n')
adamc@92 1150 end); clear F; crush; eauto;
adamc@92 1151 match goal with
adamc@92 1152 | [ H : star _ _ |- _ ] => apply star_substring_inv in H; crush; eauto
adamc@92 1153 end;
adamc@92 1154 match goal with
adamc@92 1155 | [ H1 : _ < _ - _, H2 : forall l' : nat, _ <= _ - _ -> _ |- _ ] =>
adamc@92 1156 generalize (H2 _ (lt_le_S _ _ H1)); tauto
adamc@92 1157 end.
adamc@91 1158 Defined.
adamc@91 1159
adamc@93 1160 (** Finally, we have [dec_star]. It has a straightforward implementation. We introduce a spurious match on [s] so that [simpl] will know to reduce calls to [dec_star]. The heuristic that [simpl] uses is only to unfold identifier definitions when doing so would simplify some [match] expression. *)
adamc@93 1161
adamc@214 1162 Definition dec_star : {star P s} + {~ star P s}.
adamc@204 1163 refine (match s return _ with
adamc@91 1164 | "" => Reduce (dec_star' (n := length s) 0 _)
adamc@91 1165 | _ => Reduce (dec_star' (n := length s) 0 _)
adamc@91 1166 end); crush.
adamc@91 1167 Defined.
adamc@91 1168 End dec_star.
adamc@91 1169
adamc@93 1170 (* begin hide *)
adamc@86 1171 Lemma app_cong : forall x1 y1 x2 y2,
adamc@86 1172 x1 = x2
adamc@86 1173 -> y1 = y2
adamc@86 1174 -> x1 ++ y1 = x2 ++ y2.
adamc@86 1175 congruence.
adamc@86 1176 Qed.
adamc@86 1177
adamc@86 1178 Hint Resolve app_cong.
adamc@93 1179 (* end hide *)
adamc@93 1180
adamc@93 1181 (** With these helper functions completed, the implementation of our [matches] function is refreshingly straightforward. We only need one small piece of specific tactic work beyond what [crush] does for us. *)
adamc@86 1182
adam@297 1183 Definition matches : forall P (r : regexp P) s, {P s} + {~ P s}.
adamc@214 1184 refine (fix F P (r : regexp P) s : {P s} + {~ P s} :=
adamc@86 1185 match r with
adamc@86 1186 | Char ch => string_dec s (String ch "")
adamc@86 1187 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s)
adamc@87 1188 | Or _ _ r1 r2 => F _ r1 s || F _ r2 s
adamc@91 1189 | Star _ r => dec_star _ _ _
adamc@86 1190 end); crush;
adamc@86 1191 match goal with
adamc@86 1192 | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _))
adamc@93 1193 end; tauto.
adamc@86 1194 Defined.
adamc@86 1195
adam@283 1196 (** It is interesting to pause briefly to consider alternate implementations of [matches]. Dependent types give us much latitude in how specific correctness properties may be encoded with types. For instance, we could have made [regexp] a non-indexed inductive type, along the lines of what is possible in traditional ML and Haskell. We could then have implemented a recursive function to map [regexp]s to their intended meanings, much as we have done with types and programs in other examples. That style is compatible with the [refine]-based approach that we have used here, and it might be an interesting exercise to redo the code from this subsection in that alternate style or some further encoding of the reader's choice. The main advantage of indexed inductive types is that they generally lead to the smallest amount of code. *)
adam@283 1197
adamc@93 1198 (* begin hide *)
adamc@86 1199 Example hi := Concat (Char "h"%char) (Char "i"%char).
adamc@86 1200 Eval simpl in matches hi "hi".
adamc@86 1201 Eval simpl in matches hi "bye".
adamc@87 1202
adamc@87 1203 Example a_b := Or (Char "a"%char) (Char "b"%char).
adamc@87 1204 Eval simpl in matches a_b "".
adamc@87 1205 Eval simpl in matches a_b "a".
adamc@87 1206 Eval simpl in matches a_b "aa".
adamc@87 1207 Eval simpl in matches a_b "b".
adam@283 1208 (* end hide *)
adam@283 1209
adam@283 1210 (** Many regular expression matching problems are easy to test. The reader may run each of the following queries to verify that it gives the correct answer. *)
adamc@91 1211
adamc@91 1212 Example a_star := Star (Char "a"%char).
adamc@91 1213 Eval simpl in matches a_star "".
adamc@91 1214 Eval simpl in matches a_star "a".
adamc@91 1215 Eval simpl in matches a_star "b".
adamc@91 1216 Eval simpl in matches a_star "aa".
adam@283 1217
adam@283 1218 (** Evaluation inside Coq does not scale very well, so it is easy to build other tests that run for hours or more. Such cases are better suited to execution with the extracted OCaml code. *)
adamc@101 1219
adamc@101 1220
adamc@101 1221 (** * Exercises *)
adamc@101 1222
adamc@101 1223 (** %\begin{enumerate}%#<ol>#
adamc@101 1224
adam@338 1225 %\item%#<li># Define a kind of dependently typed lists, where a list's type index gives a lower bound on how many of its elements satisfy a particular predicate. In particular, for an arbitrary set [A] and a predicate [P] over it:
adamc@101 1226 %\begin{enumerate}%#<ol>#
adamc@101 1227 %\item%#<li># Define a type [plist : nat -> Set]. Each [plist n] should be a list of [A]s, where it is guaranteed that at least [n] distinct elements satisfy [P]. There is wide latitude in choosing how to encode this. You should try to avoid using subset types or any other mechanism based on annotating non-dependent types with propositions after-the-fact.#</li>#
adamc@102 1228 %\item%#<li># Define a version of list concatenation that works on [plist]s. The type of this new function should express as much information as possible about the output [plist].#</li>#
adamc@101 1229 %\item%#<li># Define a function [plistOut] for translating [plist]s to normal [list]s.#</li>#
adam@338 1230 %\item%#<li># Define a function [plistIn] for translating [list]s to [plist]s. The type of [plistIn] should make it clear that the best bound on [P]-matching elements is chosen. You may assume that you are given a dependently typed function for deciding instances of [P].#</li>#
adamc@101 1231 %\item%#<li># Prove that, for any list [ls], [plistOut (plistIn ls) = ls]. This should be the only part of the exercise where you use tactic-based proving.#</li>#
adam@338 1232 %\item%#<li># Define a function [grab : forall n (ls : plist (][S n)), sig P]. That is, when given a [plist] guaranteed to contain at least one element satisfying [P], [grab] produces such an element. The type family [sig] is the one we met earlier for sigma types (i.e., dependent pairs of programs and proofs), and [sig P] is extensionally equivalent to [{][x : A | P x}], though the latter form uses an eta-expansion of [P] instead of [P] itself as the predicate.#</li>#
adamc@101 1233 #</ol>#%\end{enumerate}% #</li>#
adamc@101 1234
adamc@102 1235 #</ol>#%\end{enumerate}% *)