Mercurial > cpdt > repo

annotate src/MoreDep.v @ 546:306539f29eea

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Make specially licensed versions of lib files for cpdtlib.tgz. This adds an ocaml tool and calls to it in the Makefile.
author Arthur Peters <amp@singingwizard.org>
date Thu, 12 May 2016 18:09:36 -0500
parents ed829eaa91b2
children af97676583f3
rev   line source
adam@534 1 (* Copyright (c) 2008-2012, 2015, 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 *)
adam@534 11 Require Import Arith Bool List Omega.
adamc@83 12
adam@534 13 Require Import Cpdt.CpdtTactics Cpdt.MoreSpecif.
adamc@83 14
adamc@83 15 Set Implicit Arguments.
adam@534 16 Set Asymmetric Patterns.
adamc@83 17 (* end hide *)
adamc@83 18
adamc@83 19
adamc@83 20 (** %\chapter{More Dependent Types}% *)
adamc@83 21
adam@425 22 (** 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 23
adam@476 24 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 outside [Prop], a possibility that sets Coq apart from all of the competition not based on type theory. *)
adamc@83 25
adamc@84 26
adamc@84 27 (** * Length-Indexed Lists *)
adamc@84 28
adam@338 29 (** 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 30
adamc@84 31 Section ilist.
adamc@84 32 Variable A : Set.
adamc@84 33
adamc@84 34 Inductive ilist : nat -> Set :=
adamc@84 35 | Nil : ilist O
adamc@84 36 | Cons : forall n, A -> ilist n -> ilist (S n).
adamc@84 37
adamc@84 38 (** 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 39
adam@405 40 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}% _phase distinction_ that characterizes [ilist] as _dependently typed_.
adamc@84 41
adamc@213 42 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 43
adamc@213 44 Fixpoint app n1 (ls1 : ilist n1) n2 (ls2 : ilist n2) : ilist (n1 + n2) :=
adamc@213 45 match ls1 with
adamc@213 46 | Nil => ls2
adamc@213 47 | Cons _ x ls1' => Cons x (app ls1' ls2)
adamc@213 48 end.
adamc@84 49
adam@338 50 (** 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 51
adamc@100 52 (* begin thide *)
adam@338 53 Fixpoint app' n1 (ls1 : ilist n1) n2 (ls2 : ilist n2) : ilist (n1 + n2) :=
adam@338 54 match ls1 in (ilist n1) return (ilist (n1 + n2)) with
adam@338 55 | Nil => ls2
adam@338 56 | Cons _ x ls1' => Cons x (app' ls1' ls2)
adam@338 57 end.
adamc@100 58 (* end thide *)
adamc@84 59
adam@398 60 (** Using [return] alone allowed us to express a dependency of the [match] result type on the _value_ of the discriminee. What %\index{Gallina terms!in}%[in] adds to our arsenal is a way of expressing a dependency on the _type_ of the discriminee. Specifically, the [n1] in the [in] clause above is a _binding occurrence_ whose scope is the [return] clause.
adamc@84 61
adam@398 62 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 _parameters_ 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 63
adam@484 64 Our [app] function could be typed in so-called%\index{stratified type systems}% _stratified_ 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. Compile-time data may be _erased_ such that we can still execute a program. As an example where erasure would not work, consider an injection function from regular lists to length-indexed lists. Here the run-time computation actually depends on details of the compile-time argument, if we decide that the list to inject can be considered compile-time. More commonly, we think of lists as run-time data. Neither case will work with %\%naive%{}% erasure. (It is not too important to grasp the details of this run-time/compile-time distinction, since Coq's expressive power comes from avoiding such restrictions.) *)
adamc@84 65
adamc@100 66 (* EX: Implement injection from normal lists *)
adamc@100 67
adamc@100 68 (* begin thide *)
adam@454 69 Fixpoint inject (ls : list A) : ilist (length ls) :=
adam@454 70 match ls with
adam@454 71 | nil => Nil
adam@454 72 | h :: t => Cons h (inject t)
adam@454 73 end.
adamc@84 74
adamc@84 75 (** We can define an inverse conversion and prove that it really is an inverse. *)
adamc@84 76
adam@454 77 Fixpoint unject n (ls : ilist n) : list A :=
adam@454 78 match ls with
adam@454 79 | Nil => nil
adam@454 80 | Cons _ h t => h :: unject t
adam@454 81 end.
adamc@84 82
adam@454 83 Theorem inject_inverse : forall ls, unject (inject ls) = ls.
adam@454 84 induction ls; crush.
adam@454 85 Qed.
adamc@100 86 (* end thide *)
adamc@100 87
adam@338 88 (* EX: Implement statically checked "car"/"hd" *)
adamc@84 89
adam@425 90 (** Now let us attempt a function that is surprisingly tricky to write. In ML, the list head function raises an exception when passed an empty list. With length-indexed lists, we can rule out such invalid calls statically, and here is a first attempt at doing so. We write [???] as a placeholder for a term that we do not know how to write, not for any real Coq notation like those introduced two chapters ago.
adamc@84 91 [[
adam@454 92 Definition hd n (ls : ilist (S n)) : A :=
adam@454 93 match ls with
adam@454 94 | Nil => ???
adam@454 95 | Cons _ h _ => h
adam@454 96 end.
adamc@213 97 ]]
adamc@84 98 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 99 [[
adam@454 100 Definition hd n (ls : ilist (S n)) : A :=
adam@454 101 match ls with
adam@454 102 | Cons _ h _ => h
adam@454 103 end.
adam@338 104 ]]
adamc@84 105
adam@338 106 <<
adamc@84 107 Error: Non exhaustive pattern-matching: no clause found for pattern Nil
adam@338 108 >>
adamc@84 109
adam@480 110 Unlike in ML, we cannot use inexhaustive pattern matching, because there is no conception of a <<Match>> exception to be thrown. In fact, recent versions of Coq _do_ allow this, by implicit translation to a [match] that considers all constructors; the error message above was generated by an older Coq version. It is educational to discover for ourselves the encoding that the most recent Coq versions use. We might try using an [in] clause somehow.
adamc@84 111
adamc@84 112 [[
adam@454 113 Definition hd n (ls : ilist (S n)) : A :=
adam@454 114 match ls in (ilist (S n)) with
adam@454 115 | Cons _ h _ => h
adam@454 116 end.
adamc@84 117 ]]
adamc@84 118
adam@338 119 <<
adam@338 120 Error: The reference n was not found in the current environment
adam@338 121 >>
adam@338 122
adam@398 123 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 _are_ 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 124
adamc@84 125 Our final, working attempt at [hd] uses an auxiliary function and a surprising [return] annotation. *)
adamc@84 126
adamc@100 127 (* begin thide *)
adam@454 128 Definition hd' n (ls : ilist n) :=
adam@454 129 match ls in (ilist n) return (match n with O => unit | S _ => A end) with
adam@454 130 | Nil => tt
adam@454 131 | Cons _ h _ => h
adam@454 132 end.
adamc@84 133
adam@454 134 Check hd'.
adam@283 135 (** %\vspace{-.15in}% [[
adam@283 136 hd'
adam@283 137 : forall n : nat, ilist n -> match n with
adam@283 138 | 0 => unit
adam@283 139 | S _ => A
adam@283 140 end
adam@302 141 ]]
adam@302 142 *)
adam@283 143
adam@454 144 Definition hd n (ls : ilist (S n)) : A := hd' ls.
adamc@100 145 (* end thide *)
adamc@84 146
adam@338 147 End ilist.
adam@338 148
adamc@84 149 (** 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 150
adamc@85 151
adam@371 152 (** * The One Rule of Dependent Pattern Matching in Coq *)
adam@371 153
adam@405 154 (** The rest of this chapter will demonstrate a few other elegant applications of dependent types in Coq. Readers encountering such ideas for the first time often feel overwhelmed, concluding that there is some magic at work whereby Coq sometimes solves the halting problem for the programmer and sometimes does not, applying automated program understanding in a way far beyond what is found in conventional languages. The point of this section is to cut off that sort of thinking right now! Dependent type-checking in Coq follows just a few algorithmic rules. Chapters 10 and 12 introduce many of those rules more formally, and the main additional rule is centered on%\index{dependent pattern matching}% _dependent pattern matching_ of the kind we met in the previous section.
adam@371 155
adam@405 156 A dependent pattern match is a [match] expression where the type of the overall [match] is a function of the value and/or the type of the%\index{discriminee}% _discriminee_, the value being matched on. In other words, the [match] type _depends_ on the discriminee.
adam@371 157
adam@398 158 When exactly will Coq accept a dependent pattern match as well-typed? Some other dependently typed languages employ fancy decision procedures to determine when programs satisfy their very expressive types. The situation in Coq is just the opposite. Only very straightforward symbolic rules are applied. Such a design choice has its drawbacks, as it forces programmers to do more work to convince the type checker of program validity. However, the great advantage of a simple type checking algorithm is that its action on _invalid_ programs is easier to understand!
adam@371 159
adam@371 160 We come now to the one rule of dependent pattern matching in Coq. A general dependent pattern match assumes this form (with unnecessary parentheses included to make the syntax easier to parse):
adam@371 161 [[
adam@480 162 match E as y in (T x1 ... xn) return U with
adam@371 163 | C z1 ... zm => B
adam@371 164 | ...
adam@371 165 end
adam@371 166 ]]
adam@371 167
adam@480 168 The discriminee is a term [E], a value in some inductive type family [T], which takes [n] arguments. An %\index{as clause}%[as] clause binds the name [y] to refer to the discriminee [E]. An %\index{in clause}%[in] clause binds an explicit name [xi] for the [i]th argument passed to [T] in the type of [E].
adam@371 169
adam@480 170 We bind these new variables [y] and [xi] so that they may be referred to in [U], a type given in the %\index{return clause}%[return] clause. The overall type of the [match] will be [U], with [E] substituted for [y], and with each [xi] substituted by the actual argument appearing in that position within [E]'s type.
adam@371 171
adam@371 172 In general, each case of a [match] may have a pattern built up in several layers from the constructors of various inductive type families. To keep this exposition simple, we will focus on patterns that are just single applications of inductive type constructors to lists of variables. Coq actually compiles the more general kind of pattern matching into this more restricted kind automatically, so understanding the typing of [match] requires understanding the typing of [match]es lowered to match one constructor at a time.
adam@371 173
adam@371 174 The last piece of the typing rule tells how to type-check a [match] case. A generic constructor application [C z1 ... zm] has some type [T x1' ... xn'], an application of the type family used in [E]'s type, probably with occurrences of the [zi] variables. From here, a simple recipe determines what type we will require for the case body [B]. The type of [B] should be [U] with the following two substitutions applied: we replace [y] (the [as] clause variable) with [C z1 ... zm], and we replace each [xi] (the [in] clause variables) with [xi']. In other words, we specialize the result type based on what we learn based on which pattern has matched the discriminee.
adam@371 175
adam@371 176 This is an exhaustive description of the ways to specify how to take advantage of which pattern has matched! No other mechanisms come into play. For instance, there is no way to specify that the types of certain free variables should be refined based on which pattern has matched. In the rest of the book, we will learn design patterns for achieving similar effects, where each technique leads to an encoding only in terms of [in], [as], and [return] clauses.
adam@371 177
adam@425 178 A few details have been omitted above. In Chapter 3, we learned that inductive type families may have both%\index{parameters}% _parameters_ and regular arguments. Within an [in] clause, a parameter position must have the wildcard [_] written, instead of a variable. (In general, Coq uses wildcard [_]'s either to indicate pattern variables that will not be mentioned again or to indicate positions where we would like type inference to infer the appropriate terms.) Furthermore, recent Coq versions are adding more and more heuristics to infer dependent [match] annotations in certain conditions. The general annotation inference problem is undecidable, so there will always be serious limitations on how much work these heuristics can do. When in doubt about why a particular dependent [match] is failing to type-check, add an explicit [return] annotation! At that point, the mechanical rule sketched in this section will provide a complete account of "what the type checker is thinking." Be sure to avoid the common pitfall of writing a [return] annotation that does not mention any variables bound by [in] or [as]; such a [match] will never refine typing requirements based on which pattern has matched. (One simple exception to this rule is that, when the discriminee is a variable, that same variable may be treated as if it were repeated as an [as] clause.) *)
adam@371 179
adam@371 180
adamc@85 181 (** * A Tagless Interpreter *)
adamc@85 182
adam@405 183 (** 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}% _tagless_ interpreter that both removes this source of runtime inefficiency and gives us more confidence that our implementation is correct. *)
adamc@85 184
adamc@85 185 Inductive type : Set :=
adamc@85 186 | Nat : type
adamc@85 187 | Bool : type
adamc@85 188 | Prod : type -> type -> type.
adamc@85 189
adamc@85 190 Inductive exp : type -> Set :=
adamc@85 191 | NConst : nat -> exp Nat
adamc@85 192 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@85 193 | Eq : exp Nat -> exp Nat -> exp Bool
adamc@85 194
adamc@85 195 | BConst : bool -> exp Bool
adamc@85 196 | And : exp Bool -> exp Bool -> exp Bool
adamc@85 197 | If : forall t, exp Bool -> exp t -> exp t -> exp t
adamc@85 198
adamc@85 199 | Pair : forall t1 t2, exp t1 -> exp t2 -> exp (Prod t1 t2)
adamc@85 200 | Fst : forall t1 t2, exp (Prod t1 t2) -> exp t1
adamc@85 201 | Snd : forall t1 t2, exp (Prod t1 t2) -> exp t2.
adamc@85 202
adam@448 203 (** 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 204
adam@398 205 We can give types and expressions semantics in a new style, based critically on the chance for _type-level computation_. *)
adamc@85 206
adamc@85 207 Fixpoint typeDenote (t : type) : Set :=
adamc@85 208 match t with
adamc@85 209 | Nat => nat
adamc@85 210 | Bool => bool
adamc@85 211 | Prod t1 t2 => typeDenote t1 * typeDenote t2
adamc@85 212 end%type.
adamc@85 213
adam@465 214 (** 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 [%]%\coqdocvar{%#<tt>#type#</tt>#%}% 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 %\coqdocvar{%#<tt>#type#</tt>#%}% is one example of an identifier bound to a%\index{notation scope delimiter}% _notation scope delimiter_. 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 215
adamc@85 216 We can define a function [expDenote] that is typed in terms of [typeDenote]. *)
adamc@85 217
adamc@213 218 Fixpoint expDenote t (e : exp t) : typeDenote t :=
adamc@213 219 match e with
adamc@85 220 | NConst n => n
adamc@85 221 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@85 222 | Eq e1 e2 => if eq_nat_dec (expDenote e1) (expDenote e2) then true else false
adamc@85 223
adamc@85 224 | BConst b => b
adamc@85 225 | And e1 e2 => expDenote e1 && expDenote e2
adamc@85 226 | If _ e' e1 e2 => if expDenote e' then expDenote e1 else expDenote e2
adamc@85 227
adamc@85 228 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@85 229 | Fst _ _ e' => fst (expDenote e')
adamc@85 230 | Snd _ _ e' => snd (expDenote e')
adamc@85 231 end.
adamc@85 232
adam@437 233 (* begin hide *)
adam@437 234 (* begin thide *)
adam@437 235 Definition sumboool := sumbool.
adam@437 236 (* end thide *)
adam@437 237 (* end hide *)
adam@437 238
adam@448 239 (** 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 240
adamc@85 241 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 242 [[
adamc@85 243 Definition pairOut t1 t2 (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) :=
adamc@85 244 match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with
adamc@85 245 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@85 246 | _ => None
adamc@85 247 end.
adam@338 248 ]]
adamc@85 249
adam@338 250 <<
adamc@85 251 Error: The reference t2 was not found in the current environment
adam@338 252 >>
adamc@85 253
adamc@85 254 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 255
adamc@100 256 (* EX: Define a function [pairOut : forall t1 t2, exp (Prod t1 t2) -> option (exp t1 * exp t2)] *)
adamc@100 257
adamc@100 258 (* begin thide *)
adam@499 259 Definition pairOutType (t : type) := option (match t with
adam@499 260 | Prod t1 t2 => exp t1 * exp t2
adam@499 261 | _ => unit
adam@499 262 end).
adamc@85 263
adam@499 264 (** When passed a type that is a product, [pairOutType] returns our final desired type. On any other input type, [pairOutType] returns the harmless [option unit], since we do not care about extracting components of non-pairs. Now [pairOut] is easy to write. *)
adamc@85 265
adamc@85 266 Definition pairOut t (e : exp t) :=
adamc@85 267 match e in (exp t) return (pairOutType t) with
adamc@85 268 | Pair _ _ e1 e2 => Some (e1, e2)
adam@499 269 | _ => None
adamc@85 270 end.
adamc@100 271 (* end thide *)
adamc@85 272
adam@499 273 (** 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 with explicit [return] clauses. *)
adamc@85 274
adamc@204 275 Fixpoint cfold t (e : exp t) : exp t :=
adamc@204 276 match e with
adamc@85 277 | NConst n => NConst n
adamc@85 278 | Plus e1 e2 =>
adamc@85 279 let e1' := cfold e1 in
adamc@85 280 let e2' := cfold e2 in
adam@417 281 match e1', e2' return exp Nat with
adamc@85 282 | NConst n1, NConst n2 => NConst (n1 + n2)
adamc@85 283 | _, _ => Plus e1' e2'
adamc@85 284 end
adamc@85 285 | Eq e1 e2 =>
adamc@85 286 let e1' := cfold e1 in
adamc@85 287 let e2' := cfold e2 in
adam@417 288 match e1', e2' return exp Bool with
adamc@85 289 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
adamc@85 290 | _, _ => Eq e1' e2'
adamc@85 291 end
adamc@85 292
adamc@85 293 | BConst b => BConst b
adamc@85 294 | And e1 e2 =>
adamc@85 295 let e1' := cfold e1 in
adamc@85 296 let e2' := cfold e2 in
adam@417 297 match e1', e2' return exp Bool with
adamc@85 298 | BConst b1, BConst b2 => BConst (b1 && b2)
adamc@85 299 | _, _ => And e1' e2'
adamc@85 300 end
adamc@85 301 | If _ e e1 e2 =>
adamc@85 302 let e' := cfold e in
adamc@85 303 match e' with
adamc@85 304 | BConst true => cfold e1
adamc@85 305 | BConst false => cfold e2
adamc@85 306 | _ => If e' (cfold e1) (cfold e2)
adamc@85 307 end
adamc@85 308
adamc@85 309 | Pair _ _ e1 e2 => Pair (cfold e1) (cfold e2)
adamc@85 310 | Fst _ _ e =>
adamc@85 311 let e' := cfold e in
adamc@85 312 match pairOut e' with
adamc@85 313 | Some p => fst p
adamc@85 314 | None => Fst e'
adamc@85 315 end
adamc@85 316 | Snd _ _ e =>
adamc@85 317 let e' := cfold e in
adamc@85 318 match pairOut e' with
adamc@85 319 | Some p => snd p
adamc@85 320 | None => Snd e'
adamc@85 321 end
adamc@85 322 end.
adamc@85 323
adamc@85 324 (** The correctness theorem for [cfold] turns out to be easy to prove, once we get over one serious hurdle. *)
adamc@85 325
adamc@85 326 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
adamc@100 327 (* begin thide *)
adamc@85 328 induction e; crush.
adamc@85 329
adamc@85 330 (** The first remaining subgoal is:
adamc@85 331
adamc@85 332 [[
adamc@85 333 expDenote (cfold e1) + expDenote (cfold e2) =
adamc@85 334 expDenote
adamc@85 335 match cfold e1 with
adamc@85 336 | NConst n1 =>
adamc@85 337 match cfold e2 with
adamc@85 338 | NConst n2 => NConst (n1 + n2)
adamc@85 339 | Plus _ _ => Plus (cfold e1) (cfold e2)
adamc@85 340 | Eq _ _ => Plus (cfold e1) (cfold e2)
adamc@85 341 | BConst _ => Plus (cfold e1) (cfold e2)
adamc@85 342 | And _ _ => Plus (cfold e1) (cfold e2)
adamc@85 343 | If _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 344 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 345 | Fst _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 346 | Snd _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 347 end
adamc@85 348 | Plus _ _ => Plus (cfold e1) (cfold e2)
adamc@85 349 | Eq _ _ => Plus (cfold e1) (cfold e2)
adamc@85 350 | BConst _ => Plus (cfold e1) (cfold e2)
adamc@85 351 | And _ _ => Plus (cfold e1) (cfold e2)
adamc@85 352 | If _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 353 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 354 | Fst _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 355 | Snd _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 356 end
adamc@213 357
adamc@85 358 ]]
adamc@85 359
adam@454 360 We would like to do a case analysis on [cfold e1], and we attempt to do so in the way that has worked so far.
adamc@85 361 [[
adamc@85 362 destruct (cfold e1).
adam@338 363 ]]
adamc@85 364
adam@338 365 <<
adamc@85 366 User error: e1 is used in hypothesis e
adam@338 367 >>
adamc@85 368
adamc@85 369 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 370
adam@499 371 For our current proof, we can use a tactic [dep_destruct]%\index{tactics!dep\_destruct}% defined in the book's [CpdtTactics] module. General elimination/inversion of dependently typed hypotheses is undecidable, as witnessed by a simple reduction from the known-undecidable problem of higher-order unification, which has come up a few times already. 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 [dependent destruction]'s implementation, 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 372
adamc@85 373 dep_destruct (cfold e1).
adamc@85 374
adamc@85 375 (** 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 376
adam@480 377 This is the only new trick we need to learn to complete the proof. We can back up and give a short, automated proof (which again is safe to skip and uses Ltac features not introduced yet). *)
adamc@85 378
adamc@85 379 Restart.
adamc@85 380
adamc@85 381 induction e; crush;
adamc@85 382 repeat (match goal with
adam@405 383 | [ |- context[match cfold ?E with NConst _ => _ | _ => _ end] ] =>
adamc@213 384 dep_destruct (cfold E)
adamc@213 385 | [ |- context[match pairOut (cfold ?E) with Some _ => _
adamc@213 386 | None => _ end] ] =>
adamc@213 387 dep_destruct (cfold E)
adamc@85 388 | [ |- (if ?E then _ else _) = _ ] => destruct E
adamc@85 389 end; crush).
adamc@85 390 Qed.
adamc@100 391 (* end thide *)
adamc@86 392
adam@405 393 (** With this example, we get a first taste of how to build automated proofs that adapt automatically to changes in function definitions. *)
adam@405 394
adamc@86 395
adam@338 396 (** * Dependently Typed Red-Black Trees *)
adamc@94 397
adam@475 398 (** Red-black trees are a favorite purely functional data structure with an interesting invariant. We can use dependent types to guarantee 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 399
adamc@94 400 Inductive color : Set := Red | Black.
adamc@94 401
adamc@94 402 Inductive rbtree : color -> nat -> Set :=
adamc@94 403 | Leaf : rbtree Black 0
adamc@214 404 | RedNode : forall n, rbtree Black n -> nat -> rbtree Black n -> rbtree Red n
adamc@94 405 | BlackNode : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rbtree Black (S n).
adamc@94 406
adam@476 407 (** A value of type [rbtree c d] is a red-black tree whose root has color [c] and that has black depth [d]. The latter property means that there are exactly [d] black-colored nodes on any path from the root to a leaf. *)
adamc@214 408
adamc@214 409 (** 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 410
adamc@100 411 (* EX: Prove that every [rbtree] is balanced. *)
adamc@100 412
adamc@100 413 (* begin thide *)
adamc@95 414 Require Import Max Min.
adamc@95 415
adamc@95 416 Section depth.
adamc@95 417 Variable f : nat -> nat -> nat.
adamc@95 418
adamc@214 419 Fixpoint depth c n (t : rbtree c n) : nat :=
adamc@95 420 match t with
adamc@95 421 | Leaf => 0
adamc@95 422 | RedNode _ t1 _ t2 => S (f (depth t1) (depth t2))
adamc@95 423 | BlackNode _ _ _ t1 _ t2 => S (f (depth t1) (depth t2))
adamc@95 424 end.
adamc@95 425 End depth.
adamc@95 426
adam@338 427 (** 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 428
adam@283 429 Check min_dec.
adam@283 430 (** %\vspace{-.15in}% [[
adam@283 431 min_dec
adam@283 432 : forall n m : nat, {min n m = n} + {min n m = m}
adam@302 433 ]]
adam@302 434 *)
adam@283 435
adamc@95 436 Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n.
adamc@95 437 induction t; crush;
adamc@95 438 match goal with
adamc@95 439 | [ |- context[min ?X ?Y] ] => destruct (min_dec X Y)
adamc@95 440 end; crush.
adamc@95 441 Qed.
adamc@95 442
adamc@214 443 (** There is an analogous upper-bound theorem based on black depth. Unfortunately, a symmetric proof script does not suffice to establish it. *)
adamc@214 444
adamc@214 445 Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
adamc@214 446 induction t; crush;
adamc@214 447 match goal with
adamc@214 448 | [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
adamc@214 449 end; crush.
adamc@214 450
adamc@214 451 (** Two subgoals remain. One of them is: [[
adamc@214 452 n : nat
adamc@214 453 t1 : rbtree Black n
adamc@214 454 n0 : nat
adamc@214 455 t2 : rbtree Black n
adamc@214 456 IHt1 : depth max t1 <= n + (n + 0) + 1
adamc@214 457 IHt2 : depth max t2 <= n + (n + 0) + 1
adamc@214 458 e : max (depth max t1) (depth max t2) = depth max t1
adamc@214 459 ============================
adamc@214 460 S (depth max t1) <= n + (n + 0) + 1
adamc@214 461
adamc@214 462 ]]
adamc@214 463
adam@398 464 We see that [IHt1] is _almost_ 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 465
adamc@214 466 Abort.
adamc@214 467
adamc@214 468 (** 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 469
adamc@95 470 Lemma depth_max' : forall c n (t : rbtree c n), match c with
adamc@95 471 | Red => depth max t <= 2 * n + 1
adamc@95 472 | Black => depth max t <= 2 * n
adamc@95 473 end.
adamc@95 474 induction t; crush;
adamc@95 475 match goal with
adamc@95 476 | [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
adamc@100 477 end; crush;
adamc@100 478 repeat (match goal with
adamc@214 479 | [ H : context[match ?C with Red => _ | Black => _ end] |- _ ] =>
adamc@214 480 destruct C
adamc@100 481 end; crush).
adamc@95 482 Qed.
adamc@95 483
adam@338 484 (** 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 485
adamc@95 486 Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
adamc@95 487 intros; generalize (depth_max' t); destruct c; crush.
adamc@95 488 Qed.
adamc@95 489
adamc@214 490 (** 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 491
adamc@95 492 Theorem balanced : forall c n (t : rbtree c n), 2 * depth min t + 1 >= depth max t.
adamc@95 493 intros; generalize (depth_min t); generalize (depth_max t); crush.
adamc@95 494 Qed.
adamc@100 495 (* end thide *)
adamc@95 496
adamc@214 497 (** 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 498
adamc@94 499 Inductive rtree : nat -> Set :=
adamc@94 500 | RedNode' : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rtree n.
adamc@94 501
adam@338 502 (** 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 503
adamc@96 504 Section present.
adamc@96 505 Variable x : nat.
adamc@96 506
adamc@214 507 Fixpoint present c n (t : rbtree c n) : Prop :=
adamc@96 508 match t with
adamc@96 509 | Leaf => False
adamc@96 510 | RedNode _ a y b => present a \/ x = y \/ present b
adamc@96 511 | BlackNode _ _ _ a y b => present a \/ x = y \/ present b
adamc@96 512 end.
adamc@96 513
adamc@96 514 Definition rpresent n (t : rtree n) : Prop :=
adamc@96 515 match t with
adamc@96 516 | RedNode' _ _ _ a y b => present a \/ x = y \/ present b
adamc@96 517 end.
adamc@96 518 End present.
adamc@96 519
adam@338 520 (** 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 521
adamc@100 522 Locate "{ _ : _ & _ }".
adam@443 523 (** %\vspace{-.15in}%[[
adamc@214 524 Notation Scope
adamc@214 525 "{ x : A & P }" := sigT (fun x : A => P)
adam@302 526 ]]
adam@302 527 *)
adamc@214 528
adamc@100 529 Print sigT.
adam@443 530 (** %\vspace{-.15in}%[[
adamc@214 531 Inductive sigT (A : Type) (P : A -> Type) : Type :=
adamc@214 532 existT : forall x : A, P x -> sigT P
adam@302 533 ]]
adam@302 534 *)
adamc@214 535
adamc@214 536 (** It will be helpful to define a concise notation for the constructor of [sigT]. *)
adamc@100 537
adamc@94 538 Notation "{< x >}" := (existT _ _ x).
adamc@94 539
adamc@214 540 (** 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 541
adam@338 542 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 543
adam@425 544 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 545
adamc@94 546 Definition balance1 n (a : rtree n) (data : nat) c2 :=
adamc@214 547 match a in rtree n return rbtree c2 n
adamc@214 548 -> { c : color & rbtree c (S n) } with
adam@380 549 | RedNode' _ c0 _ t1 y t2 =>
adam@380 550 match t1 in rbtree c n return rbtree c0 n -> rbtree c2 n
adamc@214 551 -> { c : color & rbtree c (S n) } with
adamc@214 552 | RedNode _ a x b => fun c d =>
adamc@214 553 {<RedNode (BlackNode a x b) y (BlackNode c data d)>}
adamc@94 554 | t1' => fun t2 =>
adam@380 555 match t2 in rbtree c n return rbtree Black n -> rbtree c2 n
adamc@214 556 -> { c : color & rbtree c (S n) } with
adamc@214 557 | RedNode _ b x c => fun a d =>
adamc@214 558 {<RedNode (BlackNode a y b) x (BlackNode c data d)>}
adamc@95 559 | b => fun a t => {<BlackNode (RedNode a y b) data t>}
adamc@94 560 end t1'
adamc@94 561 end t2
adamc@94 562 end.
adamc@94 563
adam@405 564 (** We apply a trick that I call the%\index{convoy pattern}% _convoy pattern_. Recall that [match] annotations only make it possible to describe a dependence of a [match] _result type_ 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 565
adam@425 566 In particular, we can extend the [match] to return _functions over the free variables whose types we want to refine_. 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 567
adam@338 568 Here is the symmetric function [balance2], for cases where the possibly invalid tree appears on the right rather than on the left. *)
adamc@214 569
adamc@94 570 Definition balance2 n (a : rtree n) (data : nat) c2 :=
adamc@94 571 match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with
adam@380 572 | RedNode' _ c0 _ t1 z t2 =>
adam@380 573 match t1 in rbtree c n return rbtree c0 n -> rbtree c2 n
adamc@214 574 -> { c : color & rbtree c (S n) } with
adamc@214 575 | RedNode _ b y c => fun d a =>
adamc@214 576 {<RedNode (BlackNode a data b) y (BlackNode c z d)>}
adamc@94 577 | t1' => fun t2 =>
adam@380 578 match t2 in rbtree c n return rbtree Black n -> rbtree c2 n
adamc@214 579 -> { c : color & rbtree c (S n) } with
adamc@214 580 | RedNode _ c z' d => fun b a =>
adamc@214 581 {<RedNode (BlackNode a data b) z (BlackNode c z' d)>}
adamc@95 582 | b => fun a t => {<BlackNode t data (RedNode a z b)>}
adamc@94 583 end t1'
adamc@94 584 end t2
adamc@94 585 end.
adamc@94 586
adamc@214 587 (** 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 588
adamc@94 589 Section insert.
adamc@94 590 Variable x : nat.
adamc@94 591
adamc@214 592 (** 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 593
adamc@94 594 Definition insResult c n :=
adamc@94 595 match c with
adamc@94 596 | Red => rtree n
adamc@94 597 | Black => { c' : color & rbtree c' n }
adamc@94 598 end.
adamc@94 599
adam@338 600 (** 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 601
adamc@214 602 Here is the definition of [ins]. Again, we do not want to dwell on the functional details. *)
adamc@214 603
adamc@214 604 Fixpoint ins c n (t : rbtree c n) : insResult c n :=
adamc@214 605 match t with
adamc@94 606 | Leaf => {< RedNode Leaf x Leaf >}
adamc@94 607 | RedNode _ a y b =>
adamc@94 608 if le_lt_dec x y
adamc@94 609 then RedNode' (projT2 (ins a)) y b
adamc@94 610 else RedNode' a y (projT2 (ins b))
adamc@94 611 | BlackNode c1 c2 _ a y b =>
adamc@94 612 if le_lt_dec x y
adamc@94 613 then
adamc@94 614 match c1 return insResult c1 _ -> _ with
adamc@94 615 | Red => fun ins_a => balance1 ins_a y b
adamc@94 616 | _ => fun ins_a => {< BlackNode (projT2 ins_a) y b >}
adamc@94 617 end (ins a)
adamc@94 618 else
adamc@94 619 match c2 return insResult c2 _ -> _ with
adamc@94 620 | Red => fun ins_b => balance2 ins_b y a
adamc@94 621 | _ => fun ins_b => {< BlackNode a y (projT2 ins_b) >}
adamc@94 622 end (ins b)
adamc@94 623 end.
adamc@94 624
adam@479 625 (** 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 %\%naive%{}%ly 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 _the result of a recursive call_, rather than just on that call's argument.
adamc@214 626
adamc@214 627 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 628
adamc@94 629 Definition insertResult c n :=
adamc@94 630 match c with
adamc@94 631 | Red => rbtree Black (S n)
adamc@94 632 | Black => { c' : color & rbtree c' n }
adamc@94 633 end.
adamc@94 634
adamc@214 635 (** A simple clean-up procedure translates [insResult]s into [insertResult]s. *)
adamc@214 636
adamc@97 637 Definition makeRbtree c n : insResult c n -> insertResult c n :=
adamc@214 638 match c with
adamc@94 639 | Red => fun r =>
adamc@214 640 match r with
adamc@94 641 | RedNode' _ _ _ a x b => BlackNode a x b
adamc@94 642 end
adamc@94 643 | Black => fun r => r
adamc@94 644 end.
adamc@94 645
adamc@214 646 (** 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 647
adamc@97 648 Implicit Arguments makeRbtree [c n].
adamc@94 649
adamc@214 650 (** Finally, we define [insert] as a simple composition of [ins] and [makeRbtree]. *)
adamc@214 651
adamc@94 652 Definition insert c n (t : rbtree c n) : insertResult c n :=
adamc@97 653 makeRbtree (ins t).
adamc@94 654
adamc@214 655 (** 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 656
adamc@95 657 Section present.
adamc@95 658 Variable z : nat.
adamc@95 659
adamc@214 660 (** 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 661
adam@367 662 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 663
adamc@98 664 Ltac present_balance :=
adamc@98 665 crush;
adamc@98 666 repeat (match goal with
adam@425 667 | [ _ : context[match ?T with Leaf => _ | _ => _ end] |- _ ] =>
adam@425 668 dep_destruct T
adam@405 669 | [ |- context[match ?T with Leaf => _ | _ => _ end] ] => dep_destruct T
adamc@98 670 end; crush).
adamc@98 671
adamc@214 672 (** 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 673
adam@294 674 Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n),
adamc@95 675 present z (projT2 (balance1 a y b))
adamc@95 676 <-> rpresent z a \/ z = y \/ present z b.
adamc@98 677 destruct a; present_balance.
adamc@95 678 Qed.
adamc@95 679
adamc@213 680 Lemma present_balance2 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n),
adamc@95 681 present z (projT2 (balance2 a y b))
adamc@95 682 <-> rpresent z a \/ z = y \/ present z b.
adamc@98 683 destruct a; present_balance.
adamc@95 684 Qed.
adamc@95 685
adamc@214 686 (** 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 687
adamc@95 688 Definition present_insResult c n :=
adamc@95 689 match c return (rbtree c n -> insResult c n -> Prop) with
adamc@95 690 | Red => fun t r => rpresent z r <-> z = x \/ present z t
adamc@95 691 | Black => fun t r => present z (projT2 r) <-> z = x \/ present z t
adamc@95 692 end.
adamc@95 693
adamc@214 694 (** 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 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
adam@338 700 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
adamc@95 701 | [ |- context[if ?E then _ else _] ] => destruct E
adam@338 702 | [ _ : context[match ?C with Red => _ | Black => _ end]
adamc@214 703 |- _ ] => destruct C
adamc@95 704 end; crush);
adamc@95 705 try match goal with
adam@338 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
adam@338 710 | [ _ : 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 (** 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 732
adamc@213 733 Ltac present_insert :=
adamc@213 734 unfold insert; intros n t; inversion t;
adamc@97 735 generalize (present_ins t); simpl;
adamc@97 736 dep_destruct (ins t); tauto.
adamc@97 737
adamc@95 738 Theorem present_insert_Red : forall n (t : rbtree Red n),
adamc@95 739 present z (insert t)
adamc@95 740 <-> (z = x \/ present z t).
adamc@213 741 present_insert.
adamc@95 742 Qed.
adamc@95 743
adamc@95 744 Theorem present_insert_Black : forall n (t : rbtree Black n),
adamc@95 745 present z (projT2 (insert t))
adamc@95 746 <-> (z = x \/ present z t).
adamc@213 747 present_insert.
adamc@95 748 Qed.
adamc@95 749 End present.
adamc@94 750 End insert.
adamc@94 751
adam@454 752 (** 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}%<<Obj.magic>>, 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 _value_ of the function's argument, a pattern that 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 753
adam@338 754 (* begin hide *)
adam@338 755 Recursive Extraction insert.
adam@338 756 (* end hide *)
adam@283 757
adamc@94 758
adamc@86 759 (** * A Certified Regular Expression Matcher *)
adamc@86 760
adamc@93 761 (** 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 762
adam@425 763 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 [String] 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 764
adamc@86 765 Require Import Ascii String.
adamc@86 766 Open Scope string_scope.
adamc@86 767
adamc@91 768 Section star.
adamc@91 769 Variable P : string -> Prop.
adamc@91 770
adamc@91 771 Inductive star : string -> Prop :=
adamc@91 772 | Empty : star ""
adamc@91 773 | Iter : forall s1 s2,
adamc@91 774 P s1
adamc@91 775 -> star s2
adamc@91 776 -> star (s1 ++ s2).
adamc@91 777 End star.
adamc@91 778
adam@480 779 (** Now we can make our first attempt at defining a [regexp] type that is indexed by predicates on strings, such that the index of a [regexp] tells us which language (string predicate) it recognizes. 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 780 [[
adamc@93 781 Inductive regexp : (string -> Prop) -> Set :=
adamc@93 782 | Char : forall ch : ascii,
adamc@93 783 regexp (fun s => s = String ch "")
adamc@93 784 | Concat : forall (P1 P2 : string -> Prop) (r1 : regexp P1) (r2 : regexp P2),
adamc@93 785 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2).
adamc@93 786 ]]
adamc@93 787
adam@338 788 <<
adam@338 789 User error: Large non-propositional inductive types must be in Type
adam@338 790 >>
adam@338 791
adam@454 792 What is a %\index{large inductive types}%large inductive type? In Coq, it is an inductive type that has a constructor that 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 793
adamc@93 794 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 795
adamc@89 796 Inductive regexp : (string -> Prop) -> Type :=
adamc@86 797 | Char : forall ch : ascii,
adamc@86 798 regexp (fun s => s = String ch "")
adamc@86 799 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
adamc@87 800 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2)
adamc@87 801 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
adamc@91 802 regexp (fun s => P1 s \/ P2 s)
adamc@91 803 | Star : forall P (r : regexp P),
adamc@91 804 regexp (star P).
adamc@86 805
adam@425 806 (** Many theorems about strings are useful for implementing a certified regexp matcher, and few of them are in the [String] 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 807
adamc@93 808 (* begin hide *)
adamc@86 809 Open Scope specif_scope.
adamc@86 810
adamc@86 811 Lemma length_emp : length "" <= 0.
adamc@86 812 crush.
adamc@86 813 Qed.
adamc@86 814
adamc@86 815 Lemma append_emp : forall s, s = "" ++ s.
adamc@86 816 crush.
adamc@86 817 Qed.
adamc@86 818
adamc@86 819 Ltac substring :=
adamc@86 820 crush;
adamc@86 821 repeat match goal with
adamc@86 822 | [ |- context[match ?N with O => _ | S _ => _ end] ] => destruct N; crush
adamc@86 823 end.
adamc@86 824
adamc@86 825 Lemma substring_le : forall s n m,
adamc@86 826 length (substring n m s) <= m.
adamc@86 827 induction s; substring.
adamc@86 828 Qed.
adamc@86 829
adamc@86 830 Lemma substring_all : forall s,
adamc@86 831 substring 0 (length s) s = s.
adamc@86 832 induction s; substring.
adamc@86 833 Qed.
adamc@86 834
adamc@86 835 Lemma substring_none : forall s n,
adamc@93 836 substring n 0 s = "".
adamc@86 837 induction s; substring.
adamc@86 838 Qed.
adamc@86 839
adam@375 840 Hint Rewrite substring_all substring_none.
adamc@86 841
adamc@86 842 Lemma substring_split : forall s m,
adamc@86 843 substring 0 m s ++ substring m (length s - m) s = s.
adamc@86 844 induction s; substring.
adamc@86 845 Qed.
adamc@86 846
adamc@86 847 Lemma length_app1 : forall s1 s2,
adamc@86 848 length s1 <= length (s1 ++ s2).
adamc@86 849 induction s1; crush.
adamc@86 850 Qed.
adamc@86 851
adamc@86 852 Hint Resolve length_emp append_emp substring_le substring_split length_app1.
adamc@86 853
adamc@86 854 Lemma substring_app_fst : forall s2 s1 n,
adamc@86 855 length s1 = n
adamc@86 856 -> substring 0 n (s1 ++ s2) = s1.
adamc@86 857 induction s1; crush.
adamc@86 858 Qed.
adamc@86 859
adamc@86 860 Lemma substring_app_snd : forall s2 s1 n,
adamc@86 861 length s1 = n
adamc@86 862 -> substring n (length (s1 ++ s2) - n) (s1 ++ s2) = s2.
adam@375 863 Hint Rewrite <- minus_n_O.
adamc@86 864
adamc@86 865 induction s1; crush.
adamc@86 866 Qed.
adamc@86 867
adam@375 868 Hint Rewrite substring_app_fst substring_app_snd using solve [trivial].
adamc@93 869 (* end hide *)
adamc@93 870
adamc@93 871 (** 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 872
adamc@86 873 Section split.
adamc@86 874 Variables P1 P2 : string -> Prop.
adamc@214 875 Variable P1_dec : forall s, {P1 s} + {~ P1 s}.
adamc@214 876 Variable P2_dec : forall s, {P2 s} + {~ P2 s}.
adamc@93 877 (** We require a choice of two arbitrary string predicates and functions for deciding them. *)
adamc@86 878
adamc@86 879 Variable s : string.
adamc@93 880 (** 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 881
adam@338 882 (** 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 883
adam@297 884 Definition split' : forall n : nat, n <= length s
adamc@86 885 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
adamc@214 886 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2}.
adamc@86 887 refine (fix F (n : nat) : n <= length s
adamc@86 888 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
adamc@214 889 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2} :=
adamc@214 890 match n with
adamc@86 891 | O => fun _ => Reduce (P1_dec "" && P2_dec s)
adamc@93 892 | S n' => fun _ => (P1_dec (substring 0 (S n') s)
adamc@93 893 && P2_dec (substring (S n') (length s - S n') s))
adamc@86 894 || F n' _
adamc@86 895 end); clear F; crush; eauto 7;
adamc@86 896 match goal with
adamc@86 897 | [ _ : length ?S <= 0 |- _ ] => destruct S
adam@338 898 | [ _ : length ?S' <= S ?N |- _ ] => destruct (eq_nat_dec (length S') (S N))
adamc@86 899 end; crush.
adamc@86 900 Defined.
adamc@86 901
adam@338 902 (** 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 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@93 908 ]]
adamc@93 909
adam@338 910 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 911
adamc@86 912 Definition split : {exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2}
adamc@214 913 + {forall s1 s2, s = s1 ++ s2 -> ~ P1 s1 \/ ~ P2 s2}.
adamc@86 914 refine (Reduce (split' (n := length s) _)); crush; eauto.
adamc@86 915 Defined.
adamc@86 916 End split.
adamc@86 917
adamc@86 918 Implicit Arguments split [P1 P2].
adamc@86 919
adamc@93 920 (* begin hide *)
adamc@91 921 Lemma app_empty_end : forall s, s ++ "" = s.
adamc@91 922 induction s; crush.
adamc@91 923 Qed.
adamc@91 924
adam@375 925 Hint Rewrite app_empty_end.
adamc@91 926
adamc@91 927 Lemma substring_self : forall s n,
adamc@91 928 n <= 0
adamc@91 929 -> substring n (length s - n) s = s.
adamc@91 930 induction s; substring.
adamc@91 931 Qed.
adamc@91 932
adamc@91 933 Lemma substring_empty : forall s n m,
adamc@91 934 m <= 0
adamc@91 935 -> substring n m s = "".
adamc@91 936 induction s; substring.
adamc@91 937 Qed.
adamc@91 938
adam@375 939 Hint Rewrite substring_self substring_empty using omega.
adamc@91 940
adamc@91 941 Lemma substring_split' : forall s n m,
adamc@91 942 substring n m s ++ substring (n + m) (length s - (n + m)) s
adamc@91 943 = substring n (length s - n) s.
adam@375 944 Hint Rewrite substring_split.
adamc@91 945
adamc@91 946 induction s; substring.
adamc@91 947 Qed.
adamc@91 948
adamc@91 949 Lemma substring_stack : forall s n2 m1 m2,
adamc@91 950 m1 <= m2
adamc@91 951 -> substring 0 m1 (substring n2 m2 s)
adamc@91 952 = substring n2 m1 s.
adamc@91 953 induction s; substring.
adamc@91 954 Qed.
adamc@91 955
adamc@91 956 Ltac substring' :=
adamc@91 957 crush;
adamc@91 958 repeat match goal with
adamc@91 959 | [ |- context[match ?N with O => _ | S _ => _ end] ] => case_eq N; crush
adamc@91 960 end.
adamc@91 961
adamc@91 962 Lemma substring_stack' : forall s n1 n2 m1 m2,
adamc@91 963 n1 + m1 <= m2
adamc@91 964 -> substring n1 m1 (substring n2 m2 s)
adamc@91 965 = substring (n1 + n2) m1 s.
adamc@91 966 induction s; substring';
adamc@91 967 match goal with
adamc@91 968 | [ |- substring ?N1 _ _ = substring ?N2 _ _ ] =>
adamc@91 969 replace N1 with N2; crush
adamc@91 970 end.
adamc@91 971 Qed.
adamc@91 972
adamc@91 973 Lemma substring_suffix : forall s n,
adamc@91 974 n <= length s
adamc@91 975 -> length (substring n (length s - n) s) = length s - n.
adamc@91 976 induction s; substring.
adamc@91 977 Qed.
adamc@91 978
adamc@91 979 Lemma substring_suffix_emp' : forall s n m,
adamc@91 980 substring n (S m) s = ""
adamc@91 981 -> n >= length s.
adamc@91 982 induction s; crush;
adamc@91 983 match goal with
adamc@91 984 | [ |- ?N >= _ ] => destruct N; crush
adamc@91 985 end;
adamc@91 986 match goal with
adamc@91 987 [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | omega ]
adamc@91 988 end.
adamc@91 989 Qed.
adamc@91 990
adamc@91 991 Lemma substring_suffix_emp : forall s n m,
adamc@92 992 substring n m s = ""
adamc@92 993 -> m > 0
adamc@91 994 -> n >= length s.
adam@335 995 destruct m as [ | m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
adamc@91 996 Qed.
adamc@91 997
adamc@91 998 Hint Rewrite substring_stack substring_stack' substring_suffix
adam@375 999 using omega.
adamc@91 1000
adamc@91 1001 Lemma minus_minus : forall n m1 m2,
adamc@91 1002 m1 + m2 <= n
adamc@91 1003 -> n - m1 - m2 = n - (m1 + m2).
adamc@91 1004 intros; omega.
adamc@91 1005 Qed.
adamc@91 1006
adamc@91 1007 Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n.
adamc@91 1008 intros; omega.
adamc@91 1009 Qed.
adamc@91 1010
adam@375 1011 Hint Rewrite minus_minus using omega.
adamc@93 1012 (* end hide *)
adamc@93 1013
adamc@93 1014 (** 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 1015
adamc@91 1016 Section dec_star.
adamc@91 1017 Variable P : string -> Prop.
adamc@214 1018 Variable P_dec : forall s, {P s} + {~ P s}.
adamc@91 1019
adam@338 1020 (** 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 1021
adamc@93 1022 (* begin hide *)
adamc@91 1023 Hint Constructors star.
adamc@91 1024
adamc@91 1025 Lemma star_empty : forall s,
adamc@91 1026 length s = 0
adamc@91 1027 -> star P s.
adamc@91 1028 destruct s; crush.
adamc@91 1029 Qed.
adamc@91 1030
adamc@91 1031 Lemma star_singleton : forall s, P s -> star P s.
adamc@91 1032 intros; rewrite <- (app_empty_end s); auto.
adamc@91 1033 Qed.
adamc@91 1034
adamc@91 1035 Lemma star_app : forall s n m,
adamc@91 1036 P (substring n m s)
adamc@91 1037 -> star P (substring (n + m) (length s - (n + m)) s)
adamc@91 1038 -> star P (substring n (length s - n) s).
adamc@91 1039 induction n; substring;
adamc@91 1040 match goal with
adamc@91 1041 | [ H : P (substring ?N ?M ?S) |- _ ] =>
adamc@91 1042 solve [ rewrite <- (substring_split S M); auto
adamc@91 1043 | rewrite <- (substring_split' S N M); auto ]
adamc@91 1044 end.
adamc@91 1045 Qed.
adamc@91 1046
adamc@91 1047 Hint Resolve star_empty star_singleton star_app.
adamc@91 1048
adamc@91 1049 Variable s : string.
adamc@91 1050
adamc@91 1051 Lemma star_inv : forall s,
adamc@91 1052 star P s
adamc@91 1053 -> s = ""
adamc@91 1054 \/ exists i, i < length s
adamc@91 1055 /\ P (substring 0 (S i) s)
adamc@91 1056 /\ star P (substring (S i) (length s - S i) s).
adamc@91 1057 Hint Extern 1 (exists i : nat, _) =>
adamc@91 1058 match goal with
adamc@91 1059 | [ H : P (String _ ?S) |- _ ] => exists (length S); crush
adamc@91 1060 end.
adamc@91 1061
adamc@91 1062 induction 1; [
adamc@91 1063 crush
adamc@91 1064 | match goal with
adamc@91 1065 | [ _ : P ?S |- _ ] => destruct S; crush
adamc@91 1066 end
adamc@91 1067 ].
adamc@91 1068 Qed.
adamc@91 1069
adamc@91 1070 Lemma star_substring_inv : forall n,
adamc@91 1071 n <= length s
adamc@91 1072 -> star P (substring n (length s - n) s)
adamc@91 1073 -> substring n (length s - n) s = ""
adamc@91 1074 \/ exists l, l < length s - n
adamc@91 1075 /\ P (substring n (S l) s)
adamc@91 1076 /\ star P (substring (n + S l) (length s - (n + S l)) s).
adam@375 1077 Hint Rewrite plus_n_Sm'.
adamc@91 1078
adamc@91 1079 intros;
adamc@91 1080 match goal with
adamc@91 1081 | [ H : star _ _ |- _ ] => generalize (star_inv H); do 3 crush; eauto
adamc@91 1082 end.
adamc@91 1083 Qed.
adamc@93 1084 (* end hide *)
adamc@93 1085
adamc@93 1086 (** 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 1087
adamc@91 1088 Section dec_star''.
adamc@91 1089 Variable n : nat.
adam@454 1090 (** Variable [n] is the length of the prefix of [s] that we have already processed. *)
adamc@91 1091
adamc@91 1092 Variable P' : string -> Prop.
adamc@91 1093 Variable P'_dec : forall n' : nat, n' > n
adamc@91 1094 -> {P' (substring n' (length s - n') s)}
adamc@214 1095 + {~ P' (substring n' (length s - n') s)}.
adam@475 1096
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
adam@480 1108 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
adam@480 1109 + {forall l', S l' <= l
adam@480 1110 -> ~ P (substring n (S l') s)
adam@480 1111 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} :=
adam@480 1112 match l with
adam@480 1113 | O => _
adam@480 1114 | S l' =>
adam@480 1115 (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
adam@480 1116 || F l'
adam@480 1117 end); clear F; crush; eauto 7;
adam@480 1118 match goal with
adam@480 1119 | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush
adam@480 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'
adam@338 1154 || dec_star'' (n := n') (star P)
adam@338 1155 (fun n0 _ => Reduce (F n'' n0 _)) (length s - n')
adamc@92 1156 end); clear F; crush; eauto;
adamc@92 1157 match goal with
adamc@92 1158 | [ H : star _ _ |- _ ] => apply star_substring_inv in H; crush; eauto
adamc@92 1159 end;
adamc@92 1160 match goal with
adamc@92 1161 | [ H1 : _ < _ - _, H2 : forall l' : nat, _ <= _ - _ -> _ |- _ ] =>
adamc@92 1162 generalize (H2 _ (lt_le_S _ _ H1)); tauto
adamc@92 1163 end.
adamc@91 1164 Defined.
adamc@91 1165
adam@380 1166 (** Finally, we have [dec_star], defined by straightforward reduction from [dec_star']. *)
adamc@93 1167
adamc@214 1168 Definition dec_star : {star P s} + {~ star P s}.
adam@380 1169 refine (Reduce (dec_star' (n := length s) 0 _)); crush.
adamc@91 1170 Defined.
adamc@91 1171 End dec_star.
adamc@91 1172
adamc@93 1173 (* begin hide *)
adamc@86 1174 Lemma app_cong : forall x1 y1 x2 y2,
adamc@86 1175 x1 = x2
adamc@86 1176 -> y1 = y2
adamc@86 1177 -> x1 ++ y1 = x2 ++ y2.
adamc@86 1178 congruence.
adamc@86 1179 Qed.
adamc@86 1180
adamc@86 1181 Hint Resolve app_cong.
adamc@93 1182 (* end hide *)
adamc@93 1183
adamc@93 1184 (** 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 1185
adam@297 1186 Definition matches : forall P (r : regexp P) s, {P s} + {~ P s}.
adamc@214 1187 refine (fix F P (r : regexp P) s : {P s} + {~ P s} :=
adamc@86 1188 match r with
adamc@86 1189 | Char ch => string_dec s (String ch "")
adamc@86 1190 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s)
adamc@87 1191 | Or _ _ r1 r2 => F _ r1 s || F _ r2 s
adamc@91 1192 | Star _ r => dec_star _ _ _
adamc@86 1193 end); crush;
adamc@86 1194 match goal with
adam@426 1195 | [ H : _ |- _ ] => generalize (H _ _ (eq_refl _))
adamc@93 1196 end; tauto.
adamc@86 1197 Defined.
adamc@86 1198
adam@283 1199 (** 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 1200
adamc@93 1201 (* begin hide *)
adamc@86 1202 Example hi := Concat (Char "h"%char) (Char "i"%char).
adam@380 1203 Eval hnf in matches hi "hi".
adam@380 1204 Eval hnf in matches hi "bye".
adamc@87 1205
adamc@87 1206 Example a_b := Or (Char "a"%char) (Char "b"%char).
adam@380 1207 Eval hnf in matches a_b "".
adam@380 1208 Eval hnf in matches a_b "a".
adam@380 1209 Eval hnf in matches a_b "aa".
adam@380 1210 Eval hnf in matches a_b "b".
adam@283 1211 (* end hide *)
adam@283 1212
adam@454 1213 (** 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. We use evaluation strategy %\index{tactics!hnf}%[hnf] to reduce each term to%\index{head-normal form}% _head-normal form_, where the datatype constructor used to build its value is known. (Further reduction would involve wasteful simplification of proof terms justifying the answers of our procedures.) *)
adamc@91 1214
adamc@91 1215 Example a_star := Star (Char "a"%char).
adam@380 1216 Eval hnf in matches a_star "".
adam@380 1217 Eval hnf in matches a_star "a".
adam@380 1218 Eval hnf in matches a_star "b".
adam@380 1219 Eval hnf in matches a_star "aa".
adam@283 1220
adam@283 1221 (** 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. *)