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@145
|
234 (** * A Monoid Expression Simplifier *)
|
adamc@145
|
235
|
adamc@145
|
236 Section monoid.
|
adamc@145
|
237 Variable A : Set.
|
adamc@145
|
238 Variable e : A.
|
adamc@145
|
239 Variable f : A -> A -> A.
|
adamc@145
|
240
|
adamc@145
|
241 Infix "+" := f.
|
adamc@145
|
242
|
adamc@145
|
243 Hypothesis assoc : forall a b c, (a + b) + c = a + (b + c).
|
adamc@145
|
244 Hypothesis identl : forall a, e + a = a.
|
adamc@145
|
245 Hypothesis identr : forall a, a + e = a.
|
adamc@145
|
246
|
adamc@145
|
247 Inductive mexp : Set :=
|
adamc@145
|
248 | Ident : mexp
|
adamc@145
|
249 | Var : A -> mexp
|
adamc@145
|
250 | Op : mexp -> mexp -> mexp.
|
adamc@145
|
251
|
adamc@145
|
252 Fixpoint mdenote (me : mexp) : A :=
|
adamc@145
|
253 match me with
|
adamc@145
|
254 | Ident => e
|
adamc@145
|
255 | Var v => v
|
adamc@145
|
256 | Op me1 me2 => mdenote me1 + mdenote me2
|
adamc@145
|
257 end.
|
adamc@145
|
258
|
adamc@145
|
259 Fixpoint mldenote (ls : list A) : A :=
|
adamc@145
|
260 match ls with
|
adamc@145
|
261 | nil => e
|
adamc@145
|
262 | x :: ls' => x + mldenote ls'
|
adamc@145
|
263 end.
|
adamc@145
|
264
|
adamc@145
|
265 Fixpoint flatten (me : mexp) : list A :=
|
adamc@145
|
266 match me with
|
adamc@145
|
267 | Ident => nil
|
adamc@145
|
268 | Var x => x :: nil
|
adamc@145
|
269 | Op me1 me2 => flatten me1 ++ flatten me2
|
adamc@145
|
270 end.
|
adamc@145
|
271
|
adamc@145
|
272 Lemma flatten_correct' : forall ml2 ml1, f (mldenote ml1) (mldenote ml2) = mldenote (ml1 ++ ml2).
|
adamc@145
|
273 induction ml1; crush.
|
adamc@145
|
274 Qed.
|
adamc@145
|
275
|
adamc@145
|
276 Theorem flatten_correct : forall me, mdenote me = mldenote (flatten me).
|
adamc@145
|
277 Hint Resolve flatten_correct'.
|
adamc@145
|
278
|
adamc@145
|
279 induction me; crush.
|
adamc@145
|
280 Qed.
|
adamc@145
|
281
|
adamc@145
|
282 Theorem monoid_reflect : forall m1 m2,
|
adamc@145
|
283 mldenote (flatten m1) = mldenote (flatten m2)
|
adamc@145
|
284 -> mdenote m1 = mdenote m2.
|
adamc@145
|
285 intros; repeat rewrite flatten_correct; assumption.
|
adamc@145
|
286 Qed.
|
adamc@145
|
287
|
adamc@145
|
288 Ltac reflect m :=
|
adamc@145
|
289 match m with
|
adamc@145
|
290 | e => Ident
|
adamc@145
|
291 | ?m1 + ?m2 =>
|
adamc@145
|
292 let r1 := reflect m1 in
|
adamc@145
|
293 let r2 := reflect m2 in
|
adamc@145
|
294 constr:(Op r1 r2)
|
adamc@145
|
295 | _ => constr:(Var m)
|
adamc@145
|
296 end.
|
adamc@145
|
297
|
adamc@145
|
298 Ltac monoid :=
|
adamc@145
|
299 match goal with
|
adamc@145
|
300 | [ |- ?m1 = ?m2 ] =>
|
adamc@145
|
301 let r1 := reflect m1 in
|
adamc@145
|
302 let r2 := reflect m2 in
|
adamc@145
|
303 change (mdenote r1 = mdenote r2);
|
adamc@145
|
304 apply monoid_reflect; simpl mldenote
|
adamc@145
|
305 end.
|
adamc@145
|
306
|
adamc@145
|
307 Theorem t1 : forall a b c d, a + b + c + d = a + (b + c) + d.
|
adamc@145
|
308 intros.
|
adamc@145
|
309 monoid.
|
adamc@145
|
310 reflexivity.
|
adamc@145
|
311 Qed.
|
adamc@145
|
312 End monoid.
|
adamc@145
|
313
|
adamc@145
|
314
|
adamc@144
|
315 (** * A Smarter Tautology Solver *)
|
adamc@144
|
316
|
adamc@144
|
317 Require Import Quote.
|
adamc@144
|
318
|
adamc@144
|
319 Inductive formula : Set :=
|
adamc@144
|
320 | Atomic : index -> formula
|
adamc@144
|
321 | Truth : formula
|
adamc@144
|
322 | Falsehood : formula
|
adamc@144
|
323 | And : formula -> formula -> formula
|
adamc@144
|
324 | Or : formula -> formula -> formula
|
adamc@144
|
325 | Imp : formula -> formula -> formula.
|
adamc@144
|
326
|
adamc@144
|
327 Definition asgn := varmap Prop.
|
adamc@144
|
328
|
adamc@144
|
329 Definition imp (P1 P2 : Prop) := P1 -> P2.
|
adamc@144
|
330 Infix "-->" := imp (no associativity, at level 95).
|
adamc@144
|
331
|
adamc@144
|
332 Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop :=
|
adamc@144
|
333 match f with
|
adamc@144
|
334 | Atomic v => varmap_find False v atomics
|
adamc@144
|
335 | Truth => True
|
adamc@144
|
336 | Falsehood => False
|
adamc@144
|
337 | And f1 f2 => formulaDenote atomics f1 /\ formulaDenote atomics f2
|
adamc@144
|
338 | Or f1 f2 => formulaDenote atomics f1 \/ formulaDenote atomics f2
|
adamc@144
|
339 | Imp f1 f2 => formulaDenote atomics f1 --> formulaDenote atomics f2
|
adamc@144
|
340 end.
|
adamc@144
|
341
|
adamc@144
|
342 Section my_tauto.
|
adamc@144
|
343 Variable atomics : asgn.
|
adamc@144
|
344
|
adamc@144
|
345 Definition holds (v : index) := varmap_find False v atomics.
|
adamc@144
|
346
|
adamc@144
|
347 Require Import ListSet.
|
adamc@144
|
348
|
adamc@144
|
349 Definition index_eq : forall x y : index, {x = y} + {x <> y}.
|
adamc@144
|
350 decide equality.
|
adamc@144
|
351 Defined.
|
adamc@144
|
352
|
adamc@144
|
353 Definition add (s : set index) (v : index) := set_add index_eq v s.
|
adamc@144
|
354 Definition In_dec : forall v (s : set index), {In v s} + {~In v s}.
|
adamc@144
|
355 Open Local Scope specif_scope.
|
adamc@144
|
356
|
adamc@144
|
357 intro; refine (fix F (s : set index) : {In v s} + {~In v s} :=
|
adamc@144
|
358 match s return {In v s} + {~In v s} with
|
adamc@144
|
359 | nil => No
|
adamc@144
|
360 | v' :: s' => index_eq v' v || F s'
|
adamc@144
|
361 end); crush.
|
adamc@144
|
362 Defined.
|
adamc@144
|
363
|
adamc@144
|
364 Fixpoint allTrue (s : set index) : Prop :=
|
adamc@144
|
365 match s with
|
adamc@144
|
366 | nil => True
|
adamc@144
|
367 | v :: s' => holds v /\ allTrue s'
|
adamc@144
|
368 end.
|
adamc@144
|
369
|
adamc@144
|
370 Theorem allTrue_add : forall v s,
|
adamc@144
|
371 allTrue s
|
adamc@144
|
372 -> holds v
|
adamc@144
|
373 -> allTrue (add s v).
|
adamc@144
|
374 induction s; crush;
|
adamc@144
|
375 match goal with
|
adamc@144
|
376 | [ |- context[if ?E then _ else _] ] => destruct E
|
adamc@144
|
377 end; crush.
|
adamc@144
|
378 Qed.
|
adamc@144
|
379
|
adamc@144
|
380 Theorem allTrue_In : forall v s,
|
adamc@144
|
381 allTrue s
|
adamc@144
|
382 -> set_In v s
|
adamc@144
|
383 -> varmap_find False v atomics.
|
adamc@144
|
384 induction s; crush.
|
adamc@144
|
385 Qed.
|
adamc@144
|
386
|
adamc@144
|
387 Hint Resolve allTrue_add allTrue_In.
|
adamc@144
|
388
|
adamc@144
|
389 Open Local Scope partial_scope.
|
adamc@144
|
390
|
adamc@144
|
391 Definition forward (f : formula) (known : set index) (hyp : formula)
|
adamc@144
|
392 (cont : forall known', [allTrue known' -> formulaDenote atomics f])
|
adamc@144
|
393 : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f].
|
adamc@144
|
394 refine (fix F (f : formula) (known : set index) (hyp : formula)
|
adamc@144
|
395 (cont : forall known', [allTrue known' -> formulaDenote atomics f]){struct hyp}
|
adamc@144
|
396 : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f] :=
|
adamc@144
|
397 match hyp return [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f] with
|
adamc@144
|
398 | Atomic v => Reduce (cont (add known v))
|
adamc@144
|
399 | Truth => Reduce (cont known)
|
adamc@144
|
400 | Falsehood => Yes
|
adamc@144
|
401 | And h1 h2 =>
|
adamc@144
|
402 Reduce (F (Imp h2 f) known h1 (fun known' =>
|
adamc@144
|
403 Reduce (F f known' h2 cont)))
|
adamc@144
|
404 | Or h1 h2 => F f known h1 cont && F f known h2 cont
|
adamc@144
|
405 | Imp _ _ => Reduce (cont known)
|
adamc@144
|
406 end); crush.
|
adamc@144
|
407 Defined.
|
adamc@144
|
408
|
adamc@144
|
409 Definition backward (known : set index) (f : formula) : [allTrue known -> formulaDenote atomics f].
|
adamc@144
|
410 refine (fix F (known : set index) (f : formula) : [allTrue known -> formulaDenote atomics f] :=
|
adamc@144
|
411 match f return [allTrue known -> formulaDenote atomics f] with
|
adamc@144
|
412 | Atomic v => Reduce (In_dec v known)
|
adamc@144
|
413 | Truth => Yes
|
adamc@144
|
414 | Falsehood => No
|
adamc@144
|
415 | And f1 f2 => F known f1 && F known f2
|
adamc@144
|
416 | Or f1 f2 => F known f1 || F known f2
|
adamc@144
|
417 | Imp f1 f2 => forward f2 known f1 (fun known' => F known' f2)
|
adamc@144
|
418 end); crush; eauto.
|
adamc@144
|
419 Defined.
|
adamc@144
|
420
|
adamc@144
|
421 Definition my_tauto (f : formula) : [formulaDenote atomics f].
|
adamc@144
|
422 intro; refine (Reduce (backward nil f)); crush.
|
adamc@144
|
423 Defined.
|
adamc@144
|
424 End my_tauto.
|
adamc@144
|
425
|
adamc@144
|
426 Ltac my_tauto :=
|
adamc@144
|
427 repeat match goal with
|
adamc@144
|
428 | [ |- forall x : ?P, _ ] =>
|
adamc@144
|
429 match type of P with
|
adamc@144
|
430 | Prop => fail 1
|
adamc@144
|
431 | _ => intro
|
adamc@144
|
432 end
|
adamc@144
|
433 end;
|
adamc@144
|
434 quote formulaDenote;
|
adamc@144
|
435 match goal with
|
adamc@144
|
436 | [ |- formulaDenote ?m ?f ] => exact (partialOut (my_tauto m f))
|
adamc@144
|
437 end.
|
adamc@144
|
438
|
adamc@144
|
439 Theorem mt1 : True.
|
adamc@144
|
440 my_tauto.
|
adamc@144
|
441 Qed.
|
adamc@144
|
442
|
adamc@144
|
443 Print mt1.
|
adamc@144
|
444
|
adamc@144
|
445 Theorem mt2 : forall x y : nat, x = y --> x = y.
|
adamc@144
|
446 my_tauto.
|
adamc@144
|
447 Qed.
|
adamc@144
|
448
|
adamc@144
|
449 Print mt2.
|
adamc@144
|
450
|
adamc@144
|
451 Theorem mt3 : forall x y z,
|
adamc@144
|
452 (x < y /\ y > z) \/ (y > z /\ x < S y)
|
adamc@144
|
453 --> y > z /\ (x < y \/ x < S y).
|
adamc@144
|
454 my_tauto.
|
adamc@144
|
455 Qed.
|
adamc@144
|
456
|
adamc@144
|
457 Print mt3.
|
adamc@144
|
458
|
adamc@144
|
459 Theorem mt4 : True /\ True /\ True /\ True /\ True /\ True /\ False --> False.
|
adamc@144
|
460 my_tauto.
|
adamc@144
|
461 Qed.
|
adamc@144
|
462
|
adamc@144
|
463 Print mt4.
|
adamc@144
|
464
|
adamc@144
|
465 Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False.
|
adamc@144
|
466 tauto.
|
adamc@144
|
467 Qed.
|
adamc@144
|
468
|
adamc@144
|
469 Print mt4'.
|