|
adamc@83
|
1 (* Copyright (c) 2008, 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@84
|
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@84
|
43 [[
|
|
adamc@84
|
44 Fixpoint app n1 (ls1 : ilist n1) n2 (ls2 : ilist n2) {struct ls1} : ilist (n1 + n2) :=
|
|
adamc@84
|
45 match ls1 with
|
|
adamc@84
|
46 | Nil => ls2
|
|
adamc@84
|
47 | Cons _ x ls1' => Cons x (app ls1' ls2)
|
|
adamc@84
|
48 end.
|
|
adamc@84
|
49
|
|
adamc@84
|
50 Coq is not happy with this definition:
|
|
adamc@84
|
51
|
|
adamc@84
|
52 [[
|
|
adamc@84
|
53 The term "ls2" has type "ilist n2" while it is expected to have type
|
|
adamc@84
|
54 "ilist (?14 + n2)"
|
|
adamc@84
|
55 ]]
|
|
adamc@84
|
56
|
|
adamc@84
|
57 We see the return of a problem we have considered before. 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. *)
|
|
adamc@84
|
58
|
|
adamc@84
|
59 Fixpoint app n1 (ls1 : ilist n1) n2 (ls2 : ilist n2) {struct ls1} : ilist (n1 + n2) :=
|
|
adamc@84
|
60 match ls1 in (ilist n1) return (ilist (n1 + n2)) with
|
|
adamc@84
|
61 | Nil => ls2
|
|
adamc@84
|
62 | Cons _ x ls1' => Cons x (app ls1' ls2)
|
|
adamc@84
|
63 end.
|
|
adamc@84
|
64
|
|
adamc@84
|
65 (** This version of [app] passes the type checker. 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
|
66
|
|
adamc@84
|
67 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
|
68
|
|
adamc@84
|
69 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
|
70
|
|
adamc@84
|
71 Fixpoint inject (ls : list A) : ilist (length ls) :=
|
|
adamc@84
|
72 match ls return (ilist (length ls)) with
|
|
adamc@84
|
73 | nil => Nil
|
|
adamc@84
|
74 | h :: t => Cons h (inject t)
|
|
adamc@84
|
75 end.
|
|
adamc@84
|
76
|
|
adamc@84
|
77 (** We can define an inverse conversion and prove that it really is an inverse. *)
|
|
adamc@84
|
78
|
|
adamc@84
|
79 Fixpoint unject n (ls : ilist n) {struct ls} : list A :=
|
|
adamc@84
|
80 match ls with
|
|
adamc@84
|
81 | Nil => nil
|
|
adamc@84
|
82 | Cons _ h t => h :: unject t
|
|
adamc@84
|
83 end.
|
|
adamc@84
|
84
|
|
adamc@84
|
85 Theorem inject_inverse : forall ls, unject (inject ls) = ls.
|
|
adamc@84
|
86 induction ls; crush.
|
|
adamc@84
|
87 Qed.
|
|
adamc@84
|
88
|
|
adamc@84
|
89 (** Now let us attempt a function that is surprisingly tricky to write. In ML, the list head function raises an exception when passed an empty list. With length-indexed lists, we can rule out such invalid calls statically, and here is a first attempt at doing so.
|
|
adamc@84
|
90
|
|
adamc@84
|
91 [[
|
|
adamc@84
|
92 Definition hd n (ls : ilist (S n)) : A :=
|
|
adamc@84
|
93 match ls with
|
|
adamc@84
|
94 | Nil => ???
|
|
adamc@84
|
95 | Cons _ h _ => h
|
|
adamc@84
|
96 end.
|
|
adamc@84
|
97
|
|
adamc@84
|
98 It is not clear what to write for the [Nil] case, so we are stuck before we even turn our function over to the type checker. We could try omitting the [Nil] case:
|
|
adamc@84
|
99
|
|
adamc@84
|
100 [[
|
|
adamc@84
|
101 Definition hd n (ls : ilist (S n)) : A :=
|
|
adamc@84
|
102 match ls with
|
|
adamc@84
|
103 | Cons _ h _ => h
|
|
adamc@84
|
104 end.
|
|
adamc@84
|
105
|
|
adamc@84
|
106 [[
|
|
adamc@84
|
107 Error: Non exhaustive pattern-matching: no clause found for pattern Nil
|
|
adamc@84
|
108 ]]
|
|
adamc@84
|
109
|
|
adamc@84
|
110 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
|
111
|
|
adamc@84
|
112 [[
|
|
adamc@84
|
113 Definition hd n (ls : ilist (S n)) : A :=
|
|
adamc@84
|
114 match ls in (ilist (S n)) with
|
|
adamc@84
|
115 | Cons _ h _ => h
|
|
adamc@84
|
116 end.
|
|
adamc@84
|
117
|
|
adamc@84
|
118 [[
|
|
adamc@84
|
119 Error: The reference n was not found in the current environment
|
|
adamc@84
|
120 ]]
|
|
adamc@84
|
121
|
|
adamc@84
|
122 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
|
123
|
|
adamc@84
|
124 Our final, working attempt at [hd] uses an auxiliary function and a surprising [return] annotation. *)
|
|
adamc@84
|
125
|
|
adamc@84
|
126 Definition hd' n (ls : ilist n) :=
|
|
adamc@84
|
127 match ls in (ilist n) return (match n with O => unit | S _ => A end) with
|
|
adamc@84
|
128 | Nil => tt
|
|
adamc@84
|
129 | Cons _ h _ => h
|
|
adamc@84
|
130 end.
|
|
adamc@84
|
131
|
|
adamc@84
|
132 Definition hd n (ls : ilist (S n)) : A := hd' ls.
|
|
adamc@84
|
133
|
|
adamc@84
|
134 (** 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
|
135
|
|
adamc@84
|
136 End ilist.
|
|
adamc@85
|
137
|
|
adamc@85
|
138
|
|
adamc@85
|
139 (** * A Tagless Interpreter *)
|
|
adamc@85
|
140
|
|
adamc@85
|
141 (** 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
|
142
|
|
adamc@85
|
143 Inductive type : Set :=
|
|
adamc@85
|
144 | Nat : type
|
|
adamc@85
|
145 | Bool : type
|
|
adamc@85
|
146 | Prod : type -> type -> type.
|
|
adamc@85
|
147
|
|
adamc@85
|
148 Inductive exp : type -> Set :=
|
|
adamc@85
|
149 | NConst : nat -> exp Nat
|
|
adamc@85
|
150 | Plus : exp Nat -> exp Nat -> exp Nat
|
|
adamc@85
|
151 | Eq : exp Nat -> exp Nat -> exp Bool
|
|
adamc@85
|
152
|
|
adamc@85
|
153 | BConst : bool -> exp Bool
|
|
adamc@85
|
154 | And : exp Bool -> exp Bool -> exp Bool
|
|
adamc@85
|
155 | If : forall t, exp Bool -> exp t -> exp t -> exp t
|
|
adamc@85
|
156
|
|
adamc@85
|
157 | Pair : forall t1 t2, exp t1 -> exp t2 -> exp (Prod t1 t2)
|
|
adamc@85
|
158 | Fst : forall t1 t2, exp (Prod t1 t2) -> exp t1
|
|
adamc@85
|
159 | Snd : forall t1 t2, exp (Prod t1 t2) -> exp t2.
|
|
adamc@85
|
160
|
|
adamc@85
|
161 (** 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
|
162
|
|
adamc@85
|
163 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
|
164
|
|
adamc@85
|
165 Fixpoint typeDenote (t : type) : Set :=
|
|
adamc@85
|
166 match t with
|
|
adamc@85
|
167 | Nat => nat
|
|
adamc@85
|
168 | Bool => bool
|
|
adamc@85
|
169 | Prod t1 t2 => typeDenote t1 * typeDenote t2
|
|
adamc@85
|
170 end%type.
|
|
adamc@85
|
171
|
|
adamc@85
|
172 (** [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
|
173
|
|
adamc@85
|
174 We can define a function [expDenote] that is typed in terms of [typeDenote]. *)
|
|
adamc@85
|
175
|
|
adamc@85
|
176 Fixpoint expDenote t (e : exp t) {struct e} : typeDenote t :=
|
|
adamc@85
|
177 match e in (exp t) return (typeDenote t) with
|
|
adamc@85
|
178 | NConst n => n
|
|
adamc@85
|
179 | Plus e1 e2 => expDenote e1 + expDenote e2
|
|
adamc@85
|
180 | Eq e1 e2 => if eq_nat_dec (expDenote e1) (expDenote e2) then true else false
|
|
adamc@85
|
181
|
|
adamc@85
|
182 | BConst b => b
|
|
adamc@85
|
183 | And e1 e2 => expDenote e1 && expDenote e2
|
|
adamc@85
|
184 | If _ e' e1 e2 => if expDenote e' then expDenote e1 else expDenote e2
|
|
adamc@85
|
185
|
|
adamc@85
|
186 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
|
|
adamc@85
|
187 | Fst _ _ e' => fst (expDenote e')
|
|
adamc@85
|
188 | Snd _ _ e' => snd (expDenote e')
|
|
adamc@85
|
189 end.
|
|
adamc@85
|
190
|
|
adamc@85
|
191 (** Again we find that an [in] annotation is essential for type-checking a function. Besides that, the 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
|
192
|
|
adamc@85
|
193 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
|
194
|
|
adamc@85
|
195 [[
|
|
adamc@85
|
196 Definition pairOut t1 t2 (e : exp (Prod t1 t2)) : option (exp t1 * exp t2) :=
|
|
adamc@85
|
197 match e in (exp (Prod t1 t2)) return option (exp t1 * exp t2) with
|
|
adamc@85
|
198 | Pair _ _ e1 e2 => Some (e1, e2)
|
|
adamc@85
|
199 | _ => None
|
|
adamc@85
|
200 end.
|
|
adamc@85
|
201
|
|
adamc@85
|
202 [[
|
|
adamc@85
|
203 Error: The reference t2 was not found in the current environment
|
|
adamc@85
|
204 ]]
|
|
adamc@85
|
205
|
|
adamc@85
|
206 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
|
207
|
|
adamc@85
|
208 Definition pairOutType (t : type) :=
|
|
adamc@85
|
209 match t with
|
|
adamc@85
|
210 | Prod t1 t2 => option (exp t1 * exp t2)
|
|
adamc@85
|
211 | _ => unit
|
|
adamc@85
|
212 end.
|
|
adamc@85
|
213
|
|
adamc@85
|
214 (** 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
|
215
|
|
adamc@85
|
216 Definition pairOutDefault (t : type) :=
|
|
adamc@85
|
217 match t return (pairOutType t) with
|
|
adamc@85
|
218 | Prod _ _ => None
|
|
adamc@85
|
219 | _ => tt
|
|
adamc@85
|
220 end.
|
|
adamc@85
|
221
|
|
adamc@85
|
222 (** Now [pairOut] is deceptively easy to write. *)
|
|
adamc@85
|
223
|
|
adamc@85
|
224 Definition pairOut t (e : exp t) :=
|
|
adamc@85
|
225 match e in (exp t) return (pairOutType t) with
|
|
adamc@85
|
226 | Pair _ _ e1 e2 => Some (e1, e2)
|
|
adamc@85
|
227 | _ => pairOutDefault _
|
|
adamc@85
|
228 end.
|
|
adamc@85
|
229
|
|
adamc@85
|
230 (** 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
|
231
|
|
adamc@85
|
232 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. *)
|
|
adamc@85
|
233
|
|
adamc@85
|
234 Fixpoint cfold t (e : exp t) {struct e} : exp t :=
|
|
adamc@85
|
235 match e in (exp t) return (exp t) with
|
|
adamc@85
|
236 | NConst n => NConst n
|
|
adamc@85
|
237 | Plus e1 e2 =>
|
|
adamc@85
|
238 let e1' := cfold e1 in
|
|
adamc@85
|
239 let e2' := cfold e2 in
|
|
adamc@85
|
240 match e1', e2' with
|
|
adamc@85
|
241 | NConst n1, NConst n2 => NConst (n1 + n2)
|
|
adamc@85
|
242 | _, _ => Plus e1' e2'
|
|
adamc@85
|
243 end
|
|
adamc@85
|
244 | Eq e1 e2 =>
|
|
adamc@85
|
245 let e1' := cfold e1 in
|
|
adamc@85
|
246 let e2' := cfold e2 in
|
|
adamc@85
|
247 match e1', e2' with
|
|
adamc@85
|
248 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
|
|
adamc@85
|
249 | _, _ => Eq e1' e2'
|
|
adamc@85
|
250 end
|
|
adamc@85
|
251
|
|
adamc@85
|
252 | BConst b => BConst b
|
|
adamc@85
|
253 | And e1 e2 =>
|
|
adamc@85
|
254 let e1' := cfold e1 in
|
|
adamc@85
|
255 let e2' := cfold e2 in
|
|
adamc@85
|
256 match e1', e2' with
|
|
adamc@85
|
257 | BConst b1, BConst b2 => BConst (b1 && b2)
|
|
adamc@85
|
258 | _, _ => And e1' e2'
|
|
adamc@85
|
259 end
|
|
adamc@85
|
260 | If _ e e1 e2 =>
|
|
adamc@85
|
261 let e' := cfold e in
|
|
adamc@85
|
262 match e' with
|
|
adamc@85
|
263 | BConst true => cfold e1
|
|
adamc@85
|
264 | BConst false => cfold e2
|
|
adamc@85
|
265 | _ => If e' (cfold e1) (cfold e2)
|
|
adamc@85
|
266 end
|
|
adamc@85
|
267
|
|
adamc@85
|
268 | Pair _ _ e1 e2 => Pair (cfold e1) (cfold e2)
|
|
adamc@85
|
269 | Fst _ _ e =>
|
|
adamc@85
|
270 let e' := cfold e in
|
|
adamc@85
|
271 match pairOut e' with
|
|
adamc@85
|
272 | Some p => fst p
|
|
adamc@85
|
273 | None => Fst e'
|
|
adamc@85
|
274 end
|
|
adamc@85
|
275 | Snd _ _ e =>
|
|
adamc@85
|
276 let e' := cfold e in
|
|
adamc@85
|
277 match pairOut e' with
|
|
adamc@85
|
278 | Some p => snd p
|
|
adamc@85
|
279 | None => Snd e'
|
|
adamc@85
|
280 end
|
|
adamc@85
|
281 end.
|
|
adamc@85
|
282
|
|
adamc@85
|
283 (** The correctness theorem for [cfold] turns out to be easy to prove, once we get over one serious hurdle. *)
|
|
adamc@85
|
284
|
|
adamc@85
|
285 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
|
|
adamc@85
|
286 induction e; crush.
|
|
adamc@85
|
287
|
|
adamc@85
|
288 (** The first remaining subgoal is:
|
|
adamc@85
|
289
|
|
adamc@85
|
290 [[
|
|
adamc@85
|
291
|
|
adamc@85
|
292 expDenote (cfold e1) + expDenote (cfold e2) =
|
|
adamc@85
|
293 expDenote
|
|
adamc@85
|
294 match cfold e1 with
|
|
adamc@85
|
295 | NConst n1 =>
|
|
adamc@85
|
296 match cfold e2 with
|
|
adamc@85
|
297 | NConst n2 => NConst (n1 + n2)
|
|
adamc@85
|
298 | Plus _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
299 | Eq _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
300 | BConst _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
301 | And _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
302 | If _ _ _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
303 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
304 | Fst _ _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
305 | Snd _ _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
306 end
|
|
adamc@85
|
307 | Plus _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
308 | Eq _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
309 | BConst _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
310 | And _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
311 | If _ _ _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
312 | Pair _ _ _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
313 | Fst _ _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
314 | Snd _ _ _ => Plus (cfold e1) (cfold e2)
|
|
adamc@85
|
315 end
|
|
adamc@85
|
316 ]]
|
|
adamc@85
|
317
|
|
adamc@85
|
318 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
|
319
|
|
adamc@85
|
320 [[
|
|
adamc@85
|
321 destruct (cfold e1).
|
|
adamc@85
|
322
|
|
adamc@85
|
323 [[
|
|
adamc@85
|
324 User error: e1 is used in hypothesis e
|
|
adamc@85
|
325 ]]
|
|
adamc@85
|
326
|
|
adamc@85
|
327 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
|
328
|
|
adamc@85
|
329 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. 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
|
330
|
|
adamc@85
|
331 dep_destruct (cfold e1).
|
|
adamc@85
|
332
|
|
adamc@85
|
333 (** 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
|
334
|
|
adamc@85
|
335 This is the only new trick we need to learn to complete the proof. We can back up and give a short, automated proof. *)
|
|
adamc@85
|
336
|
|
adamc@85
|
337 Restart.
|
|
adamc@85
|
338
|
|
adamc@85
|
339 induction e; crush;
|
|
adamc@85
|
340 repeat (match goal with
|
|
adamc@85
|
341 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
|
|
adamc@85
|
342 | [ |- (if ?E then _ else _) = _ ] => destruct E
|
|
adamc@85
|
343 end; crush).
|
|
adamc@85
|
344 Qed.
|
|
adamc@86
|
345
|
|
adamc@86
|
346
|
|
adamc@86
|
347 (** * A Certified Regular Expression Matcher *)
|
|
adamc@86
|
348
|
|
adamc@93
|
349 (** 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
|
350
|
|
adamc@93
|
351 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
|
352
|
|
adamc@86
|
353 Require Import Ascii String.
|
|
adamc@86
|
354 Open Scope string_scope.
|
|
adamc@86
|
355
|
|
adamc@91
|
356 Section star.
|
|
adamc@91
|
357 Variable P : string -> Prop.
|
|
adamc@91
|
358
|
|
adamc@91
|
359 Inductive star : string -> Prop :=
|
|
adamc@91
|
360 | Empty : star ""
|
|
adamc@91
|
361 | Iter : forall s1 s2,
|
|
adamc@91
|
362 P s1
|
|
adamc@91
|
363 -> star s2
|
|
adamc@91
|
364 -> star (s1 ++ s2).
|
|
adamc@91
|
365 End star.
|
|
adamc@91
|
366
|
|
adamc@93
|
367 (** 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
|
368
|
|
adamc@93
|
369 [[
|
|
adamc@93
|
370 Inductive regexp : (string -> Prop) -> Set :=
|
|
adamc@93
|
371 | Char : forall ch : ascii,
|
|
adamc@93
|
372 regexp (fun s => s = String ch "")
|
|
adamc@93
|
373 | Concat : forall (P1 P2 : string -> Prop) (r1 : regexp P1) (r2 : regexp P2),
|
|
adamc@93
|
374 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2).
|
|
adamc@93
|
375
|
|
adamc@93
|
376 [[
|
|
adamc@93
|
377 User error: Large non-propositional inductive types must be in Type
|
|
adamc@93
|
378 ]]
|
|
adamc@93
|
379
|
|
adamc@93
|
380 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
|
381
|
|
adamc@93
|
382 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
|
383
|
|
adamc@89
|
384 Inductive regexp : (string -> Prop) -> Type :=
|
|
adamc@86
|
385 | Char : forall ch : ascii,
|
|
adamc@86
|
386 regexp (fun s => s = String ch "")
|
|
adamc@86
|
387 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
|
|
adamc@87
|
388 regexp (fun s => exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2)
|
|
adamc@87
|
389 | Or : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),
|
|
adamc@91
|
390 regexp (fun s => P1 s \/ P2 s)
|
|
adamc@91
|
391 | Star : forall P (r : regexp P),
|
|
adamc@91
|
392 regexp (star P).
|
|
adamc@86
|
393
|
|
adamc@93
|
394 (** 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
|
395
|
|
adamc@93
|
396 (* begin hide *)
|
|
adamc@86
|
397 Open Scope specif_scope.
|
|
adamc@86
|
398
|
|
adamc@86
|
399 Lemma length_emp : length "" <= 0.
|
|
adamc@86
|
400 crush.
|
|
adamc@86
|
401 Qed.
|
|
adamc@86
|
402
|
|
adamc@86
|
403 Lemma append_emp : forall s, s = "" ++ s.
|
|
adamc@86
|
404 crush.
|
|
adamc@86
|
405 Qed.
|
|
adamc@86
|
406
|
|
adamc@86
|
407 Ltac substring :=
|
|
adamc@86
|
408 crush;
|
|
adamc@86
|
409 repeat match goal with
|
|
adamc@86
|
410 | [ |- context[match ?N with O => _ | S _ => _ end] ] => destruct N; crush
|
|
adamc@86
|
411 end.
|
|
adamc@86
|
412
|
|
adamc@86
|
413 Lemma substring_le : forall s n m,
|
|
adamc@86
|
414 length (substring n m s) <= m.
|
|
adamc@86
|
415 induction s; substring.
|
|
adamc@86
|
416 Qed.
|
|
adamc@86
|
417
|
|
adamc@86
|
418 Lemma substring_all : forall s,
|
|
adamc@86
|
419 substring 0 (length s) s = s.
|
|
adamc@86
|
420 induction s; substring.
|
|
adamc@86
|
421 Qed.
|
|
adamc@86
|
422
|
|
adamc@86
|
423 Lemma substring_none : forall s n,
|
|
adamc@93
|
424 substring n 0 s = "".
|
|
adamc@86
|
425 induction s; substring.
|
|
adamc@86
|
426 Qed.
|
|
adamc@86
|
427
|
|
adamc@86
|
428 Hint Rewrite substring_all substring_none : cpdt.
|
|
adamc@86
|
429
|
|
adamc@86
|
430 Lemma substring_split : forall s m,
|
|
adamc@86
|
431 substring 0 m s ++ substring m (length s - m) s = s.
|
|
adamc@86
|
432 induction s; substring.
|
|
adamc@86
|
433 Qed.
|
|
adamc@86
|
434
|
|
adamc@86
|
435 Lemma length_app1 : forall s1 s2,
|
|
adamc@86
|
436 length s1 <= length (s1 ++ s2).
|
|
adamc@86
|
437 induction s1; crush.
|
|
adamc@86
|
438 Qed.
|
|
adamc@86
|
439
|
|
adamc@86
|
440 Hint Resolve length_emp append_emp substring_le substring_split length_app1.
|
|
adamc@86
|
441
|
|
adamc@86
|
442 Lemma substring_app_fst : forall s2 s1 n,
|
|
adamc@86
|
443 length s1 = n
|
|
adamc@86
|
444 -> substring 0 n (s1 ++ s2) = s1.
|
|
adamc@86
|
445 induction s1; crush.
|
|
adamc@86
|
446 Qed.
|
|
adamc@86
|
447
|
|
adamc@86
|
448 Lemma substring_app_snd : forall s2 s1 n,
|
|
adamc@86
|
449 length s1 = n
|
|
adamc@86
|
450 -> substring n (length (s1 ++ s2) - n) (s1 ++ s2) = s2.
|
|
adamc@86
|
451 Hint Rewrite <- minus_n_O : cpdt.
|
|
adamc@86
|
452
|
|
adamc@86
|
453 induction s1; crush.
|
|
adamc@86
|
454 Qed.
|
|
adamc@86
|
455
|
|
adamc@91
|
456 Hint Rewrite substring_app_fst substring_app_snd using (trivial; fail) : cpdt.
|
|
adamc@93
|
457 (* end hide *)
|
|
adamc@93
|
458
|
|
adamc@93
|
459 (** 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
|
460
|
|
adamc@86
|
461 Section split.
|
|
adamc@86
|
462 Variables P1 P2 : string -> Prop.
|
|
adamc@91
|
463 Variable P1_dec : forall s, {P1 s} + { ~P1 s}.
|
|
adamc@91
|
464 Variable P2_dec : forall s, {P2 s} + { ~P2 s}.
|
|
adamc@93
|
465 (** We require a choice of two arbitrary string predicates and functions for deciding them. *)
|
|
adamc@86
|
466
|
|
adamc@86
|
467 Variable s : string.
|
|
adamc@93
|
468 (** 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
|
469
|
|
adamc@93
|
470 (** [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
|
471
|
|
adamc@86
|
472 Definition split' (n : nat) : n <= length s
|
|
adamc@86
|
473 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
|
|
adamc@86
|
474 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~P1 s1 \/ ~P2 s2}.
|
|
adamc@86
|
475 refine (fix F (n : nat) : n <= length s
|
|
adamc@86
|
476 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
|
|
adamc@86
|
477 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~P1 s1 \/ ~P2 s2} :=
|
|
adamc@86
|
478 match n return n <= length s
|
|
adamc@86
|
479 -> {exists s1, exists s2, length s1 <= n /\ s1 ++ s2 = s /\ P1 s1 /\ P2 s2}
|
|
adamc@86
|
480 + {forall s1 s2, length s1 <= n -> s1 ++ s2 = s -> ~P1 s1 \/ ~P2 s2} with
|
|
adamc@86
|
481 | O => fun _ => Reduce (P1_dec "" && P2_dec s)
|
|
adamc@93
|
482 | S n' => fun _ => (P1_dec (substring 0 (S n') s)
|
|
adamc@93
|
483 && P2_dec (substring (S n') (length s - S n') s))
|
|
adamc@86
|
484 || F n' _
|
|
adamc@86
|
485 end); clear F; crush; eauto 7;
|
|
adamc@86
|
486 match goal with
|
|
adamc@86
|
487 | [ _ : length ?S <= 0 |- _ ] => destruct S
|
|
adamc@86
|
488 | [ _ : length ?S' <= S ?N |- _ ] =>
|
|
adamc@86
|
489 generalize (eq_nat_dec (length S') (S N)); destruct 1
|
|
adamc@86
|
490 end; crush.
|
|
adamc@86
|
491 Defined.
|
|
adamc@86
|
492
|
|
adamc@93
|
493 (** 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
|
494
|
|
adamc@93
|
495 [[
|
|
adamc@93
|
496
|
|
adamc@93
|
497 | S n' => fun _ => let n := S n' in
|
|
adamc@93
|
498 (P1_dec (substring 0 n s)
|
|
adamc@93
|
499 && P2_dec (substring n (length s - n) s))
|
|
adamc@93
|
500 || F n' _
|
|
adamc@93
|
501 ]]
|
|
adamc@93
|
502
|
|
adamc@93
|
503 [split] itself is trivial to implement in terms of [split']. We just ask [split'] to begin its search with [n = length s]. *)
|
|
adamc@93
|
504
|
|
adamc@86
|
505 Definition split : {exists s1, exists s2, s = s1 ++ s2 /\ P1 s1 /\ P2 s2}
|
|
adamc@86
|
506 + {forall s1 s2, s = s1 ++ s2 -> ~P1 s1 \/ ~P2 s2}.
|
|
adamc@86
|
507 refine (Reduce (split' (n := length s) _)); crush; eauto.
|
|
adamc@86
|
508 Defined.
|
|
adamc@86
|
509 End split.
|
|
adamc@86
|
510
|
|
adamc@86
|
511 Implicit Arguments split [P1 P2].
|
|
adamc@86
|
512
|
|
adamc@93
|
513 (* begin hide *)
|
|
adamc@91
|
514 Lemma app_empty_end : forall s, s ++ "" = s.
|
|
adamc@91
|
515 induction s; crush.
|
|
adamc@91
|
516 Qed.
|
|
adamc@91
|
517
|
|
adamc@91
|
518 Hint Rewrite app_empty_end : cpdt.
|
|
adamc@91
|
519
|
|
adamc@91
|
520 Lemma substring_self : forall s n,
|
|
adamc@91
|
521 n <= 0
|
|
adamc@91
|
522 -> substring n (length s - n) s = s.
|
|
adamc@91
|
523 induction s; substring.
|
|
adamc@91
|
524 Qed.
|
|
adamc@91
|
525
|
|
adamc@91
|
526 Lemma substring_empty : forall s n m,
|
|
adamc@91
|
527 m <= 0
|
|
adamc@91
|
528 -> substring n m s = "".
|
|
adamc@91
|
529 induction s; substring.
|
|
adamc@91
|
530 Qed.
|
|
adamc@91
|
531
|
|
adamc@91
|
532 Hint Rewrite substring_self substring_empty using omega : cpdt.
|
|
adamc@91
|
533
|
|
adamc@91
|
534 Lemma substring_split' : forall s n m,
|
|
adamc@91
|
535 substring n m s ++ substring (n + m) (length s - (n + m)) s
|
|
adamc@91
|
536 = substring n (length s - n) s.
|
|
adamc@91
|
537 Hint Rewrite substring_split : cpdt.
|
|
adamc@91
|
538
|
|
adamc@91
|
539 induction s; substring.
|
|
adamc@91
|
540 Qed.
|
|
adamc@91
|
541
|
|
adamc@91
|
542 Lemma substring_stack : forall s n2 m1 m2,
|
|
adamc@91
|
543 m1 <= m2
|
|
adamc@91
|
544 -> substring 0 m1 (substring n2 m2 s)
|
|
adamc@91
|
545 = substring n2 m1 s.
|
|
adamc@91
|
546 induction s; substring.
|
|
adamc@91
|
547 Qed.
|
|
adamc@91
|
548
|
|
adamc@91
|
549 Ltac substring' :=
|
|
adamc@91
|
550 crush;
|
|
adamc@91
|
551 repeat match goal with
|
|
adamc@91
|
552 | [ |- context[match ?N with O => _ | S _ => _ end] ] => case_eq N; crush
|
|
adamc@91
|
553 end.
|
|
adamc@91
|
554
|
|
adamc@91
|
555 Lemma substring_stack' : forall s n1 n2 m1 m2,
|
|
adamc@91
|
556 n1 + m1 <= m2
|
|
adamc@91
|
557 -> substring n1 m1 (substring n2 m2 s)
|
|
adamc@91
|
558 = substring (n1 + n2) m1 s.
|
|
adamc@91
|
559 induction s; substring';
|
|
adamc@91
|
560 match goal with
|
|
adamc@91
|
561 | [ |- substring ?N1 _ _ = substring ?N2 _ _ ] =>
|
|
adamc@91
|
562 replace N1 with N2; crush
|
|
adamc@91
|
563 end.
|
|
adamc@91
|
564 Qed.
|
|
adamc@91
|
565
|
|
adamc@91
|
566 Lemma substring_suffix : forall s n,
|
|
adamc@91
|
567 n <= length s
|
|
adamc@91
|
568 -> length (substring n (length s - n) s) = length s - n.
|
|
adamc@91
|
569 induction s; substring.
|
|
adamc@91
|
570 Qed.
|
|
adamc@91
|
571
|
|
adamc@91
|
572 Lemma substring_suffix_emp' : forall s n m,
|
|
adamc@91
|
573 substring n (S m) s = ""
|
|
adamc@91
|
574 -> n >= length s.
|
|
adamc@91
|
575 induction s; crush;
|
|
adamc@91
|
576 match goal with
|
|
adamc@91
|
577 | [ |- ?N >= _ ] => destruct N; crush
|
|
adamc@91
|
578 end;
|
|
adamc@91
|
579 match goal with
|
|
adamc@91
|
580 [ |- S ?N >= S ?E ] => assert (N >= E); [ eauto | omega ]
|
|
adamc@91
|
581 end.
|
|
adamc@91
|
582 Qed.
|
|
adamc@91
|
583
|
|
adamc@91
|
584 Lemma substring_suffix_emp : forall s n m,
|
|
adamc@92
|
585 substring n m s = ""
|
|
adamc@92
|
586 -> m > 0
|
|
adamc@91
|
587 -> n >= length s.
|
|
adamc@91
|
588 destruct m as [| m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
|
|
adamc@91
|
589 Qed.
|
|
adamc@91
|
590
|
|
adamc@91
|
591 Hint Rewrite substring_stack substring_stack' substring_suffix
|
|
adamc@91
|
592 using omega : cpdt.
|
|
adamc@91
|
593
|
|
adamc@91
|
594 Lemma minus_minus : forall n m1 m2,
|
|
adamc@91
|
595 m1 + m2 <= n
|
|
adamc@91
|
596 -> n - m1 - m2 = n - (m1 + m2).
|
|
adamc@91
|
597 intros; omega.
|
|
adamc@91
|
598 Qed.
|
|
adamc@91
|
599
|
|
adamc@91
|
600 Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n.
|
|
adamc@91
|
601 intros; omega.
|
|
adamc@91
|
602 Qed.
|
|
adamc@91
|
603
|
|
adamc@91
|
604 Hint Rewrite minus_minus using omega : cpdt.
|
|
adamc@93
|
605 (* end hide *)
|
|
adamc@93
|
606
|
|
adamc@93
|
607 (** 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
|
608
|
|
adamc@91
|
609 Section dec_star.
|
|
adamc@91
|
610 Variable P : string -> Prop.
|
|
adamc@91
|
611 Variable P_dec : forall s, {P s} + { ~P s}.
|
|
adamc@91
|
612
|
|
adamc@93
|
613 (** 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
|
614
|
|
adamc@93
|
615 (* begin hide *)
|
|
adamc@91
|
616 Hint Constructors star.
|
|
adamc@91
|
617
|
|
adamc@91
|
618 Lemma star_empty : forall s,
|
|
adamc@91
|
619 length s = 0
|
|
adamc@91
|
620 -> star P s.
|
|
adamc@91
|
621 destruct s; crush.
|
|
adamc@91
|
622 Qed.
|
|
adamc@91
|
623
|
|
adamc@91
|
624 Lemma star_singleton : forall s, P s -> star P s.
|
|
adamc@91
|
625 intros; rewrite <- (app_empty_end s); auto.
|
|
adamc@91
|
626 Qed.
|
|
adamc@91
|
627
|
|
adamc@91
|
628 Lemma star_app : forall s n m,
|
|
adamc@91
|
629 P (substring n m s)
|
|
adamc@91
|
630 -> star P (substring (n + m) (length s - (n + m)) s)
|
|
adamc@91
|
631 -> star P (substring n (length s - n) s).
|
|
adamc@91
|
632 induction n; substring;
|
|
adamc@91
|
633 match goal with
|
|
adamc@91
|
634 | [ H : P (substring ?N ?M ?S) |- _ ] =>
|
|
adamc@91
|
635 solve [ rewrite <- (substring_split S M); auto
|
|
adamc@91
|
636 | rewrite <- (substring_split' S N M); auto ]
|
|
adamc@91
|
637 end.
|
|
adamc@91
|
638 Qed.
|
|
adamc@91
|
639
|
|
adamc@91
|
640 Hint Resolve star_empty star_singleton star_app.
|
|
adamc@91
|
641
|
|
adamc@91
|
642 Variable s : string.
|
|
adamc@91
|
643
|
|
adamc@91
|
644 Lemma star_inv : forall s,
|
|
adamc@91
|
645 star P s
|
|
adamc@91
|
646 -> s = ""
|
|
adamc@91
|
647 \/ exists i, i < length s
|
|
adamc@91
|
648 /\ P (substring 0 (S i) s)
|
|
adamc@91
|
649 /\ star P (substring (S i) (length s - S i) s).
|
|
adamc@91
|
650 Hint Extern 1 (exists i : nat, _) =>
|
|
adamc@91
|
651 match goal with
|
|
adamc@91
|
652 | [ H : P (String _ ?S) |- _ ] => exists (length S); crush
|
|
adamc@91
|
653 end.
|
|
adamc@91
|
654
|
|
adamc@91
|
655 induction 1; [
|
|
adamc@91
|
656 crush
|
|
adamc@91
|
657 | match goal with
|
|
adamc@91
|
658 | [ _ : P ?S |- _ ] => destruct S; crush
|
|
adamc@91
|
659 end
|
|
adamc@91
|
660 ].
|
|
adamc@91
|
661 Qed.
|
|
adamc@91
|
662
|
|
adamc@91
|
663 Lemma star_substring_inv : forall n,
|
|
adamc@91
|
664 n <= length s
|
|
adamc@91
|
665 -> star P (substring n (length s - n) s)
|
|
adamc@91
|
666 -> substring n (length s - n) s = ""
|
|
adamc@91
|
667 \/ exists l, l < length s - n
|
|
adamc@91
|
668 /\ P (substring n (S l) s)
|
|
adamc@91
|
669 /\ star P (substring (n + S l) (length s - (n + S l)) s).
|
|
adamc@91
|
670 Hint Rewrite plus_n_Sm' : cpdt.
|
|
adamc@91
|
671
|
|
adamc@91
|
672 intros;
|
|
adamc@91
|
673 match goal with
|
|
adamc@91
|
674 | [ H : star _ _ |- _ ] => generalize (star_inv H); do 3 crush; eauto
|
|
adamc@91
|
675 end.
|
|
adamc@91
|
676 Qed.
|
|
adamc@93
|
677 (* end hide *)
|
|
adamc@93
|
678
|
|
adamc@93
|
679 (** 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
|
680
|
|
adamc@91
|
681 Section dec_star''.
|
|
adamc@91
|
682 Variable n : nat.
|
|
adamc@93
|
683 (** [n] is the length of the prefix of [s] that we have already processed. *)
|
|
adamc@91
|
684
|
|
adamc@91
|
685 Variable P' : string -> Prop.
|
|
adamc@91
|
686 Variable P'_dec : forall n' : nat, n' > n
|
|
adamc@91
|
687 -> {P' (substring n' (length s - n') s)}
|
|
adamc@91
|
688 + { ~P' (substring n' (length s - n') s)}.
|
|
adamc@93
|
689 (** 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
|
690
|
|
adamc@93
|
691 (** 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
|
692
|
|
adamc@91
|
693 Definition dec_star'' (l : nat)
|
|
adamc@91
|
694 : {exists l', S l' <= l
|
|
adamc@91
|
695 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
|
|
adamc@91
|
696 + {forall l', S l' <= l
|
|
adamc@93
|
697 -> ~P (substring n (S l') s)
|
|
adamc@93
|
698 \/ ~P' (substring (n + S l') (length s - (n + S l')) s)}.
|
|
adamc@91
|
699 refine (fix F (l : nat) : {exists l', S l' <= l
|
|
adamc@91
|
700 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
|
|
adamc@91
|
701 + {forall l', S l' <= l
|
|
adamc@93
|
702 -> ~P (substring n (S l') s)
|
|
adamc@93
|
703 \/ ~P' (substring (n + S l') (length s - (n + S l')) s)} :=
|
|
adamc@91
|
704 match l return {exists l', S l' <= l
|
|
adamc@91
|
705 /\ P (substring n (S l') s) /\ P' (substring (n + S l') (length s - (n + S l')) s)}
|
|
adamc@91
|
706 + {forall l', S l' <= l ->
|
|
adamc@93
|
707 ~P (substring n (S l') s)
|
|
adamc@93
|
708 \/ ~P' (substring (n + S l') (length s - (n + S l')) s)} with
|
|
adamc@91
|
709 | O => _
|
|
adamc@91
|
710 | S l' =>
|
|
adamc@91
|
711 (P_dec (substring n (S l') s) && P'_dec (n' := n + S l') _)
|
|
adamc@91
|
712 || F l'
|
|
adamc@91
|
713 end); clear F; crush; eauto 7;
|
|
adamc@91
|
714 match goal with
|
|
adamc@91
|
715 | [ H : ?X <= S ?Y |- _ ] => destruct (eq_nat_dec X (S Y)); crush
|
|
adamc@91
|
716 end.
|
|
adamc@91
|
717 Defined.
|
|
adamc@91
|
718 End dec_star''.
|
|
adamc@91
|
719
|
|
adamc@93
|
720 (* begin hide *)
|
|
adamc@92
|
721 Lemma star_length_contra : forall n,
|
|
adamc@92
|
722 length s > n
|
|
adamc@92
|
723 -> n >= length s
|
|
adamc@92
|
724 -> False.
|
|
adamc@92
|
725 crush.
|
|
adamc@92
|
726 Qed.
|
|
adamc@92
|
727
|
|
adamc@92
|
728 Lemma star_length_flip : forall n n',
|
|
adamc@92
|
729 length s - n <= S n'
|
|
adamc@92
|
730 -> length s > n
|
|
adamc@92
|
731 -> length s - n > 0.
|
|
adamc@92
|
732 crush.
|
|
adamc@92
|
733 Qed.
|
|
adamc@92
|
734
|
|
adamc@92
|
735 Hint Resolve star_length_contra star_length_flip substring_suffix_emp.
|
|
adamc@93
|
736 (* end hide *)
|
|
adamc@92
|
737
|
|
adamc@93
|
738 (** 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
|
739
|
|
adamc@91
|
740 Definition dec_star' (n n' : nat) : length s - n' <= n
|
|
adamc@91
|
741 -> {star P (substring n' (length s - n') s)}
|
|
adamc@93
|
742 + { ~star P (substring n' (length s - n') s)}.
|
|
adamc@91
|
743 refine (fix F (n n' : nat) {struct n} : length s - n' <= n
|
|
adamc@91
|
744 -> {star P (substring n' (length s - n') s)}
|
|
adamc@93
|
745 + { ~star P (substring n' (length s - n') s)} :=
|
|
adamc@91
|
746 match n return length s - n' <= n
|
|
adamc@91
|
747 -> {star P (substring n' (length s - n') s)}
|
|
adamc@93
|
748 + { ~star P (substring n' (length s - n') s)} with
|
|
adamc@91
|
749 | O => fun _ => Yes
|
|
adamc@91
|
750 | S n'' => fun _ =>
|
|
adamc@91
|
751 le_gt_dec (length s) n'
|
|
adamc@91
|
752 || dec_star'' (n := n') (star P) (fun n0 _ => Reduce (F n'' n0 _)) (length s - n')
|
|
adamc@92
|
753 end); clear F; crush; eauto;
|
|
adamc@92
|
754 match goal with
|
|
adamc@92
|
755 | [ H : star _ _ |- _ ] => apply star_substring_inv in H; crush; eauto
|
|
adamc@92
|
756 end;
|
|
adamc@92
|
757 match goal with
|
|
adamc@92
|
758 | [ H1 : _ < _ - _, H2 : forall l' : nat, _ <= _ - _ -> _ |- _ ] =>
|
|
adamc@92
|
759 generalize (H2 _ (lt_le_S _ _ H1)); tauto
|
|
adamc@92
|
760 end.
|
|
adamc@91
|
761 Defined.
|
|
adamc@91
|
762
|
|
adamc@93
|
763 (** 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
|
764
|
|
adamc@91
|
765 Definition dec_star : {star P s} + { ~star P s}.
|
|
adamc@91
|
766 refine (match s with
|
|
adamc@91
|
767 | "" => Reduce (dec_star' (n := length s) 0 _)
|
|
adamc@91
|
768 | _ => Reduce (dec_star' (n := length s) 0 _)
|
|
adamc@91
|
769 end); crush.
|
|
adamc@91
|
770 Defined.
|
|
adamc@91
|
771 End dec_star.
|
|
adamc@91
|
772
|
|
adamc@93
|
773 (* begin hide *)
|
|
adamc@86
|
774 Lemma app_cong : forall x1 y1 x2 y2,
|
|
adamc@86
|
775 x1 = x2
|
|
adamc@86
|
776 -> y1 = y2
|
|
adamc@86
|
777 -> x1 ++ y1 = x2 ++ y2.
|
|
adamc@86
|
778 congruence.
|
|
adamc@86
|
779 Qed.
|
|
adamc@86
|
780
|
|
adamc@86
|
781 Hint Resolve app_cong.
|
|
adamc@93
|
782 (* end hide *)
|
|
adamc@93
|
783
|
|
adamc@93
|
784 (** 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
|
785
|
|
adamc@86
|
786 Definition matches P (r : regexp P) s : {P s} + { ~P s}.
|
|
adamc@86
|
787 refine (fix F P (r : regexp P) s : {P s} + { ~P s} :=
|
|
adamc@86
|
788 match r with
|
|
adamc@86
|
789 | Char ch => string_dec s (String ch "")
|
|
adamc@86
|
790 | Concat _ _ r1 r2 => Reduce (split (F _ r1) (F _ r2) s)
|
|
adamc@87
|
791 | Or _ _ r1 r2 => F _ r1 s || F _ r2 s
|
|
adamc@91
|
792 | Star _ r => dec_star _ _ _
|
|
adamc@86
|
793 end); crush;
|
|
adamc@86
|
794 match goal with
|
|
adamc@86
|
795 | [ H : _ |- _ ] => generalize (H _ _ (refl_equal _))
|
|
adamc@93
|
796 end; tauto.
|
|
adamc@86
|
797 Defined.
|
|
adamc@86
|
798
|
|
adamc@93
|
799 (* begin hide *)
|
|
adamc@86
|
800 Example hi := Concat (Char "h"%char) (Char "i"%char).
|
|
adamc@86
|
801 Eval simpl in matches hi "hi".
|
|
adamc@86
|
802 Eval simpl in matches hi "bye".
|
|
adamc@87
|
803
|
|
adamc@87
|
804 Example a_b := Or (Char "a"%char) (Char "b"%char).
|
|
adamc@87
|
805 Eval simpl in matches a_b "".
|
|
adamc@87
|
806 Eval simpl in matches a_b "a".
|
|
adamc@87
|
807 Eval simpl in matches a_b "aa".
|
|
adamc@87
|
808 Eval simpl in matches a_b "b".
|
|
adamc@91
|
809
|
|
adamc@91
|
810 Example a_star := Star (Char "a"%char).
|
|
adamc@91
|
811 Eval simpl in matches a_star "".
|
|
adamc@91
|
812 Eval simpl in matches a_star "a".
|
|
adamc@91
|
813 Eval simpl in matches a_star "b".
|
|
adamc@91
|
814 Eval simpl in matches a_star "aa".
|
|
adamc@93
|
815 (* end hide *)
|
