Mercurial > cpdt > repo
comparison src/LogicProg.v @ 374:f3146d40c2a1
Prose for third LogicProg section
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Mon, 26 Mar 2012 16:24:19 -0400 |
parents | b13f76abc724 |
children | d1276004eec9 |
comparison
equal
deleted
inserted
replaced
373:b13f76abc724 | 374:f3146d40c2a1 |
---|---|
598 (** We could continue through exercises of this kind, but even more interesting than finding lists automatically is finding %\emph{%#<i>#programs#</i>#%}% automatically. *) | 598 (** We could continue through exercises of this kind, but even more interesting than finding lists automatically is finding %\emph{%#<i>#programs#</i>#%}% automatically. *) |
599 | 599 |
600 | 600 |
601 (** * Synthesizing Programs *) | 601 (** * Synthesizing Programs *) |
602 | 602 |
603 (** Here is a simple syntax type for arithmetic expressions, similar to those we have used several times before in the book. In this case, we allow expressions to mention exactly one distinguished variable. *) | |
604 | |
603 Inductive exp : Set := | 605 Inductive exp : Set := |
604 | Const : nat -> exp | 606 | Const : nat -> exp |
605 | Var : exp | 607 | Var : exp |
606 | Plus : exp -> exp -> exp. | 608 | Plus : exp -> exp -> exp. |
609 | |
610 (** An inductive relation specifies the semantics of an expression, relating a variable value and an expression to the expression value. *) | |
607 | 611 |
608 Inductive eval (var : nat) : exp -> nat -> Prop := | 612 Inductive eval (var : nat) : exp -> nat -> Prop := |
609 | EvalConst : forall n, eval var (Const n) n | 613 | EvalConst : forall n, eval var (Const n) n |
610 | EvalVar : eval var Var var | 614 | EvalVar : eval var Var var |
611 | EvalPlus : forall e1 e2 n1 n2, eval var e1 n1 | 615 | EvalPlus : forall e1 e2 n1 n2, eval var e1 n1 |
614 | 618 |
615 (* begin thide *) | 619 (* begin thide *) |
616 Hint Constructors eval. | 620 Hint Constructors eval. |
617 (* end thide *) | 621 (* end thide *) |
618 | 622 |
623 (** We can use [auto] to execute the semantics for specific expressions. *) | |
624 | |
619 Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)). | 625 Example eval1 : forall var, eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)). |
620 (* begin thide *) | 626 (* begin thide *) |
621 auto. | 627 auto. |
622 Qed. | 628 Qed. |
623 (* end thide *) | 629 (* end thide *) |
630 | |
631 (** Unfortunately, just the constructors of [eval] are not enough to prove theorems like the following, which depends on an arithmetic identity. *) | |
624 | 632 |
625 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8). | 633 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8). |
626 (* begin thide *) | 634 (* begin thide *) |
627 eauto. | 635 eauto. |
628 Abort. | 636 Abort. |
629 (* end thide *) | 637 (* end thide *) |
638 | |
639 (** To help prove [eval1'], we prove an alternate version of [EvalPlus] that inserts an extra equality premise. *) | |
630 | 640 |
631 (* begin thide *) | 641 (* begin thide *) |
632 Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1 | 642 Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1 |
633 -> eval var e2 n2 | 643 -> eval var e2 n2 |
634 -> n1 + n2 = n | 644 -> n1 + n2 = n |
636 crush. | 646 crush. |
637 Qed. | 647 Qed. |
638 | 648 |
639 Hint Resolve EvalPlus'. | 649 Hint Resolve EvalPlus'. |
640 | 650 |
651 (** Further, we instruct [eauto] to apply %\index{tactics!omega}%[omega], a standard tactic that provides a complete decision procedure for quantifier-free linear arithmetic. Via [Hint Extern], we ask for use of [omega] on any equality goal. The [abstract] tactical generates a new lemma for every such successful proof, so that, in the final proof term, the lemma may be referenced in place of dropping in the full proof of the arithmetic equality. *) | |
652 | |
641 Hint Extern 1 (_ = _) => abstract omega. | 653 Hint Extern 1 (_ = _) => abstract omega. |
642 (* end thide *) | 654 (* end thide *) |
643 | 655 |
656 (** Now we can return to [eval1'] and prove it automatically. *) | |
657 | |
644 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8). | 658 Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8). |
645 (* begin thide *) | 659 (* begin thide *) |
646 eauto. | 660 eauto. |
647 Qed. | 661 Qed. |
648 (* end thide *) | 662 (* end thide *) |
649 | 663 |
650 Print eval1'. | 664 Print eval1'. |
665 (** %\vspace{-.15in}%[[ | |
666 eval1' = | |
667 fun var : nat => | |
668 EvalPlus' (EvalVar var) (EvalPlus (EvalConst var 8) (EvalVar var)) | |
669 (eval1'_subproof var) | |
670 : forall var : nat, | |
671 eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8) | |
672 ]] | |
673 *) | |
674 | |
675 (** The lemma [eval1'_subproof] was generated by [abstract omega]. | |
676 | |
677 Now we are ready to take advantage of logic programming's flexibility by searching for a program (arithmetic expression) that always evaluates to a particular symbolic value. *) | |
651 | 678 |
652 Example synthesize1 : exists e, forall var, eval var e (var + 7). | 679 Example synthesize1 : exists e, forall var, eval var e (var + 7). |
653 (* begin thide *) | 680 (* begin thide *) |
654 eauto. | 681 eauto. |
655 Qed. | 682 Qed. |
656 (* end thide *) | 683 (* end thide *) |
657 | 684 |
658 Print synthesize1. | 685 Print synthesize1. |
686 (** %\vspace{-.15in}%[[ | |
687 synthesize1 = | |
688 ex_intro (fun e : exp => forall var : nat, eval var e (var + 7)) | |
689 (Plus Var (Const 7)) | |
690 (fun var : nat => EvalPlus (EvalVar var) (EvalConst var 7)) | |
691 ]] | |
692 *) | |
693 | |
694 (** Here are two more examples showing off our program synthesis abilities. *) | |
659 | 695 |
660 Example synthesize2 : exists e, forall var, eval var e (2 * var + 8). | 696 Example synthesize2 : exists e, forall var, eval var e (2 * var + 8). |
661 (* begin thide *) | 697 (* begin thide *) |
662 eauto. | 698 eauto. |
663 Qed. | 699 Qed. |
664 (* end thide *) | 700 (* end thide *) |
665 | 701 |
702 (* begin hide *) | |
666 Print synthesize2. | 703 Print synthesize2. |
704 (* end hide *) | |
667 | 705 |
668 Example synthesize3 : exists e, forall var, eval var e (3 * var + 42). | 706 Example synthesize3 : exists e, forall var, eval var e (3 * var + 42). |
669 (* begin thide *) | 707 (* begin thide *) |
670 eauto. | 708 eauto. |
671 Qed. | 709 Qed. |
672 (* end thide *) | 710 (* end thide *) |
673 | 711 |
712 (* begin hide *) | |
674 Print synthesize3. | 713 Print synthesize3. |
714 (* end hide *) | |
715 | |
716 (** These examples show linear expressions over the variable [var]. Any such expression is equivalent to [k * var + n] for some [k] and [n]. It is probably not so surprising that we can prove that any expression's semantics is equivalent to some such linear expression, but it is tedious to prove such a fact manually. To finish this section, we will use [eauto] to complete the proof, finding [k] and [n] values automatically. | |
717 | |
718 We prove a series of lemmas and add them as hints. We have alternate [eval] constructor lemmas and some facts about arithmetic. *) | |
675 | 719 |
676 (* begin thide *) | 720 (* begin thide *) |
677 Theorem EvalConst' : forall var n m, n = m | 721 Theorem EvalConst' : forall var n m, n = m |
678 -> eval var (Const n) m. | 722 -> eval var (Const n) m. |
679 crush. | 723 crush. |
707 crush. | 751 crush. |
708 Qed. | 752 Qed. |
709 | 753 |
710 Hint Resolve plus_0 times_1. | 754 Hint Resolve plus_0 times_1. |
711 | 755 |
756 (** We finish with one more arithmetic lemma that is particularly specialized to this theorem. This fact happens to follow by the axioms of the %\emph{%#<i>#ring#</i>#%}% algebraic structure, so, since the naturals form a ring, we can use the built-in tactic %\index{tactics!ring}%[ring]. *) | |
757 | |
712 Require Import Arith Ring. | 758 Require Import Arith Ring. |
713 | 759 |
714 Theorem combine : forall x k1 k2 n1 n2, | 760 Theorem combine : forall x k1 k2 n1 n2, |
715 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2). | 761 (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2). |
716 intros; ring. | 762 intros; ring. |
717 Qed. | 763 Qed. |
718 | 764 |
719 Hint Resolve combine. | 765 Hint Resolve combine. |
720 | 766 |
767 (** Our choice of hints is cheating, to an extent, by telegraphing the procedure for choosing values of [k] and [n]. Nonetheless, with these lemmas in place, we achieve an automated proof without explicitly orchestrating the lemmas' composition. *) | |
768 | |
721 Theorem linear : forall e, exists k, exists n, | 769 Theorem linear : forall e, exists k, exists n, |
722 forall var, eval var e (k * var + n). | 770 forall var, eval var e (k * var + n). |
723 induction e; crush; eauto. | 771 induction e; crush; eauto. |
724 Qed. | 772 Qed. |
725 | 773 |
774 (* begin hide *) | |
726 Print linear. | 775 Print linear. |
727 (* end thide *) | 776 (* end hide *) |
777 (* end thide *) | |
778 | |
779 (** By printing the proof term, it is possible to see the procedure that is used to choose the constants for each input term. *) | |
728 | 780 |
729 | 781 |
730 (** * More on [auto] Hints *) | 782 (** * More on [auto] Hints *) |
731 | 783 |
732 (** Another class of built-in tactics includes [auto], [eauto], and [autorewrite]. These are based on %\textit{%#<i>#hint databases#</i>#%}%, which we have seen extended in many examples so far. These tactics are important, because, in Ltac programming, we cannot create %``%#"#global variables#"#%''% whose values can be extended seamlessly by different modules in different source files. We have seen the advantages of hints so far, where [crush] can be defined once and for all, while still automatically applying the hints we add throughout developments. | 784 (** Another class of built-in tactics includes [auto], [eauto], and [autorewrite]. These are based on %\textit{%#<i>#hint databases#</i>#%}%, which we have seen extended in many examples so far. These tactics are important, because, in Ltac programming, we cannot create %``%#"#global variables#"#%''% whose values can be extended seamlessly by different modules in different source files. We have seen the advantages of hints so far, where [crush] can be defined once and for all, while still automatically applying the hints we add throughout developments. |