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),