Mercurial > cpdt > repo

annotate src/Reflection.v @ 144:5ea9a0bff8f7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Code for my_tauto
author Adam Chlipala <adamc@hcoop.net>
date Tue, 28 Oct 2008 14:28:22 -0400
parents f3e018e167f8
children 617323a60cc4
rev   line source
adamc@142 1 (* Copyright (c) 2008, Adam Chlipala
adamc@142 2 *
adamc@142 3 * This work is licensed under a
adamc@142 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@142 5 * Unported License.
adamc@142 6 * The license text is available at:
adamc@142 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@142 8 *)
adamc@142 9
adamc@142 10 (* begin hide *)
adamc@142 11 Require Import List.
adamc@142 12
adamc@142 13 Require Import Tactics MoreSpecif.
adamc@142 14
adamc@142 15 Set Implicit Arguments.
adamc@142 16 (* end hide *)
adamc@142 17
adamc@142 18
adamc@142 19 (** %\chapter{Proof by Reflection}% *)
adamc@142 20
adamc@142 21 (** The last chapter highlighted a very heuristic approach to proving. In this chapter, we will study an alternative technique, %\textit{%#<i>#proof by reflection#</i>#%}%. We will write, in Gallina, decision procedures with proofs of correctness, and we will appeal to these procedures in writing very short proofs. Such a proof is checked by running the decision procedure. The term %\textit{%#<i>#reflection#</i>#%}% applies because we will need to translate Gallina propositions into values of inductive types representing syntax, so that Gallina programs may analyze them. *)
adamc@142 22
adamc@142 23
adamc@142 24 (** * Proving Evenness *)
adamc@142 25
adamc@142 26 (** Proving that particular natural number constants are even is certainly something we would rather have happen automatically. The Ltac-programming techniques that we learned in the last chapter make it easy to implement such a procedure. *)
adamc@142 27
adamc@142 28 Inductive isEven : nat -> Prop :=
adamc@144 29 | Even_O : isEven O
adamc@144 30 | Even_SS : forall n, isEven n -> isEven (S (S n)).
adamc@142 31
adamc@142 32 Ltac prove_even := repeat constructor.
adamc@142 33
adamc@142 34 Theorem even_256 : isEven 256.
adamc@142 35 prove_even.
adamc@142 36 Qed.
adamc@142 37
adamc@142 38 Print even_256.
adamc@142 39 (** [[
adamc@142 40
adamc@142 41 even_256 =
adamc@142 42 Even_SS
adamc@142 43 (Even_SS
adamc@142 44 (Even_SS
adamc@142 45 (Even_SS
adamc@142 46 ]]
adamc@142 47
adamc@142 48 ...and so on. This procedure always works (at least on machines with infinite resources), but it has a serious drawback, which we see when we print the proof it generates that 256 is even. The final proof term has length linear in the input value. This seems like a shame, since we could write a trivial and trustworthy program to verify evenness of constants. The proof checker could simply call our program where needed.
adamc@142 49
adamc@142 50 It is also unfortunate not to have static typing guarantees that our tactic always behaves appropriately. Other invocations of similar tactics might fail with dynamic type errors, and we would not know about the bugs behind these errors until we happened to attempt to prove complex enough goals.
adamc@142 51
adamc@142 52 The techniques of proof by reflection address both complaints. We will be able to write proofs like this with constant size overhead beyond the size of the input, and we will do it with verified decision procedures written in Gallina.
adamc@142 53
adamc@142 54 For this example, we begin by using a type from the [MoreSpecif] module to write a certified evenness checker. *)
adamc@142 55
adamc@142 56 Print partial.
adamc@142 57 (** [[
adamc@142 58
adamc@142 59 Inductive partial (P : Prop) : Set := Proved : P -> [P] | Uncertain : [P]
adamc@142 60 ]] *)
adamc@142 61
adamc@142 62 (** A [partial P] value is an optional proof of [P]. The notation [[P]] stands for [partial P]. *)
adamc@142 63
adamc@142 64 Open Local Scope partial_scope.
adamc@142 65
adamc@142 66 (** We bring into scope some notations for the [partial] type. These overlap with some of the notations we have seen previously for specification types, so they were placed in a separate scope that needs separate opening. *)
adamc@142 67
adamc@142 68 Definition check_even (n : nat) : [isEven n].
adamc@142 69 Hint Constructors isEven.
adamc@142 70
adamc@142 71 refine (fix F (n : nat) : [isEven n] :=
adamc@142 72 match n return [isEven n] with
adamc@142 73 | 0 => Yes
adamc@142 74 | 1 => No
adamc@142 75 | S (S n') => Reduce (F n')
adamc@142 76 end); auto.
adamc@142 77 Defined.
adamc@142 78
adamc@142 79 (** We can use dependent pattern-matching to write a function that performs a surprising feat. When given a [partial P], this function [partialOut] returns a proof of [P] if the [partial] value contains a proof, and it returns a (useless) proof of [True] otherwise. From the standpoint of ML and Haskell programming, it seems impossible to write such a type, but it is trivial with a [return] annotation. *)
adamc@142 80
adamc@142 81 Definition partialOut (P : Prop) (x : [P]) :=
adamc@142 82 match x return (match x with
adamc@142 83 | Proved _ => P
adamc@142 84 | Uncertain => True
adamc@142 85 end) with
adamc@142 86 | Proved pf => pf
adamc@142 87 | Uncertain => I
adamc@142 88 end.
adamc@142 89
adamc@142 90 (** It may seem strange to define a function like this. However, it turns out to be very useful in writing a reflective verison of our earlier [prove_even] tactic: *)
adamc@142 91
adamc@142 92 Ltac prove_even_reflective :=
adamc@142 93 match goal with
adamc@142 94 | [ |- isEven ?N] => exact (partialOut (check_even N))
adamc@142 95 end.
adamc@142 96
adamc@142 97 (** We identify which natural number we are considering, and we "prove" its evenness by pulling the proof out of the appropriate [check_even] call. *)
adamc@142 98
adamc@142 99 Theorem even_256' : isEven 256.
adamc@142 100 prove_even_reflective.
adamc@142 101 Qed.
adamc@142 102
adamc@142 103 Print even_256'.
adamc@142 104 (** [[
adamc@142 105
adamc@142 106 even_256' = partialOut (check_even 256)
adamc@142 107 : isEven 256
adamc@142 108 ]]
adamc@142 109
adamc@142 110 We can see a constant wrapper around the object of the proof. For any even number, this form of proof will suffice. What happens if we try the tactic with an odd number? *)
adamc@142 111
adamc@142 112 Theorem even_255 : isEven 255.
adamc@142 113 (** [[
adamc@142 114
adamc@142 115 prove_even_reflective.
adamc@142 116
adamc@142 117 [[
adamc@142 118
adamc@142 119 User error: No matching clauses for match goal
adamc@142 120 ]]
adamc@142 121
adamc@142 122 Thankfully, the tactic fails. To see more precisely what goes wrong, we can run manually the body of the [match].
adamc@142 123
adamc@142 124 [[
adamc@142 125
adamc@142 126 exact (partialOut (check_even 255)).
adamc@142 127
adamc@142 128 [[
adamc@142 129
adamc@142 130 Error: The term "partialOut (check_even 255)" has type
adamc@142 131 "match check_even 255 with
adamc@142 132 | Yes => isEven 255
adamc@142 133 | No => True
adamc@142 134 end" while it is expected to have type "isEven 255"
adamc@142 135 ]]
adamc@142 136
adamc@142 137 As usual, the type-checker performs no reductions to simplify error messages. If we reduced the first term ourselves, we would see that [check_even 255] reduces to a [No], so that the first term is equivalent to [True], which certainly does not unify with [isEven 255]. *)
adamc@142 138 Abort.
adamc@143 139
adamc@143 140
adamc@143 141 (** * Reflecting the Syntax of a Trivial Tautology Language *)
adamc@143 142
adamc@143 143 (** We might also like to have reflective proofs of trivial tautologies like this one: *)
adamc@143 144
adamc@143 145 Theorem true_galore : (True /\ True) -> (True \/ (True /\ (True -> True))).
adamc@143 146 tauto.
adamc@143 147 Qed.
adamc@143 148
adamc@143 149 Print true_galore.
adamc@143 150
adamc@143 151 (** [[
adamc@143 152
adamc@143 153 true_galore =
adamc@143 154 fun H : True /\ True =>
adamc@143 155 and_ind (fun _ _ : True => or_introl (True /\ (True -> True)) I) H
adamc@143 156 : True /\ True -> True \/ True /\ (True -> True)
adamc@143 157 ]]
adamc@143 158
adamc@143 159 As we might expect, the proof that [tauto] builds contains explicit applications of natural deduction rules. For large formulas, this can add a linear amount of proof size overhead, beyond the size of the input.
adamc@143 160
adamc@143 161 To write a reflective procedure for this class of goals, we will need to get into the actual "reflection" part of "proof by reflection." It is impossible to case-analyze a [Prop] in any way in Gallina. We must %\textit{%#<i>#reflect#</i>#%}% [Prop] into some type that we %\textit{%#<i>#can#</i>#%}% analyze. This inductive type is a good candidate: *)
adamc@143 162
adamc@143 163 Inductive taut : Set :=
adamc@143 164 | TautTrue : taut
adamc@143 165 | TautAnd : taut -> taut -> taut
adamc@143 166 | TautOr : taut -> taut -> taut
adamc@143 167 | TautImp : taut -> taut -> taut.
adamc@143 168
adamc@143 169 (** We write a recursive function to "unreflect" this syntax back to [Prop]. *)
adamc@143 170
adamc@143 171 Fixpoint tautDenote (t : taut) : Prop :=
adamc@143 172 match t with
adamc@143 173 | TautTrue => True
adamc@143 174 | TautAnd t1 t2 => tautDenote t1 /\ tautDenote t2
adamc@143 175 | TautOr t1 t2 => tautDenote t1 \/ tautDenote t2
adamc@143 176 | TautImp t1 t2 => tautDenote t1 -> tautDenote t2
adamc@143 177 end.
adamc@143 178
adamc@143 179 (** It is easy to prove that every formula in the range of [tautDenote] is true. *)
adamc@143 180
adamc@143 181 Theorem tautTrue : forall t, tautDenote t.
adamc@143 182 induction t; crush.
adamc@143 183 Qed.
adamc@143 184
adamc@143 185 (** To use [tautTrue] to prove particular formulas, we need to implement the syntax reflection process. A recursive Ltac function does the job. *)
adamc@143 186
adamc@143 187 Ltac tautReflect P :=
adamc@143 188 match P with
adamc@143 189 | True => TautTrue
adamc@143 190 | ?P1 /\ ?P2 =>
adamc@143 191 let t1 := tautReflect P1 in
adamc@143 192 let t2 := tautReflect P2 in
adamc@143 193 constr:(TautAnd t1 t2)
adamc@143 194 | ?P1 \/ ?P2 =>
adamc@143 195 let t1 := tautReflect P1 in
adamc@143 196 let t2 := tautReflect P2 in
adamc@143 197 constr:(TautOr t1 t2)
adamc@143 198 | ?P1 -> ?P2 =>
adamc@143 199 let t1 := tautReflect P1 in
adamc@143 200 let t2 := tautReflect P2 in
adamc@143 201 constr:(TautImp t1 t2)
adamc@143 202 end.
adamc@143 203
adamc@143 204 (** With [tautReflect] available, it is easy to finish our reflective tactic. We look at the goal formula, reflect it, and apply [tautTrue] to the reflected formula. *)
adamc@143 205
adamc@143 206 Ltac obvious :=
adamc@143 207 match goal with
adamc@143 208 | [ |- ?P ] =>
adamc@143 209 let t := tautReflect P in
adamc@143 210 exact (tautTrue t)
adamc@143 211 end.
adamc@143 212
adamc@143 213 (** We can verify that [obvious] solves our original example, with a proof term that does not mention details of the proof. *)
adamc@143 214
adamc@143 215 Theorem true_galore' : (True /\ True) -> (True \/ (True /\ (True -> True))).
adamc@143 216 obvious.
adamc@143 217 Qed.
adamc@143 218
adamc@143 219 Print true_galore'.
adamc@143 220
adamc@143 221 (** [[
adamc@143 222
adamc@143 223 true_galore' =
adamc@143 224 tautTrue
adamc@143 225 (TautImp (TautAnd TautTrue TautTrue)
adamc@143 226 (TautOr TautTrue (TautAnd TautTrue (TautImp TautTrue TautTrue))))
adamc@143 227 : True /\ True -> True \/ True /\ (True -> True)
adamc@143 228
adamc@143 229 ]]
adamc@143 230
adamc@143 231 It is worth considering how the reflective tactic improves on a pure-Ltac implementation. The formula reflection process is just as ad-hoc as before, so we gain little there. In general, proofs will be more complicated than formula translation, and the "generic proof rule" that we apply here %\textit{%#<i>#is#</i>#%}% on much better formal footing than a recursive Ltac function. The dependent type of the proof guarantees that it "works" on any input formula. This is all in addition to the proof-size improvement that we have already seen. *)
adamc@144 232
adamc@144 233
adamc@144 234 (** * A Smarter Tautology Solver *)
adamc@144 235
adamc@144 236 Require Import Quote.
adamc@144 237
adamc@144 238 Inductive formula : Set :=
adamc@144 239 | Atomic : index -> formula
adamc@144 240 | Truth : formula
adamc@144 241 | Falsehood : formula
adamc@144 242 | And : formula -> formula -> formula
adamc@144 243 | Or : formula -> formula -> formula
adamc@144 244 | Imp : formula -> formula -> formula.
adamc@144 245
adamc@144 246 Definition asgn := varmap Prop.
adamc@144 247
adamc@144 248 Definition imp (P1 P2 : Prop) := P1 -> P2.
adamc@144 249 Infix "-->" := imp (no associativity, at level 95).
adamc@144 250
adamc@144 251 Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop :=
adamc@144 252 match f with
adamc@144 253 | Atomic v => varmap_find False v atomics
adamc@144 254 | Truth => True
adamc@144 255 | Falsehood => False
adamc@144 256 | And f1 f2 => formulaDenote atomics f1 /\ formulaDenote atomics f2
adamc@144 257 | Or f1 f2 => formulaDenote atomics f1 \/ formulaDenote atomics f2
adamc@144 258 | Imp f1 f2 => formulaDenote atomics f1 --> formulaDenote atomics f2
adamc@144 259 end.
adamc@144 260
adamc@144 261 Section my_tauto.
adamc@144 262 Variable atomics : asgn.
adamc@144 263
adamc@144 264 Definition holds (v : index) := varmap_find False v atomics.
adamc@144 265
adamc@144 266 Require Import ListSet.
adamc@144 267
adamc@144 268 Definition index_eq : forall x y : index, {x = y} + {x <> y}.
adamc@144 269 decide equality.
adamc@144 270 Defined.
adamc@144 271
adamc@144 272 Definition add (s : set index) (v : index) := set_add index_eq v s.
adamc@144 273 Definition In_dec : forall v (s : set index), {In v s} + {~In v s}.
adamc@144 274 Open Local Scope specif_scope.
adamc@144 275
adamc@144 276 intro; refine (fix F (s : set index) : {In v s} + {~In v s} :=
adamc@144 277 match s return {In v s} + {~In v s} with
adamc@144 278 | nil => No
adamc@144 279 | v' :: s' => index_eq v' v || F s'
adamc@144 280 end); crush.
adamc@144 281 Defined.
adamc@144 282
adamc@144 283 Fixpoint allTrue (s : set index) : Prop :=
adamc@144 284 match s with
adamc@144 285 | nil => True
adamc@144 286 | v :: s' => holds v /\ allTrue s'
adamc@144 287 end.
adamc@144 288
adamc@144 289 Theorem allTrue_add : forall v s,
adamc@144 290 allTrue s
adamc@144 291 -> holds v
adamc@144 292 -> allTrue (add s v).
adamc@144 293 induction s; crush;
adamc@144 294 match goal with
adamc@144 295 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@144 296 end; crush.
adamc@144 297 Qed.
adamc@144 298
adamc@144 299 Theorem allTrue_In : forall v s,
adamc@144 300 allTrue s
adamc@144 301 -> set_In v s
adamc@144 302 -> varmap_find False v atomics.
adamc@144 303 induction s; crush.
adamc@144 304 Qed.
adamc@144 305
adamc@144 306 Hint Resolve allTrue_add allTrue_In.
adamc@144 307
adamc@144 308 Open Local Scope partial_scope.
adamc@144 309
adamc@144 310 Definition forward (f : formula) (known : set index) (hyp : formula)
adamc@144 311 (cont : forall known', [allTrue known' -> formulaDenote atomics f])
adamc@144 312 : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f].
adamc@144 313 refine (fix F (f : formula) (known : set index) (hyp : formula)
adamc@144 314 (cont : forall known', [allTrue known' -> formulaDenote atomics f]){struct hyp}
adamc@144 315 : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f] :=
adamc@144 316 match hyp return [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f] with
adamc@144 317 | Atomic v => Reduce (cont (add known v))
adamc@144 318 | Truth => Reduce (cont known)
adamc@144 319 | Falsehood => Yes
adamc@144 320 | And h1 h2 =>
adamc@144 321 Reduce (F (Imp h2 f) known h1 (fun known' =>
adamc@144 322 Reduce (F f known' h2 cont)))
adamc@144 323 | Or h1 h2 => F f known h1 cont && F f known h2 cont
adamc@144 324 | Imp _ _ => Reduce (cont known)
adamc@144 325 end); crush.
adamc@144 326 Defined.
adamc@144 327
adamc@144 328 Definition backward (known : set index) (f : formula) : [allTrue known -> formulaDenote atomics f].
adamc@144 329 refine (fix F (known : set index) (f : formula) : [allTrue known -> formulaDenote atomics f] :=
adamc@144 330 match f return [allTrue known -> formulaDenote atomics f] with
adamc@144 331 | Atomic v => Reduce (In_dec v known)
adamc@144 332 | Truth => Yes
adamc@144 333 | Falsehood => No
adamc@144 334 | And f1 f2 => F known f1 && F known f2
adamc@144 335 | Or f1 f2 => F known f1 || F known f2
adamc@144 336 | Imp f1 f2 => forward f2 known f1 (fun known' => F known' f2)
adamc@144 337 end); crush; eauto.
adamc@144 338 Defined.
adamc@144 339
adamc@144 340 Definition my_tauto (f : formula) : [formulaDenote atomics f].
adamc@144 341 intro; refine (Reduce (backward nil f)); crush.
adamc@144 342 Defined.
adamc@144 343 End my_tauto.
adamc@144 344
adamc@144 345 Ltac my_tauto :=
adamc@144 346 repeat match goal with
adamc@144 347 | [ |- forall x : ?P, _ ] =>
adamc@144 348 match type of P with
adamc@144 349 | Prop => fail 1
adamc@144 350 | _ => intro
adamc@144 351 end
adamc@144 352 end;
adamc@144 353 quote formulaDenote;
adamc@144 354 match goal with
adamc@144 355 | [ |- formulaDenote ?m ?f ] => exact (partialOut (my_tauto m f))
adamc@144 356 end.
adamc@144 357
adamc@144 358 Theorem mt1 : True.
adamc@144 359 my_tauto.
adamc@144 360 Qed.
adamc@144 361
adamc@144 362 Print mt1.
adamc@144 363
adamc@144 364 Theorem mt2 : forall x y : nat, x = y --> x = y.
adamc@144 365 my_tauto.
adamc@144 366 Qed.
adamc@144 367
adamc@144 368 Print mt2.
adamc@144 369
adamc@144 370 Theorem mt3 : forall x y z,
adamc@144 371 (x < y /\ y > z) \/ (y > z /\ x < S y)
adamc@144 372 --> y > z /\ (x < y \/ x < S y).
adamc@144 373 my_tauto.
adamc@144 374 Qed.
adamc@144 375
adamc@144 376 Print mt3.
adamc@144 377
adamc@144 378 Theorem mt4 : True /\ True /\ True /\ True /\ True /\ True /\ False --> False.
adamc@144 379 my_tauto.
adamc@144 380 Qed.
adamc@144 381
adamc@144 382 Print mt4.
adamc@144 383
adamc@144 384 Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False.
adamc@144 385 tauto.
adamc@144 386 Qed.
adamc@144 387
adamc@144 388 Print mt4'.