Mercurial > cpdt > repo

comparison src/Predicates.v @ 46:29058fd5448b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
[tauto] and [intuition]
author Adam Chlipala <adamc@hcoop.net>
date Sat, 27 Sep 2008 15:13:01 -0400
parents cb135b19adb8
children be4efaee371f
comparison
equal deleted inserted replaced
45:cb135b19adb8 46:29058fd5448b
44 (** * Propositional logic *) 44 (** * Propositional logic *)
45 45
46 (** Let us begin with a brief tour through the definitions of the connectives for propositional logic. We will work within a Coq section that provides us with a set of propositional variables. In Coq parlance, these are just terms of type [Prop.] *) 46 (** Let us begin with a brief tour through the definitions of the connectives for propositional logic. We will work within a Coq section that provides us with a set of propositional variables. In Coq parlance, these are just terms of type [Prop.] *)
47 47
48 Section Propositional. 48 Section Propositional.
49 Variables P Q : Prop. 49 Variables P Q R : Prop.
50 50
51 (** In Coq, the most basic propositional connective is implication, written [->], which we have already used in almost every proof. Rather than being defined inductively, implication is built into Coq as the function type constructor. 51 (** In Coq, the most basic propositional connective is implication, written [->], which we have already used in almost every proof. Rather than being defined inductively, implication is built into Coq as the function type constructor.
52 52
53 We have also already seen the definition of [True]. For a demonstration of a lower-level way of establishing proofs of inductive predicates, we turn to this trivial theorem. *) 53 We have also already seen the definition of [True]. For a demonstration of a lower-level way of establishing proofs of inductive predicates, we turn to this trivial theorem. *)
54 54
204 ]] *) 204 ]] *)
205 205
206 left; assumption. 206 left; assumption.
207 Qed. 207 Qed.
208 208
209
210 (* begin hide *)
211 (* In-class exercises *)
212
213 Theorem contra : P -> ~P -> R.
214 Admitted.
215
216 Theorem and_assoc : (P /\ Q) /\ R -> P /\ (Q /\ R).
217 Admitted.
218
219 Theorem or_assoc : (P \/ Q) \/ R -> P \/ (Q \/ R).
220 Admitted.
221
222 (* end hide *)
223
224
225 (** It would be a shame to have to plod manually through all proofs about propositional logic. Luckily, there is no need. One of the most basic Coq automation tactics is [tauto], which is a complete decision procedure for constructive propositional logic. (More on what "constructive" means in the next section.) We can use [tauto] to dispatch all of the purely propositional theorems we have proved so far. *)
226
227 Theorem or_comm' : P \/ Q -> Q \/ P.
228 tauto.
229 Qed.
230
231 (** Sometimes propositional reasoning forms important plumbing for the proof of a theorem, but we still need to apply some other smarts about, say, arithmetic. [intuition] is a generalization of [tauto] that proves everything it can using propositional reasoning. When some goals remain, it uses propositional laws to simplify them as far as possible. Consider this example, which uses the list concatenation operator [++] from the standard library. *)
232
233 Theorem arith_comm : forall ls1 ls2 : list nat,
234 length ls1 = length ls2 \/ length ls1 + length ls2 = 6
235 -> length (ls1 ++ ls2) = 6 \/ length ls1 = length ls2.
236 intuition.
237
238 (** A lot of the proof structure has been generated for us by [intuition], but the final proof depends on a fact about lists. The remaining subgoal hints at what cleverness we need to inject. *)
239
240 (** [[
241
242 ls1 : list nat
243 ls2 : list nat
244 H0 : length ls1 + length ls2 = 6
245 ============================
246 length (ls1 ++ ls2) = 6 \/ length ls1 = length ls2
247 ]] *)
248
249 (** We can see that we need a theorem about lengths of concatenated lists, which we proved last chapter and is also in the standard library. *)
250
251 rewrite app_length.
252 (** [[
253
254 ls1 : list nat
255 ls2 : list nat
256 H0 : length ls1 + length ls2 = 6
257 ============================
258 length ls1 + length ls2 = 6 \/ length ls1 = length ls2
259 ]] *)
260
261 (** Now the subgoal follows by purely propositional reasoning. That is, we could replace [length ls1 + length ls2 = 6] with [P] and [length ls1 = length ls2] with [Q] and arrive at a tautology of propositional logic. *)
262
263 tauto.
264 Qed.
265
266 (** [intuition] is one of the main bits of glue in the implementation of [crush], so, with a little help, we can get a short automated proof of the theorem. *)
267
268 Theorem arith_comm' : forall ls1 ls2 : list nat,
269 length ls1 = length ls2 \/ length ls1 + length ls2 = 6
270 -> length (ls1 ++ ls2) = 6 \/ length ls1 = length ls2.
271 Hint Rewrite app_length : cpdt.
272
273 crush.
274 Qed.
275
209 End Propositional. 276 End Propositional.
210 277
278
279
280