## Mercurial > cpdt > repo

### comparison src/Match.v @ 488:31258618ef73

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

Incorporate feedback from Nathan Collins

author | Adam Chlipala <adam@chlipala.net> |
---|---|

date | Tue, 08 Jan 2013 14:38:56 -0500 |

parents | 5025a401ad9e |

children | 49f3b2d70302 |

comparison

equal
deleted
inserted
replaced

487:8bfb27cf0121 | 488:31258618ef73 |
---|---|

580 (P --> Q /\ True) | 580 (P --> Q /\ True) |

581 -> (P --> Q). | 581 -> (P --> Q). |

582 imp. | 582 imp. |

583 Qed. | 583 Qed. |

584 | 584 |

585 Theorem assoc_prem1 : forall P Q R S, | 585 Theorem pick_prem1 : forall P Q R S, |

586 (P /\ (Q /\ R) --> S) | 586 (P /\ (Q /\ R) --> S) |

587 -> ((P /\ Q) /\ R --> S). | 587 -> ((P /\ Q) /\ R --> S). |

588 imp. | 588 imp. |

589 Qed. | 589 Qed. |

590 | 590 |

591 Theorem assoc_prem2 : forall P Q R S, | 591 Theorem pick_prem2 : forall P Q R S, |

592 (Q /\ (P /\ R) --> S) | 592 (Q /\ (P /\ R) --> S) |

593 -> ((P /\ Q) /\ R --> S). | 593 -> ((P /\ Q) /\ R --> S). |

594 imp. | 594 imp. |

595 Qed. | 595 Qed. |

596 | 596 |

598 (P /\ Q --> R) | 598 (P /\ Q --> R) |

599 -> (Q /\ P --> R). | 599 -> (Q /\ P --> R). |

600 imp. | 600 imp. |

601 Qed. | 601 Qed. |

602 | 602 |

603 Theorem assoc_conc1 : forall P Q R S, | 603 Theorem pick_conc1 : forall P Q R S, |

604 (S --> P /\ (Q /\ R)) | 604 (S --> P /\ (Q /\ R)) |

605 -> (S --> (P /\ Q) /\ R). | 605 -> (S --> (P /\ Q) /\ R). |

606 imp. | 606 imp. |

607 Qed. | 607 Qed. |

608 | 608 |

609 Theorem assoc_conc2 : forall P Q R S, | 609 Theorem pick_conc2 : forall P Q R S, |

610 (S --> Q /\ (P /\ R)) | 610 (S --> Q /\ (P /\ R)) |

611 -> (S --> (P /\ Q) /\ R). | 611 -> (S --> (P /\ Q) /\ R). |

612 imp. | 612 imp. |

613 Qed. | 613 Qed. |

614 | 614 |

624 let rec search P := | 624 let rec search P := |

625 tac | 625 tac |

626 || (apply and_True_prem; tac) | 626 || (apply and_True_prem; tac) |

627 || match P with | 627 || match P with |

628 | ?P1 /\ ?P2 => | 628 | ?P1 /\ ?P2 => |

629 (apply assoc_prem1; search P1) | 629 (apply pick_prem1; search P1) |

630 || (apply assoc_prem2; search P2) | 630 || (apply pick_prem2; search P2) |

631 end | 631 end |

632 in match goal with | 632 in match goal with |

633 | [ |- ?P /\ _ --> _ ] => search P | 633 | [ |- ?P /\ _ --> _ ] => search P |

634 | [ |- _ /\ ?P --> _ ] => apply comm_prem; search P | 634 | [ |- _ /\ ?P --> _ ] => apply comm_prem; search P |

635 | [ |- _ --> _ ] => progress (tac || (apply and_True_prem; tac)) | 635 | [ |- _ --> _ ] => progress (tac || (apply and_True_prem; tac)) |

636 end. | 636 end. |

637 | 637 |

