Mercurial > cpdt > repo

comparison src/LogicProg.v @ 484:5025a401ad9e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Last round of feedback from class at Penn
author Adam Chlipala <adam@chlipala.net>
date Sun, 06 Jan 2013 16:23:26 -0500
parents 1fd4109f7b31
children 05c0f872a129
comparison
equal deleted inserted replaced
483:582cf453878e 484:5025a401ad9e
318 Section slow. 318 Section slow.
319 Hint Resolve eq_trans. 319 Hint Resolve eq_trans.
320 320
321 (** The following fact is false, but that does not stop [eauto] from taking a very long time to search for proofs of it. We use the handy %\index{Vernacular commands!Time}%[Time] command to measure how long a proof step takes to run. None of the following steps make any progress. *) 321 (** The following fact is false, but that does not stop [eauto] from taking a very long time to search for proofs of it. We use the handy %\index{Vernacular commands!Time}%[Time] command to measure how long a proof step takes to run. None of the following steps make any progress. *)
322 322
323 Example three_minus_four_zero : exists x, 1 + x = 0. 323 Example zero_minus_one : exists x, 1 + x = 0.
324 Time eauto 1. 324 Time eauto 1.
325 (** %\vspace{-.15in}% 325 (** %\vspace{-.15in}%
326 << 326 <<
327 Finished transaction in 0. secs (0.u,0.s) 327 Finished transaction in 0. secs (0.u,0.s)
328 >> 328 >>
486 Qed. 486 Qed.
487 487
488 Hint Resolve length_O length_S. 488 Hint Resolve length_O length_S.
489 (* end thide *) 489 (* end thide *)
490 490
491 (** Let us apply these hints to prove that a [list nat] of length 2 exists. *) 491 (** Let us apply these hints to prove that a [list nat] of length 2 exists. (Here we register [length_O] with [Hint Resolve] instead of [Hint Immediate] merely as a convenience to use the same command as for [length_S]; [Resolve] and [Immediate] have the same meaning for a premise-free hint.) *)
492 492
493 Example length_is_2 : exists ls : list nat, length ls = 2. 493 Example length_is_2 : exists ls : list nat, length ls = 2.
494 (* begin thide *) 494 (* begin thide *)
495 eauto. 495 eauto.
496 (** << 496 (** <<
658 (* begin thide *) 658 (* begin thide *)
659 eauto. 659 eauto.
660 Abort. 660 Abort.
661 (* end thide *) 661 (* end thide *)
662 662
663 (** To help prove [eval1'], we prove an alternate version of [EvalPlus] that inserts an extra equality premise. *) 663 (** To help prove [eval1'], we prove an alternate version of [EvalPlus] that inserts an extra equality premise. This sort of staging is helpful to get around limitations of [eauto]'s unification: [EvalPlus] as a direct hint will only match goals whose results are already expressed as additions, rather than as constants. With the alternate version below, to prove the first two premises, [eauto] is given free reign in deciding the values of [n1] and [n2], while the third premise can then be proved by [reflexivity], no matter how each of its sides is decomposed as a tree of additions. *)
664 664
665 (* begin thide *) 665 (* begin thide *)
666 Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1 666 Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1
667 -> eval var e2 n2 667 -> eval var e2 n2
668 -> n1 + n2 = n 668 -> n1 + n2 = n
813 813
814 (** Let us stop at this point and take stock of the possibilities for [auto] and [eauto] hints. Hints are contained within _hint databases_, which we have seen extended in many examples so far. When no hint database is specified, a default database is used. Hints in the default database are always used by [auto] or [eauto]. The chance to extend hint databases imperatively is 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. In fact, [crush] is defined in terms of [auto], which explains how we achieve this extensibility. Other user-defined tactics can take similar advantage of [auto] and [eauto]. 814 (** Let us stop at this point and take stock of the possibilities for [auto] and [eauto] hints. Hints are contained within _hint databases_, which we have seen extended in many examples so far. When no hint database is specified, a default database is used. Hints in the default database are always used by [auto] or [eauto]. The chance to extend hint databases imperatively is 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. In fact, [crush] is defined in terms of [auto], which explains how we achieve this extensibility. Other user-defined tactics can take similar advantage of [auto] and [eauto].
815 815
816 The basic hints for [auto] and [eauto] are: %\index{Vernacular commands!Hint Immediate}%[Hint Immediate lemma], asking to try solving a goal immediately by applying a lemma and discharging any hypotheses with a single proof step each; %\index{Vernacular commands!Hint Resolve}%[Resolve lemma], which does the same but may add new premises that are themselves to be subjects of nested proof search; %\index{Vernacular commands!Hint Constructors}%[Constructors type], which acts like [Resolve] applied to every constructor of an inductive type; and %\index{Vernacular commands!Hint Unfold}%[Unfold ident], which tries unfolding [ident] when it appears at the head of a proof goal. Each of these [Hint] commands may be used with a suffix, as in [Hint Resolve lemma : my_db]. This adds the hint only to the specified database, so that it would only be used by, for instance, [auto with my_db]. An additional argument to [auto] specifies the maximum depth of proof trees to search in depth-first order, as in [auto 8] or [auto 8 with my_db]. The default depth is 5. 816 The basic hints for [auto] and [eauto] are: %\index{Vernacular commands!Hint Immediate}%[Hint Immediate lemma], asking to try solving a goal immediately by applying a lemma and discharging any hypotheses with a single proof step each; %\index{Vernacular commands!Hint Resolve}%[Resolve lemma], which does the same but may add new premises that are themselves to be subjects of nested proof search; %\index{Vernacular commands!Hint Constructors}%[Constructors type], which acts like [Resolve] applied to every constructor of an inductive type; and %\index{Vernacular commands!Hint Unfold}%[Unfold ident], which tries unfolding [ident] when it appears at the head of a proof goal. Each of these [Hint] commands may be used with a suffix, as in [Hint Resolve lemma : my_db]. This adds the hint only to the specified database, so that it would only be used by, for instance, [auto with my_db]. An additional argument to [auto] specifies the maximum depth of proof trees to search in depth-first order, as in [auto 8] or [auto 8 with my_db]. The default depth is 5.
817 817
818 All of these [Hint] commands can be issued alternatively with a more primitive hint kind, [Extern]. A few more examples of [Hint Extern] should illustrate more of the possibilities. *) 818 All of these [Hint] commands can be expressed with a more primitive hint kind, [Extern]. A few more examples of [Hint Extern] should illustrate more of the possibilities. *)
819 819
820 Theorem bool_neq : true <> false. 820 Theorem bool_neq : true <> false.
821 (* begin thide *) 821 (* begin thide *)
822 auto. 822 auto.
823 823