Mercurial > cpdt > repo

annotate src/MoreDep.v @ 213:c4b1c0de7af9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of MoreDep port; new [dep_destruct] based on [dependent destruction]
author Adam Chlipala <adamc@hcoop.net>
date Wed, 11 Nov 2009 10:27:47 -0500
parents cbf2f74a5130
children 768889c969e9
rev   line source
adamc@213 1 (* Copyright (c) 2008-2009, 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
adamc@86 13 Require Import Tactics 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
adamc@83 21 (** Subset types and their relatives help us integrate verification with programming. Though they reorganize the certified programmer's workflow, they tend not to have deep effects on proofs. We write largely the same proofs as we would for classical verification, with some of the structure moved into the programs themselves. It turns out that, when we use dependent types to their full potential, we warp the development and proving process even more than that, picking up "free theorems" to the extent that often a certified program is hardly more complex than its uncertified counterpart in Haskell or ML.
adamc@83 22
adamc@83 23 In particular, we have only scratched the tip of the iceberg that is Coq's inductive definition mechanism. The inductive types we have seen so far have their counterparts in the other proof assistants that we surveyed in Chapter 1. This chapter explores the strange new world of dependent inductive datatypes (that is, dependent inductive types outside [Prop]), a possibility which sets Coq apart from all of the competition not based on type theory. *)
adamc@83 24
adamc@84 25
adamc@84 26 (** * Length-Indexed Lists *)
adamc@84 27
adamc@84 28 (** Many introductions to dependent types start out by showing how to use them to eliminate array bounds checks. When the type of an array tells you how many elements it has, your compiler can detect out-of-bounds dereferences statically. Since we are working in a pure functional language, the next best thing is length-indexed lists, which the following code defines. *)
adamc@84 29
adamc@84 30 Section ilist.
adamc@84 31 Variable A : Set.
adamc@84 32
adamc@84 33 Inductive ilist : nat -> Set :=
adamc@84 34 | Nil : ilist O
adamc@84 35 | Cons : forall n, A -> ilist n -> ilist (S n).
adamc@84 36
adamc@84 37 (** We see that, within its section, [ilist] is given type [nat -> Set]. Previously, every inductive type we have seen has either had plain [Set] as its type or has been a predicate with some type ending in [Prop]. The full generality of inductive definitions lets us integrate the expressivity of predicates directly into our normal programming.
adamc@84 38
adamc@84 39 The [nat] argument to [ilist] tells us the length of the list. The types of [ilist]'s constructors tell us that a [Nil] list has length [O] and that a [Cons] list has length one greater than the length of its sublist. We may apply [ilist] to any natural number, even natural numbers that are only known at runtime. It is this breaking of the %\textit{%#<i>#phase distinction#</i>#%}% that characterizes [ilist] as %\textit{%#<i>#dependently typed#</i>#%}%.
adamc@84 40
adamc@213 41 In expositions of list types, we usually see the length function defined first, but here that would not be a very productive function to code. Instead, let us implement list concatenation. *)
adamc@84 42
adamc@213 43 Fixpoint app n1 (ls1 : ilist n1) n2 (ls2 : ilist n2) : ilist (n1 + n2) :=
adamc@213 44 match ls1 with
adamc@213 45 | Nil => ls2
adamc@213 46 | Cons _ x ls1' => Cons x (app ls1' ls2)
adamc@213 47 end.
adamc@84 48
adamc@213 49 (** In Coq version 8.1 and earlier, this definition leads to an error message:
adamc@84 50
adamc@84 51 [[
adamc@84 52 The term "ls2" has type "ilist n2" while it is expected to have type
adamc@84 53 "ilist (?14 + n2)"
adamc@213 54
adamc@84 55 ]]
adamc@84 56
adamc@213 57 In Coq's core language, without explicit annotations, Coq does not enrich our typing assumptions in the branches of a [match] expression. It is clear that the unification variable [?14] should be resolved to 0 in this context, so that we have [0 + n2] reducing to [n2], but Coq does not realize that. We cannot fix the problem using just the simple [return] clauses we applied in the last chapter. We need to combine a [return] clause with a new kind of annotation, an [in] clause. This is exactly what the inference heuristics do in Coq 8.2 and later.
adamc@213 58
adamc@213 59 Specifically, Coq infers the following definition from the simpler one. *)
adamc@84 60
adamc@100 61 (* EX: Implement concatenation *)
adamc@100 62
adamc@100 63 (* begin thide *)
adamc@213 64 Fixpoint app' n1 (ls1 : ilist n1) n2 (ls2 : ilist n2) : ilist (n1 + n2) :=
adamc@84 65 match ls1 in (ilist n1) return (ilist (n1 + n2)) with
adamc@84 66 | Nil => ls2
adamc@213 67 | Cons _ x ls1' => Cons x (app' ls1' ls2)
adamc@84 68 end.
adamc@100 69 (* end thide *)
adamc@84 70
adamc@213 71 (** Using [return] alone allowed us to express a dependency of the [match] result type on the %\textit{%#<i>#value#</i>#%}% of the discriminee. What [in] adds to our arsenal is a way of expressing a dependency on the %\textit{%#<i>#type#</i>#%}% of the discriminee. Specifically, the [n1] in the [in] clause above is a %\textit{%#<i>#binding occurrence#</i>#%}% whose scope is the [return] clause.
adamc@84 72
adamc@84 73 We may use [in] clauses only to bind names for the arguments of an inductive type family. That is, each [in] clause must be an inductive type family name applied to a sequence of underscores and variable names of the proper length. The positions for %\textit{%#<i>#parameters#</i>#%}% to the type family must all be underscores. Parameters are those arguments declared with section variables or with entries to the left of the first colon in an inductive definition. They cannot vary depending on which constructor was used to build the discriminee, so Coq prohibits pointless matches on them. It is those arguments defined in the type to the right of the colon that we may name with [in] clauses.
adamc@84 74
adamc@84 75 Our [app] function could be typed in so-called %\textit{%#<i>#stratified#</i>#%}% type systems, which avoid true dependency. We could consider the length indices to lists to live in a separate, compile-time-only universe from the lists themselves. Our next example would be harder to implement in a stratified system. We write an injection function from regular lists to length-indexed lists. A stratified implementation would need to duplicate the definition of lists across compile-time and run-time versions, and the run-time versions would need to be indexed by the compile-time versions. *)
adamc@84 76
adamc@100 77 (* EX: Implement injection from normal lists *)
adamc@100 78
adamc@100 79 (* begin thide *)
adamc@84 80 Fixpoint inject (ls : list A) : ilist (length ls) :=
adamc@213 81 match ls with
adamc@84 82 | nil => Nil
adamc@84 83 | h :: t => Cons h (inject t)
adamc@84 84 end.
adamc@84 85
adamc@84 86 (** We can define an inverse conversion and prove that it really is an inverse. *)
adamc@84 87
adamc@213 88 Fixpoint unject n (ls : ilist n) : list A :=
adamc@84 89 match ls with
adamc@84 90 | Nil => nil
adamc@84 91 | Cons _ h t => h :: unject t
adamc@84 92 end.
adamc@84 93
adamc@84 94 Theorem inject_inverse : forall ls, unject (inject ls) = ls.
adamc@84 95 induction ls; crush.
adamc@84 96 Qed.
adamc@100 97 (* end thide *)
adamc@100 98
adamc@100 99 (* EX: Implement statically-checked "car"/"hd" *)
adamc@84 100
adamc@84 101 (** Now let us attempt a function that is surprisingly tricky to write. In ML, the list head function raises an exception when passed an empty list. With length-indexed lists, we can rule out such invalid calls statically, and here is a first attempt at doing so.
adamc@84 102
adamc@84 103 [[
adamc@84 104 Definition hd n (ls : ilist (S n)) : A :=
adamc@84 105 match ls with
adamc@84 106 | Nil => ???
adamc@84 107 | Cons _ h _ => h
adamc@84 108 end.
adamc@213 109
adamc@213 110 ]]
adamc@84 111
adamc@84 112 It is not clear what to write for the [Nil] case, so we are stuck before we even turn our function over to the type checker. We could try omitting the [Nil] case:
adamc@84 113
adamc@84 114 [[
adamc@84 115 Definition hd n (ls : ilist (S n)) : A :=
adamc@84 116 match ls with
adamc@84 117 | Cons _ h _ => h
adamc@84 118 end.
adamc@84 119
adamc@84 120 Error: Non exhaustive pattern-matching: no clause found for pattern Nil
adamc@213 121
adamc@84 122 ]]
adamc@84 123
adamc@84 124 Unlike in ML, we cannot use inexhaustive pattern matching, becuase there is no conception of a %\texttt{%#<tt>#Match#</tt>#%}% exception to be thrown. We might try using an [in] clause somehow.
adamc@84 125
adamc@84 126 [[
adamc@84 127 Definition hd n (ls : ilist (S n)) : A :=
adamc@84 128 match ls in (ilist (S n)) with
adamc@84 129 | Cons _ h _ => h
adamc@84 130 end.
adamc@84 131
adamc@84 132 Error: The reference n was not found in the current environment
adamc@213 133
adamc@84 134 ]]
adamc@84 135
adamc@84 136 In this and other cases, we feel like we want [in] clauses with type family arguments that are not variables. Unfortunately, Coq only supports variables in those positions. A completely general mechanism could only be supported with a solution to the problem of higher-order unification, which is undecidable. There %\textit{%#<i>#are#</i>#%}% useful heuristics for handling non-variable indices which are gradually making their way into Coq, but we will spend some time in this and the next few chapters on effective pattern matching on dependent types using only the primitive [match] annotations.
adamc@84 137
adamc@84 138 Our final, working attempt at [hd] uses an auxiliary function and a surprising [return] annotation. *)
adamc@84 139
adamc@100 140 (* begin thide *)
adamc@84 141 Definition hd' n (ls : ilist n) :=
adamc@84 142 match ls in (ilist n) return (match n with O => unit | S _ => A end) with
adamc@84 143 | Nil => tt
adamc@84 144 | Cons _ h _ => h
adamc@84 145 end.
adamc@84 146
adamc@84 147 Definition hd n (ls : ilist (S n)) : A := hd' ls.
adamc@100 148 (* end thide *)
adamc@84 149
adamc@84 150 (** 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 151
adamc@84 152 End ilist.
adamc@85 153
adamc@85 154
adamc@85 155 (** * A Tagless Interpreter *)
adamc@85 156
adamc@85 157 (** A favorite example for motivating the power of functional programming is implementation of a simple expression language interpreter. In ML and Haskell, such interpreters are often implemented using an algebraic datatype of values, where at many points it is checked that a value was built with the right constructor of the value type. With dependent types, we can implement a %\textit{%#<i>#tagless#</i>#%}% interpreter that both removes this source of runtime ineffiency and gives us more confidence that our implementation is correct. *)
adamc@85 158
adamc@85 159 Inductive type : Set :=
adamc@85 160 | Nat : type
adamc@85 161 | Bool : type
adamc@85 162 | Prod : type -> type -> type.
adamc@85 163
adamc@85 164 Inductive exp : type -> Set :=
adamc@85 165 | NConst : nat -> exp Nat
adamc@85 166 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@85 167 | Eq : exp Nat -> exp Nat -> exp Bool
adamc@85 168
adamc@85 169 | BConst : bool -> exp Bool
adamc@85 170 | And : exp Bool -> exp Bool -> exp Bool
adamc@85 171 | If : forall t, exp Bool -> exp t -> exp t -> exp t
adamc@85 172
adamc@85 173 | Pair : forall t1 t2, exp t1 -> exp t2 -> exp (Prod t1 t2)
adamc@85 174 | Fst : forall t1 t2, exp (Prod t1 t2) -> exp t1
adamc@85 175 | Snd : forall t1 t2, exp (Prod t1 t2) -> exp t2.
adamc@85 176
adamc@85 177 (** 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 178
adamc@85 179 We can give types and expressions semantics in a new style, based critically on the chance for %\textit{%#<i>#type-level computation#</i>#%}%. *)
adamc@85 180
adamc@85 181 Fixpoint typeDenote (t : type) : Set :=
adamc@85 182 match t with
adamc@85 183 | Nat => nat
adamc@85 184 | Bool => bool
adamc@85 185 | Prod t1 t2 => typeDenote t1 * typeDenote t2
adamc@85 186 end%type.
adamc@85 187
adamc@85 188 (** [typeDenote] compiles types of our object language into "native" Coq types. It is deceptively easy to implement. The only new thing we see is the [%type] annotation, which tells Coq to parse the [match] expression using the notations associated with types. Without this annotation, the [*] would be interpreted as multiplication on naturals, rather than as the product type constructor. [type] is one example of an identifer bound to a %\textit{%#<i>#notation scope#</i>#%}%. We will deal more explicitly with notations and notation scopes in later chapters.
adamc@85 189
adamc@85 190 We can define a function [expDenote] that is typed in terms of [typeDenote]. *)
adamc@85 191
adamc@213 192 Fixpoint expDenote t (e : exp t) : typeDenote t :=
adamc@213 193 match e with
adamc@85 194 | NConst n => n
adamc@85 195 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@85 196 | Eq e1 e2 => if eq_nat_dec (expDenote e1) (expDenote e2) then true else false
adamc@85 197
adamc@85 198 | BConst b => b
adamc@85 199 | And e1 e2 => expDenote e1 && expDenote e2
adamc@85 200 | If _ e' e1 e2 => if expDenote e' then expDenote e1 else expDenote e2
adamc@85 201
adamc@85 202 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@85 203 | Fst _ _ e' => fst (expDenote e')
adamc@85 204 | Snd _ _ e' => snd (expDenote e')
adamc@85 205 end.
adamc@85 206
adamc@213 207 (** 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 208
adamc@85 209 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 210
adamc@85 211 [[
adamc@85 212 Definition pairOut t1 t2 (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) :=
adamc@85 213 match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with
adamc@85 214 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@85 215 | _ => None
adamc@85 216 end.
adamc@85 217
adamc@85 218 Error: The reference t2 was not found in the current environment
adamc@213 219 ]]
adamc@85 220
adamc@85 221 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 222
adamc@100 223 (* EX: Define a function [pairOut : forall t1 t2, exp (Prod t1 t2) -> option (exp t1 * exp t2)] *)
adamc@100 224
adamc@100 225 (* begin thide *)
adamc@85 226 Definition pairOutType (t : type) :=
adamc@85 227 match t with
adamc@85 228 | Prod t1 t2 => option (exp t1 * exp t2)
adamc@85 229 | _ => unit
adamc@85 230 end.
adamc@85 231
adamc@85 232 (** 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 233
adamc@85 234 Definition pairOutDefault (t : type) :=
adamc@85 235 match t return (pairOutType t) with
adamc@85 236 | Prod _ _ => None
adamc@85 237 | _ => tt
adamc@85 238 end.
adamc@85 239
adamc@85 240 (** Now [pairOut] is deceptively easy to write. *)
adamc@85 241
adamc@85 242 Definition pairOut t (e : exp t) :=
adamc@85 243 match e in (exp t) return (pairOutType t) with
adamc@85 244 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@85 245 | _ => pairOutDefault _
adamc@85 246 end.
adamc@100 247 (* end thide *)
adamc@85 248
adamc@85 249 (** There is one important subtlety in this definition. Coq allows us to use convenient ML-style pattern matching notation, but, internally and in proofs, we see that patterns are expanded out completely, matching one level of inductive structure at a time. Thus, the default case in the [match] above expands out to one case for each constructor of [exp] besides [Pair], and the underscore in [pairOutDefault _] is resolved differently in each case. From an ML or Haskell programmer's perspective, what we have here is type inference determining which code is run (returning either [None] or [tt]), which goes beyond what is possible with type inference guiding parametric polymorphism in Hindley-Milner languages, but is similar to what goes on with Haskell type classes.
adamc@85 250
adamc@213 251 With [pairOut] available, we can write [cfold] in a straightforward way. There are really no surprises beyond that Coq verifies that this code has such an expressive type, given the small annotation burden. In some places, we see that Coq's [match] annotation inference is too smart for its own good, and we have to turn that inference off by writing [return _]. *)
adamc@85 252
adamc@204 253 Fixpoint cfold t (e : exp t) : exp t :=
adamc@204 254 match e with
adamc@85 255 | NConst n => NConst n
adamc@85 256 | Plus e1 e2 =>
adamc@85 257 let e1' := cfold e1 in
adamc@85 258 let e2' := cfold e2 in
adamc@204 259 match e1', e2' return _ with
adamc@85 260 | NConst n1, NConst n2 => NConst (n1 + n2)
adamc@85 261 | _, _ => Plus e1' e2'
adamc@85 262 end
adamc@85 263 | Eq e1 e2 =>
adamc@85 264 let e1' := cfold e1 in
adamc@85 265 let e2' := cfold e2 in
adamc@204 266 match e1', e2' return _ with
adamc@85 267 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
adamc@85 268 | _, _ => Eq e1' e2'
adamc@85 269 end
adamc@85 270
adamc@85 271 | BConst b => BConst b
adamc@85 272 | And e1 e2 =>
adamc@85 273 let e1' := cfold e1 in
adamc@85 274 let e2' := cfold e2 in
adamc@204 275 match e1', e2' return _ with
adamc@85 276 | BConst b1, BConst b2 => BConst (b1 && b2)
adamc@85 277 | _, _ => And e1' e2'
adamc@85 278 end
adamc@85 279 | If _ e e1 e2 =>
adamc@85 280 let e' := cfold e in
adamc@85 281 match e' with
adamc@85 282 | BConst true => cfold e1
adamc@85 283 | BConst false => cfold e2
adamc@85 284 | _ => If e' (cfold e1) (cfold e2)
adamc@85 285 end
adamc@85 286
adamc@85 287 | Pair _ _ e1 e2 => Pair (cfold e1) (cfold e2)
adamc@85 288 | Fst _ _ e =>
adamc@85 289 let e' := cfold e in
adamc@85 290 match pairOut e' with
adamc@85 291 | Some p => fst p
adamc@85 292 | None => Fst e'
adamc@85 293 end
adamc@85 294 | Snd _ _ e =>
adamc@85 295 let e' := cfold e in
adamc@85 296 match pairOut e' with
adamc@85 297 | Some p => snd p
adamc@85 298 | None => Snd e'
adamc@85 299 end
adamc@85 300 end.
adamc@85 301
adamc@85 302 (** The correctness theorem for [cfold] turns out to be easy to prove, once we get over one serious hurdle. *)
adamc@85 303
adamc@85 304 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
adamc@100 305 (* begin thide *)
adamc@85 306 induction e; crush.
adamc@85 307
adamc@85 308 (** The first remaining subgoal is:
adamc@85 309
adamc@85 310 [[
adamc@85 311 expDenote (cfold e1) + expDenote (cfold e2) =
adamc@85 312 expDenote
adamc@85 313 match cfold e1 with
adamc@85 314 | NConst n1 =>
adamc@85 315 match cfold e2 with
adamc@85 316 | NConst n2 => NConst (n1 + n2)
adamc@85 317 | Plus _ _ => Plus (cfold e1) (cfold e2)
adamc@85 318 | Eq _ _ => Plus (cfold e1) (cfold e2)
adamc@85 319 | BConst _ => Plus (cfold e1) (cfold e2)
adamc@85 320 | And _ _ => Plus (cfold e1) (cfold e2)
adamc@85 321 | If _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 322 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 323 | Fst _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 324 | Snd _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 325 end
adamc@85 326 | Plus _ _ => Plus (cfold e1) (cfold e2)
adamc@85 327 | Eq _ _ => Plus (cfold e1) (cfold e2)
adamc@85 328 | BConst _ => Plus (cfold e1) (cfold e2)
adamc@85 329 | And _ _ => Plus (cfold e1) (cfold e2)
adamc@85 330 | If _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 331 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 332 | Fst _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 333 | Snd _ _ _ => Plus (cfold e1) (cfold e2)
adamc@85 334 end
adamc@213 335
adamc@85 336 ]]
adamc@85 337
adamc@85 338 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 339
adamc@85 340 [[
adamc@85 341 destruct (cfold e1).
adamc@85 342
adamc@85 343 User error: e1 is used in hypothesis e
adamc@213 344
adamc@85 345 ]]
adamc@85 346
adamc@85 347 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 348
adamc@213 349 For our current proof, we can use a tactic [dep_destruct] defined in the book [Tactics] module. General elimination/inversion of dependently-typed hypotheses is undecidable, since it must be implemented with [match] expressions that have the restriction on [in] clauses that we have already discussed. [dep_destruct] makes a best effort to handle some common cases, relying upon the more primitive [dependent destruction] tactic that comes with Coq. In a future chapter, we will learn about the explicit manipulation of equality proofs that is behind [dep_destruct]'s implementation in Ltac, but for now, we treat it as a useful black box. *)
adamc@85 350
adamc@85 351 dep_destruct (cfold e1).
adamc@85 352
adamc@85 353 (** 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 354
adamc@213 355 This is the only new trick we need to learn to complete the proof. We can back up and give a short, automated proof. The main inconvenience in the proof is that we cannot write a pattern that matches a [match] without including a case for every constructor of the inductive type we match over. *)
adamc@85 356
adamc@85 357 Restart.
adamc@85 358
adamc@85 359 induction e; crush;
adamc@85 360 repeat (match goal with
adamc@213 361 | [ |- context[match cfold ?E with NConst _ => _ | Plus _ _ => _
adamc@213 362 | Eq _ _ => _ | BConst _ => _ | And _ _ => _
adamc@213 363 | If _ _ _ _ => _ | Pair _ _ _ _ => _
adamc@213 364 | Fst _ _ _ => _ | Snd _ _ _ => _ end] ] =>
adamc@213 365 dep_destruct (cfold E)
adamc@213 366 | [ |- context[match pairOut (cfold ?E) with Some _ => _
adamc@213 367 | None => _ end] ] =>
adamc@213 368 dep_destruct (cfold E)
adamc@85 369 | [ |- (if ?E then _ else _) = _ ] => destruct E
adamc@85 370 end; crush).
adamc@85 371 Qed.
adamc@100 372 (* end thide *)
adamc@86 373
adamc@86 374
adamc@103 375 (** * Dependently-Typed Red-Black Trees *)
adamc@94 376
adamc@100 377 (** TODO: Add commentary for this section. *)
adamc@100 378
adamc@94 379 Inductive color : Set := Red | Black.
adamc@94 380
adamc@94 381 Inductive rbtree : color -> nat -> Set :=
adamc@94 382 | Leaf : rbtree Black 0
adamc@94 383 | RedNode : forall n, rbtree Black n -> nat-> rbtree Black n -> rbtree Red n
adamc@94 384 | BlackNode : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rbtree Black (S n).
adamc@94 385
adamc@100 386 (* EX: Prove that every [rbtree] is balanced. *)
adamc@100 387
adamc@100 388 (* begin thide *)
adamc@95 389 Require Import Max Min.
adamc@95 390
adamc@95 391 Section depth.
adamc@95 392 Variable f : nat -> nat -> nat.
adamc@95 393
adamc@95 394 Fixpoint depth c n (t : rbtree c n) {struct t} : nat :=
adamc@95 395 match t with
adamc@95 396 | Leaf => 0
adamc@95 397 | RedNode _ t1 _ t2 => S (f (depth t1) (depth t2))
adamc@95 398 | BlackNode _ _ _ t1 _ t2 => S (f (depth t1) (depth t2))
adamc@95 399 end.
adamc@95 400 End depth.
adamc@95 401
adamc@95 402 Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n.
adamc@95 403 induction t; crush;
adamc@95 404 match goal with
adamc@95 405 | [ |- context[min ?X ?Y] ] => destruct (min_dec X Y)
adamc@95 406 end; crush.
adamc@95 407 Qed.
adamc@95 408
adamc@95 409 Lemma depth_max' : forall c n (t : rbtree c n), match c with
adamc@95 410 | Red => depth max t <= 2 * n + 1
adamc@95 411 | Black => depth max t <= 2 * n
adamc@95 412 end.
adamc@95 413 induction t; crush;
adamc@95 414 match goal with
adamc@95 415 | [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
adamc@100 416 end; crush;
adamc@100 417 repeat (match goal with
adamc@100 418 | [ H : context[match ?C with Red => _ | Black => _ end] |- _ ] => destruct C
adamc@100 419 end; crush).
adamc@95 420 Qed.
adamc@95 421
adamc@95 422 Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
adamc@95 423 intros; generalize (depth_max' t); destruct c; crush.
adamc@95 424 Qed.
adamc@95 425
adamc@95 426 Theorem balanced : forall c n (t : rbtree c n), 2 * depth min t + 1 >= depth max t.
adamc@95 427 intros; generalize (depth_min t); generalize (depth_max t); crush.
adamc@95 428 Qed.
adamc@100 429 (* end thide *)
adamc@95 430
adamc@95 431
adamc@94 432 Inductive rtree : nat -> Set :=
adamc@94 433 | RedNode' : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rtree n.
adamc@94 434
adamc@96 435 Section present.
adamc@96 436 Variable x : nat.
adamc@96 437
adamc@96 438 Fixpoint present c n (t : rbtree c n) {struct t} : Prop :=
adamc@96 439 match t with
adamc@96 440 | Leaf => False
adamc@96 441 | RedNode _ a y b => present a \/ x = y \/ present b
adamc@96 442 | BlackNode _ _ _ a y b => present a \/ x = y \/ present b
adamc@96 443 end.
adamc@96 444
adamc@96 445 Definition rpresent n (t : rtree n) : Prop :=
adamc@96 446 match t with
adamc@96 447 | RedNode' _ _ _ a y b => present a \/ x = y \/ present b
adamc@96 448 end.
adamc@96 449 End present.
adamc@96 450
adamc@100 451 Locate "{ _ : _ & _ }".
adamc@100 452 Print sigT.
adamc@100 453
adamc@94 454 Notation "{< x >}" := (existT _ _ x).
adamc@94 455
adamc@94 456 Definition balance1 n (a : rtree n) (data : nat) c2 :=
adamc@94 457 match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with
adamc@94 458 | RedNode' _ _ _ t1 y t2 =>
adamc@94 459 match t1 in rbtree c n return rbtree _ n -> rbtree c2 n -> { c : color & rbtree c (S n) } with
adamc@94 460 | RedNode _ a x b => fun c d => {<RedNode (BlackNode a x b) y (BlackNode c data d)>}
adamc@94 461 | t1' => fun t2 =>
adamc@94 462 match t2 in rbtree c n return rbtree _ n -> rbtree c2 n -> { c : color & rbtree c (S n) } with
adamc@94 463 | RedNode _ b x c => fun a d => {<RedNode (BlackNode a y b) x (BlackNode c data d)>}
adamc@95 464 | b => fun a t => {<BlackNode (RedNode a y b) data t>}
adamc@94 465 end t1'
adamc@94 466 end t2
adamc@94 467 end.
adamc@94 468
adamc@94 469 Definition balance2 n (a : rtree n) (data : nat) c2 :=
adamc@94 470 match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with
adamc@94 471 | RedNode' _ _ _ t1 z t2 =>
adamc@94 472 match t1 in rbtree c n return rbtree _ n -> rbtree c2 n -> { c : color & rbtree c (S n) } with
adamc@94 473 | RedNode _ b y c => fun d a => {<RedNode (BlackNode a data b) y (BlackNode c z d)>}
adamc@94 474 | t1' => fun t2 =>
adamc@94 475 match t2 in rbtree c n return rbtree _ n -> rbtree c2 n -> { c : color & rbtree c (S n) } with
adamc@94 476 | RedNode _ c z' d => fun b a => {<RedNode (BlackNode a data b) z (BlackNode c z' d)>}
adamc@95 477 | b => fun a t => {<BlackNode t data (RedNode a z b)>}
adamc@94 478 end t1'
adamc@94 479 end t2
adamc@94 480 end.
adamc@94 481
adamc@94 482 Section insert.
adamc@94 483 Variable x : nat.
adamc@94 484
adamc@94 485 Definition insResult c n :=
adamc@94 486 match c with
adamc@94 487 | Red => rtree n
adamc@94 488 | Black => { c' : color & rbtree c' n }
adamc@94 489 end.
adamc@94 490
adamc@94 491 Fixpoint ins c n (t : rbtree c n) {struct t} : insResult c n :=
adamc@94 492 match t in (rbtree c n) return (insResult c n) with
adamc@94 493 | Leaf => {< RedNode Leaf x Leaf >}
adamc@94 494 | RedNode _ a y b =>
adamc@94 495 if le_lt_dec x y
adamc@94 496 then RedNode' (projT2 (ins a)) y b
adamc@94 497 else RedNode' a y (projT2 (ins b))
adamc@94 498 | BlackNode c1 c2 _ a y b =>
adamc@94 499 if le_lt_dec x y
adamc@94 500 then
adamc@94 501 match c1 return insResult c1 _ -> _ with
adamc@94 502 | Red => fun ins_a => balance1 ins_a y b
adamc@94 503 | _ => fun ins_a => {< BlackNode (projT2 ins_a) y b >}
adamc@94 504 end (ins a)
adamc@94 505 else
adamc@94 506 match c2 return insResult c2 _ -> _ with
adamc@94 507 | Red => fun ins_b => balance2 ins_b y a
adamc@94 508 | _ => fun ins_b => {< BlackNode a y (projT2 ins_b) >}
adamc@94 509 end (ins b)
adamc@94 510 end.
adamc@94 511
adamc@94 512 Definition insertResult c n :=
adamc@94 513 match c with
adamc@94 514 | Red => rbtree Black (S n)
adamc@94 515 | Black => { c' : color & rbtree c' n }
adamc@94 516 end.
adamc@94 517
adamc@97 518 Definition makeRbtree c n : insResult c n -> insertResult c n :=
adamc@94 519 match c return insResult c n -> insertResult c n with
adamc@94 520 | Red => fun r =>
adamc@94 521 match r in rtree n return insertResult Red n with
adamc@94 522 | RedNode' _ _ _ a x b => BlackNode a x b
adamc@94 523 end
adamc@94 524 | Black => fun r => r
adamc@94 525 end.
adamc@94 526
adamc@97 527 Implicit Arguments makeRbtree [c n].
adamc@94 528
adamc@94 529 Definition insert c n (t : rbtree c n) : insertResult c n :=
adamc@97 530 makeRbtree (ins t).
adamc@94 531
adamc@95 532 Section present.
adamc@95 533 Variable z : nat.
adamc@95 534
adamc@98 535 Ltac present_balance :=
adamc@98 536 crush;
adamc@98 537 repeat (match goal with
adamc@98 538 | [ H : context[match ?T with
adamc@98 539 | Leaf => _
adamc@98 540 | RedNode _ _ _ _ => _
adamc@98 541 | BlackNode _ _ _ _ _ _ => _
adamc@98 542 end] |- _ ] => dep_destruct T
adamc@98 543 | [ |- context[match ?T with
adamc@98 544 | Leaf => _
adamc@98 545 | RedNode _ _ _ _ => _
adamc@98 546 | BlackNode _ _ _ _ _ _ => _
adamc@98 547 end] ] => dep_destruct T
adamc@98 548 end; crush).
adamc@98 549
adamc@95 550 Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) ,
adamc@95 551 present z (projT2 (balance1 a y b))
adamc@95 552 <-> rpresent z a \/ z = y \/ present z b.
adamc@98 553 destruct a; present_balance.
adamc@95 554 Qed.
adamc@95 555
adamc@213 556 Lemma present_balance2 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n),
adamc@95 557 present z (projT2 (balance2 a y b))
adamc@95 558 <-> rpresent z a \/ z = y \/ present z b.
adamc@98 559 destruct a; present_balance.
adamc@95 560 Qed.
adamc@95 561
adamc@95 562 Definition present_insResult c n :=
adamc@95 563 match c return (rbtree c n -> insResult c n -> Prop) with
adamc@95 564 | Red => fun t r => rpresent z r <-> z = x \/ present z t
adamc@95 565 | Black => fun t r => present z (projT2 r) <-> z = x \/ present z t
adamc@95 566 end.
adamc@95 567
adamc@95 568 Theorem present_ins : forall c n (t : rbtree c n),
adamc@95 569 present_insResult t (ins t).
adamc@95 570 induction t; crush;
adamc@95 571 repeat (match goal with
adamc@95 572 | [ H : context[if ?E then _ else _] |- _ ] => destruct E
adamc@95 573 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@95 574 | [ H : context[match ?C with Red => _ | Black => _ end] |- _ ] => destruct C
adamc@95 575 end; crush);
adamc@95 576 try match goal with
adamc@95 577 | [ H : context[balance1 ?A ?B ?C] |- _ ] =>
adamc@95 578 generalize (present_balance1 A B C)
adamc@95 579 end;
adamc@95 580 try match goal with
adamc@95 581 | [ H : context[balance2 ?A ?B ?C] |- _ ] =>
adamc@95 582 generalize (present_balance2 A B C)
adamc@95 583 end;
adamc@95 584 try match goal with
adamc@95 585 | [ |- context[balance1 ?A ?B ?C] ] =>
adamc@95 586 generalize (present_balance1 A B C)
adamc@95 587 end;
adamc@95 588 try match goal with
adamc@95 589 | [ |- context[balance2 ?A ?B ?C] ] =>
adamc@95 590 generalize (present_balance2 A B C)
adamc@95 591 end;
adamc@95 592 intuition;
adamc@95 593 match goal with
adamc@95 594 | [ z : nat, x : nat |- _ ] =>
adamc@95 595 match goal with
adamc@95 596 | [ H : z = x |- _ ] => rewrite H in *; clear H
adamc@95 597 end
adamc@95 598 end;
adamc@95 599 tauto.
adamc@95 600 Qed.
adamc@95 601
adamc@213 602 Ltac present_insert :=
adamc@213 603 unfold insert; intros n t; inversion t;
adamc@97 604 generalize (present_ins t); simpl;
adamc@97 605 dep_destruct (ins t); tauto.
adamc@97 606
adamc@95 607 Theorem present_insert_Red : forall n (t : rbtree Red n),
adamc@95 608 present z (insert t)
adamc@95 609 <-> (z = x \/ present z t).
adamc@213 610 present_insert.
adamc@95 611 Qed.
adamc@95 612
adamc@95 613 Theorem present_insert_Black : forall n (t : rbtree Black n),
adamc@95 614 present z (projT2 (insert t))
adamc@95 615 <-> (z = x \/ present z t).
adamc@213 616 present_insert.
adamc@95 617 Qed.
adamc@95 618 End present.
adamc@94 619 End insert.
adamc@94 620
adamc@94 621
adamc@86 622 (** * A Certified Regular Expression Matcher *)
adamc@86 623
adamc@93 624 (** 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 625
adamc@93 626 Before defining the syntax of expressions, it is helpful to define an inductive type capturing the meaning of the Kleene star. We use Coq's string support, which comes through a combination of the [Strings] library and some parsing notations built into Coq. Operators like [++] and functions like [length] that we know from lists are defined again for strings. Notation scopes help us control which versions we want to use in particular contexts. *)
adamc@93 627
adamc@86 628 Require Import Ascii String.
adamc@86 629 Open Scope string_scope.
adamc@86 630
adamc@91 631 Section star.
adamc@91 632 Variable P : string -> Prop.
adamc@91 633
adamc@91 634 Inductive star : string -> Prop :=
adamc@91 635 | Empty : star ""
adamc@91 636 | Iter : forall s1 s2,
adamc@91 637 P s1
adamc@91 638 -> star s2
adamc@91 639 -> star (s1 ++ s2).
adamc@91 640 End star.
adamc@91 641
adamc@93 642 (** 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.
adamc@93 643
adamc@93 644 [[
adamc@93 645 Inductive regexp : (string -> Prop) -> Set :=
adamc@93 646 | Char : forall ch : ascii,
adamc@93 647 regexp (fun s => s = String ch "")
adamc@93 648 | Concat : forall (P1 P2 : string -> Prop) (r1 : regexp P1) (r2 : regexp P2),
adamc@93 649 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2).
adamc@93 650
adamc@93 651 [[
adamc@93 652 User error: Large non-propositional inductive types must be in Type
adamc@93 653 ]]
adamc@93 654
adamc@93 655 What is a large inductive type? In Coq, it is an inductive type that has a constructor which quantifies over some type of type [Type]. We have not worked with [Type] very much to this point. Every term of CIC has a type, including [Set] and [Prop], which are assigned type [Type]. The type [string -> Prop] from the failed definition also has type [Type].
adamc@93 656
adamc@93 657 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 658
adamc@89 659 Inductive regexp : (string -> Prop) -> Type :=
adamc@86 660 | Char : forall ch : ascii,
adamc@86 661 regexp (fun s => s = String ch "")
adamc@86 662 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
adamc@87 663 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2)
adamc@87 664 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
adamc@91 665 regexp (fun s => P1 s \/ P2 s)
adamc@91 666 | Star : forall P (r : regexp P),
adamc@91 667 regexp (star P).
adamc@86 668
adamc@93 669 (** 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 omittted theorems. Since they are orthogonal to our use of dependent types, we hide them in the rendered versions of this book. *)
adamc@93 670
adamc@93 671 (* begin hide *)
adamc@86 672 Open Scope specif_scope.
adamc@86 673
adamc@86 674 Lemma length_emp : length "" <= 0.
adamc@86 675 crush.
adamc@86 676 Qed.
adamc@86 677
adamc@86 678 Lemma append_emp : forall s, s = "" ++ s.
adamc@86 679 crush.
adamc@86 680 Qed.
adamc@86 681
adamc@86 682 Ltac substring :=
adamc@86 683 crush;
adamc@86 684 repeat match goal with
adamc@86 685 | [ |- context[match ?N with O => _ | S _ => _ end] ] => destruct N; crush
adamc@86 686 end.
adamc@86 687
adamc@86 688 Lemma substring_le : forall s n m,
adamc@86 689 length (substring n m s) <= m.
adamc@86 690 induction s; substring.
adamc@86 691 Qed.
adamc@86 692
adamc@86 693 Lemma substring_all : forall s,
adamc@86 694 substring 0 (length s) s = s.
adamc@86 695 induction s; substring.
adamc@86 696 Qed.
adamc@86 697
adamc@86 698 Lemma substring_none : forall s n,
adamc@93 699 substring n 0 s = "".
adamc@86 700 induction s; substring.
adamc@86 701 Qed.
adamc@86 702
adamc@86 703 Hint Rewrite substring_all substring_none : cpdt.
adamc@86 704
adamc@86 705 Lemma substring_split : forall s m,
adamc@86 706 substring 0 m s ++ substring m (length s - m) s = s.
adamc@86 707 induction s; substring.
adamc@86 708 Qed.
adamc@86 709
adamc@86 710 Lemma length_app1 : forall s1 s2,
adamc@86 711 length s1 <= length (s1 ++ s2).
adamc@86 712 induction s1; crush.
adamc@86 713 Qed.
adamc@86 714
adamc@86 715 Hint Resolve length_emp append_emp substring_le substring_split length_app1.
adamc@86 716
adamc@86 717 Lemma substring_app_fst : forall s2 s1 n,
adamc@86 718 length s1 = n
adamc@86 719 -> substring 0 n (s1 ++ s2) = s1.
adamc@86 720 induction s1; crush.
adamc@86 721 Qed.
adamc@86 722
adamc@86 723 Lemma substring_app_snd : forall s2 s1 n,
adamc@86 724 length s1 = n
adamc@86 725 -> substring n (length (s1 ++ s2) - n) (s1 ++ s2) = s2.
adamc@86 726 Hint Rewrite <- minus_n_O : cpdt.
adamc@86 727
adamc@86 728 induction s1; crush.
adamc@86 729 Qed.
adamc@86 730
adamc@91 731 Hint Rewrite substring_app_fst substring_app_snd using (trivial; fail) : cpdt.
adamc@93 732 (* end hide *)
adamc@93 733
adamc@93 734 (** 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 735
adamc@86 736 Section split.
adamc@86 737 Variables P1 P2 : string -> Prop.
adamc@91 738 Variable P1_dec : forall s, {P1 s} + { ~P1 s}.
adamc@91 739 Variable P2_dec : forall s, {P2 s} + { ~P2 s}.
adamc@93 740 (** We require a choice of two arbitrary string predicates and functions for deciding them. *)
adamc@86 741
adamc@86 742 Variable s : string.
adamc@93 743 (** 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 744
adamc@93 745 (** [split'] is the workhorse behind [split]. It searches through the possible ways of splitting [s] into two pieces, checking the two predicates against each such pair. [split'] progresses right-to-left, from splitting all of [s] into the first piece to splitting all of [s] into the second piece. It takes an extra argument, [n], which specifies how far along we are in this search process. *)
adamc@86 746
adamc@86 747 Definition split' (n : nat) : n <= length s
adamc@86 748 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
adamc@86 749 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~P1 s1 \/ ~P2 s2}.
adamc@86 750 refine (fix F (n : nat) : n <= length s
adamc@86 751 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
adamc@86 752 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~P1 s1 \/ ~P2 s2} :=
adamc@86 753 match n return n <= length s
adamc@86 754 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
adamc@86 755 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~P1 s1 \/ ~P2 s2} with
adamc@86 756 | O => fun _ => Reduce (P1_dec "" && P2_dec s)
adamc@93 757 | S n' => fun _ => (P1_dec (substring 0 (S n') s)
adamc@93 758 && P2_dec (substring (S n') (length s - S n') s))
adamc@86 759 || F n' _
adamc@86 760 end); clear F; crush; eauto 7;
adamc@86 761 match goal with
adamc@86 762 | [ _ : length ?S <= 0 |- _ ] => destruct S
adamc@86 763 | [ _ : length ?S' <= S ?N |- _ ] =>
adamc@86 764 generalize (eq_nat_dec (length S') (S N)); destruct 1
adamc@86 765 end; crush.
adamc@86 766 Defined.
adamc@86 767
adamc@93 768 (** 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 769
adamc@93 770 [[
adamc@93 771
adamc@93 772 | S n' => fun _ => let n := S n' in
adamc@93 773 (P1_dec (substring 0 n s)
adamc@93 774 && P2_dec (substring n (length s - n) s))
adamc@93 775 || F n' _
adamc@93 776 ]]
adamc@93 777
adamc@93 778 [split] itself is trivial to implement in terms of [split']. We just ask [split'] to begin its search with [n = length s]. *)
adamc@93 779
adamc@86 780 Definition split : {exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2}
adamc@86 781 + {forall s1 s2, s = s1 ++ s2 -> ~P1 s1 \/ ~P2 s2}.
adamc@86 782 refine (Reduce (split' (n := length s) _)); crush; eauto.
adamc@86 783 Defined.
adamc@86 784 End split.
adamc@86 785
adamc@86 786 Implicit Arguments split [P1 P2].
adamc@86 787
adamc@93 788 (* begin hide *)
adamc@91 789 Lemma app_empty_end : forall s, s ++ "" = s.
adamc@91 790 induction s; crush.
adamc@91 791 Qed.
adamc@91 792
adamc@91 793 Hint Rewrite app_empty_end : cpdt.
adamc@91 794
adamc@91 795 Lemma substring_self : forall s n,
adamc@91 796 n <= 0
adamc@91 797 -> substring n (length s - n) s = s.
adamc@91 798 induction s; substring.
adamc@91 799 Qed.
adamc@91 800
adamc@91 801 Lemma substring_empty : forall s n m,
adamc@91 802 m <= 0
adamc@91 803 -> substring n m s = "".
adamc@91 804 induction s; substring.
adamc@91 805 Qed.
adamc@91 806
adamc@91 807 Hint Rewrite substring_self substring_empty using omega : cpdt.
adamc@91 808
adamc@91 809 Lemma substring_split' : forall s n m,
adamc@91 810 substring n m s ++ substring (n + m) (length s - (n + m)) s
adamc@91 811 = substring n (length s - n) s.
adamc@91 812 Hint Rewrite substring_split : cpdt.
adamc@91 813
adamc@91 814 induction s; substring.
adamc@91 815 Qed.
adamc@91 816
adamc@91 817 Lemma substring_stack : forall s n2 m1 m2,
adamc@91 818 m1 <= m2
adamc@91 819 -> substring 0 m1 (substring n2 m2 s)
adamc@91 820 = substring n2 m1 s.
adamc@91 821 induction s; substring.
adamc@91 822 Qed.
adamc@91 823
adamc@91 824 Ltac substring' :=
adamc@91 825 crush;
adamc@91 826 repeat match goal with
adamc@91 827 | [ |- context[match ?N with O => _ | S _ => _ end] ] => case_eq N; crush
adamc@91 828 end.
adamc@91 829
adamc@91 830 Lemma substring_stack' : forall s n1 n2 m1 m2,
adamc@91 831 n1 + m1 <= m2
adamc@91 832 -> substring n1 m1 (substring n2 m2 s)
adamc@91 833 = substring (n1 + n2) m1 s.
adamc@91 834 induction s; substring';
adamc@91 835 match goal with
adamc@91 836 | [ |- substring ?N1 _ _ = substring ?N2 _ _ ] =>
adamc@91 837 replace N1 with N2; crush
adamc@91 838 end.
adamc@91 839 Qed.
adamc@91 840
adamc@91 841 Lemma substring_suffix : forall s n,
adamc@91 842 n <= length s
adamc@91 843 -> length (substring n (length s - n) s) = length s - n.
adamc@91 844 induction s; substring.
adamc@91 845 Qed.
adamc@91 846
adamc@91 847 Lemma substring_suffix_emp' : forall s n m,
adamc@91 848 substring n (S m) s = ""
adamc@91 849 -> n >= length s.
adamc@91 850 induction s; crush;
adamc@91 851 match goal with
adamc@91 852 | [ |- ?N >= _ ] => destruct N; crush
adamc@91 853 end;
adamc@91 854 match goal with
adamc@91 855 [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | omega ]
adamc@91 856 end.
adamc@91 857 Qed.
adamc@91 858
adamc@91 859 Lemma substring_suffix_emp : forall s n m,
adamc@92 860 substring n m s = ""
adamc@92 861 -> m > 0
adamc@91 862 -> n >= length s.
adamc@91 863 destruct m as [| m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
adamc@91 864 Qed.
adamc@91 865
adamc@91 866 Hint Rewrite substring_stack substring_stack' substring_suffix
adamc@91 867 using omega : cpdt.
adamc@91 868
adamc@91 869 Lemma minus_minus : forall n m1 m2,
adamc@91 870 m1 + m2 <= n
adamc@91 871 -> n - m1 - m2 = n - (m1 + m2).
adamc@91 872 intros; omega.
adamc@91 873 Qed.
adamc@91 874
adamc@91 875 Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n.
adamc@91 876 intros; omega.
adamc@91 877 Qed.
adamc@91 878
adamc@91 879 Hint Rewrite minus_minus using omega : cpdt.
adamc@93 880 (* end hide *)
adamc@93 881
adamc@93 882 (** 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 883
adamc@91 884 Section dec_star.
adamc@91 885 Variable P : string -> Prop.
adamc@91 886 Variable P_dec : forall s, {P s} + { ~P s}.
adamc@91 887
adamc@93 888 (** Some new lemmas and hints about the [star] type family are useful here. We omit them here; they are included in the book source at this point. *)
adamc@93 889
adamc@93 890 (* begin hide *)
adamc@91 891 Hint Constructors star.
adamc@91 892
adamc@91 893 Lemma star_empty : forall s,
adamc@91 894 length s = 0
adamc@91 895 -> star P s.
adamc@91 896 destruct s; crush.
adamc@91 897 Qed.
adamc@91 898
adamc@91 899 Lemma star_singleton : forall s, P s -> star P s.
adamc@91 900 intros; rewrite <- (app_empty_end s); auto.
adamc@91 901 Qed.
adamc@91 902
adamc@91 903 Lemma star_app : forall s n m,
adamc@91 904 P (substring n m s)
adamc@91 905 -> star P (substring (n + m) (length s - (n + m)) s)
adamc@91 906 -> star P (substring n (length s - n) s).
adamc@91 907 induction n; substring;
adamc@91 908 match goal with
adamc@91 909 | [ H : P (substring ?N ?M ?S) |- _ ] =>
adamc@91 910 solve [ rewrite <- (substring_split S M); auto
adamc@91 911 | rewrite <- (substring_split' S N M); auto ]
adamc@91 912 end.
adamc@91 913 Qed.
adamc@91 914
adamc@91 915 Hint Resolve star_empty star_singleton star_app.
adamc@91 916
adamc@91 917 Variable s : string.
adamc@91 918
adamc@91 919 Lemma star_inv : forall s,
adamc@91 920 star P s
adamc@91 921 -> s = ""
adamc@91 922 \/ exists i, i < length s
adamc@91 923 /\ P (substring 0 (S i) s)
adamc@91 924 /\ star P (substring (S i) (length s - S i) s).
adamc@91 925 Hint Extern 1 (exists i : nat, _) =>
adamc@91 926 match goal with
adamc@91 927 | [ H : P (String _ ?S) |- _ ] => exists (length S); crush
adamc@91 928 end.
adamc@91 929
adamc@91 930 induction 1; [
adamc@91 931 crush
adamc@91 932 | match goal with
adamc@91 933 | [ _ : P ?S |- _ ] => destruct S; crush
adamc@91 934 end
adamc@91 935 ].
adamc@91 936 Qed.
adamc@91 937
adamc@91 938 Lemma star_substring_inv : forall n,
adamc@91 939 n <= length s
adamc@91 940 -> star P (substring n (length s - n) s)
adamc@91 941 -> substring n (length s - n) s = ""
adamc@91 942 \/ exists l, l < length s - n
adamc@91 943 /\ P (substring n (S l) s)
adamc@91 944 /\ star P (substring (n + S l) (length s - (n + S l)) s).
adamc@91 945 Hint Rewrite plus_n_Sm' : cpdt.
adamc@91 946
adamc@91 947 intros;
adamc@91 948 match goal with
adamc@91 949 | [ H : star _ _ |- _ ] => generalize (star_inv H); do 3 crush; eauto
adamc@91 950 end.
adamc@91 951 Qed.
adamc@93 952 (* end hide *)
adamc@93 953
adamc@93 954 (** 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 955
adamc@91 956 Section dec_star''.
adamc@91 957 Variable n : nat.
adamc@93 958 (** [n] is the length of the prefix of [s] that we have already processed. *)
adamc@91 959
adamc@91 960 Variable P' : string -> Prop.
adamc@91 961 Variable P'_dec : forall n' : nat, n' > n
adamc@91 962 -> {P' (substring n' (length s - n') s)}
adamc@91 963 + { ~P' (substring n' (length s - n') s)}.
adamc@93 964 (** 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 965
adamc@93 966 (** 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 967
adamc@91 968 Definition dec_star'' (l : nat)
adamc@91 969 : {exists l', S l' <= l
adamc@91 970 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
adamc@91 971 + {forall l', S l' <= l
adamc@93 972 -> ~P (substring n (S l') s)
adamc@93 973 \/ ~P' (substring (n + S l') (length s - (n + S l')) s)}.
adamc@91 974 refine (fix F (l : nat) : {exists l', S l' <= l
adamc@91 975 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
adamc@91 976 + {forall l', S l' <= l
adamc@93 977 -> ~P (substring n (S l') s)
adamc@93 978 \/ ~P' (substring (n + S l') (length s - (n + S l')) s)} :=
adamc@91 979 match l return {exists l', S l' <= l
adamc@91 980 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
adamc@91 981 + {forall l', S l' <= l ->
adamc@93 982 ~P (substring n (S l') s)
adamc@93 983 \/ ~P' (substring (n + S l') (length s - (n + S l')) s)} with
adamc@91 984 | O => _
adamc@91 985 | S l' =>
adamc@91 986 (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
adamc@91 987 || F l'
adamc@91 988 end); clear F; crush; eauto 7;
adamc@91 989 match goal with
adamc@91 990 | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush
adamc@91 991 end.
adamc@91 992 Defined.
adamc@91 993 End dec_star''.
adamc@91 994
adamc@93 995 (* begin hide *)
adamc@92 996 Lemma star_length_contra : forall n,
adamc@92 997 length s > n
adamc@92 998 -> n >= length s
adamc@92 999 -> False.
adamc@92 1000 crush.
adamc@92 1001 Qed.
adamc@92 1002
adamc@92 1003 Lemma star_length_flip : forall n n',
adamc@92 1004 length s - n <= S n'
adamc@92 1005 -> length s > n
adamc@92 1006 -> length s - n > 0.
adamc@92 1007 crush.
adamc@92 1008 Qed.
adamc@92 1009
adamc@92 1010 Hint Resolve star_length_contra star_length_flip substring_suffix_emp.
adamc@93 1011 (* end hide *)
adamc@92 1012
adamc@93 1013 (** 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 1014
adamc@91 1015 Definition dec_star' (n n' : nat) : length s - n' <= n
adamc@91 1016 -> {star P (substring n' (length s - n') s)}
adamc@93 1017 + { ~star P (substring n' (length s - n') s)}.
adamc@91 1018 refine (fix F (n n' : nat) {struct n} : length s - n' <= n
adamc@91 1019 -> {star P (substring n' (length s - n') s)}
adamc@93 1020 + { ~star P (substring n' (length s - n') s)} :=
adamc@91 1021 match n return length s - n' <= n
adamc@91 1022 -> {star P (substring n' (length s - n') s)}
adamc@93 1023 + { ~star P (substring n' (length s - n') s)} with
adamc@91 1024 | O => fun _ => Yes
adamc@91 1025 | S n'' => fun _ =>
adamc@91 1026 le_gt_dec (length s) n'
adamc@91 1027 || dec_star'' (n := n') (star P) (fun n0 _ => Reduce (F n'' n0 _)) (length s - n')
adamc@92 1028 end); clear F; crush; eauto;
adamc@92 1029 match goal with
adamc@92 1030 | [ H : star _ _ |- _ ] => apply star_substring_inv in H; crush; eauto
adamc@92 1031 end;
adamc@92 1032 match goal with
adamc@92 1033 | [ H1 : _ < _ - _, H2 : forall l' : nat, _ <= _ - _ -> _ |- _ ] =>
adamc@92 1034 generalize (H2 _ (lt_le_S _ _ H1)); tauto
adamc@92 1035 end.
adamc@91 1036 Defined.
adamc@91 1037
adamc@93 1038 (** Finally, we have [dec_star]. It has a straightforward implementation. We introduce a spurious match on [s] so that [simpl] will know to reduce calls to [dec_star]. The heuristic that [simpl] uses is only to unfold identifier definitions when doing so would simplify some [match] expression. *)
adamc@93 1039
adamc@91 1040 Definition dec_star : {star P s} + { ~star P s}.
adamc@204 1041 refine (match s return _ with
adamc@91 1042 | "" => Reduce (dec_star' (n := length s) 0 _)
adamc@91 1043 | _ => Reduce (dec_star' (n := length s) 0 _)
adamc@91 1044 end); crush.
adamc@91 1045 Defined.
adamc@91 1046 End dec_star.
adamc@91 1047
adamc@93 1048 (* begin hide *)
adamc@86 1049 Lemma app_cong : forall x1 y1 x2 y2,
adamc@86 1050 x1 = x2
adamc@86 1051 -> y1 = y2
adamc@86 1052 -> x1 ++ y1 = x2 ++ y2.
adamc@86 1053 congruence.
adamc@86 1054 Qed.
adamc@86 1055
adamc@86 1056 Hint Resolve app_cong.
adamc@93 1057 (* end hide *)
adamc@93 1058
adamc@93 1059 (** 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 1060
adamc@86 1061 Definition matches P (r : regexp P) s : {P s} + { ~P s}.
adamc@86 1062 refine (fix F P (r : regexp P) s : {P s} + { ~P s} :=
adamc@86 1063 match r with
adamc@86 1064 | Char ch => string_dec s (String ch "")
adamc@86 1065 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s)
adamc@87 1066 | Or _ _ r1 r2 => F _ r1 s || F _ r2 s
adamc@91 1067 | Star _ r => dec_star _ _ _
adamc@86 1068 end); crush;
adamc@86 1069 match goal with
adamc@86 1070 | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _))
adamc@93 1071 end; tauto.
adamc@86 1072 Defined.
adamc@86 1073
adamc@93 1074 (* begin hide *)
adamc@86 1075 Example hi := Concat (Char "h"%char) (Char "i"%char).
adamc@86 1076 Eval simpl in matches hi "hi".
adamc@86 1077 Eval simpl in matches hi "bye".
adamc@87 1078
adamc@87 1079 Example a_b := Or (Char "a"%char) (Char "b"%char).
adamc@87 1080 Eval simpl in matches a_b "".
adamc@87 1081 Eval simpl in matches a_b "a".
adamc@87 1082 Eval simpl in matches a_b "aa".
adamc@87 1083 Eval simpl in matches a_b "b".
adamc@91 1084
adamc@91 1085 Example a_star := Star (Char "a"%char).
adamc@91 1086 Eval simpl in matches a_star "".
adamc@91 1087 Eval simpl in matches a_star "a".
adamc@91 1088 Eval simpl in matches a_star "b".
adamc@91 1089 Eval simpl in matches a_star "aa".
adamc@93 1090 (* end hide *)
adamc@101 1091
adamc@101 1092
adamc@101 1093 (** * Exercises *)
adamc@101 1094
adamc@101 1095 (** %\begin{enumerate}%#<ol>#
adamc@101 1096
adamc@101 1097 %\item%#<li># Define a kind of dependently-typed lists, where a list's type index gives a lower bound on how many of its elements satisfy a particular predicate. In particular, for an arbitrary set [A] and a predicate [P] over it:
adamc@101 1098 %\begin{enumerate}%#<ol>#
adamc@101 1099 %\item%#<li># Define a type [plist : nat -> Set]. Each [plist n] should be a list of [A]s, where it is guaranteed that at least [n] distinct elements satisfy [P]. There is wide latitude in choosing how to encode this. You should try to avoid using subset types or any other mechanism based on annotating non-dependent types with propositions after-the-fact.#</li>#
adamc@102 1100 %\item%#<li># Define a version of list concatenation that works on [plist]s. The type of this new function should express as much information as possible about the output [plist].#</li>#
adamc@101 1101 %\item%#<li># Define a function [plistOut] for translating [plist]s to normal [list]s.#</li>#
adamc@101 1102 %\item%#<li># Define a function [plistIn] for translating [list]s to [plist]s. The type of [plistIn] should make it clear that the best bound on [P]-matching elements is chosen. You may assume that you are given a dependently-typed function for deciding instances of [P].#</li>#
adamc@101 1103 %\item%#<li># Prove that, for any list [ls], [plistOut (plistIn ls) = ls]. This should be the only part of the exercise where you use tactic-based proving.#</li>#
adamc@101 1104 %\item%#<li># Define a function [grab : forall n (ls : plist (S n)), sig P]. That is, when given a [plist] guaranteed to contain at least one element satisfying [P], [grab] produces such an element. [sig] is the type family of sigma types, and [sig P] is extensionally equivalent to [{x : A | P x}], though the latter form uses an eta-expansion of [P] instead of [P] itself as the predicate.#</li>#
adamc@101 1105 #</ol>#%\end{enumerate}% #</li>#
adamc@101 1106
adamc@102 1107 #</ol>#%\end{enumerate}% *)