638 (** To understand how [search_prem] works, we turn first to the final [match]. If the premise begins with a conjunction, we call the [search] procedure on each of the conjuncts, or only the first conjunct, if that already yields a case where [tac] does not fail. The call [search P] expects and maintains the invariant that the premise is of the form [P /\ Q] for some [Q]. We pass [P] explicitly as a kind of decreasing induction measure, to avoid looping forever when [tac] always fails. The second [match] case calls a commutativity lemma to realize this invariant, before passing control to [search]. The final [match] case tries applying [tac] directly and then, if that fails, changes the form of the goal by adding an extraneous [True] conjunct and calls [tac] again. The %\index{tactics!progress}%[progress] tactical fails when its argument tactic succeeds without changing the current subgoal. | 638 (** To understand how [search_prem] works, we turn first to the final [match]. If the premise begins with a conjunction, we call the [search] procedure on each of the conjuncts, or only the first conjunct, if that already yields a case where [tac] does not fail. The call [search P] expects and maintains the invariant that the premise is of the form [P /\ Q] for some [Q]. We pass [P] explicitly as a kind of decreasing induction measure, to avoid looping forever when [tac] always fails. The second [match] case calls a commutativity lemma to realize this invariant, before passing control to [search]. The final [match] case tries applying [tac] directly and then, if that fails, changes the form of the goal by adding an extraneous [True] conjunct and calls [tac] again. The %\index{tactics!progress}%[progress] tactical fails when its argument tactic succeeds without changing the current subgoal. |

639 | 639 |

640 The [search] function itself tries the same tricks as in the last case of the final [match]. Additionally, if neither works, it checks if [P] is a conjunction. If so, it calls itself recursively on each conjunct, first applying associativity lemmas to maintain the goal-form invariant. | 640 The [search] function itself tries the same tricks as in the last case of the final [match], using the [||] operator as a shorthand for trying one tactic and then, if the first fails, trying another. Additionally, if neither works, it checks if [P] is a conjunction. If so, it calls itself recursively on each conjunct, first applying associativity lemmas to maintain the goal-form invariant. |

641 | 641 |

642 We will also want a dual function [search_conc], which does tree search through an [imp] conclusion. *) | 642 We will also want a dual function [search_conc], which does tree search through an [imp] conclusion. *) |

643 | 643 |

644 Ltac search_conc tac := | 644 Ltac search_conc tac := |

645 let rec search P := | 645 let rec search P := |

646 tac | 646 tac |

647 || (apply and_True_conc; tac) | 647 || (apply and_True_conc; tac) |

648 || match P with | 648 || match P with |

649 | ?P1 /\ ?P2 => | 649 | ?P1 /\ ?P2 => |

650 (apply assoc_conc1; search P1) | 650 (apply pick_conc1; search P1) |

651 || (apply assoc_conc2; search P2) | 651 || (apply pick_conc2; search P2) |

652 end | 652 end |

653 in match goal with | 653 in match goal with |

654 | [ |- _ --> ?P /\ _ ] => search P | 654 | [ |- _ --> ?P /\ _ ] => search P |

655 | [ |- _ --> _ /\ ?P ] => apply comm_conc; search P | 655 | [ |- _ --> _ /\ ?P ] => apply comm_conc; search P |

656 | [ |- _ --> _ ] => progress (tac || (apply and_True_conc; tac)) | 656 | [ |- _ --> _ ] => progress (tac || (apply and_True_conc; tac)) |

716 | 716 |

717 Print t2. | 717 Print t2. |

718 (** %\vspace{-.15in}% [[ | 718 (** %\vspace{-.15in}% [[ |

719 t2 = | 719 t2 = |

720 fun P Q : Prop => | 720 fun P Q : Prop => |

721 comm_prem (assoc_prem1 (assoc_prem2 (False_prem (P:=P /\ P /\ Q) (P /\ Q)))) | 721 comm_prem (pick_prem1 (pick_prem2 (False_prem (P:=P /\ P /\ Q) (P /\ Q)))) |

722 : forall P Q : Prop, Q /\ (P /\ False) /\ P --> P /\ Q | 722 : forall P Q : Prop, Q /\ (P /\ False) /\ P --> P /\ Q |

723 ]] | 723 ]] |

724 | 724 |

725 %\smallskip{}%We can also see that [matcher] is well-suited for cases where some human intervention is needed after the automation finishes. *) | 725 %\smallskip{}%We can also see that [matcher] is well-suited for cases where some human intervention is needed after the automation finishes. *) |

726 | 726 |

748 t4 = | 748 t4 = |

749 fun (P : nat -> Prop) (Q : Prop) => | 749 fun (P : nat -> Prop) (Q : Prop) => |

750 and_True_prem | 750 and_True_prem |

751 (ex_prem (P:=fun x : nat => P x /\ Q) | 751 (ex_prem (P:=fun x : nat => P x /\ Q) |

752 (fun x : nat => | 752 (fun x : nat => |

753 assoc_prem2 | 753 pick_prem2 |

754 (Match (P:=Q) | 754 (Match (P:=Q) |

755 (and_True_conc | 755 (and_True_conc |

756 (ex_conc (fun x0 : nat => P x0) x | 756 (ex_conc (fun x0 : nat => P x0) x |

757 (Match (P:=P x) (imp_True (P:=True)))))))) | 757 (Match (P:=P x) (imp_True (P:=True)))))))) |

758 : forall (P : nat -> Prop) (Q : Prop), | 758 : forall (P : nat -> Prop) (Q : Prop), |