Mercurial > cpdt > repo
comparison src/Match.v @ 139:a9e90bacbd16
inster example
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 26 Oct 2008 17:10:20 -0400 |
| parents | 59a2110acf64 |
| children | 8cce3247496b |
comparison
equal
deleted
inserted
replaced
| 138:59a2110acf64 | 139:a9e90bacbd16 |
|---|---|
| 544 False | 544 False |
| 545 ]] *) | 545 ]] *) |
| 546 Abort. | 546 Abort. |
| 547 | 547 |
| 548 | 548 |
| 549 (** * Proof Search in Continuation-Passing Style *) | 549 (** * Recursive Proof Search *) |
| 550 | |
| 551 (** Deciding how to instantiate quantifiers is one of the hardest parts of automated first-order theorem proving. For a given problem, we can consider all possible bounded-length sequences of quantifier instantiations, applying only propositional reasoning at the end. This is probably a bad idea for almost all goals, but it makes for a nice example of recursive proof search procedures in Ltac. | |
| 552 | |
| 553 We can consider the maximum "dependency chain" length for a first-order proof. We define the chain length for a hypothesis to be 0, and the chain length for an instantiation of a quantified fact to be one greater than the length for that fact. The tactic [inster n] is meant to try all possible proofs with chain length at most [n]. *) | |
| 554 | |
| 555 Ltac inster n := | |
| 556 intuition; | |
| 557 match n with | |
| 558 | S ?n' => | |
| 559 match goal with | |
| 560 | [ H : forall x : ?T, _, x : ?T |- _ ] => generalize (H x); inster n' | |
| 561 end | |
| 562 end. | |
| 563 | |
| 564 (** [inster] begins by applying propositional simplification. Next, it checks if any chain length remains. If so, it tries all possible ways of instantiating quantified hypotheses with properly-typed local variables. It is critical to realize that, if the recursive call [inster n'] fails, then the [match goal] just seeks out another way of unifying its pattern against proof state. Thus, this small amount of code provides an elegant demonstration of how backtracking [match] enables exhaustive search. | |
| 565 | |
| 566 We can verify the efficacy of [inster] with two short examples. The built-in [firstorder] tactic (with no extra arguments) is able to prove the first but not the second. *) | |
| 567 | |
| 568 Section test_inster. | |
| 569 Variable A : Set. | |
| 570 Variables P Q : A -> Prop. | |
| 571 Variable f : A -> A. | |
| 572 Variable g : A -> A -> A. | |
| 573 | |
| 574 Hypothesis H1 : forall x y, P (g x y) -> Q (f x). | |
| 575 | |
| 576 Theorem test_inster : forall x y, P (g x y) -> Q (f x). | |
| 577 intros; inster 2. | |
| 578 Qed. | |
| 579 | |
| 580 Hypothesis H3 : forall u v, P u /\ P v /\ u <> v -> P (g u v). | |
| 581 Hypothesis H4 : forall u, Q (f u) -> P u /\ P (f u). | |
| 582 | |
| 583 Theorem test_inster2 : forall x y, x <> y -> P x -> Q (f y) -> Q (f x). | |
| 584 intros; inster 3. | |
| 585 Qed. | |
| 586 End test_inster. | |
| 587 | |
| 550 | 588 |
| 551 Definition imp (P1 P2 : Prop) := P1 -> P2. | 589 Definition imp (P1 P2 : Prop) := P1 -> P2. |
| 552 | 590 |
| 553 Infix "-->" := imp (no associativity, at level 95). | 591 Infix "-->" := imp (no associativity, at level 95). |
| 554 | 592 |