|
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
|
|
adam@275
|
124 Unlike in ML, we cannot use inexhaustive pattern matching, because there is no conception of a %\texttt{%#<tt>#Match#</tt>#%}% exception to be thrown. In fact, recent versions of Coq %\textit{%#<i>#do#</i>#%}% allow this, by implicit translation to a [match] that considers all constructors. It is educational to discover that encoding ourselves directly. We might try using an [in] clause somehow.
|
|
adamc@84
|
125
|
|
adamc@84
|
126 [[
|
|
adamc@84
|
127 Definition hd n (ls : ilist (S n)) : A :=
|
|
adamc@84
|
128 match ls in (ilist (S n)) with
|
|
adamc@84
|
129 | Cons _ h _ => h
|
|
adamc@84
|
130 end.
|
|
adamc@84
|
131
|
|
adamc@84
|
132 Error: The reference n was not found in the current environment
|
|
adamc@213
|
133
|
|
adamc@84
|
134 ]]
|
|
adamc@84
|
135
|
|
adamc@84
|
136 In this and other cases, we feel like we want [in] clauses with type family arguments that are not variables. Unfortunately, Coq only supports variables in those positions. A completely general mechanism could only be supported with a solution to the problem of higher-order unification, which is undecidable. There %\textit{%#<i>#are#</i>#%}% useful heuristics for handling non-variable indices which are gradually making their way into Coq, but we will spend some time in this and the next few chapters on effective pattern matching on dependent types using only the primitive [match] annotations.
|
|
adamc@84
|
137
|
|
adamc@84
|
138 Our final, working attempt at [hd] uses an auxiliary function and a surprising [return] annotation. *)
|
|
adamc@84
|
139
|
|
adamc@100
|
140 (* begin thide *)
|
|
adamc@84
|
141 Definition hd' n (ls : ilist n) :=
|
|
adamc@84
|
142 match ls in (ilist n) return (match n with O => unit | S _ => A end) with
|
|
adamc@84
|
143 | Nil => tt
|
|
adamc@84
|
144 | Cons _ h _ => h
|
|
adamc@84
|
145 end.
|
|
adamc@84
|
146
|
|
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@214
|
377 (** 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
|
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@214
|
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@214
|
386 (** 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
|
387
|
|
adamc@214
|
388 (** 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
|
389
|
|
adamc@100
|
390 (* EX: Prove that every [rbtree] is balanced. *)
|
|
adamc@100
|
391
|
|
adamc@100
|
392 (* begin thide *)
|
|
adamc@95
|
393 Require Import Max Min.
|
|
adamc@95
|
394
|
|
adamc@95
|
395 Section depth.
|
|
adamc@95
|
396 Variable f : nat -> nat -> nat.
|
|
adamc@95
|
397
|
|
adamc@214
|
398 Fixpoint depth c n (t : rbtree c n) : nat :=
|
|
adamc@95
|
399 match t with
|
|
adamc@95
|
400 | Leaf => 0
|
|
adamc@95
|
401 | RedNode _ t1 _ t2 => S (f (depth t1) (depth t2))
|
|
adamc@95
|
402 | BlackNode _ _ _ t1 _ t2 => S (f (depth t1) (depth t2))
|
|
adamc@95
|
403 end.
|
|
adamc@95
|
404 End depth.
|
|
adamc@95
|
405
|
|
adamc@214
|
406 (** 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
|
407
|
|
adamc@95
|
408 Theorem depth_min : forall c n (t : rbtree c n), depth min t >= n.
|
|
adamc@95
|
409 induction t; crush;
|
|
adamc@95
|
410 match goal with
|
|
adamc@95
|
411 | [ |- context[min ?X ?Y] ] => destruct (min_dec X Y)
|
|
adamc@95
|
412 end; crush.
|
|
adamc@95
|
413 Qed.
|
|
adamc@95
|
414
|
|
adamc@214
|
415 (** There is an analogous upper-bound theorem based on black depth. Unfortunately, a symmetric proof script does not suffice to establish it. *)
|
|
adamc@214
|
416
|
|
adamc@214
|
417 Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
|
|
adamc@214
|
418 induction t; crush;
|
|
adamc@214
|
419 match goal with
|
|
adamc@214
|
420 | [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
|
|
adamc@214
|
421 end; crush.
|
|
adamc@214
|
422
|
|
adamc@214
|
423 (** Two subgoals remain. One of them is: [[
|
|
adamc@214
|
424 n : nat
|
|
adamc@214
|
425 t1 : rbtree Black n
|
|
adamc@214
|
426 n0 : nat
|
|
adamc@214
|
427 t2 : rbtree Black n
|
|
adamc@214
|
428 IHt1 : depth max t1 <= n + (n + 0) + 1
|
|
adamc@214
|
429 IHt2 : depth max t2 <= n + (n + 0) + 1
|
|
adamc@214
|
430 e : max (depth max t1) (depth max t2) = depth max t1
|
|
adamc@214
|
431 ============================
|
|
adamc@214
|
432 S (depth max t1) <= n + (n + 0) + 1
|
|
adamc@214
|
433
|
|
adamc@214
|
434 ]]
|
|
adamc@214
|
435
|
|
adamc@214
|
436 We see that [IHt1] is %\textit{%#<i>#almost#</i>#%}% the fact we need, but it is not quite strong enough. We will need to strengthen our induction hypothesis to get the proof to go through. *)
|
|
adamc@214
|
437
|
|
adamc@214
|
438 Abort.
|
|
adamc@214
|
439
|
|
adamc@214
|
440 (** 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
|
441
|
|
adamc@95
|
442 Lemma depth_max' : forall c n (t : rbtree c n), match c with
|
|
adamc@95
|
443 | Red => depth max t <= 2 * n + 1
|
|
adamc@95
|
444 | Black => depth max t <= 2 * n
|
|
adamc@95
|
445 end.
|
|
adamc@95
|
446 induction t; crush;
|
|
adamc@95
|
447 match goal with
|
|
adamc@95
|
448 | [ |- context[max ?X ?Y] ] => destruct (max_dec X Y)
|
|
adamc@100
|
449 end; crush;
|
|
adamc@100
|
450 repeat (match goal with
|
|
adamc@214
|
451 | [ H : context[match ?C with Red => _ | Black => _ end] |- _ ] =>
|
|
adamc@214
|
452 destruct C
|
|
adamc@100
|
453 end; crush).
|
|
adamc@95
|
454 Qed.
|
|
adamc@95
|
455
|
|
adamc@214
|
456 (** The original theorem follows easily from the lemma. We use the tactic [generalize pf], which, when [pf] proves the proposition [P], changes the goal from [Q] to [P -> Q]. It is useful to do this because it makes the truth of [P] manifest syntactically, so that automation machinery can rely on [P], even if that machinery is not smart enough to establish [P] on its own. *)
|
|
adamc@214
|
457
|
|
adamc@95
|
458 Theorem depth_max : forall c n (t : rbtree c n), depth max t <= 2 * n + 1.
|
|
adamc@95
|
459 intros; generalize (depth_max' t); destruct c; crush.
|
|
adamc@95
|
460 Qed.
|
|
adamc@95
|
461
|
|
adamc@214
|
462 (** 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
|
463
|
|
adamc@95
|
464 Theorem balanced : forall c n (t : rbtree c n), 2 * depth min t + 1 >= depth max t.
|
|
adamc@95
|
465 intros; generalize (depth_min t); generalize (depth_max t); crush.
|
|
adamc@95
|
466 Qed.
|
|
adamc@100
|
467 (* end thide *)
|
|
adamc@95
|
468
|
|
adamc@214
|
469 (** 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
|
470
|
|
adamc@94
|
471 Inductive rtree : nat -> Set :=
|
|
adamc@94
|
472 | RedNode' : forall c1 c2 n, rbtree c1 n -> nat -> rbtree c2 n -> rtree n.
|
|
adamc@94
|
473
|
|
adamc@214
|
474 (** 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
|
475
|
|
adamc@96
|
476 Section present.
|
|
adamc@96
|
477 Variable x : nat.
|
|
adamc@96
|
478
|
|
adamc@214
|
479 Fixpoint present c n (t : rbtree c n) : Prop :=
|
|
adamc@96
|
480 match t with
|
|
adamc@96
|
481 | Leaf => False
|
|
adamc@96
|
482 | RedNode _ a y b => present a \/ x = y \/ present b
|
|
adamc@96
|
483 | BlackNode _ _ _ a y b => present a \/ x = y \/ present b
|
|
adamc@96
|
484 end.
|
|
adamc@96
|
485
|
|
adamc@96
|
486 Definition rpresent n (t : rtree n) : Prop :=
|
|
adamc@96
|
487 match t with
|
|
adamc@96
|
488 | RedNode' _ _ _ a y b => present a \/ x = y \/ present b
|
|
adamc@96
|
489 end.
|
|
adamc@96
|
490 End present.
|
|
adamc@96
|
491
|
|
adamc@214
|
492 (** Insertion relies on two balancing operations. It will be useful to give types to these operations using a relative of the subset types from last chapter. While subset types let us pair a value with a proof about that value, here we want to pair a value with another non-proof dependently-typed value. The [sigT] type fills this role. *)
|
|
adamc@214
|
493
|
|
adamc@100
|
494 Locate "{ _ : _ & _ }".
|
|
adamc@214
|
495 (** [[
|
|
adamc@214
|
496 Notation Scope
|
|
adamc@214
|
497 "{ x : A & P }" := sigT (fun x : A => P)
|
|
adamc@214
|
498 ]] *)
|
|
adamc@214
|
499
|
|
adamc@100
|
500 Print sigT.
|
|
adamc@214
|
501 (** [[
|
|
adamc@214
|
502 Inductive sigT (A : Type) (P : A -> Type) : Type :=
|
|
adamc@214
|
503 existT : forall x : A, P x -> sigT P
|
|
adamc@214
|
504 ]] *)
|
|
adamc@214
|
505
|
|
adamc@214
|
506 (** It will be helpful to define a concise notation for the constructor of [sigT]. *)
|
|
adamc@100
|
507
|
|
adamc@94
|
508 Notation "{< x >}" := (existT _ _ x).
|
|
adamc@94
|
509
|
|
adamc@214
|
510 (** 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
|
511
|
|
adamc@214
|
512 A balance operation may return a tree whose root is of either color. Thus, we use a [sigT] type to package the result tree with the color of its root. Here is the definition of the first balance operation, which applies when the possibly-invalid [rtree] belongs to the left of the valid [rbtree]. *)
|
|
adamc@214
|
513
|
|
adamc@94
|
514 Definition balance1 n (a : rtree n) (data : nat) c2 :=
|
|
adamc@214
|
515 match a in rtree n return rbtree c2 n
|
|
adamc@214
|
516 -> { c : color & rbtree c (S n) } with
|
|
adamc@94
|
517 | RedNode' _ _ _ t1 y t2 =>
|
|
adamc@214
|
518 match t1 in rbtree c n return rbtree _ n -> rbtree c2 n
|
|
adamc@214
|
519 -> { c : color & rbtree c (S n) } with
|
|
adamc@214
|
520 | RedNode _ a x b => fun c d =>
|
|
adamc@214
|
521 {<RedNode (BlackNode a x b) y (BlackNode c data d)>}
|
|
adamc@94
|
522 | t1' => fun t2 =>
|
|
adamc@214
|
523 match t2 in rbtree c n return rbtree _ n -> rbtree c2 n
|
|
adamc@214
|
524 -> { c : color & rbtree c (S n) } with
|
|
adamc@214
|
525 | RedNode _ b x c => fun a d =>
|
|
adamc@214
|
526 {<RedNode (BlackNode a y b) x (BlackNode c data d)>}
|
|
adamc@95
|
527 | b => fun a t => {<BlackNode (RedNode a y b) data t>}
|
|
adamc@94
|
528 end t1'
|
|
adamc@94
|
529 end t2
|
|
adamc@94
|
530 end.
|
|
adamc@94
|
531
|
|
adamc@214
|
532 (** We apply a trick that I call the %\textit{%#<i>#convoy pattern#</i>#%}%. Recall that [match] annotations only make it possible to describe a dependence of a [match] %\textit{%#<i>#result type#</i>#%}% on the discriminee. There is no automatic refinement of the types of free variables. However, it is possible to effect such a refinement by finding a way to encode free variable type dependencies in the [match] result type, so that a [return] clause can express the connection.
|
|
adamc@214
|
533
|
|
adamc@214
|
534 In particular, we can extend the [match] to return %\textit{%#<i>#functions over the free variables whose types we want to refine#</i>#%}%. In the case of [balance1], we only find ourselves wanting to refine the type of one tree variable at a time. We match on one subtree of a node, and we want the type of the other subtree to be refined based on what we learn. We indicate this with a [return] clause starting like [rbtree _ n -> ...], where [n] is bound in an [in] pattern. Such a [match] expression is applied immediately to the "old version" of the variable to be refined, and the type checker is happy.
|
|
adamc@214
|
535
|
|
adamc@214
|
536 After writing this code, even I do not understand the precise details of how balancing works. I consulted Chris Okasaki's paper "Red-Black Trees in a Functional Setting" and transcribed the code to use dependent types. Luckily, the details are not so important here; types alone will tell us that insertion preserves balanced-ness, and we will prove that insertion produces trees containing the right keys.
|
|
adamc@214
|
537
|
|
adamc@214
|
538 Here is the symmetric function [balance2], for cases where the possibly-invalid tree appears on the right rather than on the left. *)
|
|
adamc@214
|
539
|
|
adamc@94
|
540 Definition balance2 n (a : rtree n) (data : nat) c2 :=
|
|
adamc@94
|
541 match a in rtree n return rbtree c2 n -> { c : color & rbtree c (S n) } with
|
|
adamc@94
|
542 | RedNode' _ _ _ t1 z t2 =>
|
|
adamc@214
|
543 match t1 in rbtree c n return rbtree _ n -> rbtree c2 n
|
|
adamc@214
|
544 -> { c : color & rbtree c (S n) } with
|
|
adamc@214
|
545 | RedNode _ b y c => fun d a =>
|
|
adamc@214
|
546 {<RedNode (BlackNode a data b) y (BlackNode c z d)>}
|
|
adamc@94
|
547 | t1' => fun t2 =>
|
|
adamc@214
|
548 match t2 in rbtree c n return rbtree _ n -> rbtree c2 n
|
|
adamc@214
|
549 -> { c : color & rbtree c (S n) } with
|
|
adamc@214
|
550 | RedNode _ c z' d => fun b a =>
|
|
adamc@214
|
551 {<RedNode (BlackNode a data b) z (BlackNode c z' d)>}
|
|
adamc@95
|
552 | b => fun a t => {<BlackNode t data (RedNode a z b)>}
|
|
adamc@94
|
553 end t1'
|
|
adamc@94
|
554 end t2
|
|
adamc@94
|
555 end.
|
|
adamc@94
|
556
|
|
adamc@214
|
557 (** 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
|
558
|
|
adamc@94
|
559 Section insert.
|
|
adamc@94
|
560 Variable x : nat.
|
|
adamc@94
|
561
|
|
adamc@214
|
562 (** 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
|
563
|
|
adamc@94
|
564 Definition insResult c n :=
|
|
adamc@94
|
565 match c with
|
|
adamc@94
|
566 | Red => rtree n
|
|
adamc@94
|
567 | Black => { c' : color & rbtree c' n }
|
|
adamc@94
|
568 end.
|
|
adamc@94
|
569
|
|
adamc@214
|
570 (** 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 arbitary color.
|
|
adamc@214
|
571
|
|
adamc@214
|
572 Here is the definition of [ins]. Again, we do not want to dwell on the functional details. *)
|
|
adamc@214
|
573
|
|
adamc@214
|
574 Fixpoint ins c n (t : rbtree c n) : insResult c n :=
|
|
adamc@214
|
575 match t with
|
|
adamc@94
|
576 | Leaf => {< RedNode Leaf x Leaf >}
|
|
adamc@94
|
577 | RedNode _ a y b =>
|
|
adamc@94
|
578 if le_lt_dec x y
|
|
adamc@94
|
579 then RedNode' (projT2 (ins a)) y b
|
|
adamc@94
|
580 else RedNode' a y (projT2 (ins b))
|
|
adamc@94
|
581 | BlackNode c1 c2 _ a y b =>
|
|
adamc@94
|
582 if le_lt_dec x y
|
|
adamc@94
|
583 then
|
|
adamc@94
|
584 match c1 return insResult c1 _ -> _ with
|
|
adamc@94
|
585 | Red => fun ins_a => balance1 ins_a y b
|
|
adamc@94
|
586 | _ => fun ins_a => {< BlackNode (projT2 ins_a) y b >}
|
|
adamc@94
|
587 end (ins a)
|
|
adamc@94
|
588 else
|
|
adamc@94
|
589 match c2 return insResult c2 _ -> _ with
|
|
adamc@94
|
590 | Red => fun ins_b => balance2 ins_b y a
|
|
adamc@94
|
591 | _ => fun ins_b => {< BlackNode a y (projT2 ins_b) >}
|
|
adamc@94
|
592 end (ins b)
|
|
adamc@94
|
593 end.
|
|
adamc@94
|
594
|
|
adamc@214
|
595 (** 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 satisifies the type checker per se, but it does not satisfy the termination checker. Inside each [match], we would be calling [ins] recursively on a locally-bound variable. The termination checker is not smart enough to trace the dataflow into that variable, so the checker does not know that this recursive argument is smaller than the original argument. We make this fact clearer by applying the convoy pattern on %\textit{%#<i>#the result of a recursive call#</i>#%}%, rather than just on that call's argument.
|
|
adamc@214
|
596
|
|
adamc@214
|
597 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
|
598
|
|
adamc@94
|
599 Definition insertResult c n :=
|
|
adamc@94
|
600 match c with
|
|
adamc@94
|
601 | Red => rbtree Black (S n)
|
|
adamc@94
|
602 | Black => { c' : color & rbtree c' n }
|
|
adamc@94
|
603 end.
|
|
adamc@94
|
604
|
|
adamc@214
|
605 (** A simple clean-up procedure translates [insResult]s into [insertResult]s. *)
|
|
adamc@214
|
606
|
|
adamc@97
|
607 Definition makeRbtree c n : insResult c n -> insertResult c n :=
|
|
adamc@214
|
608 match c with
|
|
adamc@94
|
609 | Red => fun r =>
|
|
adamc@214
|
610 match r with
|
|
adamc@94
|
611 | RedNode' _ _ _ a x b => BlackNode a x b
|
|
adamc@94
|
612 end
|
|
adamc@94
|
613 | Black => fun r => r
|
|
adamc@94
|
614 end.
|
|
adamc@94
|
615
|
|
adamc@214
|
616 (** 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
|
617
|
|
adamc@97
|
618 Implicit Arguments makeRbtree [c n].
|
|
adamc@94
|
619
|
|
adamc@214
|
620 (** Finally, we define [insert] as a simple composition of [ins] and [makeRbtree]. *)
|
|
adamc@214
|
621
|
|
adamc@94
|
622 Definition insert c n (t : rbtree c n) : insertResult c n :=
|
|
adamc@97
|
623 makeRbtree (ins t).
|
|
adamc@94
|
624
|
|
adamc@214
|
625 (** 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
|
626
|
|
adamc@95
|
627 Section present.
|
|
adamc@95
|
628 Variable z : nat.
|
|
adamc@95
|
629
|
|
adamc@214
|
630 (** 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
|
631
|
|
adamc@214
|
632 We start by proving the correctness of the balance operations. It is useful to define a custom tactic [present_balance] that encapsulates the reasoning common to the two proofs. We use the keyword [Ltac] to assign a name to a proof script. This particular script just iterates between [crush] and identification of a tree that is being pattern-matched on and should be destructed. *)
|
|
adamc@214
|
633
|
|
adamc@98
|
634 Ltac present_balance :=
|
|
adamc@98
|
635 crush;
|
|
adamc@98
|
636 repeat (match goal with
|
|
adamc@98
|
637 | [ H : context[match ?T with
|
|
adamc@98
|
638 | Leaf => _
|
|
adamc@98
|
639 | RedNode _ _ _ _ => _
|
|
adamc@98
|
640 | BlackNode _ _ _ _ _ _ => _
|
|
adamc@98
|
641 end] |- _ ] => dep_destruct T
|
|
adamc@98
|
642 | [ |- context[match ?T with
|
|
adamc@98
|
643 | Leaf => _
|
|
adamc@98
|
644 | RedNode _ _ _ _ => _
|
|
adamc@98
|
645 | BlackNode _ _ _ _ _ _ => _
|
|
adamc@98
|
646 end] ] => dep_destruct T
|
|
adamc@98
|
647 end; crush).
|
|
adamc@98
|
648
|
|
adamc@214
|
649 (** 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
|
650
|
|
adamc@95
|
651 Lemma present_balance1 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n) ,
|
|
adamc@95
|
652 present z (projT2 (balance1 a y b))
|
|
adamc@95
|
653 <-> rpresent z a \/ z = y \/ present z b.
|
|
adamc@98
|
654 destruct a; present_balance.
|
|
adamc@95
|
655 Qed.
|
|
adamc@95
|
656
|
|
adamc@213
|
657 Lemma present_balance2 : forall n (a : rtree n) (y : nat) c2 (b : rbtree c2 n),
|
|
adamc@95
|
658 present z (projT2 (balance2 a y b))
|
|
adamc@95
|
659 <-> rpresent z a \/ z = y \/ present z b.
|
|
adamc@98
|
660 destruct a; present_balance.
|
|
adamc@95
|
661 Qed.
|
|
adamc@95
|
662
|
|
adamc@214
|
663 (** 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
|
664
|
|
adamc@95
|
665 Definition present_insResult c n :=
|
|
adamc@95
|
666 match c return (rbtree c n -> insResult c n -> Prop) with
|
|
adamc@95
|
667 | Red => fun t r => rpresent z r <-> z = x \/ present z t
|
|
adamc@95
|
668 | Black => fun t r => present z (projT2 r) <-> z = x \/ present z t
|
|
adamc@95
|
669 end.
|
|
adamc@95
|
670
|
|
adamc@214
|
671 (** 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
|
672
|
|
adamc@214
|
673 (** printing * $*$ *)
|
|
adamc@214
|
674
|
|
adamc@95
|
675 Theorem present_ins : forall c n (t : rbtree c n),
|
|
adamc@95
|
676 present_insResult t (ins t).
|
|
adamc@95
|
677 induction t; crush;
|
|
adamc@95
|
678 repeat (match goal with
|
|
adamc@95
|
679 | [ H : context[if ?E then _ else _] |- _ ] => destruct E
|
|
adamc@95
|
680 | [ |- context[if ?E then _ else _] ] => destruct E
|
|
adamc@214
|
681 | [ H : context[match ?C with Red => _ | Black => _ end]
|
|
adamc@214
|
682 |- _ ] => destruct C
|
|
adamc@95
|
683 end; crush);
|
|
adamc@95
|
684 try match goal with
|
|
adamc@95
|
685 | [ H : context[balance1 ?A ?B ?C] |- _ ] =>
|
|
adamc@95
|
686 generalize (present_balance1 A B C)
|
|
adamc@95
|
687 end;
|
|
adamc@95
|
688 try match goal with
|
|
adamc@95
|
689 | [ H : context[balance2 ?A ?B ?C] |- _ ] =>
|
|
adamc@95
|
690 generalize (present_balance2 A B C)
|
|
adamc@95
|
691 end;
|
|
adamc@95
|
692 try match goal with
|
|
adamc@95
|
693 | [ |- context[balance1 ?A ?B ?C] ] =>
|
|
adamc@95
|
694 generalize (present_balance1 A B C)
|
|
adamc@95
|
695 end;
|
|
adamc@95
|
696 try match goal with
|
|
adamc@95
|
697 | [ |- context[balance2 ?A ?B ?C] ] =>
|
|
adamc@95
|
698 generalize (present_balance2 A B C)
|
|
adamc@95
|
699 end;
|
|
adamc@214
|
700 crush;
|
|
adamc@95
|
701 match goal with
|
|
adamc@95
|
702 | [ z : nat, x : nat |- _ ] =>
|
|
adamc@95
|
703 match goal with
|
|
adamc@95
|
704 | [ H : z = x |- _ ] => rewrite H in *; clear H
|
|
adamc@95
|
705 end
|
|
adamc@95
|
706 end;
|
|
adamc@95
|
707 tauto.
|
|
adamc@95
|
708 Qed.
|
|
adamc@95
|
709
|
|
adamc@214
|
710 (** printing * $\times$ *)
|
|
adamc@214
|
711
|
|
adamc@214
|
712 (** 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
|
713
|
|
adamc@213
|
714 Ltac present_insert :=
|
|
adamc@213
|
715 unfold insert; intros n t; inversion t;
|
|
adamc@97
|
716 generalize (present_ins t); simpl;
|
|
adamc@97
|
717 dep_destruct (ins t); tauto.
|
|
adamc@97
|
718
|
|
adamc@95
|
719 Theorem present_insert_Red : forall n (t : rbtree Red n),
|
|
adamc@95
|
720 present z (insert t)
|
|
adamc@95
|
721 <-> (z = x \/ present z t).
|
|
adamc@213
|
722 present_insert.
|
|
adamc@95
|
723 Qed.
|
|
adamc@95
|
724
|
|
adamc@95
|
725 Theorem present_insert_Black : forall n (t : rbtree Black n),
|
|
adamc@95
|
726 present z (projT2 (insert t))
|
|
adamc@95
|
727 <-> (z = x \/ present z t).
|
|
adamc@213
|
728 present_insert.
|
|
adamc@95
|
729 Qed.
|
|
adamc@95
|
730 End present.
|
|
adamc@94
|
731 End insert.
|
|
adamc@94
|
732
|
|
adamc@94
|
733
|
|
adamc@86
|
734 (** * A Certified Regular Expression Matcher *)
|
|
adamc@86
|
735
|
|
adamc@93
|
736 (** 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
|
737
|
|
adamc@93
|
738 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
|
739
|
|
adamc@86
|
740 Require Import Ascii String.
|
|
adamc@86
|
741 Open Scope string_scope.
|
|
adamc@86
|
742
|
|
adamc@91
|
743 Section star.
|
|
adamc@91
|
744 Variable P : string -> Prop.
|
|
adamc@91
|
745
|
|
adamc@91
|
746 Inductive star : string -> Prop :=
|
|
adamc@91
|
747 | Empty : star ""
|
|
adamc@91
|
748 | Iter : forall s1 s2,
|
|
adamc@91
|
749 P s1
|
|
adamc@91
|
750 -> star s2
|
|
adamc@91
|
751 -> star (s1 ++ s2).
|
|
adamc@91
|
752 End star.
|
|
adamc@91
|
753
|
|
adamc@93
|
754 (** 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
|
755
|
|
adamc@93
|
756 [[
|
|
adamc@93
|
757 Inductive regexp : (string -> Prop) -> Set :=
|
|
adamc@93
|
758 | Char : forall ch : ascii,
|
|
adamc@93
|
759 regexp (fun s => s = String ch "")
|
|
adamc@93
|
760 | Concat : forall (P1 P2 : string -> Prop) (r1 : regexp P1) (r2 : regexp P2),
|
|
adamc@93
|
761 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2).
|
|
adamc@93
|
762
|
|
adamc@93
|
763 User error: Large non-propositional inductive types must be in Type
|
|
adamc@214
|
764
|
|
adamc@93
|
765 ]]
|
|
adamc@93
|
766
|
|
adamc@93
|
767 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
|
768
|
|
adamc@93
|
769 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
|
770
|
|
adamc@89
|
771 Inductive regexp : (string -> Prop) -> Type :=
|
|
adamc@86
|
772 | Char : forall ch : ascii,
|
|
adamc@86
|
773 regexp (fun s => s = String ch "")
|
|
adamc@86
|
774 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
|
|
adamc@87
|
775 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2)
|
|
adamc@87
|
776 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
|
|
adamc@91
|
777 regexp (fun s => P1 s \/ P2 s)
|
|
adamc@91
|
778 | Star : forall P (r : regexp P),
|
|
adamc@91
|
779 regexp (star P).
|
|
adamc@86
|
780
|
|
adamc@93
|
781 (** 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
|
782
|
|
adamc@93
|
783 (* begin hide *)
|
|
adamc@86
|
784 Open Scope specif_scope.
|
|
adamc@86
|
785
|
|
adamc@86
|
786 Lemma length_emp : length "" <= 0.
|
|
adamc@86
|
787 crush.
|
|
adamc@86
|
788 Qed.
|
|
adamc@86
|
789
|
|
adamc@86
|
790 Lemma append_emp : forall s, s = "" ++ s.
|
|
adamc@86
|
791 crush.
|
|
adamc@86
|
792 Qed.
|
|
adamc@86
|
793
|
|
adamc@86
|
794 Ltac substring :=
|
|
adamc@86
|
795 crush;
|
|
adamc@86
|
796 repeat match goal with
|
|
adamc@86
|
797 | [ |- context[match ?N with O => _ | S _ => _ end] ] => destruct N; crush
|
|
adamc@86
|
798 end.
|
|
adamc@86
|
799
|
|
adamc@86
|
800 Lemma substring_le : forall s n m,
|
|
adamc@86
|
801 length (substring n m s) <= m.
|
|
adamc@86
|
802 induction s; substring.
|
|
adamc@86
|
803 Qed.
|
|
adamc@86
|
804
|
|
adamc@86
|
805 Lemma substring_all : forall s,
|
|
adamc@86
|
806 substring 0 (length s) s = s.
|
|
adamc@86
|
807 induction s; substring.
|
|
adamc@86
|
808 Qed.
|
|
adamc@86
|
809
|
|
adamc@86
|
810 Lemma substring_none : forall s n,
|
|
adamc@93
|
811 substring n 0 s = "".
|
|
adamc@86
|
812 induction s; substring.
|
|
adamc@86
|
813 Qed.
|
|
adamc@86
|
814
|
|
adamc@86
|
815 Hint Rewrite substring_all substring_none : cpdt.
|
|
adamc@86
|
816
|
|
adamc@86
|
817 Lemma substring_split : forall s m,
|
|
adamc@86
|
818 substring 0 m s ++ substring m (length s - m) s = s.
|
|
adamc@86
|
819 induction s; substring.
|
|
adamc@86
|
820 Qed.
|
|
adamc@86
|
821
|
|
adamc@86
|
822 Lemma length_app1 : forall s1 s2,
|
|
adamc@86
|
823 length s1 <= length (s1 ++ s2).
|
|
adamc@86
|
824 induction s1; crush.
|
|
adamc@86
|
825 Qed.
|
|
adamc@86
|
826
|
|
adamc@86
|
827 Hint Resolve length_emp append_emp substring_le substring_split length_app1.
|
|
adamc@86
|
828
|
|
adamc@86
|
829 Lemma substring_app_fst : forall s2 s1 n,
|
|
adamc@86
|
830 length s1 = n
|
|
adamc@86
|
831 -> substring 0 n (s1 ++ s2) = s1.
|
|
adamc@86
|
832 induction s1; crush.
|
|
adamc@86
|
833 Qed.
|
|
adamc@86
|
834
|
|
adamc@86
|
835 Lemma substring_app_snd : forall s2 s1 n,
|
|
adamc@86
|
836 length s1 = n
|
|
adamc@86
|
837 -> substring n (length (s1 ++ s2) - n) (s1 ++ s2) = s2.
|
|
adamc@86
|
838 Hint Rewrite <- minus_n_O : cpdt.
|
|
adamc@86
|
839
|
|
adamc@86
|
840 induction s1; crush.
|
|
adamc@86
|
841 Qed.
|
|
adamc@86
|
842
|
|
adamc@214
|
843 Hint Rewrite substring_app_fst substring_app_snd using solve [trivial] : cpdt.
|
|
adamc@93
|
844 (* end hide *)
|
|
adamc@93
|
845
|
|
adamc@93
|
846 (** 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
|
847
|
|
adamc@86
|
848 Section split.
|
|
adamc@86
|
849 Variables P1 P2 : string -> Prop.
|
|
adamc@214
|
850 Variable P1_dec : forall s, {P1 s} + {~ P1 s}.
|
|
adamc@214
|
851 Variable P2_dec : forall s, {P2 s} + {~ P2 s}.
|
|
adamc@93
|
852 (** We require a choice of two arbitrary string predicates and functions for deciding them. *)
|
|
adamc@86
|
853
|
|
adamc@86
|
854 Variable s : string.
|
|
adamc@93
|
855 (** 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
|
856
|
|
adamc@93
|
857 (** [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
|
858
|
|
adamc@86
|
859 Definition split' (n : nat) : n <= length s
|
|
adamc@86
|
860 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
|
|
adamc@214
|
861 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2}.
|
|
adamc@86
|
862 refine (fix F (n : nat) : n <= length s
|
|
adamc@86
|
863 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
|
|
adamc@214
|
864 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~ P1 s1 \/ ~ P2 s2} :=
|
|
adamc@214
|
865 match n with
|
|
adamc@86
|
866 | O => fun _ => Reduce (P1_dec "" && P2_dec s)
|
|
adamc@93
|
867 | S n' => fun _ => (P1_dec (substring 0 (S n') s)
|
|
adamc@93
|
868 && P2_dec (substring (S n') (length s - S n') s))
|
|
adamc@86
|
869 || F n' _
|
|
adamc@86
|
870 end); clear F; crush; eauto 7;
|
|
adamc@86
|
871 match goal with
|
|
adamc@86
|
872 | [ _ : length ?S <= 0 |- _ ] => destruct S
|
|
adamc@86
|
873 | [ _ : length ?S' <= S ?N |- _ ] =>
|
|
adamc@86
|
874 generalize (eq_nat_dec (length S') (S N)); destruct 1
|
|
adamc@86
|
875 end; crush.
|
|
adamc@86
|
876 Defined.
|
|
adamc@86
|
877
|
|
adamc@93
|
878 (** 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
|
879
|
|
adamc@93
|
880 [[
|
|
adamc@93
|
881 | S n' => fun _ => let n := S n' in
|
|
adamc@93
|
882 (P1_dec (substring 0 n s)
|
|
adamc@93
|
883 && P2_dec (substring n (length s - n) s))
|
|
adamc@93
|
884 || F n' _
|
|
adamc@214
|
885
|
|
adamc@93
|
886 ]]
|
|
adamc@93
|
887
|
|
adamc@93
|
888 [split] itself is trivial to implement in terms of [split']. We just ask [split'] to begin its search with [n = length s]. *)
|
|
adamc@93
|
889
|
|
adamc@86
|
890 Definition split : {exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2}
|
|
adamc@214
|
891 + {forall s1 s2, s = s1 ++ s2 -> ~ P1 s1 \/ ~ P2 s2}.
|
|
adamc@86
|
892 refine (Reduce (split' (n := length s) _)); crush; eauto.
|
|
adamc@86
|
893 Defined.
|
|
adamc@86
|
894 End split.
|
|
adamc@86
|
895
|
|
adamc@86
|
896 Implicit Arguments split [P1 P2].
|
|
adamc@86
|
897
|
|
adamc@93
|
898 (* begin hide *)
|
|
adamc@91
|
899 Lemma app_empty_end : forall s, s ++ "" = s.
|
|
adamc@91
|
900 induction s; crush.
|
|
adamc@91
|
901 Qed.
|
|
adamc@91
|
902
|
|
adamc@91
|
903 Hint Rewrite app_empty_end : cpdt.
|
|
adamc@91
|
904
|
|
adamc@91
|
905 Lemma substring_self : forall s n,
|
|
adamc@91
|
906 n <= 0
|
|
adamc@91
|
907 -> substring n (length s - n) s = s.
|
|
adamc@91
|
908 induction s; substring.
|
|
adamc@91
|
909 Qed.
|
|
adamc@91
|
910
|
|
adamc@91
|
911 Lemma substring_empty : forall s n m,
|
|
adamc@91
|
912 m <= 0
|
|
adamc@91
|
913 -> substring n m s = "".
|
|
adamc@91
|
914 induction s; substring.
|
|
adamc@91
|
915 Qed.
|
|
adamc@91
|
916
|
|
adamc@91
|
917 Hint Rewrite substring_self substring_empty using omega : cpdt.
|
|
adamc@91
|
918
|
|
adamc@91
|
919 Lemma substring_split' : forall s n m,
|
|
adamc@91
|
920 substring n m s ++ substring (n + m) (length s - (n + m)) s
|
|
adamc@91
|
921 = substring n (length s - n) s.
|
|
adamc@91
|
922 Hint Rewrite substring_split : cpdt.
|
|
adamc@91
|
923
|
|
adamc@91
|
924 induction s; substring.
|
|
adamc@91
|
925 Qed.
|
|
adamc@91
|
926
|
|
adamc@91
|
927 Lemma substring_stack : forall s n2 m1 m2,
|
|
adamc@91
|
928 m1 <= m2
|
|
adamc@91
|
929 -> substring 0 m1 (substring n2 m2 s)
|
|
adamc@91
|
930 = substring n2 m1 s.
|
|
adamc@91
|
931 induction s; substring.
|
|
adamc@91
|
932 Qed.
|
|
adamc@91
|
933
|
|
adamc@91
|
934 Ltac substring' :=
|
|
adamc@91
|
935 crush;
|
|
adamc@91
|
936 repeat match goal with
|
|
adamc@91
|
937 | [ |- context[match ?N with O => _ | S _ => _ end] ] => case_eq N; crush
|
|
adamc@91
|
938 end.
|
|
adamc@91
|
939
|
|
adamc@91
|
940 Lemma substring_stack' : forall s n1 n2 m1 m2,
|
|
adamc@91
|
941 n1 + m1 <= m2
|
|
adamc@91
|
942 -> substring n1 m1 (substring n2 m2 s)
|
|
adamc@91
|
943 = substring (n1 + n2) m1 s.
|
|
adamc@91
|
944 induction s; substring';
|
|
adamc@91
|
945 match goal with
|
|
adamc@91
|
946 | [ |- substring ?N1 _ _ = substring ?N2 _ _ ] =>
|
|
adamc@91
|
947 replace N1 with N2; crush
|
|
adamc@91
|
948 end.
|
|
adamc@91
|
949 Qed.
|
|
adamc@91
|
950
|
|
adamc@91
|
951 Lemma substring_suffix : forall s n,
|
|
adamc@91
|
952 n <= length s
|
|
adamc@91
|
953 -> length (substring n (length s - n) s) = length s - n.
|
|
adamc@91
|
954 induction s; substring.
|
|
adamc@91
|
955 Qed.
|
|
adamc@91
|
956
|
|
adamc@91
|
957 Lemma substring_suffix_emp' : forall s n m,
|
|
adamc@91
|
958 substring n (S m) s = ""
|
|
adamc@91
|
959 -> n >= length s.
|
|
adamc@91
|
960 induction s; crush;
|
|
adamc@91
|
961 match goal with
|
|
adamc@91
|
962 | [ |- ?N >= _ ] => destruct N; crush
|
|
adamc@91
|
963 end;
|
|
adamc@91
|
964 match goal with
|
|
adamc@91
|
965 [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | omega ]
|
|
adamc@91
|
966 end.
|
|
adamc@91
|
967 Qed.
|
|
adamc@91
|
968
|
|
adamc@91
|
969 Lemma substring_suffix_emp : forall s n m,
|
|
adamc@92
|
970 substring n m s = ""
|
|
adamc@92
|
971 -> m > 0
|
|
adamc@91
|
972 -> n >= length s.
|
|
adamc@91
|
973 destruct m as [| m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
|
|
adamc@91
|
974 Qed.
|
|
adamc@91
|
975
|
|
adamc@91
|
976 Hint Rewrite substring_stack substring_stack' substring_suffix
|
|
adamc@91
|
977 using omega : cpdt.
|
|
adamc@91
|
978
|
|
adamc@91
|
979 Lemma minus_minus : forall n m1 m2,
|
|
adamc@91
|
980 m1 + m2 <= n
|
|
adamc@91
|
981 -> n - m1 - m2 = n - (m1 + m2).
|
|
adamc@91
|
982 intros; omega.
|
|
adamc@91
|
983 Qed.
|
|
adamc@91
|
984
|
|
adamc@91
|
985 Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n.
|
|
adamc@91
|
986 intros; omega.
|
|
adamc@91
|
987 Qed.
|
|
adamc@91
|
988
|
|
adamc@91
|
989 Hint Rewrite minus_minus using omega : cpdt.
|
|
adamc@93
|
990 (* end hide *)
|
|
adamc@93
|
991
|
|
adamc@93
|
992 (** 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
|
993
|
|
adamc@91
|
994 Section dec_star.
|
|
adamc@91
|
995 Variable P : string -> Prop.
|
|
adamc@214
|
996 Variable P_dec : forall s, {P s} + {~ P s}.
|
|
adamc@91
|
997
|
|
adamc@93
|
998 (** 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
|
999
|
|
adamc@93
|
1000 (* begin hide *)
|
|
adamc@91
|
1001 Hint Constructors star.
|
|
adamc@91
|
1002
|
|
adamc@91
|
1003 Lemma star_empty : forall s,
|
|
adamc@91
|
1004 length s = 0
|
|
adamc@91
|
1005 -> star P s.
|
|
adamc@91
|
1006 destruct s; crush.
|
|
adamc@91
|
1007 Qed.
|
|
adamc@91
|
1008
|
|
adamc@91
|
1009 Lemma star_singleton : forall s, P s -> star P s.
|
|
adamc@91
|
1010 intros; rewrite <- (app_empty_end s); auto.
|
|
adamc@91
|
1011 Qed.
|
|
adamc@91
|
1012
|
|
adamc@91
|
1013 Lemma star_app : forall s n m,
|
|
adamc@91
|
1014 P (substring n m s)
|
|
adamc@91
|
1015 -> star P (substring (n + m) (length s - (n + m)) s)
|
|
adamc@91
|
1016 -> star P (substring n (length s - n) s).
|
|
adamc@91
|
1017 induction n; substring;
|
|
adamc@91
|
1018 match goal with
|
|
adamc@91
|
1019 | [ H : P (substring ?N ?M ?S) |- _ ] =>
|
|
adamc@91
|
1020 solve [ rewrite <- (substring_split S M); auto
|
|
adamc@91
|
1021 | rewrite <- (substring_split' S N M); auto ]
|
|
adamc@91
|
1022 end.
|
|
adamc@91
|
1023 Qed.
|
|
adamc@91
|
1024
|
|
adamc@91
|
1025 Hint Resolve star_empty star_singleton star_app.
|
|
adamc@91
|
1026
|
|
adamc@91
|
1027 Variable s : string.
|
|
adamc@91
|
1028
|
|
adamc@91
|
1029 Lemma star_inv : forall s,
|
|
adamc@91
|
1030 star P s
|
|
adamc@91
|
1031 -> s = ""
|
|
adamc@91
|
1032 \/ exists i, i < length s
|
|
adamc@91
|
1033 /\ P (substring 0 (S i) s)
|
|
adamc@91
|
1034 /\ star P (substring (S i) (length s - S i) s).
|
|
adamc@91
|
1035 Hint Extern 1 (exists i : nat, _) =>
|
|
adamc@91
|
1036 match goal with
|
|
adamc@91
|
1037 | [ H : P (String _ ?S) |- _ ] => exists (length S); crush
|
|
adamc@91
|
1038 end.
|
|
adamc@91
|
1039
|
|
adamc@91
|
1040 induction 1; [
|
|
adamc@91
|
1041 crush
|
|
adamc@91
|
1042 | match goal with
|
|
adamc@91
|
1043 | [ _ : P ?S |- _ ] => destruct S; crush
|
|
adamc@91
|
1044 end
|
|
adamc@91
|
1045 ].
|
|
adamc@91
|
1046 Qed.
|
|
adamc@91
|
1047
|
|
adamc@91
|
1048 Lemma star_substring_inv : forall n,
|
|
adamc@91
|
1049 n <= length s
|
|
adamc@91
|
1050 -> star P (substring n (length s - n) s)
|
|
adamc@91
|
1051 -> substring n (length s - n) s = ""
|
|
adamc@91
|
1052 \/ exists l, l < length s - n
|
|
adamc@91
|
1053 /\ P (substring n (S l) s)
|
|
adamc@91
|
1054 /\ star P (substring (n + S l) (length s - (n + S l)) s).
|
|
adamc@91
|
1055 Hint Rewrite plus_n_Sm' : cpdt.
|
|
adamc@91
|
1056
|
|
adamc@91
|
1057 intros;
|
|
adamc@91
|
1058 match goal with
|
|
adamc@91
|
1059 | [ H : star _ _ |- _ ] => generalize (star_inv H); do 3 crush; eauto
|
|
adamc@91
|
1060 end.
|
|
adamc@91
|
1061 Qed.
|
|
adamc@93
|
1062 (* end hide *)
|
|
adamc@93
|
1063
|
|
adamc@93
|
1064 (** 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
|
1065
|
|
adamc@91
|
1066 Section dec_star''.
|
|
adamc@91
|
1067 Variable n : nat.
|
|
adamc@93
|
1068 (** [n] is the length of the prefix of [s] that we have already processed. *)
|
|
adamc@91
|
1069
|
|
adamc@91
|
1070 Variable P' : string -> Prop.
|
|
adamc@91
|
1071 Variable P'_dec : forall n' : nat, n' > n
|
|
adamc@91
|
1072 -> {P' (substring n' (length s - n') s)}
|
|
adamc@214
|
1073 + {~ P' (substring n' (length s - n') s)}.
|
|
adamc@93
|
1074 (** 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
|
1075
|
|
adamc@93
|
1076 (** 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
|
1077
|
|
adamc@91
|
1078 Definition dec_star'' (l : nat)
|
|
adamc@91
|
1079 : {exists l', S l' <= l
|
|
adamc@91
|
1080 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
|
|
adamc@91
|
1081 + {forall l', S l' <= l
|
|
adamc@214
|
1082 -> ~ P (substring n (S l') s)
|
|
adamc@214
|
1083 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)}.
|
|
adamc@91
|
1084 refine (fix F (l : nat) : {exists l', S l' <= l
|
|
adamc@91
|
1085 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
|
|
adamc@91
|
1086 + {forall l', S l' <= l
|
|
adamc@214
|
1087 -> ~ P (substring n (S l') s)
|
|
adamc@214
|
1088 \/ ~ P' (substring (n + S l') (length s - (n + S l')) s)} :=
|
|
adamc@214
|
1089 match l with
|
|
adamc@91
|
1090 | O => _
|
|
adamc@91
|
1091 | S l' =>
|
|
adamc@91
|
1092 (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
|
|
adamc@91
|
1093 || F l'
|
|
adamc@91
|
1094 end); clear F; crush; eauto 7;
|
|
adamc@91
|
1095 match goal with
|
|
adamc@91
|
1096 | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush
|
|
adamc@91
|
1097 end.
|
|
adamc@91
|
1098 Defined.
|
|
adamc@91
|
1099 End dec_star''.
|
|
adamc@91
|
1100
|
|
adamc@93
|
1101 (* begin hide *)
|
|
adamc@92
|
1102 Lemma star_length_contra : forall n,
|
|
adamc@92
|
1103 length s > n
|
|
adamc@92
|
1104 -> n >= length s
|
|
adamc@92
|
1105 -> False.
|
|
adamc@92
|
1106 crush.
|
|
adamc@92
|
1107 Qed.
|
|
adamc@92
|
1108
|
|
adamc@92
|
1109 Lemma star_length_flip : forall n n',
|
|
adamc@92
|
1110 length s - n <= S n'
|
|
adamc@92
|
1111 -> length s > n
|
|
adamc@92
|
1112 -> length s - n > 0.
|
|
adamc@92
|
1113 crush.
|
|
adamc@92
|
1114 Qed.
|
|
adamc@92
|
1115
|
|
adamc@92
|
1116 Hint Resolve star_length_contra star_length_flip substring_suffix_emp.
|
|
adamc@93
|
1117 (* end hide *)
|
|
adamc@92
|
1118
|
|
adamc@93
|
1119 (** 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
|
1120
|
|
adamc@91
|
1121 Definition dec_star' (n n' : nat) : length s - n' <= n
|
|
adamc@91
|
1122 -> {star P (substring n' (length s - n') s)}
|
|
adamc@214
|
1123 + {~ star P (substring n' (length s - n') s)}.
|
|
adamc@214
|
1124 refine (fix F (n n' : nat) : length s - n' <= n
|
|
adamc@91
|
1125 -> {star P (substring n' (length s - n') s)}
|
|
adamc@214
|
1126 + {~ star P (substring n' (length s - n') s)} :=
|
|
adamc@214
|
1127 match n with
|
|
adamc@91
|
1128 | O => fun _ => Yes
|
|
adamc@91
|
1129 | S n'' => fun _ =>
|
|
adamc@91
|
1130 le_gt_dec (length s) n'
|
|
adamc@91
|
1131 || dec_star'' (n := n') (star P) (fun n0 _ => Reduce (F n'' n0 _)) (length s - n')
|
|
adamc@92
|
1132 end); clear F; crush; eauto;
|
|
adamc@92
|
1133 match goal with
|
|
adamc@92
|
1134 | [ H : star _ _ |- _ ] => apply star_substring_inv in H; crush; eauto
|
|
adamc@92
|
1135 end;
|
|
adamc@92
|
1136 match goal with
|
|
adamc@92
|
1137 | [ H1 : _ < _ - _, H2 : forall l' : nat, _ <= _ - _ -> _ |- _ ] =>
|
|
adamc@92
|
1138 generalize (H2 _ (lt_le_S _ _ H1)); tauto
|
|
adamc@92
|
1139 end.
|
|
adamc@91
|
1140 Defined.
|
|
adamc@91
|
1141
|
|
adamc@93
|
1142 (** 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
|
1143
|
|
adamc@214
|
1144 Definition dec_star : {star P s} + {~ star P s}.
|
|
adamc@204
|
1145 refine (match s return _ with
|
|
adamc@91
|
1146 | "" => Reduce (dec_star' (n := length s) 0 _)
|
|
adamc@91
|
1147 | _ => Reduce (dec_star' (n := length s) 0 _)
|
|
adamc@91
|
1148 end); crush.
|
|
adamc@91
|
1149 Defined.
|
|
adamc@91
|
1150 End dec_star.
|
|
adamc@91
|
1151
|
|
adamc@93
|
1152 (* begin hide *)
|
|
adamc@86
|
1153 Lemma app_cong : forall x1 y1 x2 y2,
|
|
adamc@86
|
1154 x1 = x2
|
|
adamc@86
|
1155 -> y1 = y2
|
|
adamc@86
|
1156 -> x1 ++ y1 = x2 ++ y2.
|
|
adamc@86
|
1157 congruence.
|
|
adamc@86
|
1158 Qed.
|
|
adamc@86
|
1159
|
|
adamc@86
|
1160 Hint Resolve app_cong.
|
|
adamc@93
|
1161 (* end hide *)
|
|
adamc@93
|
1162
|
|
adamc@93
|
1163 (** 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
|
1164
|
|
adamc@214
|
1165 Definition matches P (r : regexp P) s : {P s} + {~ P s}.
|
|
adamc@214
|
1166 refine (fix F P (r : regexp P) s : {P s} + {~ P s} :=
|
|
adamc@86
|
1167 match r with
|
|
adamc@86
|
1168 | Char ch => string_dec s (String ch "")
|
|
adamc@86
|
1169 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s)
|
|
adamc@87
|
1170 | Or _ _ r1 r2 => F _ r1 s || F _ r2 s
|
|
adamc@91
|
1171 | Star _ r => dec_star _ _ _
|
|
adamc@86
|
1172 end); crush;
|
|
adamc@86
|
1173 match goal with
|
|
adamc@86
|
1174 | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _))
|
|
adamc@93
|
1175 end; tauto.
|
|
adamc@86
|
1176 Defined.
|
|
adamc@86
|
1177
|
|
adamc@93
|
1178 (* begin hide *)
|
|
adamc@86
|
1179 Example hi := Concat (Char "h"%char) (Char "i"%char).
|
|
adamc@86
|
1180 Eval simpl in matches hi "hi".
|
|
adamc@86
|
1181 Eval simpl in matches hi "bye".
|
|
adamc@87
|
1182
|
|
adamc@87
|
1183 Example a_b := Or (Char "a"%char) (Char "b"%char).
|
|
adamc@87
|
1184 Eval simpl in matches a_b "".
|
|
adamc@87
|
1185 Eval simpl in matches a_b "a".
|
|
adamc@87
|
1186 Eval simpl in matches a_b "aa".
|
|
adamc@87
|
1187 Eval simpl in matches a_b "b".
|
|
adamc@91
|
1188
|
|
adamc@91
|
1189 Example a_star := Star (Char "a"%char).
|
|
adamc@91
|
1190 Eval simpl in matches a_star "".
|
|
adamc@91
|
1191 Eval simpl in matches a_star "a".
|
|
adamc@91
|
1192 Eval simpl in matches a_star "b".
|
|
adamc@91
|
1193 Eval simpl in matches a_star "aa".
|
|
adamc@93
|
1194 (* end hide *)
|
|
adamc@101
|
1195
|
|
adamc@101
|
1196
|
|
adamc@101
|
1197 (** * Exercises *)
|
|
adamc@101
|
1198
|
|
adamc@101
|
1199 (** %\begin{enumerate}%#<ol>#
|
|
adamc@101
|
1200
|
|
adamc@101
|
1201 %\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
|
1202 %\begin{enumerate}%#<ol>#
|
|
adamc@101
|
1203 %\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
|
1204 %\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
|
1205 %\item%#<li># Define a function [plistOut] for translating [plist]s to normal [list]s.#</li>#
|
|
adamc@101
|
1206 %\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
|
1207 %\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
|
1208 %\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
|
1209 #</ol>#%\end{enumerate}% #</li>#
|
|
adamc@101
|
1210
|
|
adamc@102
|
1211 #</ol>#%\end{enumerate}% *)
|
