Mercurial > cpdt > repo

annotate src/MoreDep.v @ 319:6838c7be18fa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New release
author Adam Chlipala <adam@chlipala.net>
date Mon, 12 Sep 2011 16:47:43 -0400
parents d5787b70cf48
children 1f57a8d0ed3d
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
adamc@83 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 which 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
adamc@84 28 (** Many introductions to dependent types start out by showing how to use them to eliminate 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, 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
adamc@84 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 sublist. We may apply [ilist] to any natural number, even natural numbers that are only known at runtime. It is this breaking of the %\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
adamc@213 49 (** In Coq version 8.1 and earlier, this definition leads to an error message:
adamc@84 50
adamc@84 51 [[
adamc@84 52 The term "ls2" has type "ilist n2" while it is expected to have type
adamc@84 53 "ilist (?14 + n2)"
adamc@213 54
adamc@84 55 ]]
adamc@84 56
adamc@213 57 In Coq's core language, without explicit annotations, Coq does not enrich our typing assumptions in the branches of a [match] expression. It is clear that the unification variable [?14] should be resolved to 0 in this context, so that we have [0 + n2] reducing to [n2], but Coq does not realize that. We cannot fix the problem using just the simple [return] clauses we applied in the last chapter. We need to combine a [return] clause with a new kind of annotation, an [in] clause. This is exactly what the inference heuristics do in Coq 8.2 and later.
adamc@213 58
adamc@213 59 Specifically, Coq infers the following definition from the simpler one. *)
adamc@84 60
adamc@100 61 (* EX: Implement concatenation *)
adamc@100 62
adamc@100 63 (* begin thide *)
adamc@213 64 Fixpoint app' n1 (ls1 : ilist n1) n2 (ls2 : ilist n2) : ilist (n1 + n2) :=
adamc@84 65 match ls1 in (ilist n1) return (ilist (n1 + n2)) with
adamc@84 66 | Nil => ls2
adamc@213 67 | Cons _ x ls1' => Cons x (app' ls1' ls2)
adamc@84 68 end.
adamc@100 69 (* end thide *)
adamc@84 70
adamc@213 71 (** Using [return] alone allowed us to express a dependency of the [match] result type on the %\textit{%#<i>#value#</i>#%}% of the discriminee. What [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 72
adamc@84 73 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 74
adam@283 75 Our [app] function could be typed in so-called %\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 76
adamc@100 77 (* EX: Implement injection from normal lists *)
adamc@100 78
adamc@100 79 (* begin thide *)
adamc@84 80 Fixpoint inject (ls : list A) : ilist (length ls) :=
adamc@213 81 match ls with
adamc@84 82 | nil => Nil
adamc@84 83 | h :: t => Cons h (inject t)
adamc@84 84 end.
adamc@84 85
adamc@84 86 (** We can define an inverse conversion and prove that it really is an inverse. *)
adamc@84 87
adamc@213 88 Fixpoint unject n (ls : ilist n) : list A :=
adamc@84 89 match ls with
adamc@84 90 | Nil => nil
adamc@84 91 | Cons _ h t => h :: unject t
adamc@84 92 end.
adamc@84 93
adamc@84 94 Theorem inject_inverse : forall ls, unject (inject ls) = ls.
adamc@84 95 induction ls; crush.
adamc@84 96 Qed.
adamc@100 97 (* end thide *)
adamc@100 98
adamc@100 99 (* EX: Implement statically-checked "car"/"hd" *)
adamc@84 100
adam@283 101 (** 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 102
adamc@84 103 [[
adamc@84 104 Definition hd n (ls : ilist (S n)) : A :=
adamc@84 105 match ls with
adamc@84 106 | Nil => ???
adamc@84 107 | Cons _ h _ => h
adamc@84 108 end.
adamc@213 109
adamc@213 110 ]]
adamc@84 111
adamc@84 112 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 113
adamc@84 114 [[
adamc@84 115 Definition hd n (ls : ilist (S n)) : A :=
adamc@84 116 match ls with
adamc@84 117 | Cons _ h _ => h
adamc@84 118 end.
adamc@84 119
adamc@84 120 Error: Non exhaustive pattern-matching: no clause found for pattern Nil
adamc@213 121
adamc@84 122 ]]
adamc@84 123
adam@275 124 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 125
adamc@84 126 [[
adamc@84 127 Definition hd n (ls : ilist (S n)) : A :=
adamc@84 128 match ls in (ilist (S n)) with
adamc@84 129 | Cons _ h _ => h
adamc@84 130 end.
adamc@84 131
adamc@84 132 Error: The reference n was not found in the current environment
adamc@213 133
adamc@84 134 ]]
adamc@84 135
adamc@84 136 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, 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 137
adamc@84 138 Our final, working attempt at [hd] uses an auxiliary function and a surprising [return] annotation. *)
adamc@84 139
adamc@100 140 (* begin thide *)
adamc@84 141 Definition hd' n (ls : ilist n) :=
adamc@84 142 match ls in (ilist n) return (match n with O => unit | S _ => A end) with
adamc@84 143 | Nil => tt
adamc@84 144 | Cons _ h _ => h
adamc@84 145 end.
adamc@84 146
adam@283 147 Check hd'.
adam@283 148 (** %\vspace{-.15in}% [[
adam@283 149 hd'
adam@283 150 : forall n : nat, ilist n -> match n with
adam@283 151 | 0 => unit
adam@283 152 | S _ => A
adam@283 153 end
adam@283 154
adam@302 155 ]]
adam@302 156 *)
adam@283 157
adamc@84 158 Definition hd n (ls : ilist (S n)) : A := hd' ls.
adamc@100 159 (* end thide *)
adamc@84 160
adamc@84 161 (** 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 162
adamc@84 163 End ilist.
adamc@85 164
adamc@85 165
adamc@85 166 (** * A Tagless Interpreter *)
adamc@85 167
adam@296 168 (** 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 %\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 169
adamc@85 170 Inductive type : Set :=
adamc@85 171 | Nat : type
adamc@85 172 | Bool : type
adamc@85 173 | Prod : type -> type -> type.
adamc@85 174
adamc@85 175 Inductive exp : type -> Set :=
adamc@85 176 | NConst : nat -> exp Nat
adamc@85 177 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@85 178 | Eq : exp Nat -> exp Nat -> exp Bool
adamc@85 179
adamc@85 180 | BConst : bool -> exp Bool
adamc@85 181 | And : exp Bool -> exp Bool -> exp Bool
adamc@85 182 | If : forall t, exp Bool -> exp t -> exp t -> exp t
adamc@85 183
adamc@85 184 | Pair : forall t1 t2, exp t1 -> exp t2 -> exp (Prod t1 t2)
adamc@85 185 | Fst : forall t1 t2, exp (Prod t1 t2) -> exp t1
adamc@85 186 | Snd : forall t1 t2, exp (Prod t1 t2) -> exp t2.
adamc@85 187
adamc@85 188 (** 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 189
adamc@85 190 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 191
adamc@85 192 Fixpoint typeDenote (t : type) : Set :=
adamc@85 193 match t with
adamc@85 194 | Nat => nat
adamc@85 195 | Bool => bool
adamc@85 196 | Prod t1 t2 => typeDenote t1 * typeDenote t2
adamc@85 197 end%type.
adamc@85 198
adam@292 199 (** [typeDenote] 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. [type] is one example of an identifer bound to a %\textit{%#<i>#notation scope#</i>#%}%. We will deal more explicitly with notations and notation scopes in later chapters.
adamc@85 200
adamc@85 201 We can define a function [expDenote] that is typed in terms of [typeDenote]. *)
adamc@85 202
adamc@213 203 Fixpoint expDenote t (e : exp t) : typeDenote t :=
adamc@213 204 match e with
adamc@85 205 | NConst n => n
adamc@85 206 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@85 207 | Eq e1 e2 => if eq_nat_dec (expDenote e1) (expDenote e2) then true else false
adamc@85 208
adamc@85 209 | BConst b => b
adamc@85 210 | And e1 e2 => expDenote e1 && expDenote e2
adamc@85 211 | If _ e' e1 e2 => if expDenote e' then expDenote e1 else expDenote e2
adamc@85 212
adamc@85 213 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@85 214 | Fst _ _ e' => fst (expDenote e')
adamc@85 215 | Snd _ _ e' => snd (expDenote e')
adamc@85 216 end.
adamc@85 217
adamc@213 218 (** 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 219
adamc@85 220 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 221
adamc@85 222 [[
adamc@85 223 Definition pairOut t1 t2 (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) :=
adamc@85 224 match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with
adamc@85 225 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@85 226 | _ => None
adamc@85 227 end.
adamc@85 228
adamc@85 229 Error: The reference t2 was not found in the current environment
adamc@213 230 ]]
adamc@85 231
adamc@85 232 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 233
adamc@100 234 (* EX: Define a function [pairOut : forall t1 t2, exp (Prod t1 t2) -> option (exp t1 * exp t2)] *)
adamc@100 235
adamc@100 236 (* begin thide *)
adamc@85 237 Definition pairOutType (t : type) :=
adamc@85 238 match t with
adamc@85 239 | Prod t1 t2 => option (exp t1 * exp t2)
adamc@85 240 | _ => unit
adamc@85 241 end.
adamc@85 242
adamc@85 243 (** 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 244
adamc@85 245 Definition pairOutDefault (t : type) :=
adamc@85 246 match t return (pairOutType t) with
adamc@85 247 | Prod _ _ => None
adamc@85 248 | _ => tt
adamc@85 249 end.
adamc@85 250
adamc@85 251 (** Now [pairOut] is deceptively easy to write. *)
adamc@85 252
adamc@85 253 Definition pairOut t (e : exp t) :=
adamc@85 254 match e in (exp t) return (pairOutType t) with
adamc@85 255 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@85 256 | _ => pairOutDefault _
adamc@85 257 end.
adamc@100 258 (* end thide *)
adamc@85 259
adamc@85 260 (** 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, but is similar to what goes on with Haskell type classes.
adamc@85 261
adamc@213 262 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 263
adamc@204 264 Fixpoint cfold t (e : exp t) : exp t :=
adamc@204 265 match e with
adamc@85 266 | NConst n => NConst n
adamc@85 267 | Plus e1 e2 =>
adamc@85 268 let e1' := cfold e1 in
adamc@85 269 let e2' := cfold e2 in
adamc@204 270 match e1', e2' return _ with
adamc@85 271 | NConst n1, NConst n2 => NConst (n1 + n2)
adamc@85 272 | _, _ => Plus e1' e2'
adamc@85 273 end
adamc@85 274 | Eq e1 e2 =>
adamc@85 275 let e1' := cfold e1 in
adamc@85 276 let e2' := cfold e2 in
adamc@204 277 match e1', e2' return _ with
adamc@85 278 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
adamc@85 279 | _, _ => Eq e1' e2'
adamc@85 280 end
adamc@85 281
adamc@85 282 | BConst b => BConst b
adamc@85 283 | And e1 e2 =>
adamc@85 284 let e1' := cfold e1 in
adamc@85 285 let e2' := cfold e2 in
adamc@204 286 match e1', e2' return _ with
adamc@85 287 | BConst b1, BConst b2 => BConst (b1 && b2)
adamc@85 288 | _, _ => And e1' e2'
adamc@85 289 end
adamc@85 290 | If _ e e1 e2 =>
adamc@85 291 let e' := cfold e in
adamc@85 292 match e' with
adamc@85 293 | BConst true => cfold e1
adamc@85 294 | BConst false => cfold e2
adamc@85 295 | _ => If e' (cfold e1) (cfold e2)
adamc@85 296 end
adamc@85 297
adamc@85 298 | Pair _ _ e1 e2 => Pair (cfold e1) (cfold e2)
adamc@85 299 | Fst _ _ e =>
adamc@85 300 let e' := cfold e in
adamc@85 301 match pairOut e' with
adamc@85 302 | Some p => fst p
adamc@85 303 | None => Fst e'
adamc@85 304 end
adamc@85 305 | Snd _ _ e =>
adamc@85 306 let e' := cfold e in
adamc@85 307 match pairOut e' with
adamc@85 308 | Some p => snd p
adamc@85 309 | None => Snd e'
adamc@85 310 end
adamc@85 311 end.
adamc@85 312
adamc@85 313 (** The correctness theorem for [cfold] turns out to be easy to prove, once we get over one serious hurdle. *)
adamc@85 314
adamc@85 315 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
adamc@100 316 (* begin thide *)
adamc@85 317 induction e; crush.
adamc@85 318
adamc@85 319 (** The first remaining subgoal is:
adamc@85 320
adamc@85 321 [[
adamc@85 322 expDenote (cfold e1) + expDenote (cfold e2) =
adamc@85 323 expDenote
adamc@85 324 match cfold e1 with
adamc@85 325 | NConst n1 =>
adamc@85 326 match cfold e2 with
adamc@85 327 | NConst n2 => NConst (n1 + n2)
adamc@85 328 | Plus _ _ => Plus (cfold e1) (cfold e2)
adamc@85 329 | Eq _ _ => Plus (cfold e1) (cfold e2)
adamc@85 330 | BConst _ => Plus (cfold e1) (cfold e2)
adamc@85 331 | And _ _ => Plus (cfold e1) (cfold e2)
adamc@85 332 | If _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 333 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 334 | Fst _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 335 | Snd _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 336 end
adamc@85 337 | Plus _ _ => Plus (cfold e1) (cfold e2)
adamc@85 338 | Eq _ _ => Plus (cfold e1) (cfold e2)
adamc@85 339 | BConst _ => Plus (cfold e1) (cfold e2)
adamc@85 340 | And _ _ => Plus (cfold e1) (cfold e2)
adamc@85 341 | If _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 342 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 343 | Fst _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 344 | Snd _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 345 end
adamc@213 346
adamc@85 347 ]]
adamc@85 348
adamc@85 349 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 350
adamc@85 351 [[
adamc@85 352 destruct (cfold e1).
adamc@85 353
adamc@85 354 User error: e1 is used in hypothesis e
adamc@213 355
adamc@85 356 ]]
adamc@85 357
adamc@85 358 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 359
adamc@213 360 For our current proof, we can use a tactic [dep_destruct] defined in the book [Tactics] 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. [dep_destruct] makes a best effort to handle some common cases, relying upon the more primitive [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. *)
adamc@85 361
adamc@85 362 dep_destruct (cfold e1).
adamc@85 363
adamc@85 364 (** 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 365
adamc@213 366 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 367
adamc@85 368 Restart.
adamc@85 369
adamc@85 370 induction e; crush;
adamc@85 371 repeat (match goal with
adamc@213 372 | [ |- context[match cfold ?E with NConst _ => _ | Plus _ _ => _
adamc@213 373 | Eq _ _ => _ | BConst _ => _ | And _ _ => _
adamc@213 374 | If _ _ _ _ => _ | Pair _ _ _ _ => _
adamc@213 375 | Fst _ _ _ => _ | Snd _ _ _ => _ end] ] =>
adamc@213 376 dep_destruct (cfold E)
adamc@213 377 | [ |- context[match pairOut (cfold ?E) with Some _ => _
adamc@213 378 | None => _ end] ] =>
adamc@213 379 dep_destruct (cfold E)
adamc@85 380 | [ |- (if ?E then _ else _) = _ ] => destruct E
adamc@85 381 end; crush).
adamc@85 382 Qed.
adamc@100 383 (* end thide *)
adamc@86 384
adamc@86 385
adamc@103 386 (** * Dependently-Typed Red-Black Trees *)
adamc@94 387
adamc@214 388 (** 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 389
adamc@94 390 Inductive color : Set := Red | Black.
adamc@94 391
adamc@94 392 Inductive rbtree : color -> nat -> Set :=
adamc@94 393 | Leaf : rbtree Black 0
adamc@214 394 | RedNode : forall n, rbtree Black n -> nat -> rbtree Black n -> rbtree Red n
adamc@94 395 | BlackNode : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rbtree Black (S n).
adamc@94 396
adamc@214 397 (** 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 398
adamc@214 399 (** 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 400
adamc@100 401 (* EX: Prove that every [rbtree] is balanced. *)
adamc@100 402
adamc@100 403 (* begin thide *)
adamc@95 404 Require Import Max Min.
adamc@95 405
adamc@95 406 Section depth.
adamc@95 407 Variable f : nat -> nat -> nat.
adamc@95 408
adamc@214 409 Fixpoint depth c n (t : rbtree c n) : nat :=
adamc@95 410 match t with
adamc@95 411 | Leaf => 0
adamc@95 412 | RedNode _ t1 _ t2 => S (f (depth t1) (depth t2))
adamc@95 413 | BlackNode _ _ _ t1 _ t2 => S (f (depth t1) (depth t2))
adamc@95 414 end.
adamc@95 415 End depth.
adamc@95 416
adamc@214 417 (** 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 418
adam@283 419 Check min_dec.
adam@283 420 (** %\vspace{-.15in}% [[
adam@283 421 min_dec
adam@283 422 : forall n m : nat, {min n m = n} + {min n m = m}
adam@283 423
adam@302 424 ]]
adam@302 425 *)
adam@283 426
adamc@95 427 Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n.
adamc@95 428 induction t; crush;
adamc@95 429 match goal with
adamc@95 430 | [ |- context[min ?X ?Y] ] => destruct (min_dec X Y)
adamc@95 431 end; crush.
adamc@95 432 Qed.
adamc@95 433
adamc@214 434 (** There is an analogous upper-bound theorem based on black depth. Unfortunately, a symmetric proof script does not suffice to establish it. *)
adamc@214 435
adamc@214 436 Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
adamc@214 437 induction t; crush;
adamc@214 438 match goal with
adamc@214 439 | [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
adamc@214 440 end; crush.
adamc@214 441
adamc@214 442 (** Two subgoals remain. One of them is: [[
adamc@214 443 n : nat
adamc@214 444 t1 : rbtree Black n
adamc@214 445 n0 : nat
adamc@214 446 t2 : rbtree Black n
adamc@214 447 IHt1 : depth max t1 <= n + (n + 0) + 1
adamc@214 448 IHt2 : depth max t2 <= n + (n + 0) + 1
adamc@214 449 e : max (depth max t1) (depth max t2) = depth max t1
adamc@214 450 ============================
adamc@214 451 S (depth max t1) <= n + (n + 0) + 1
adamc@214 452
adamc@214 453 ]]
adamc@214 454
adamc@214 455 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 456
adamc@214 457 Abort.
adamc@214 458
adamc@214 459 (** 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 460
adamc@95 461 Lemma depth_max' : forall c n (t : rbtree c n), match c with
adamc@95 462 | Red => depth max t <= 2 * n + 1
adamc@95 463 | Black => depth max t <= 2 * n
adamc@95 464 end.
adamc@95 465 induction t; crush;
adamc@95 466 match goal with
adamc@95 467 | [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
adamc@100 468 end; crush;
adamc@100 469 repeat (match goal with
adamc@214 470 | [ H : context[match ?C with Red => _ | Black => _ end] |- _ ] =>
adamc@214 471 destruct C
adamc@100 472 end; crush).
adamc@95 473 Qed.
adamc@95 474
adamc@214 475 (** The original theorem follows easily from the lemma. We use the tactic [generalize pf], which, when [pf] proves the proposition [P], changes the goal from [Q] to [P -> Q]. It is useful to do this 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 476
adamc@95 477 Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
adamc@95 478 intros; generalize (depth_max' t); destruct c; crush.
adamc@95 479 Qed.
adamc@95 480
adamc@214 481 (** 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 482
adamc@95 483 Theorem balanced : forall c n (t : rbtree c n), 2 * depth min t + 1 >= depth max t.
adamc@95 484 intros; generalize (depth_min t); generalize (depth_max t); crush.
adamc@95 485 Qed.
adamc@100 486 (* end thide *)
adamc@95 487
adamc@214 488 (** 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 489
adamc@94 490 Inductive rtree : nat -> Set :=
adamc@94 491 | RedNode' : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rtree n.
adamc@94 492
adamc@214 493 (** 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 494
adamc@96 495 Section present.
adamc@96 496 Variable x : nat.
adamc@96 497
adamc@214 498 Fixpoint present c n (t : rbtree c n) : Prop :=
adamc@96 499 match t with
adamc@96 500 | Leaf => False
adamc@96 501 | RedNode _ a y b => present a \/ x = y \/ present b
adamc@96 502 | BlackNode _ _ _ a y b => present a \/ x = y \/ present b
adamc@96 503 end.
adamc@96 504
adamc@96 505 Definition rpresent n (t : rtree n) : Prop :=
adamc@96 506 match t with
adamc@96 507 | RedNode' _ _ _ a y b => present a \/ x = y \/ present b
adamc@96 508 end.
adamc@96 509 End present.
adamc@96 510
adamc@214 511 (** 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 [sigT] type fills this role. *)
adamc@214 512
adamc@100 513 Locate "{ _ : _ & _ }".
adamc@214 514 (** [[
adamc@214 515 Notation Scope
adamc@214 516 "{ x : A & P }" := sigT (fun x : A => P)
adam@302 517 ]]
adam@302 518 *)
adamc@214 519
adamc@100 520 Print sigT.
adamc@214 521 (** [[
adamc@214 522 Inductive sigT (A : Type) (P : A -> Type) : Type :=
adamc@214 523 existT : forall x : A, P x -> sigT P
adam@302 524 ]]
adam@302 525 *)
adamc@214 526
adamc@214 527 (** It will be helpful to define a concise notation for the constructor of [sigT]. *)
adamc@100 528
adamc@94 529 Notation "{< x >}" := (existT _ _ x).
adamc@94 530
adamc@214 531 (** 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 532
adamc@214 533 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]. *)
adamc@214 534
adamc@94 535 Definition balance1 n (a : rtree n) (data : nat) c2 :=
adamc@214 536 match a in rtree n return rbtree c2 n
adamc@214 537 -> { c : color & rbtree c (S n) } with
adamc@94 538 | RedNode' _ _ _ t1 y t2 =>
adamc@214 539 match t1 in rbtree c n return rbtree _ n -> rbtree c2 n
adamc@214 540 -> { c : color & rbtree c (S n) } with
adamc@214 541 | RedNode _ a x b => fun c d =>
adamc@214 542 {<RedNode (BlackNode a x b) y (BlackNode c data d)>}
adamc@94 543 | t1' => fun t2 =>
adamc@214 544 match t2 in rbtree c n return rbtree _ n -> rbtree c2 n
adamc@214 545 -> { c : color & rbtree c (S n) } with
adamc@214 546 | RedNode _ b x c => fun a d =>
adamc@214 547 {<RedNode (BlackNode a y b) x (BlackNode c data d)>}
adamc@95 548 | b => fun a t => {<BlackNode (RedNode a y b) data t>}
adamc@94 549 end t1'
adamc@94 550 end t2
adamc@94 551 end.
adamc@94 552
adamc@214 553 (** We apply a trick that I call the %\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 554
adam@292 555 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 556
adam@292 557 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#"#%''% 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 558
adamc@214 559 Here is the symmetric function [balance2], for cases where the possibly-invalid tree appears on the right rather than on the left. *)
adamc@214 560
adamc@94 561 Definition balance2 n (a : rtree n) (data : nat) c2 :=
adamc@94 562 match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with
adamc@94 563 | RedNode' _ _ _ t1 z t2 =>
adamc@214 564 match t1 in rbtree c n return rbtree _ n -> rbtree c2 n
adamc@214 565 -> { c : color & rbtree c (S n) } with
adamc@214 566 | RedNode _ b y c => fun d a =>
adamc@214 567 {<RedNode (BlackNode a data b) y (BlackNode c z d)>}
adamc@94 568 | t1' => fun t2 =>
adamc@214 569 match t2 in rbtree c n return rbtree _ n -> rbtree c2 n
adamc@214 570 -> { c : color & rbtree c (S n) } with
adamc@214 571 | RedNode _ c z' d => fun b a =>
adamc@214 572 {<RedNode (BlackNode a data b) z (BlackNode c z' d)>}
adamc@95 573 | b => fun a t => {<BlackNode t data (RedNode a z b)>}
adamc@94 574 end t1'
adamc@94 575 end t2
adamc@94 576 end.
adamc@94 577
adamc@214 578 (** 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 579
adamc@94 580 Section insert.
adamc@94 581 Variable x : nat.
adamc@94 582
adamc@214 583 (** 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 584
adamc@94 585 Definition insResult c n :=
adamc@94 586 match c with
adamc@94 587 | Red => rtree n
adamc@94 588 | Black => { c' : color & rbtree c' n }
adamc@94 589 end.
adamc@94 590
adam@296 591 (** 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 592
adamc@214 593 Here is the definition of [ins]. Again, we do not want to dwell on the functional details. *)
adamc@214 594
adamc@214 595 Fixpoint ins c n (t : rbtree c n) : insResult c n :=
adamc@214 596 match t with
adamc@94 597 | Leaf => {< RedNode Leaf x Leaf >}
adamc@94 598 | RedNode _ a y b =>
adamc@94 599 if le_lt_dec x y
adamc@94 600 then RedNode' (projT2 (ins a)) y b
adamc@94 601 else RedNode' a y (projT2 (ins b))
adamc@94 602 | BlackNode c1 c2 _ a y b =>
adamc@94 603 if le_lt_dec x y
adamc@94 604 then
adamc@94 605 match c1 return insResult c1 _ -> _ with
adamc@94 606 | Red => fun ins_a => balance1 ins_a y b
adamc@94 607 | _ => fun ins_a => {< BlackNode (projT2 ins_a) y b >}
adamc@94 608 end (ins a)
adamc@94 609 else
adamc@94 610 match c2 return insResult c2 _ -> _ with
adamc@94 611 | Red => fun ins_b => balance2 ins_b y a
adamc@94 612 | _ => fun ins_b => {< BlackNode a y (projT2 ins_b) >}
adamc@94 613 end (ins b)
adamc@94 614 end.
adamc@94 615
adam@296 616 (** 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 617
adamc@214 618 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 619
adamc@94 620 Definition insertResult c n :=
adamc@94 621 match c with
adamc@94 622 | Red => rbtree Black (S n)
adamc@94 623 | Black => { c' : color & rbtree c' n }
adamc@94 624 end.
adamc@94 625
adamc@214 626 (** A simple clean-up procedure translates [insResult]s into [insertResult]s. *)
adamc@214 627
adamc@97 628 Definition makeRbtree c n : insResult c n -> insertResult c n :=
adamc@214 629 match c with
adamc@94 630 | Red => fun r =>
adamc@214 631 match r with
adamc@94 632 | RedNode' _ _ _ a x b => BlackNode a x b
adamc@94 633 end
adamc@94 634 | Black => fun r => r
adamc@94 635 end.
adamc@94 636
adamc@214 637 (** 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 638
adamc@97 639 Implicit Arguments makeRbtree [c n].
adamc@94 640
adamc@214 641 (** Finally, we define [insert] as a simple composition of [ins] and [makeRbtree]. *)
adamc@214 642
adamc@94 643 Definition insert c n (t : rbtree c n) : insertResult c n :=
adamc@97 644 makeRbtree (ins t).
adamc@94 645
adamc@214 646 (** 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 647
adamc@95 648 Section present.
adamc@95 649 Variable z : nat.
adamc@95 650
adamc@214 651 (** 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 652
adamc@214 653 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 [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 654
adamc@98 655 Ltac present_balance :=
adamc@98 656 crush;
adamc@98 657 repeat (match goal with
adamc@98 658 | [ H : context[match ?T with
adamc@98 659 | Leaf => _
adamc@98 660 | RedNode _ _ _ _ => _
adamc@98 661 | BlackNode _ _ _ _ _ _ => _
adamc@98 662 end] |- _ ] => dep_destruct T
adamc@98 663 | [ |- context[match ?T with
adamc@98 664 | Leaf => _
adamc@98 665 | RedNode _ _ _ _ => _
adamc@98 666 | BlackNode _ _ _ _ _ _ => _
adamc@98 667 end] ] => dep_destruct T
adamc@98 668 end; crush).
adamc@98 669
adamc@214 670 (** 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 671
adam@294 672 Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n),
adamc@95 673 present z (projT2 (balance1 a y b))
adamc@95 674 <-> rpresent z a \/ z = y \/ present z b.
adamc@98 675 destruct a; present_balance.
adamc@95 676 Qed.
adamc@95 677
adamc@213 678 Lemma present_balance2 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n),
adamc@95 679 present z (projT2 (balance2 a y b))
adamc@95 680 <-> rpresent z a \/ z = y \/ present z b.
adamc@98 681 destruct a; present_balance.
adamc@95 682 Qed.
adamc@95 683
adamc@214 684 (** 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 685
adamc@95 686 Definition present_insResult c n :=
adamc@95 687 match c return (rbtree c n -> insResult c n -> Prop) with
adamc@95 688 | Red => fun t r => rpresent z r <-> z = x \/ present z t
adamc@95 689 | Black => fun t r => present z (projT2 r) <-> z = x \/ present z t
adamc@95 690 end.
adamc@95 691
adamc@214 692 (** 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 693
adamc@214 694 (** printing * $*$ *)
adamc@214 695
adamc@95 696 Theorem present_ins : forall c n (t : rbtree c n),
adamc@95 697 present_insResult t (ins t).
adamc@95 698 induction t; crush;
adamc@95 699 repeat (match goal with
adamc@95 700 | [ H : context[if ?E then _ else _] |- _ ] => destruct E
adamc@95 701 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@214 702 | [ H : context[match ?C with Red => _ | Black => _ end]
adamc@214 703 |- _ ] => destruct C
adamc@95 704 end; crush);
adamc@95 705 try match goal with
adamc@95 706 | [ H : 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 | [ H : context[balance2 ?A ?B ?C] |- _ ] =>
adamc@95 711 generalize (present_balance2 A B C)
adamc@95 712 end;
adamc@95 713 try match goal with
adamc@95 714 | [ |- context[balance1 ?A ?B ?C] ] =>
adamc@95 715 generalize (present_balance1 A B C)
adamc@95 716 end;
adamc@95 717 try match goal with
adamc@95 718 | [ |- context[balance2 ?A ?B ?C] ] =>
adamc@95 719 generalize (present_balance2 A B C)
adamc@95 720 end;
adamc@214 721 crush;
adamc@95 722 match goal with
adamc@95 723 | [ z : nat, x : nat |- _ ] =>
adamc@95 724 match goal with
adamc@95 725 | [ H : z = x |- _ ] => rewrite H in *; clear H
adamc@95 726 end
adamc@95 727 end;
adamc@95 728 tauto.
adamc@95 729 Qed.
adamc@95 730
adamc@214 731 (** printing * $\times$ *)
adamc@214 732
adamc@214 733 (** 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 734
adamc@213 735 Ltac present_insert :=
adamc@213 736 unfold insert; intros n t; inversion t;
adamc@97 737 generalize (present_ins t); simpl;
adamc@97 738 dep_destruct (ins t); tauto.
adamc@97 739
adamc@95 740 Theorem present_insert_Red : forall n (t : rbtree Red n),
adamc@95 741 present z (insert t)
adamc@95 742 <-> (z = x \/ present z t).
adamc@213 743 present_insert.
adamc@95 744 Qed.
adamc@95 745
adamc@95 746 Theorem present_insert_Black : forall n (t : rbtree Black n),
adamc@95 747 present z (projT2 (insert t))
adamc@95 748 <-> (z = x \/ present z t).
adamc@213 749 present_insert.
adamc@95 750 Qed.
adamc@95 751 End present.
adamc@94 752 End insert.
adamc@94 753
adam@283 754 (** We can generate executable OCaml code with the command [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 %\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@283 755
adamc@94 756
adamc@86 757 (** * A Certified Regular Expression Matcher *)
adamc@86 758
adamc@93 759 (** 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 760
adam@283 761 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. *)
adamc@93 762
adamc@86 763 Require Import Ascii String.
adamc@86 764 Open Scope string_scope.
adamc@86 765
adamc@91 766 Section star.
adamc@91 767 Variable P : string -> Prop.
adamc@91 768
adamc@91 769 Inductive star : string -> Prop :=
adamc@91 770 | Empty : star ""
adamc@91 771 | Iter : forall s1 s2,
adamc@91 772 P s1
adamc@91 773 -> star s2
adamc@91 774 -> star (s1 ++ s2).
adamc@91 775 End star.
adamc@91 776
adam@283 777 (** 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 778
adamc@93 779 [[
adamc@93 780 Inductive regexp : (string -> Prop) -> Set :=
adamc@93 781 | Char : forall ch : ascii,
adamc@93 782 regexp (fun s => s = String ch "")
adamc@93 783 | Concat : forall (P1 P2 : string -> Prop) (r1 : regexp P1) (r2 : regexp P2),
adamc@93 784 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2).
adamc@93 785
adamc@93 786 User error: Large non-propositional inductive types must be in Type
adamc@214 787
adamc@93 788 ]]
adamc@93 789
adamc@93 790 What is a 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 791
adamc@93 792 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 793
adamc@89 794 Inductive regexp : (string -> Prop) -> Type :=
adamc@86 795 | Char : forall ch : ascii,
adamc@86 796 regexp (fun s => s = String ch "")
adamc@86 797 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
adamc@87 798 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2)
adamc@87 799 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
adamc@91 800 regexp (fun s => P1 s \/ P2 s)
adamc@91 801 | Star : forall P (r : regexp P),
adamc@91 802 regexp (star P).
adamc@86 803
adam@296 804 (** 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 805
adamc@93 806 (* begin hide *)
adamc@86 807 Open Scope specif_scope.
adamc@86 808
adamc@86 809 Lemma length_emp : length "" <= 0.
adamc@86 810 crush.
adamc@86 811 Qed.
adamc@86 812
adamc@86 813 Lemma append_emp : forall s, s = "" ++ s.
adamc@86 814 crush.
adamc@86 815 Qed.
adamc@86 816
adamc@86 817 Ltac substring :=
adamc@86 818 crush;
adamc@86 819 repeat match goal with
adamc@86 820 | [ |- context[match ?N with O => _ | S _ => _ end] ] => destruct N; crush
adamc@86 821 end.
adamc@86 822
adamc@86 823 Lemma substring_le : forall s n m,
adamc@86 824 length (substring n m s) <= m.
adamc@86 825 induction s; substring.
adamc@86 826 Qed.
adamc@86 827
adamc@86 828 Lemma substring_all : forall s,
adamc@86 829 substring 0 (length s) s = s.
adamc@86 830 induction s; substring.
adamc@86 831 Qed.
adamc@86 832
adamc@86 833 Lemma substring_none : forall s n,
adamc@93 834 substring n 0 s = "".
adamc@86 835 induction s; substring.
adamc@86 836 Qed.
adamc@86 837
adamc@86 838 Hint Rewrite substring_all substring_none : cpdt.
adamc@86 839
adamc@86 840 Lemma substring_split : forall s m,
adamc@86 841 substring 0 m s ++ substring m (length s - m) s = s.
adamc@86 842 induction s; substring.
adamc@86 843 Qed.
adamc@86 844
adamc@86 845 Lemma length_app1 : forall s1 s2,
adamc@86 846 length s1 <= length (s1 ++ s2).
adamc@86 847 induction s1; crush.
adamc@86 848 Qed.
adamc@86 849
adamc@86 850 Hint Resolve length_emp append_emp substring_le substring_split length_app1.
adamc@86 851
adamc@86 852 Lemma substring_app_fst : forall s2 s1 n,
adamc@86 853 length s1 = n
adamc@86 854 -> substring 0 n (s1 ++ s2) = s1.
adamc@86 855 induction s1; crush.
adamc@86 856 Qed.
adamc@86 857
adamc@86 858 Lemma substring_app_snd : forall s2 s1 n,
adamc@86 859 length s1 = n
adamc@86 860 -> substring n (length (s1 ++ s2) - n) (s1 ++ s2) = s2.
adamc@86 861 Hint Rewrite <- minus_n_O : cpdt.
adamc@86 862
adamc@86 863 induction s1; crush.
adamc@86 864 Qed.
adamc@86 865
adamc@214 866 Hint Rewrite substring_app_fst substring_app_snd using solve [trivial] : cpdt.
adamc@93 867 (* end hide *)
adamc@93 868
adamc@93 869 (** 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 870
adamc@86 871 Section split.
adamc@86 872 Variables P1 P2 : string -> Prop.
adamc@214 873 Variable P1_dec : forall s, {P1 s} + {~ P1 s}.
adamc@214 874 Variable P2_dec : forall s, {P2 s} + {~ P2 s}.
adamc@93 875 (** We require a choice of two arbitrary string predicates and functions for deciding them. *)
adamc@86 876
adamc@86 877 Variable s : string.
adamc@93 878 (** 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 879
adamc@93 880 (** [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. [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 881
adam@297 882 Definition split' : forall n : nat, n <= length s
adamc@86 883 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
adamc@214 884 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2}.
adamc@86 885 refine (fix F (n : nat) : n <= length s
adamc@86 886 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
adamc@214 887 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2} :=
adamc@214 888 match n with
adamc@86 889 | O => fun _ => Reduce (P1_dec "" && P2_dec s)
adamc@93 890 | S n' => fun _ => (P1_dec (substring 0 (S n') s)
adamc@93 891 && P2_dec (substring (S n') (length s - S n') s))
adamc@86 892 || F n' _
adamc@86 893 end); clear F; crush; eauto 7;
adamc@86 894 match goal with
adamc@86 895 | [ _ : length ?S <= 0 |- _ ] => destruct S
adamc@86 896 | [ _ : length ?S' <= S ?N |- _ ] =>
adamc@86 897 generalize (eq_nat_dec (length S') (S N)); destruct 1
adamc@86 898 end; crush.
adamc@86 899 Defined.
adamc@86 900
adamc@93 901 (** 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 902
adamc@93 903 [[
adamc@93 904 | S n' => fun _ => let n := S n' in
adamc@93 905 (P1_dec (substring 0 n s)
adamc@93 906 && P2_dec (substring n (length s - n) s))
adamc@93 907 || F n' _
adamc@214 908
adamc@93 909 ]]
adamc@93 910
adamc@93 911 [split] itself is trivial to implement in terms of [split']. We just ask [split'] to begin its search with [n = length s]. *)
adamc@93 912
adamc@86 913 Definition split : {exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2}
adamc@214 914 + {forall s1 s2, s = s1 ++ s2 -> ~ P1 s1 \/ ~ P2 s2}.
adamc@86 915 refine (Reduce (split' (n := length s) _)); crush; eauto.
adamc@86 916 Defined.
adamc@86 917 End split.
adamc@86 918
adamc@86 919 Implicit Arguments split [P1 P2].
adamc@86 920
adamc@93 921 (* begin hide *)
adamc@91 922 Lemma app_empty_end : forall s, s ++ "" = s.
adamc@91 923 induction s; crush.
adamc@91 924 Qed.
adamc@91 925
adamc@91 926 Hint Rewrite app_empty_end : cpdt.
adamc@91 927
adamc@91 928 Lemma substring_self : forall s n,
adamc@91 929 n <= 0
adamc@91 930 -> substring n (length s - n) s = s.
adamc@91 931 induction s; substring.
adamc@91 932 Qed.
adamc@91 933
adamc@91 934 Lemma substring_empty : forall s n m,
adamc@91 935 m <= 0
adamc@91 936 -> substring n m s = "".
adamc@91 937 induction s; substring.
adamc@91 938 Qed.
adamc@91 939
adamc@91 940 Hint Rewrite substring_self substring_empty using omega : cpdt.
adamc@91 941
adamc@91 942 Lemma substring_split' : forall s n m,
adamc@91 943 substring n m s ++ substring (n + m) (length s - (n + m)) s
adamc@91 944 = substring n (length s - n) s.
adamc@91 945 Hint Rewrite substring_split : cpdt.
adamc@91 946
adamc@91 947 induction s; substring.
adamc@91 948 Qed.
adamc@91 949
adamc@91 950 Lemma substring_stack : forall s n2 m1 m2,
adamc@91 951 m1 <= m2
adamc@91 952 -> substring 0 m1 (substring n2 m2 s)
adamc@91 953 = substring n2 m1 s.
adamc@91 954 induction s; substring.
adamc@91 955 Qed.
adamc@91 956
adamc@91 957 Ltac substring' :=
adamc@91 958 crush;
adamc@91 959 repeat match goal with
adamc@91 960 | [ |- context[match ?N with O => _ | S _ => _ end] ] => case_eq N; crush
adamc@91 961 end.
adamc@91 962
adamc@91 963 Lemma substring_stack' : forall s n1 n2 m1 m2,
adamc@91 964 n1 + m1 <= m2
adamc@91 965 -> substring n1 m1 (substring n2 m2 s)
adamc@91 966 = substring (n1 + n2) m1 s.
adamc@91 967 induction s; substring';
adamc@91 968 match goal with
adamc@91 969 | [ |- substring ?N1 _ _ = substring ?N2 _ _ ] =>
adamc@91 970 replace N1 with N2; crush
adamc@91 971 end.
adamc@91 972 Qed.
adamc@91 973
adamc@91 974 Lemma substring_suffix : forall s n,
adamc@91 975 n <= length s
adamc@91 976 -> length (substring n (length s - n) s) = length s - n.
adamc@91 977 induction s; substring.
adamc@91 978 Qed.
adamc@91 979
adamc@91 980 Lemma substring_suffix_emp' : forall s n m,
adamc@91 981 substring n (S m) s = ""
adamc@91 982 -> n >= length s.
adamc@91 983 induction s; crush;
adamc@91 984 match goal with
adamc@91 985 | [ |- ?N >= _ ] => destruct N; crush
adamc@91 986 end;
adamc@91 987 match goal with
adamc@91 988 [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | omega ]
adamc@91 989 end.
adamc@91 990 Qed.
adamc@91 991
adamc@91 992 Lemma substring_suffix_emp : forall s n m,
adamc@92 993 substring n m s = ""
adamc@92 994 -> m > 0
adamc@91 995 -> n >= length s.
adamc@91 996 destruct m as [| m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
adamc@91 997 Qed.
adamc@91 998
adamc@91 999 Hint Rewrite substring_stack substring_stack' substring_suffix
adamc@91 1000 using omega : cpdt.
adamc@91 1001
adamc@91 1002 Lemma minus_minus : forall n m1 m2,
adamc@91 1003 m1 + m2 <= n
adamc@91 1004 -> n - m1 - m2 = n - (m1 + m2).
adamc@91 1005 intros; omega.
adamc@91 1006 Qed.
adamc@91 1007
adamc@91 1008 Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n.
adamc@91 1009 intros; omega.
adamc@91 1010 Qed.
adamc@91 1011
adamc@91 1012 Hint Rewrite minus_minus using omega : cpdt.
adamc@93 1013 (* end hide *)
adamc@93 1014
adamc@93 1015 (** 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 1016
adamc@91 1017 Section dec_star.
adamc@91 1018 Variable P : string -> Prop.
adamc@214 1019 Variable P_dec : forall s, {P s} + {~ P s}.
adamc@91 1020
adamc@93 1021 (** Some new lemmas and hints about the [star] type family are useful here. We omit them here; they are included in the book source at this point. *)
adamc@93 1022
adamc@93 1023 (* begin hide *)
adamc@91 1024 Hint Constructors star.
adamc@91 1025
adamc@91 1026 Lemma star_empty : forall s,
adamc@91 1027 length s = 0
adamc@91 1028 -> star P s.
adamc@91 1029 destruct s; crush.
adamc@91 1030 Qed.
adamc@91 1031
adamc@91 1032 Lemma star_singleton : forall s, P s -> star P s.
adamc@91 1033 intros; rewrite <- (app_empty_end s); auto.
adamc@91 1034 Qed.
adamc@91 1035
adamc@91 1036 Lemma star_app : forall s n m,
adamc@91 1037 P (substring n m s)
adamc@91 1038 -> star P (substring (n + m) (length s - (n + m)) s)
adamc@91 1039 -> star P (substring n (length s - n) s).
adamc@91 1040 induction n; substring;
adamc@91 1041 match goal with
adamc@91 1042 | [ H : P (substring ?N ?M ?S) |- _ ] =>
adamc@91 1043 solve [ rewrite <- (substring_split S M); auto
adamc@91 1044 | rewrite <- (substring_split' S N M); auto ]
adamc@91 1045 end.
adamc@91 1046 Qed.
adamc@91 1047
adamc@91 1048 Hint Resolve star_empty star_singleton star_app.
adamc@91 1049
adamc@91 1050 Variable s : string.
adamc@91 1051
adamc@91 1052 Lemma star_inv : forall s,
adamc@91 1053 star P s
adamc@91 1054 -> s = ""
adamc@91 1055 \/ exists i, i < length s
adamc@91 1056 /\ P (substring 0 (S i) s)
adamc@91 1057 /\ star P (substring (S i) (length s - S i) s).
adamc@91 1058 Hint Extern 1 (exists i : nat, _) =>
adamc@91 1059 match goal with
adamc@91 1060 | [ H : P (String _ ?S) |- _ ] => exists (length S); crush
adamc@91 1061 end.
adamc@91 1062
adamc@91 1063 induction 1; [
adamc@91 1064 crush
adamc@91 1065 | match goal with
adamc@91 1066 | [ _ : P ?S |- _ ] => destruct S; crush
adamc@91 1067 end
adamc@91 1068 ].
adamc@91 1069 Qed.
adamc@91 1070
adamc@91 1071 Lemma star_substring_inv : forall n,
adamc@91 1072 n <= length s
adamc@91 1073 -> star P (substring n (length s - n) s)
adamc@91 1074 -> substring n (length s - n) s = ""
adamc@91 1075 \/ exists l, l < length s - n
adamc@91 1076 /\ P (substring n (S l) s)
adamc@91 1077 /\ star P (substring (n + S l) (length s - (n + S l)) s).
adamc@91 1078 Hint Rewrite plus_n_Sm' : cpdt.
adamc@91 1079
adamc@91 1080 intros;
adamc@91 1081 match goal with
adamc@91 1082 | [ H : star _ _ |- _ ] => generalize (star_inv H); do 3 crush; eauto
adamc@91 1083 end.
adamc@91 1084 Qed.
adamc@93 1085 (* end hide *)
adamc@93 1086
adamc@93 1087 (** 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 1088
adamc@91 1089 Section dec_star''.
adamc@91 1090 Variable n : nat.
adamc@93 1091 (** [n] is the length of the prefix of [s] that we have already processed. *)
adamc@91 1092
adamc@91 1093 Variable P' : string -> Prop.
adamc@91 1094 Variable P'_dec : forall n' : nat, n' > n
adamc@91 1095 -> {P' (substring n' (length s - n') s)}
adamc@214 1096 + {~ P' (substring n' (length s - n') s)}.
adamc@93 1097 (** 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 1098
adamc@93 1099 (** 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 1100
adam@297 1101 Definition dec_star'' : forall l : nat,
adam@297 1102 {exists l', S l' <= l
adamc@91 1103 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
adamc@91 1104 + {forall l', S l' <= l
adamc@214 1105 -> ~ P (substring n (S l') s)
adamc@214 1106 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)}.
adamc@91 1107 refine (fix F (l : nat) : {exists l', S l' <= l
adamc@91 1108 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
adamc@91 1109 + {forall l', S l' <= l
adamc@214 1110 -> ~ P (substring n (S l') s)
adamc@214 1111 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} :=
adamc@214 1112 match l with
adamc@91 1113 | O => _
adamc@91 1114 | S l' =>
adamc@91 1115 (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
adamc@91 1116 || F l'
adamc@91 1117 end); clear F; crush; eauto 7;
adamc@91 1118 match goal with
adamc@91 1119 | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush
adamc@91 1120 end.
adamc@91 1121 Defined.
adamc@91 1122 End dec_star''.
adamc@91 1123
adamc@93 1124 (* begin hide *)
adamc@92 1125 Lemma star_length_contra : forall n,
adamc@92 1126 length s > n
adamc@92 1127 -> n >= length s
adamc@92 1128 -> False.
adamc@92 1129 crush.
adamc@92 1130 Qed.
adamc@92 1131
adamc@92 1132 Lemma star_length_flip : forall n n',
adamc@92 1133 length s - n <= S n'
adamc@92 1134 -> length s > n
adamc@92 1135 -> length s - n > 0.
adamc@92 1136 crush.
adamc@92 1137 Qed.
adamc@92 1138
adamc@92 1139 Hint Resolve star_length_contra star_length_flip substring_suffix_emp.
adamc@93 1140 (* end hide *)
adamc@92 1141
adamc@93 1142 (** 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 1143
adam@297 1144 Definition dec_star' : forall n n' : nat, length s - n' <= n
adamc@91 1145 -> {star P (substring n' (length s - n') s)}
adamc@214 1146 + {~ star P (substring n' (length s - n') s)}.
adamc@214 1147 refine (fix F (n n' : nat) : length s - n' <= n
adamc@91 1148 -> {star P (substring n' (length s - n') s)}
adamc@214 1149 + {~ star P (substring n' (length s - n') s)} :=
adamc@214 1150 match n with
adamc@91 1151 | O => fun _ => Yes
adamc@91 1152 | S n'' => fun _ =>
adamc@91 1153 le_gt_dec (length s) n'
adamc@91 1154 || dec_star'' (n := n') (star P) (fun n0 _ => Reduce (F n'' n0 _)) (length s - n')
adamc@92 1155 end); clear F; crush; eauto;
adamc@92 1156 match goal with
adamc@92 1157 | [ H : star _ _ |- _ ] => apply star_substring_inv in H; crush; eauto
adamc@92 1158 end;
adamc@92 1159 match goal with
adamc@92 1160 | [ H1 : _ < _ - _, H2 : forall l' : nat, _ <= _ - _ -> _ |- _ ] =>
adamc@92 1161 generalize (H2 _ (lt_le_S _ _ H1)); tauto
adamc@92 1162 end.
adamc@91 1163 Defined.
adamc@91 1164
adamc@93 1165 (** 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 1166
adamc@214 1167 Definition dec_star : {star P s} + {~ star P s}.
adamc@204 1168 refine (match s return _ with
adamc@91 1169 | "" => Reduce (dec_star' (n := length s) 0 _)
adamc@91 1170 | _ => Reduce (dec_star' (n := length s) 0 _)
adamc@91 1171 end); crush.
adamc@91 1172 Defined.
adamc@91 1173 End dec_star.
adamc@91 1174
adamc@93 1175 (* begin hide *)
adamc@86 1176 Lemma app_cong : forall x1 y1 x2 y2,
adamc@86 1177 x1 = x2
adamc@86 1178 -> y1 = y2
adamc@86 1179 -> x1 ++ y1 = x2 ++ y2.
adamc@86 1180 congruence.
adamc@86 1181 Qed.
adamc@86 1182
adamc@86 1183 Hint Resolve app_cong.
adamc@93 1184 (* end hide *)
adamc@93 1185
adamc@93 1186 (** 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 1187
adam@297 1188 Definition matches : forall P (r : regexp P) s, {P s} + {~ P s}.
adamc@214 1189 refine (fix F P (r : regexp P) s : {P s} + {~ P s} :=
adamc@86 1190 match r with
adamc@86 1191 | Char ch => string_dec s (String ch "")
adamc@86 1192 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s)
adamc@87 1193 | Or _ _ r1 r2 => F _ r1 s || F _ r2 s
adamc@91 1194 | Star _ r => dec_star _ _ _
adamc@86 1195 end); crush;
adamc@86 1196 match goal with
adamc@86 1197 | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _))
adamc@93 1198 end; tauto.
adamc@86 1199 Defined.
adamc@86 1200
adam@283 1201 (** 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 1202
adamc@93 1203 (* begin hide *)
adamc@86 1204 Example hi := Concat (Char "h"%char) (Char "i"%char).
adamc@86 1205 Eval simpl in matches hi "hi".
adamc@86 1206 Eval simpl in matches hi "bye".
adamc@87 1207
adamc@87 1208 Example a_b := Or (Char "a"%char) (Char "b"%char).
adamc@87 1209 Eval simpl in matches a_b "".
adamc@87 1210 Eval simpl in matches a_b "a".
adamc@87 1211 Eval simpl in matches a_b "aa".
adamc@87 1212 Eval simpl in matches a_b "b".
adam@283 1213 (* end hide *)
adam@283 1214
adam@283 1215 (** 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 1216
adamc@91 1217 Example a_star := Star (Char "a"%char).
adamc@91 1218 Eval simpl in matches a_star "".
adamc@91 1219 Eval simpl in matches a_star "a".
adamc@91 1220 Eval simpl in matches a_star "b".
adamc@91 1221 Eval simpl in matches a_star "aa".
adam@283 1222
adam@283 1223 (** 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 1224
adamc@101 1225
adamc@101 1226 (** * Exercises *)
adamc@101 1227
adamc@101 1228 (** %\begin{enumerate}%#<ol>#
adamc@101 1229
adamc@101 1230 %\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 1231 %\begin{enumerate}%#<ol>#
adamc@101 1232 %\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 1233 %\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 1234 %\item%#<li># Define a function [plistOut] for translating [plist]s to normal [list]s.#</li>#
adamc@101 1235 %\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 1236 %\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>#
adamc@101 1237 %\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. [sig] is the type family of sigma types, 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 1238 #</ol>#%\end{enumerate}% #</li>#
adamc@101 1239
adamc@102 1240 #</ol>#%\end{enumerate}% *)