Mercurial > cpdt > repo

annotate src/MoreDep.v @ 420:671a6e7e1f29

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through InductiveTypes, to incorporate new coqdoc features
author Adam Chlipala <adam@chlipala.net>
date Wed, 25 Jul 2012 16:15:50 -0400
parents 539ed97750bb
children 6ed5ee4845e4
rev   line source
adam@371 1 (* Copyright (c) 2008-2012, Adam Chlipala
adamc@83 2 *
adamc@83 3 * This work is licensed under a
adamc@83 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@83 5 * Unported License.
adamc@83 6 * The license text is available at:
adamc@83 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@83 8 *)
adamc@83 9
adamc@83 10 (* begin hide *)
adamc@85 11 Require Import Arith Bool List.
adamc@83 12
adam@314 13 Require Import CpdtTactics MoreSpecif.
adamc@83 14
adamc@83 15 Set Implicit Arguments.
adamc@83 16 (* end hide *)
adamc@83 17
adamc@83 18
adamc@83 19 (** %\chapter{More Dependent Types}% *)
adamc@83 20
adam@292 21 (** Subset types and their relatives help us integrate verification with programming. Though they reorganize the certified programmer's workflow, they tend not to have deep effects on proofs. We write largely the same proofs as we would for classical verification, with some of the structure moved into the programs themselves. It turns out that, when we use dependent types to their full potential, we warp the development and proving process even more than that, picking up %``%#"#free theorems#"#%''% to the extent that often a certified program is hardly more complex than its uncertified counterpart in Haskell or ML.
adamc@83 22
adam@338 23 In particular, we have only scratched the tip of the iceberg that is Coq's inductive definition mechanism. The inductive types we have seen so far have their counterparts in the other proof assistants that we surveyed in Chapter 1. This chapter explores the strange new world of dependent inductive datatypes (that is, dependent inductive types outside [Prop]), a possibility that sets Coq apart from all of the competition not based on type theory. *)
adamc@83 24
adamc@84 25
adamc@84 26 (** * Length-Indexed Lists *)
adamc@84 27
adam@338 28 (** Many introductions to dependent types start out by showing how to use them to eliminate array bounds checks%\index{array bounds checks}%. When the type of an array tells you how many elements it has, your compiler can detect out-of-bounds dereferences statically. Since we are working in a pure functional language, the next best thing is length-indexed lists%\index{length-indexed lists}%, which the following code defines. *)
adamc@84 29
adamc@84 30 Section ilist.
adamc@84 31 Variable A : Set.
adamc@84 32
adamc@84 33 Inductive ilist : nat -> Set :=
adamc@84 34 | Nil : ilist O
adamc@84 35 | Cons : forall n, A -> ilist n -> ilist (S n).
adamc@84 36
adamc@84 37 (** We see that, within its section, [ilist] is given type [nat -> Set]. Previously, every inductive type we have seen has either had plain [Set] as its type or has been a predicate with some type ending in [Prop]. The full generality of inductive definitions lets us integrate the expressivity of predicates directly into our normal programming.
adamc@84 38
adam@405 39 The [nat] argument to [ilist] tells us the length of the list. The types of [ilist]'s constructors tell us that a [Nil] list has length [O] and that a [Cons] list has length one greater than the length of its tail. We may apply [ilist] to any natural number, even natural numbers that are only known at runtime. It is this breaking of the%\index{phase distinction}% _phase distinction_ that characterizes [ilist] as _dependently typed_.
adamc@84 40
adamc@213 41 In expositions of list types, we usually see the length function defined first, but here that would not be a very productive function to code. Instead, let us implement list concatenation. *)
adamc@84 42
adamc@213 43 Fixpoint app n1 (ls1 : ilist n1) n2 (ls2 : ilist n2) : ilist (n1 + n2) :=
adamc@213 44 match ls1 with
adamc@213 45 | Nil => ls2
adamc@213 46 | Cons _ x ls1' => Cons x (app ls1' ls2)
adamc@213 47 end.
adamc@84 48
adam@338 49 (** Past Coq versions signalled an error for this definition. The code is still invalid within Coq's core language, but current Coq versions automatically add annotations to the original program, producing a valid core program. These are the annotations on [match] discriminees that we began to study in the previous chapter. We can rewrite [app] to give the annotations explicitly. *)
adamc@100 50
adamc@100 51 (* begin thide *)
adam@338 52 Fixpoint app' n1 (ls1 : ilist n1) n2 (ls2 : ilist n2) : ilist (n1 + n2) :=
adam@338 53 match ls1 in (ilist n1) return (ilist (n1 + n2)) with
adam@338 54 | Nil => ls2
adam@338 55 | Cons _ x ls1' => Cons x (app' ls1' ls2)
adam@338 56 end.
adamc@100 57 (* end thide *)
adamc@84 58
adam@398 59 (** 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 60
adam@398 61 We may use [in] clauses only to bind names for the arguments of an inductive type family. That is, each [in] clause must be an inductive type family name applied to a sequence of underscores and variable names of the proper length. The positions for _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 62
adam@405 63 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. This stratification between a compile-time universe and a run-time universe, with no references to the latter in the former, gives rise to the terminology %``%#"#stratified.#"#%''% Our next example would be harder to implement in a stratified system. We write an injection function from regular lists to length-indexed lists. A stratified implementation would need to duplicate the definition of lists across compile-time and run-time versions, and the run-time versions would need to be indexed by the compile-time versions. *)
adamc@84 64
adamc@100 65 (* EX: Implement injection from normal lists *)
adamc@100 66
adamc@100 67 (* begin thide *)
adamc@84 68 Fixpoint inject (ls : list A) : ilist (length ls) :=
adamc@213 69 match ls with
adamc@84 70 | nil => Nil
adamc@84 71 | h :: t => Cons h (inject t)
adamc@84 72 end.
adamc@84 73
adamc@84 74 (** We can define an inverse conversion and prove that it really is an inverse. *)
adamc@84 75
adamc@213 76 Fixpoint unject n (ls : ilist n) : list A :=
adamc@84 77 match ls with
adamc@84 78 | Nil => nil
adamc@84 79 | Cons _ h t => h :: unject t
adamc@84 80 end.
adamc@84 81
adamc@84 82 Theorem inject_inverse : forall ls, unject (inject ls) = ls.
adamc@84 83 induction ls; crush.
adamc@84 84 Qed.
adamc@100 85 (* end thide *)
adamc@100 86
adam@338 87 (* EX: Implement statically checked "car"/"hd" *)
adamc@84 88
adam@283 89 (** Now let us attempt a function that is surprisingly tricky to write. In ML, the list head function raises an exception when passed an empty list. With length-indexed lists, we can rule out such invalid calls statically, and here is a first attempt at doing so. We write [???] as a placeholder for a term that we do not know how to write, not for any real Coq notation like those introduced in the previous chapter.
adamc@84 90
adamc@84 91 [[
adamc@84 92 Definition hd n (ls : ilist (S n)) : A :=
adamc@84 93 match ls with
adamc@84 94 | Nil => ???
adamc@84 95 | Cons _ h _ => h
adamc@84 96 end.
adamc@213 97
adamc@213 98 ]]
adamc@84 99
adamc@84 100 It is not clear what to write for the [Nil] case, so we are stuck before we even turn our function over to the type checker. We could try omitting the [Nil] case:
adamc@84 101
adamc@84 102 [[
adamc@84 103 Definition hd n (ls : ilist (S n)) : A :=
adamc@84 104 match ls with
adamc@84 105 | Cons _ h _ => h
adamc@84 106 end.
adam@338 107 ]]
adamc@84 108
adam@338 109 <<
adamc@84 110 Error: Non exhaustive pattern-matching: no clause found for pattern Nil
adam@338 111 >>
adamc@84 112
adam@398 113 Unlike in ML, we cannot use inexhaustive pattern matching, because there is no conception of a %\texttt{%#<tt>#Match#</tt>#%}% exception to be thrown. In fact, recent versions of Coq _do_ allow this, by implicit translation to a [match] that considers all constructors. It is educational to discover that encoding ourselves directly. We might try using an [in] clause somehow.
adamc@84 114
adamc@84 115 [[
adamc@84 116 Definition hd n (ls : ilist (S n)) : A :=
adamc@84 117 match ls in (ilist (S n)) with
adamc@84 118 | Cons _ h _ => h
adamc@84 119 end.
adamc@84 120 ]]
adamc@84 121
adam@338 122 <<
adam@338 123 Error: The reference n was not found in the current environment
adam@338 124 >>
adam@338 125
adam@398 126 In this and other cases, we feel like we want [in] clauses with type family arguments that are not variables. Unfortunately, Coq only supports variables in those positions. A completely general mechanism could only be supported with a solution to the problem of higher-order unification%~\cite{HOU}%, which is undecidable. There _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 127
adamc@84 128 Our final, working attempt at [hd] uses an auxiliary function and a surprising [return] annotation. *)
adamc@84 129
adamc@100 130 (* begin thide *)
adamc@84 131 Definition hd' n (ls : ilist n) :=
adamc@84 132 match ls in (ilist n) return (match n with O => unit | S _ => A end) with
adamc@84 133 | Nil => tt
adamc@84 134 | Cons _ h _ => h
adamc@84 135 end.
adamc@84 136
adam@283 137 Check hd'.
adam@283 138 (** %\vspace{-.15in}% [[
adam@283 139 hd'
adam@283 140 : forall n : nat, ilist n -> match n with
adam@283 141 | 0 => unit
adam@283 142 | S _ => A
adam@283 143 end
adam@283 144
adam@302 145 ]]
adam@302 146 *)
adam@283 147
adamc@84 148 Definition hd n (ls : ilist (S n)) : A := hd' ls.
adamc@100 149 (* end thide *)
adamc@84 150
adam@338 151 End ilist.
adam@338 152
adamc@84 153 (** We annotate our main [match] with a type that is itself a [match]. We write that the function [hd'] returns [unit] when the list is empty and returns the carried type [A] in all other cases. In the definition of [hd], we just call [hd']. Because the index of [ls] is known to be nonzero, the type checker reduces the [match] in the type of [hd'] to [A]. *)
adamc@84 154
adamc@85 155
adam@371 156 (** * The One Rule of Dependent Pattern Matching in Coq *)
adam@371 157
adam@405 158 (** 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 159
adam@405 160 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 161
adam@398 162 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 163
adam@371 164 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 165 [[
adam@371 166 match E in (T x1 ... xn) as y return U with
adam@371 167 | C z1 ... zm => B
adam@371 168 | ...
adam@371 169 end
adam@371 170 ]]
adam@371 171
adam@371 172 The discriminee is a term [E], a value in some inductive type family [T], which takes [n] arguments. An %\index{in clause}%[in] clause binds an explicit name [xi] for the [i]th argument passed to [T] in the type of [E]. An %\index{as clause}%[as] clause binds the name [y] to refer to the discriminee [E].
adam@371 173
adam@371 174 We bind these new variables [xi] and [y] 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 175
adam@371 176 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 177
adam@371 178 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 179
adam@371 180 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 181
adam@405 182 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 183
adam@371 184
adamc@85 185 (** * A Tagless Interpreter *)
adamc@85 186
adam@405 187 (** 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 188
adamc@85 189 Inductive type : Set :=
adamc@85 190 | Nat : type
adamc@85 191 | Bool : type
adamc@85 192 | Prod : type -> type -> type.
adamc@85 193
adamc@85 194 Inductive exp : type -> Set :=
adamc@85 195 | NConst : nat -> exp Nat
adamc@85 196 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@85 197 | Eq : exp Nat -> exp Nat -> exp Bool
adamc@85 198
adamc@85 199 | BConst : bool -> exp Bool
adamc@85 200 | And : exp Bool -> exp Bool -> exp Bool
adamc@85 201 | If : forall t, exp Bool -> exp t -> exp t -> exp t
adamc@85 202
adamc@85 203 | Pair : forall t1 t2, exp t1 -> exp t2 -> exp (Prod t1 t2)
adamc@85 204 | Fst : forall t1 t2, exp (Prod t1 t2) -> exp t1
adamc@85 205 | Snd : forall t1 t2, exp (Prod t1 t2) -> exp t2.
adamc@85 206
adamc@85 207 (** 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 208
adam@398 209 We can give types and expressions semantics in a new style, based critically on the chance for _type-level computation_. *)
adamc@85 210
adamc@85 211 Fixpoint typeDenote (t : type) : Set :=
adamc@85 212 match t with
adamc@85 213 | Nat => nat
adamc@85 214 | Bool => bool
adamc@85 215 | Prod t1 t2 => typeDenote t1 * typeDenote t2
adamc@85 216 end%type.
adamc@85 217
adam@416 218 (** 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 identifer 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 219
adamc@85 220 We can define a function [expDenote] that is typed in terms of [typeDenote]. *)
adamc@85 221
adamc@213 222 Fixpoint expDenote t (e : exp t) : typeDenote t :=
adamc@213 223 match e with
adamc@85 224 | NConst n => n
adamc@85 225 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@85 226 | Eq e1 e2 => if eq_nat_dec (expDenote e1) (expDenote e2) then true else false
adamc@85 227
adamc@85 228 | BConst b => b
adamc@85 229 | And e1 e2 => expDenote e1 && expDenote e2
adamc@85 230 | If _ e' e1 e2 => if expDenote e' then expDenote e1 else expDenote e2
adamc@85 231
adamc@85 232 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@85 233 | Fst _ _ e' => fst (expDenote e')
adamc@85 234 | Snd _ _ e' => snd (expDenote e')
adamc@85 235 end.
adamc@85 236
adamc@213 237 (** 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 238
adamc@85 239 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 240
adamc@85 241 [[
adamc@85 242 Definition pairOut t1 t2 (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) :=
adamc@85 243 match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with
adamc@85 244 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@85 245 | _ => None
adamc@85 246 end.
adam@338 247 ]]
adamc@85 248
adam@338 249 <<
adamc@85 250 Error: The reference t2 was not found in the current environment
adam@338 251 >>
adamc@85 252
adamc@85 253 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 254
adamc@100 255 (* EX: Define a function [pairOut : forall t1 t2, exp (Prod t1 t2) -> option (exp t1 * exp t2)] *)
adamc@100 256
adamc@100 257 (* begin thide *)
adamc@85 258 Definition pairOutType (t : type) :=
adamc@85 259 match t with
adamc@85 260 | Prod t1 t2 => option (exp t1 * exp t2)
adamc@85 261 | _ => unit
adamc@85 262 end.
adamc@85 263
adamc@85 264 (** 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 265
adamc@85 266 Definition pairOutDefault (t : type) :=
adamc@85 267 match t return (pairOutType t) with
adamc@85 268 | Prod _ _ => None
adamc@85 269 | _ => tt
adamc@85 270 end.
adamc@85 271
adamc@85 272 (** Now [pairOut] is deceptively easy to write. *)
adamc@85 273
adamc@85 274 Definition pairOut t (e : exp t) :=
adamc@85 275 match e in (exp t) return (pairOutType t) with
adamc@85 276 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@85 277 | _ => pairOutDefault _
adamc@85 278 end.
adamc@100 279 (* end thide *)
adamc@85 280
adam@338 281 (** There is one important subtlety in this definition. Coq allows us to use convenient ML-style pattern matching notation, but, internally and in proofs, we see that patterns are expanded out completely, matching one level of inductive structure at a time. Thus, the default case in the [match] above expands out to one case for each constructor of [exp] besides [Pair], and the underscore in [pairOutDefault _] is resolved differently in each case. From an ML or Haskell programmer's perspective, what we have here is type inference determining which code is run (returning either [None] or [tt]), which goes beyond what is possible with type inference guiding parametric polymorphism in Hindley-Milner languages%\index{Hindley-Milner}%, but is similar to what goes on with Haskell type classes%\index{type classes}%.
adamc@85 282
adam@417 283 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 with explicit [return] clauses. *)
adamc@85 284
adamc@204 285 Fixpoint cfold t (e : exp t) : exp t :=
adamc@204 286 match e with
adamc@85 287 | NConst n => NConst n
adamc@85 288 | Plus e1 e2 =>
adamc@85 289 let e1' := cfold e1 in
adamc@85 290 let e2' := cfold e2 in
adam@417 291 match e1', e2' return exp Nat with
adamc@85 292 | NConst n1, NConst n2 => NConst (n1 + n2)
adamc@85 293 | _, _ => Plus e1' e2'
adamc@85 294 end
adamc@85 295 | Eq e1 e2 =>
adamc@85 296 let e1' := cfold e1 in
adamc@85 297 let e2' := cfold e2 in
adam@417 298 match e1', e2' return exp Bool with
adamc@85 299 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
adamc@85 300 | _, _ => Eq e1' e2'
adamc@85 301 end
adamc@85 302
adamc@85 303 | BConst b => BConst b
adamc@85 304 | And e1 e2 =>
adamc@85 305 let e1' := cfold e1 in
adamc@85 306 let e2' := cfold e2 in
adam@417 307 match e1', e2' return exp Bool with
adamc@85 308 | BConst b1, BConst b2 => BConst (b1 && b2)
adamc@85 309 | _, _ => And e1' e2'
adamc@85 310 end
adamc@85 311 | If _ e e1 e2 =>
adamc@85 312 let e' := cfold e in
adamc@85 313 match e' with
adamc@85 314 | BConst true => cfold e1
adamc@85 315 | BConst false => cfold e2
adamc@85 316 | _ => If e' (cfold e1) (cfold e2)
adamc@85 317 end
adamc@85 318
adamc@85 319 | Pair _ _ e1 e2 => Pair (cfold e1) (cfold e2)
adamc@85 320 | Fst _ _ e =>
adamc@85 321 let e' := cfold e in
adamc@85 322 match pairOut e' with
adamc@85 323 | Some p => fst p
adamc@85 324 | None => Fst e'
adamc@85 325 end
adamc@85 326 | Snd _ _ e =>
adamc@85 327 let e' := cfold e in
adamc@85 328 match pairOut e' with
adamc@85 329 | Some p => snd p
adamc@85 330 | None => Snd e'
adamc@85 331 end
adamc@85 332 end.
adamc@85 333
adamc@85 334 (** The correctness theorem for [cfold] turns out to be easy to prove, once we get over one serious hurdle. *)
adamc@85 335
adamc@85 336 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
adamc@100 337 (* begin thide *)
adamc@85 338 induction e; crush.
adamc@85 339
adamc@85 340 (** The first remaining subgoal is:
adamc@85 341
adamc@85 342 [[
adamc@85 343 expDenote (cfold e1) + expDenote (cfold e2) =
adamc@85 344 expDenote
adamc@85 345 match cfold e1 with
adamc@85 346 | NConst n1 =>
adamc@85 347 match cfold e2 with
adamc@85 348 | NConst n2 => NConst (n1 + n2)
adamc@85 349 | Plus _ _ => Plus (cfold e1) (cfold e2)
adamc@85 350 | Eq _ _ => Plus (cfold e1) (cfold e2)
adamc@85 351 | BConst _ => Plus (cfold e1) (cfold e2)
adamc@85 352 | And _ _ => Plus (cfold e1) (cfold e2)
adamc@85 353 | If _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 354 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 355 | Fst _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 356 | Snd _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 357 end
adamc@85 358 | Plus _ _ => Plus (cfold e1) (cfold e2)
adamc@85 359 | Eq _ _ => Plus (cfold e1) (cfold e2)
adamc@85 360 | BConst _ => Plus (cfold e1) (cfold e2)
adamc@85 361 | And _ _ => Plus (cfold e1) (cfold e2)
adamc@85 362 | If _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 363 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 364 | Fst _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 365 | Snd _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 366 end
adamc@213 367
adamc@85 368 ]]
adamc@85 369
adamc@85 370 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 371
adamc@85 372 [[
adamc@85 373 destruct (cfold e1).
adam@338 374 ]]
adamc@85 375
adam@338 376 <<
adamc@85 377 User error: e1 is used in hypothesis e
adam@338 378 >>
adamc@85 379
adamc@85 380 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 381
adam@350 382 For our current proof, we can use a tactic [dep_destruct]%\index{tactics!dep\_destruct}% defined in the book [CpdtTactics] module. General elimination/inversion of dependently typed hypotheses is undecidable, since it must be implemented with [match] expressions that have the restriction on [in] clauses that we have already discussed. The tactic [dep_destruct] makes a best effort to handle some common cases, relying upon the more primitive %\index{tactics!dependent destruction}%[dependent destruction] tactic that comes with Coq. In a future chapter, we will learn about the explicit manipulation of equality proofs that is behind [dep_destruct]'s implementation in Ltac, but for now, we treat it as a useful black box. (In Chapter 12, we will also see how [dependent destruction] forces us to make a larger philosophical commitment about our logic than we might like, and we will see some workarounds.) *)
adamc@85 383
adamc@85 384 dep_destruct (cfold e1).
adamc@85 385
adamc@85 386 (** 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 387
adam@405 388 This is the only new trick we need to learn to complete the proof. We can back up and give a short, automated proof. *)
adamc@85 389
adamc@85 390 Restart.
adamc@85 391
adamc@85 392 induction e; crush;
adamc@85 393 repeat (match goal with
adam@405 394 | [ |- context[match cfold ?E with NConst _ => _ | _ => _ end] ] =>
adamc@213 395 dep_destruct (cfold E)
adamc@213 396 | [ |- context[match pairOut (cfold ?E) with Some _ => _
adamc@213 397 | None => _ end] ] =>
adamc@213 398 dep_destruct (cfold E)
adamc@85 399 | [ |- (if ?E then _ else _) = _ ] => destruct E
adamc@85 400 end; crush).
adamc@85 401 Qed.
adamc@100 402 (* end thide *)
adamc@86 403
adam@405 404 (** With this example, we get a first taste of how to build automated proofs that adapt automatically to changes in function definitions. *)
adam@405 405
adamc@86 406
adam@338 407 (** * Dependently Typed Red-Black Trees *)
adamc@94 408
adam@338 409 (** 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 410
adamc@94 411 Inductive color : Set := Red | Black.
adamc@94 412
adamc@94 413 Inductive rbtree : color -> nat -> Set :=
adamc@94 414 | Leaf : rbtree Black 0
adamc@214 415 | RedNode : forall n, rbtree Black n -> nat -> rbtree Black n -> rbtree Red n
adamc@94 416 | BlackNode : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rbtree Black (S n).
adamc@94 417
adamc@214 418 (** 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 419
adamc@214 420 (** 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 421
adamc@100 422 (* EX: Prove that every [rbtree] is balanced. *)
adamc@100 423
adamc@100 424 (* begin thide *)
adamc@95 425 Require Import Max Min.
adamc@95 426
adamc@95 427 Section depth.
adamc@95 428 Variable f : nat -> nat -> nat.
adamc@95 429
adamc@214 430 Fixpoint depth c n (t : rbtree c n) : nat :=
adamc@95 431 match t with
adamc@95 432 | Leaf => 0
adamc@95 433 | RedNode _ t1 _ t2 => S (f (depth t1) (depth t2))
adamc@95 434 | BlackNode _ _ _ t1 _ t2 => S (f (depth t1) (depth t2))
adamc@95 435 end.
adamc@95 436 End depth.
adamc@95 437
adam@338 438 (** 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 439
adam@283 440 Check min_dec.
adam@283 441 (** %\vspace{-.15in}% [[
adam@283 442 min_dec
adam@283 443 : forall n m : nat, {min n m = n} + {min n m = m}
adam@302 444 ]]
adam@302 445 *)
adam@283 446
adamc@95 447 Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n.
adamc@95 448 induction t; crush;
adamc@95 449 match goal with
adamc@95 450 | [ |- context[min ?X ?Y] ] => destruct (min_dec X Y)
adamc@95 451 end; crush.
adamc@95 452 Qed.
adamc@95 453
adamc@214 454 (** There is an analogous upper-bound theorem based on black depth. Unfortunately, a symmetric proof script does not suffice to establish it. *)
adamc@214 455
adamc@214 456 Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
adamc@214 457 induction t; crush;
adamc@214 458 match goal with
adamc@214 459 | [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
adamc@214 460 end; crush.
adamc@214 461
adamc@214 462 (** Two subgoals remain. One of them is: [[
adamc@214 463 n : nat
adamc@214 464 t1 : rbtree Black n
adamc@214 465 n0 : nat
adamc@214 466 t2 : rbtree Black n
adamc@214 467 IHt1 : depth max t1 <= n + (n + 0) + 1
adamc@214 468 IHt2 : depth max t2 <= n + (n + 0) + 1
adamc@214 469 e : max (depth max t1) (depth max t2) = depth max t1
adamc@214 470 ============================
adamc@214 471 S (depth max t1) <= n + (n + 0) + 1
adamc@214 472
adamc@214 473 ]]
adamc@214 474
adam@398 475 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 476
adamc@214 477 Abort.
adamc@214 478
adamc@214 479 (** 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 480
adamc@95 481 Lemma depth_max' : forall c n (t : rbtree c n), match c with
adamc@95 482 | Red => depth max t <= 2 * n + 1
adamc@95 483 | Black => depth max t <= 2 * n
adamc@95 484 end.
adamc@95 485 induction t; crush;
adamc@95 486 match goal with
adamc@95 487 | [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
adamc@100 488 end; crush;
adamc@100 489 repeat (match goal with
adamc@214 490 | [ H : context[match ?C with Red => _ | Black => _ end] |- _ ] =>
adamc@214 491 destruct C
adamc@100 492 end; crush).
adamc@95 493 Qed.
adamc@95 494
adam@338 495 (** 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 496
adamc@95 497 Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
adamc@95 498 intros; generalize (depth_max' t); destruct c; crush.
adamc@95 499 Qed.
adamc@95 500
adamc@214 501 (** 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 502
adamc@95 503 Theorem balanced : forall c n (t : rbtree c n), 2 * depth min t + 1 >= depth max t.
adamc@95 504 intros; generalize (depth_min t); generalize (depth_max t); crush.
adamc@95 505 Qed.
adamc@100 506 (* end thide *)
adamc@95 507
adamc@214 508 (** 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 509
adamc@94 510 Inductive rtree : nat -> Set :=
adamc@94 511 | RedNode' : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rtree n.
adamc@94 512
adam@338 513 (** 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 514
adamc@96 515 Section present.
adamc@96 516 Variable x : nat.
adamc@96 517
adamc@214 518 Fixpoint present c n (t : rbtree c n) : Prop :=
adamc@96 519 match t with
adamc@96 520 | Leaf => False
adamc@96 521 | RedNode _ a y b => present a \/ x = y \/ present b
adamc@96 522 | BlackNode _ _ _ a y b => present a \/ x = y \/ present b
adamc@96 523 end.
adamc@96 524
adamc@96 525 Definition rpresent n (t : rtree n) : Prop :=
adamc@96 526 match t with
adamc@96 527 | RedNode' _ _ _ a y b => present a \/ x = y \/ present b
adamc@96 528 end.
adamc@96 529 End present.
adamc@96 530
adam@338 531 (** 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 532
adamc@100 533 Locate "{ _ : _ & _ }".
adamc@214 534 (** [[
adamc@214 535 Notation Scope
adamc@214 536 "{ x : A & P }" := sigT (fun x : A => P)
adam@302 537 ]]
adam@302 538 *)
adamc@214 539
adamc@100 540 Print sigT.
adamc@214 541 (** [[
adamc@214 542 Inductive sigT (A : Type) (P : A -> Type) : Type :=
adamc@214 543 existT : forall x : A, P x -> sigT P
adam@302 544 ]]
adam@302 545 *)
adamc@214 546
adamc@214 547 (** It will be helpful to define a concise notation for the constructor of [sigT]. *)
adamc@100 548
adamc@94 549 Notation "{< x >}" := (existT _ _ x).
adamc@94 550
adamc@214 551 (** 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 552
adam@338 553 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 554
adam@338 555 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 556
adamc@94 557 Definition balance1 n (a : rtree n) (data : nat) c2 :=
adamc@214 558 match a in rtree n return rbtree c2 n
adamc@214 559 -> { c : color & rbtree c (S n) } with
adam@380 560 | RedNode' _ c0 _ t1 y t2 =>
adam@380 561 match t1 in rbtree c n return rbtree c0 n -> rbtree c2 n
adamc@214 562 -> { c : color & rbtree c (S n) } with
adamc@214 563 | RedNode _ a x b => fun c d =>
adamc@214 564 {<RedNode (BlackNode a x b) y (BlackNode c data d)>}
adamc@94 565 | t1' => fun t2 =>
adam@380 566 match t2 in rbtree c n return rbtree Black n -> rbtree c2 n
adamc@214 567 -> { c : color & rbtree c (S n) } with
adamc@214 568 | RedNode _ b x c => fun a d =>
adamc@214 569 {<RedNode (BlackNode a y b) x (BlackNode c data d)>}
adamc@95 570 | b => fun a t => {<BlackNode (RedNode a y b) data t>}
adamc@94 571 end t1'
adamc@94 572 end t2
adamc@94 573 end.
adamc@94 574
adam@405 575 (** 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 576
adam@398 577 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 578
adam@338 579 Here is the symmetric function [balance2], for cases where the possibly invalid tree appears on the right rather than on the left. *)
adamc@214 580
adamc@94 581 Definition balance2 n (a : rtree n) (data : nat) c2 :=
adamc@94 582 match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with
adam@380 583 | RedNode' _ c0 _ t1 z t2 =>
adam@380 584 match t1 in rbtree c n return rbtree c0 n -> rbtree c2 n
adamc@214 585 -> { c : color & rbtree c (S n) } with
adamc@214 586 | RedNode _ b y c => fun d a =>
adamc@214 587 {<RedNode (BlackNode a data b) y (BlackNode c z d)>}
adamc@94 588 | t1' => fun t2 =>
adam@380 589 match t2 in rbtree c n return rbtree Black n -> rbtree c2 n
adamc@214 590 -> { c : color & rbtree c (S n) } with
adamc@214 591 | RedNode _ c z' d => fun b a =>
adamc@214 592 {<RedNode (BlackNode a data b) z (BlackNode c z' d)>}
adamc@95 593 | b => fun a t => {<BlackNode t data (RedNode a z b)>}
adamc@94 594 end t1'
adamc@94 595 end t2
adamc@94 596 end.
adamc@94 597
adamc@214 598 (** 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 599
adamc@94 600 Section insert.
adamc@94 601 Variable x : nat.
adamc@94 602
adamc@214 603 (** 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 604
adamc@94 605 Definition insResult c n :=
adamc@94 606 match c with
adamc@94 607 | Red => rtree n
adamc@94 608 | Black => { c' : color & rbtree c' n }
adamc@94 609 end.
adamc@94 610
adam@338 611 (** 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 612
adamc@214 613 Here is the definition of [ins]. Again, we do not want to dwell on the functional details. *)
adamc@214 614
adamc@214 615 Fixpoint ins c n (t : rbtree c n) : insResult c n :=
adamc@214 616 match t with
adamc@94 617 | Leaf => {< RedNode Leaf x Leaf >}
adamc@94 618 | RedNode _ a y b =>
adamc@94 619 if le_lt_dec x y
adamc@94 620 then RedNode' (projT2 (ins a)) y b
adamc@94 621 else RedNode' a y (projT2 (ins b))
adamc@94 622 | BlackNode c1 c2 _ a y b =>
adamc@94 623 if le_lt_dec x y
adamc@94 624 then
adamc@94 625 match c1 return insResult c1 _ -> _ with
adamc@94 626 | Red => fun ins_a => balance1 ins_a y b
adamc@94 627 | _ => fun ins_a => {< BlackNode (projT2 ins_a) y b >}
adamc@94 628 end (ins a)
adamc@94 629 else
adamc@94 630 match c2 return insResult c2 _ -> _ with
adamc@94 631 | Red => fun ins_b => balance2 ins_b y a
adamc@94 632 | _ => fun ins_b => {< BlackNode a y (projT2 ins_b) >}
adamc@94 633 end (ins b)
adamc@94 634 end.
adamc@94 635
adam@398 636 (** 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 _the result of a recursive call_, rather than just on that call's argument.
adamc@214 637
adamc@214 638 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 639
adamc@94 640 Definition insertResult c n :=
adamc@94 641 match c with
adamc@94 642 | Red => rbtree Black (S n)
adamc@94 643 | Black => { c' : color & rbtree c' n }
adamc@94 644 end.
adamc@94 645
adamc@214 646 (** A simple clean-up procedure translates [insResult]s into [insertResult]s. *)
adamc@214 647
adamc@97 648 Definition makeRbtree c n : insResult c n -> insertResult c n :=
adamc@214 649 match c with
adamc@94 650 | Red => fun r =>
adamc@214 651 match r with
adamc@94 652 | RedNode' _ _ _ a x b => BlackNode a x b
adamc@94 653 end
adamc@94 654 | Black => fun r => r
adamc@94 655 end.
adamc@94 656
adamc@214 657 (** 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 658
adamc@97 659 Implicit Arguments makeRbtree [c n].
adamc@94 660
adamc@214 661 (** Finally, we define [insert] as a simple composition of [ins] and [makeRbtree]. *)
adamc@214 662
adamc@94 663 Definition insert c n (t : rbtree c n) : insertResult c n :=
adamc@97 664 makeRbtree (ins t).
adamc@94 665
adamc@214 666 (** 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 667
adamc@95 668 Section present.
adamc@95 669 Variable z : nat.
adamc@95 670
adamc@214 671 (** 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 672
adam@367 673 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 674
adamc@98 675 Ltac present_balance :=
adamc@98 676 crush;
adamc@98 677 repeat (match goal with
adam@405 678 | [ _ : context[match ?T with Leaf => _ | _ => _ end] |- _ ] => dep_destruct T
adam@405 679 | [ |- context[match ?T with Leaf => _ | _ => _ end] ] => dep_destruct T
adamc@98 680 end; crush).
adamc@98 681
adamc@214 682 (** 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 683
adam@294 684 Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n),
adamc@95 685 present z (projT2 (balance1 a y b))
adamc@95 686 <-> rpresent z a \/ z = y \/ present z b.
adamc@98 687 destruct a; present_balance.
adamc@95 688 Qed.
adamc@95 689
adamc@213 690 Lemma present_balance2 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n),
adamc@95 691 present z (projT2 (balance2 a y b))
adamc@95 692 <-> rpresent z a \/ z = y \/ present z b.
adamc@98 693 destruct a; present_balance.
adamc@95 694 Qed.
adamc@95 695
adamc@214 696 (** 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 697
adamc@95 698 Definition present_insResult c n :=
adamc@95 699 match c return (rbtree c n -> insResult c n -> Prop) with
adamc@95 700 | Red => fun t r => rpresent z r <-> z = x \/ present z t
adamc@95 701 | Black => fun t r => present z (projT2 r) <-> z = x \/ present z t
adamc@95 702 end.
adamc@95 703
adamc@214 704 (** 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 705
adamc@95 706 Theorem present_ins : forall c n (t : rbtree c n),
adamc@95 707 present_insResult t (ins t).
adamc@95 708 induction t; crush;
adamc@95 709 repeat (match goal with
adam@338 710 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
adamc@95 711 | [ |- context[if ?E then _ else _] ] => destruct E
adam@338 712 | [ _ : context[match ?C with Red => _ | Black => _ end]
adamc@214 713 |- _ ] => destruct C
adamc@95 714 end; crush);
adamc@95 715 try match goal with
adam@338 716 | [ _ : context[balance1 ?A ?B ?C] |- _ ] =>
adamc@95 717 generalize (present_balance1 A B C)
adamc@95 718 end;
adamc@95 719 try match goal with
adam@338 720 | [ _ : context[balance2 ?A ?B ?C] |- _ ] =>
adamc@95 721 generalize (present_balance2 A B C)
adamc@95 722 end;
adamc@95 723 try match goal with
adamc@95 724 | [ |- context[balance1 ?A ?B ?C] ] =>
adamc@95 725 generalize (present_balance1 A B C)
adamc@95 726 end;
adamc@95 727 try match goal with
adamc@95 728 | [ |- context[balance2 ?A ?B ?C] ] =>
adamc@95 729 generalize (present_balance2 A B C)
adamc@95 730 end;
adamc@214 731 crush;
adamc@95 732 match goal with
adamc@95 733 | [ z : nat, x : nat |- _ ] =>
adamc@95 734 match goal with
adamc@95 735 | [ H : z = x |- _ ] => rewrite H in *; clear H
adamc@95 736 end
adamc@95 737 end;
adamc@95 738 tauto.
adamc@95 739 Qed.
adamc@95 740
adamc@214 741 (** 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 742
adamc@213 743 Ltac present_insert :=
adamc@213 744 unfold insert; intros n t; inversion t;
adamc@97 745 generalize (present_ins t); simpl;
adamc@97 746 dep_destruct (ins t); tauto.
adamc@97 747
adamc@95 748 Theorem present_insert_Red : forall n (t : rbtree Red n),
adamc@95 749 present z (insert t)
adamc@95 750 <-> (z = x \/ present z t).
adamc@213 751 present_insert.
adamc@95 752 Qed.
adamc@95 753
adamc@95 754 Theorem present_insert_Black : forall n (t : rbtree Black n),
adamc@95 755 present z (projT2 (insert t))
adamc@95 756 <-> (z = x \/ present z t).
adamc@213 757 present_insert.
adamc@95 758 Qed.
adamc@95 759 End present.
adamc@94 760 End insert.
adamc@94 761
adam@398 762 (** We can generate executable OCaml code with the command %\index{Vernacular commands!Recursive Extraction}%[Recursive Extraction insert], which also automatically outputs the OCaml versions of all of [insert]'s dependencies. In our previous extractions, we wound up with clean OCaml code. Here, we find uses of %\index{Obj.magic}\texttt{%#<tt>#Obj.magic#</tt>#%}%, OCaml's unsafe cast operator for tweaking the apparent type of an expression in an arbitrary way. Casts appear for this example because the return type of [insert] depends on the _value_ of the function's argument, a pattern which OCaml cannot handle. Since Coq's type system is much more expressive than OCaml's, such casts are unavoidable in general. Since the OCaml type-checker is no longer checking full safety of programs, we must rely on Coq's extractor to use casts only in provably safe ways. *)
adam@338 763
adam@338 764 (* begin hide *)
adam@338 765 Recursive Extraction insert.
adam@338 766 (* end hide *)
adam@283 767
adamc@94 768
adamc@86 769 (** * A Certified Regular Expression Matcher *)
adamc@86 770
adamc@93 771 (** 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 772
adam@338 773 Before defining the syntax of expressions, it is helpful to define an inductive type capturing the meaning of the Kleene star. That is, a string [s] matches regular expression [star e] if and only if [s] can be decomposed into a sequence of substrings that all match [e]. We use Coq's string support, which comes through a combination of the [Strings] library and some parsing notations built into Coq. Operators like [++] and functions like [length] that we know from lists are defined again for strings. Notation scopes help us control which versions we want to use in particular contexts.%\index{Vernacular commands!Open Scope}% *)
adamc@93 774
adamc@86 775 Require Import Ascii String.
adamc@86 776 Open Scope string_scope.
adamc@86 777
adamc@91 778 Section star.
adamc@91 779 Variable P : string -> Prop.
adamc@91 780
adamc@91 781 Inductive star : string -> Prop :=
adamc@91 782 | Empty : star ""
adamc@91 783 | Iter : forall s1 s2,
adamc@91 784 P s1
adamc@91 785 -> star s2
adamc@91 786 -> star (s1 ++ s2).
adamc@91 787 End star.
adamc@91 788
adam@283 789 (** 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 790 [[
adamc@93 791 Inductive regexp : (string -> Prop) -> Set :=
adamc@93 792 | Char : forall ch : ascii,
adamc@93 793 regexp (fun s => s = String ch "")
adamc@93 794 | Concat : forall (P1 P2 : string -> Prop) (r1 : regexp P1) (r2 : regexp P2),
adamc@93 795 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2).
adamc@93 796 ]]
adamc@93 797
adam@338 798 <<
adam@338 799 User error: Large non-propositional inductive types must be in Type
adam@338 800 >>
adam@338 801
adam@338 802 What is a %\index{large inductive types}%large inductive type? In Coq, it is an inductive type that has a constructor which quantifies over some type of type [Type]. We have not worked with [Type] very much to this point. Every term of CIC has a type, including [Set] and [Prop], which are assigned type [Type]. The type [string -> Prop] from the failed definition also has type [Type].
adamc@93 803
adamc@93 804 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 805
adamc@89 806 Inductive regexp : (string -> Prop) -> Type :=
adamc@86 807 | Char : forall ch : ascii,
adamc@86 808 regexp (fun s => s = String ch "")
adamc@86 809 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
adamc@87 810 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2)
adamc@87 811 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
adamc@91 812 regexp (fun s => P1 s \/ P2 s)
adamc@91 813 | Star : forall P (r : regexp P),
adamc@91 814 regexp (star P).
adamc@86 815
adam@296 816 (** 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 817
adamc@93 818 (* begin hide *)
adamc@86 819 Open Scope specif_scope.
adamc@86 820
adamc@86 821 Lemma length_emp : length "" <= 0.
adamc@86 822 crush.
adamc@86 823 Qed.
adamc@86 824
adamc@86 825 Lemma append_emp : forall s, s = "" ++ s.
adamc@86 826 crush.
adamc@86 827 Qed.
adamc@86 828
adamc@86 829 Ltac substring :=
adamc@86 830 crush;
adamc@86 831 repeat match goal with
adamc@86 832 | [ |- context[match ?N with O => _ | S _ => _ end] ] => destruct N; crush
adamc@86 833 end.
adamc@86 834
adamc@86 835 Lemma substring_le : forall s n m,
adamc@86 836 length (substring n m s) <= m.
adamc@86 837 induction s; substring.
adamc@86 838 Qed.
adamc@86 839
adamc@86 840 Lemma substring_all : forall s,
adamc@86 841 substring 0 (length s) s = s.
adamc@86 842 induction s; substring.
adamc@86 843 Qed.
adamc@86 844
adamc@86 845 Lemma substring_none : forall s n,
adamc@93 846 substring n 0 s = "".
adamc@86 847 induction s; substring.
adamc@86 848 Qed.
adamc@86 849
adam@375 850 Hint Rewrite substring_all substring_none.
adamc@86 851
adamc@86 852 Lemma substring_split : forall s m,
adamc@86 853 substring 0 m s ++ substring m (length s - m) s = s.
adamc@86 854 induction s; substring.
adamc@86 855 Qed.
adamc@86 856
adamc@86 857 Lemma length_app1 : forall s1 s2,
adamc@86 858 length s1 <= length (s1 ++ s2).
adamc@86 859 induction s1; crush.
adamc@86 860 Qed.
adamc@86 861
adamc@86 862 Hint Resolve length_emp append_emp substring_le substring_split length_app1.
adamc@86 863
adamc@86 864 Lemma substring_app_fst : forall s2 s1 n,
adamc@86 865 length s1 = n
adamc@86 866 -> substring 0 n (s1 ++ s2) = s1.
adamc@86 867 induction s1; crush.
adamc@86 868 Qed.
adamc@86 869
adamc@86 870 Lemma substring_app_snd : forall s2 s1 n,
adamc@86 871 length s1 = n
adamc@86 872 -> substring n (length (s1 ++ s2) - n) (s1 ++ s2) = s2.
adam@375 873 Hint Rewrite <- minus_n_O.
adamc@86 874
adamc@86 875 induction s1; crush.
adamc@86 876 Qed.
adamc@86 877
adam@375 878 Hint Rewrite substring_app_fst substring_app_snd using solve [trivial].
adamc@93 879 (* end hide *)
adamc@93 880
adamc@93 881 (** 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 882
adamc@86 883 Section split.
adamc@86 884 Variables P1 P2 : string -> Prop.
adamc@214 885 Variable P1_dec : forall s, {P1 s} + {~ P1 s}.
adamc@214 886 Variable P2_dec : forall s, {P2 s} + {~ P2 s}.
adamc@93 887 (** We require a choice of two arbitrary string predicates and functions for deciding them. *)
adamc@86 888
adamc@86 889 Variable s : string.
adamc@93 890 (** 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 891
adam@338 892 (** 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 893
adam@297 894 Definition split' : forall n : nat, n <= length s
adamc@86 895 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
adamc@214 896 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2}.
adamc@86 897 refine (fix F (n : nat) : n <= length s
adamc@86 898 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
adamc@214 899 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2} :=
adamc@214 900 match n with
adamc@86 901 | O => fun _ => Reduce (P1_dec "" && P2_dec s)
adamc@93 902 | S n' => fun _ => (P1_dec (substring 0 (S n') s)
adamc@93 903 && P2_dec (substring (S n') (length s - S n') s))
adamc@86 904 || F n' _
adamc@86 905 end); clear F; crush; eauto 7;
adamc@86 906 match goal with
adamc@86 907 | [ _ : length ?S <= 0 |- _ ] => destruct S
adam@338 908 | [ _ : length ?S' <= S ?N |- _ ] => destruct (eq_nat_dec (length S') (S N))
adamc@86 909 end; crush.
adamc@86 910 Defined.
adamc@86 911
adam@338 912 (** 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 913 [[
adamc@93 914 | S n' => fun _ => let n := S n' in
adamc@93 915 (P1_dec (substring 0 n s)
adamc@93 916 && P2_dec (substring n (length s - n) s))
adamc@93 917 || F n' _
adamc@214 918
adamc@93 919 ]]
adamc@93 920
adam@338 921 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 922
adamc@86 923 Definition split : {exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2}
adamc@214 924 + {forall s1 s2, s = s1 ++ s2 -> ~ P1 s1 \/ ~ P2 s2}.
adamc@86 925 refine (Reduce (split' (n := length s) _)); crush; eauto.
adamc@86 926 Defined.
adamc@86 927 End split.
adamc@86 928
adamc@86 929 Implicit Arguments split [P1 P2].
adamc@86 930
adamc@93 931 (* begin hide *)
adamc@91 932 Lemma app_empty_end : forall s, s ++ "" = s.
adamc@91 933 induction s; crush.
adamc@91 934 Qed.
adamc@91 935
adam@375 936 Hint Rewrite app_empty_end.
adamc@91 937
adamc@91 938 Lemma substring_self : forall s n,
adamc@91 939 n <= 0
adamc@91 940 -> substring n (length s - n) s = s.
adamc@91 941 induction s; substring.
adamc@91 942 Qed.
adamc@91 943
adamc@91 944 Lemma substring_empty : forall s n m,
adamc@91 945 m <= 0
adamc@91 946 -> substring n m s = "".
adamc@91 947 induction s; substring.
adamc@91 948 Qed.
adamc@91 949
adam@375 950 Hint Rewrite substring_self substring_empty using omega.
adamc@91 951
adamc@91 952 Lemma substring_split' : forall s n m,
adamc@91 953 substring n m s ++ substring (n + m) (length s - (n + m)) s
adamc@91 954 = substring n (length s - n) s.
adam@375 955 Hint Rewrite substring_split.
adamc@91 956
adamc@91 957 induction s; substring.
adamc@91 958 Qed.
adamc@91 959
adamc@91 960 Lemma substring_stack : forall s n2 m1 m2,
adamc@91 961 m1 <= m2
adamc@91 962 -> substring 0 m1 (substring n2 m2 s)
adamc@91 963 = substring n2 m1 s.
adamc@91 964 induction s; substring.
adamc@91 965 Qed.
adamc@91 966
adamc@91 967 Ltac substring' :=
adamc@91 968 crush;
adamc@91 969 repeat match goal with
adamc@91 970 | [ |- context[match ?N with O => _ | S _ => _ end] ] => case_eq N; crush
adamc@91 971 end.
adamc@91 972
adamc@91 973 Lemma substring_stack' : forall s n1 n2 m1 m2,
adamc@91 974 n1 + m1 <= m2
adamc@91 975 -> substring n1 m1 (substring n2 m2 s)
adamc@91 976 = substring (n1 + n2) m1 s.
adamc@91 977 induction s; substring';
adamc@91 978 match goal with
adamc@91 979 | [ |- substring ?N1 _ _ = substring ?N2 _ _ ] =>
adamc@91 980 replace N1 with N2; crush
adamc@91 981 end.
adamc@91 982 Qed.
adamc@91 983
adamc@91 984 Lemma substring_suffix : forall s n,
adamc@91 985 n <= length s
adamc@91 986 -> length (substring n (length s - n) s) = length s - n.
adamc@91 987 induction s; substring.
adamc@91 988 Qed.
adamc@91 989
adamc@91 990 Lemma substring_suffix_emp' : forall s n m,
adamc@91 991 substring n (S m) s = ""
adamc@91 992 -> n >= length s.
adamc@91 993 induction s; crush;
adamc@91 994 match goal with
adamc@91 995 | [ |- ?N >= _ ] => destruct N; crush
adamc@91 996 end;
adamc@91 997 match goal with
adamc@91 998 [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | omega ]
adamc@91 999 end.
adamc@91 1000 Qed.
adamc@91 1001
adamc@91 1002 Lemma substring_suffix_emp : forall s n m,
adamc@92 1003 substring n m s = ""
adamc@92 1004 -> m > 0
adamc@91 1005 -> n >= length s.
adam@335 1006 destruct m as [ | m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
adamc@91 1007 Qed.
adamc@91 1008
adamc@91 1009 Hint Rewrite substring_stack substring_stack' substring_suffix
adam@375 1010 using omega.
adamc@91 1011
adamc@91 1012 Lemma minus_minus : forall n m1 m2,
adamc@91 1013 m1 + m2 <= n
adamc@91 1014 -> n - m1 - m2 = n - (m1 + m2).
adamc@91 1015 intros; omega.
adamc@91 1016 Qed.
adamc@91 1017
adamc@91 1018 Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n.
adamc@91 1019 intros; omega.
adamc@91 1020 Qed.
adamc@91 1021
adam@375 1022 Hint Rewrite minus_minus using omega.
adamc@93 1023 (* end hide *)
adamc@93 1024
adamc@93 1025 (** 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 1026
adamc@91 1027 Section dec_star.
adamc@91 1028 Variable P : string -> Prop.
adamc@214 1029 Variable P_dec : forall s, {P s} + {~ P s}.
adamc@91 1030
adam@338 1031 (** 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 1032
adamc@93 1033 (* begin hide *)
adamc@91 1034 Hint Constructors star.
adamc@91 1035
adamc@91 1036 Lemma star_empty : forall s,
adamc@91 1037 length s = 0
adamc@91 1038 -> star P s.
adamc@91 1039 destruct s; crush.
adamc@91 1040 Qed.
adamc@91 1041
adamc@91 1042 Lemma star_singleton : forall s, P s -> star P s.
adamc@91 1043 intros; rewrite <- (app_empty_end s); auto.
adamc@91 1044 Qed.
adamc@91 1045
adamc@91 1046 Lemma star_app : forall s n m,
adamc@91 1047 P (substring n m s)
adamc@91 1048 -> star P (substring (n + m) (length s - (n + m)) s)
adamc@91 1049 -> star P (substring n (length s - n) s).
adamc@91 1050 induction n; substring;
adamc@91 1051 match goal with
adamc@91 1052 | [ H : P (substring ?N ?M ?S) |- _ ] =>
adamc@91 1053 solve [ rewrite <- (substring_split S M); auto
adamc@91 1054 | rewrite <- (substring_split' S N M); auto ]
adamc@91 1055 end.
adamc@91 1056 Qed.
adamc@91 1057
adamc@91 1058 Hint Resolve star_empty star_singleton star_app.
adamc@91 1059
adamc@91 1060 Variable s : string.
adamc@91 1061
adamc@91 1062 Lemma star_inv : forall s,
adamc@91 1063 star P s
adamc@91 1064 -> s = ""
adamc@91 1065 \/ exists i, i < length s
adamc@91 1066 /\ P (substring 0 (S i) s)
adamc@91 1067 /\ star P (substring (S i) (length s - S i) s).
adamc@91 1068 Hint Extern 1 (exists i : nat, _) =>
adamc@91 1069 match goal with
adamc@91 1070 | [ H : P (String _ ?S) |- _ ] => exists (length S); crush
adamc@91 1071 end.
adamc@91 1072
adamc@91 1073 induction 1; [
adamc@91 1074 crush
adamc@91 1075 | match goal with
adamc@91 1076 | [ _ : P ?S |- _ ] => destruct S; crush
adamc@91 1077 end
adamc@91 1078 ].
adamc@91 1079 Qed.
adamc@91 1080
adamc@91 1081 Lemma star_substring_inv : forall n,
adamc@91 1082 n <= length s
adamc@91 1083 -> star P (substring n (length s - n) s)
adamc@91 1084 -> substring n (length s - n) s = ""
adamc@91 1085 \/ exists l, l < length s - n
adamc@91 1086 /\ P (substring n (S l) s)
adamc@91 1087 /\ star P (substring (n + S l) (length s - (n + S l)) s).
adam@375 1088 Hint Rewrite plus_n_Sm'.
adamc@91 1089
adamc@91 1090 intros;
adamc@91 1091 match goal with
adamc@91 1092 | [ H : star _ _ |- _ ] => generalize (star_inv H); do 3 crush; eauto
adamc@91 1093 end.
adamc@91 1094 Qed.
adamc@93 1095 (* end hide *)
adamc@93 1096
adamc@93 1097 (** 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 1098
adamc@91 1099 Section dec_star''.
adamc@91 1100 Variable n : nat.
adamc@93 1101 (** [n] is the length of the prefix of [s] that we have already processed. *)
adamc@91 1102
adamc@91 1103 Variable P' : string -> Prop.
adamc@91 1104 Variable P'_dec : forall n' : nat, n' > n
adamc@91 1105 -> {P' (substring n' (length s - n') s)}
adamc@214 1106 + {~ P' (substring n' (length s - n') s)}.
adamc@93 1107 (** 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 1108
adamc@93 1109 (** 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 1110
adam@297 1111 Definition dec_star'' : forall l : nat,
adam@297 1112 {exists l', S l' <= l
adamc@91 1113 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
adamc@91 1114 + {forall l', S l' <= l
adamc@214 1115 -> ~ P (substring n (S l') s)
adamc@214 1116 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)}.
adamc@91 1117 refine (fix F (l : nat) : {exists l', S l' <= l
adamc@91 1118 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
adamc@91 1119 + {forall l', S l' <= l
adamc@214 1120 -> ~ P (substring n (S l') s)
adamc@214 1121 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} :=
adam@380 1122 match l return {exists l', S l' <= l
adam@380 1123 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
adam@380 1124 + {forall l', S l' <= l
adam@380 1125 -> ~ P (substring n (S l') s)
adam@380 1126 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} with
adamc@91 1127 | O => _
adamc@91 1128 | S l' =>
adamc@91 1129 (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
adamc@91 1130 || F l'
adamc@91 1131 end); clear F; crush; eauto 7;
adamc@91 1132 match goal with
adamc@91 1133 | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush
adamc@91 1134 end.
adamc@91 1135 Defined.
adamc@91 1136 End dec_star''.
adamc@91 1137
adamc@93 1138 (* begin hide *)
adamc@92 1139 Lemma star_length_contra : forall n,
adamc@92 1140 length s > n
adamc@92 1141 -> n >= length s
adamc@92 1142 -> False.
adamc@92 1143 crush.
adamc@92 1144 Qed.
adamc@92 1145
adamc@92 1146 Lemma star_length_flip : forall n n',
adamc@92 1147 length s - n <= S n'
adamc@92 1148 -> length s > n
adamc@92 1149 -> length s - n > 0.
adamc@92 1150 crush.
adamc@92 1151 Qed.
adamc@92 1152
adamc@92 1153 Hint Resolve star_length_contra star_length_flip substring_suffix_emp.
adamc@93 1154 (* end hide *)
adamc@92 1155
adamc@93 1156 (** 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 1157
adam@297 1158 Definition dec_star' : forall n n' : nat, length s - n' <= n
adamc@91 1159 -> {star P (substring n' (length s - n') s)}
adamc@214 1160 + {~ star P (substring n' (length s - n') s)}.
adamc@214 1161 refine (fix F (n n' : nat) : length s - n' <= n
adamc@91 1162 -> {star P (substring n' (length s - n') s)}
adamc@214 1163 + {~ star P (substring n' (length s - n') s)} :=
adamc@214 1164 match n with
adamc@91 1165 | O => fun _ => Yes
adamc@91 1166 | S n'' => fun _ =>
adamc@91 1167 le_gt_dec (length s) n'
adam@338 1168 || dec_star'' (n := n') (star P)
adam@338 1169 (fun n0 _ => Reduce (F n'' n0 _)) (length s - n')
adamc@92 1170 end); clear F; crush; eauto;
adamc@92 1171 match goal with
adamc@92 1172 | [ H : star _ _ |- _ ] => apply star_substring_inv in H; crush; eauto
adamc@92 1173 end;
adamc@92 1174 match goal with
adamc@92 1175 | [ H1 : _ < _ - _, H2 : forall l' : nat, _ <= _ - _ -> _ |- _ ] =>
adamc@92 1176 generalize (H2 _ (lt_le_S _ _ H1)); tauto
adamc@92 1177 end.
adamc@91 1178 Defined.
adamc@91 1179
adam@380 1180 (** Finally, we have [dec_star], defined by straightforward reduction from [dec_star']. *)
adamc@93 1181
adamc@214 1182 Definition dec_star : {star P s} + {~ star P s}.
adam@380 1183 refine (Reduce (dec_star' (n := length s) 0 _)); crush.
adamc@91 1184 Defined.
adamc@91 1185 End dec_star.
adamc@91 1186
adamc@93 1187 (* begin hide *)
adamc@86 1188 Lemma app_cong : forall x1 y1 x2 y2,
adamc@86 1189 x1 = x2
adamc@86 1190 -> y1 = y2
adamc@86 1191 -> x1 ++ y1 = x2 ++ y2.
adamc@86 1192 congruence.
adamc@86 1193 Qed.
adamc@86 1194
adamc@86 1195 Hint Resolve app_cong.
adamc@93 1196 (* end hide *)
adamc@93 1197
adamc@93 1198 (** 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 1199
adam@297 1200 Definition matches : forall P (r : regexp P) s, {P s} + {~ P s}.
adamc@214 1201 refine (fix F P (r : regexp P) s : {P s} + {~ P s} :=
adamc@86 1202 match r with
adamc@86 1203 | Char ch => string_dec s (String ch "")
adamc@86 1204 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s)
adamc@87 1205 | Or _ _ r1 r2 => F _ r1 s || F _ r2 s
adamc@91 1206 | Star _ r => dec_star _ _ _
adamc@86 1207 end); crush;
adamc@86 1208 match goal with
adamc@86 1209 | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _))
adamc@93 1210 end; tauto.
adamc@86 1211 Defined.
adamc@86 1212
adam@283 1213 (** 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 1214
adamc@93 1215 (* begin hide *)
adamc@86 1216 Example hi := Concat (Char "h"%char) (Char "i"%char).
adam@380 1217 Eval hnf in matches hi "hi".
adam@380 1218 Eval hnf in matches hi "bye".
adamc@87 1219
adamc@87 1220 Example a_b := Or (Char "a"%char) (Char "b"%char).
adam@380 1221 Eval hnf in matches a_b "".
adam@380 1222 Eval hnf in matches a_b "a".
adam@380 1223 Eval hnf in matches a_b "aa".
adam@380 1224 Eval hnf in matches a_b "b".
adam@283 1225 (* end hide *)
adam@283 1226
adam@405 1227 (** 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. *)
adamc@91 1228
adamc@91 1229 Example a_star := Star (Char "a"%char).
adam@380 1230 Eval hnf in matches a_star "".
adam@380 1231 Eval hnf in matches a_star "a".
adam@380 1232 Eval hnf in matches a_star "b".
adam@380 1233 Eval hnf in matches a_star "aa".
adam@283 1234
adam@283 1235 (** 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. *)