Certified Programming with Dependent Types: src/LogicProg.v comparison

comparison src/LogicProg.v @ 430:610568369aee

Pass through LogicProg, to incorporate new coqdoc features

author	Adam Chlipala <adam@chlipala.net>
date	Thu, 26 Jul 2012 14:18:15 -0400
parents	b4c37245502e
children	8077352044b2

comparison

equal deleted inserted replaced

-:5744842c36a8
+:610568369aee
 (** %\part{Proof Engineering}
 \chapter{Proof Search by Logic Programming}% *)
-(** The Curry-Howard correspondence tells us that proving is %``%#"#just#"#%''% programming, but the pragmatics of the two activities are very different.  Generally we care about properties of a program besides its type, but the same is not true about proofs.  Any proof of a theorem will do just as well.  As a result, automated proof search is conceptually simpler than automated programming.
+(** The Curry-Howard correspondence tells us that proving is "just" programming, but the pragmatics of the two activities are very different.  Generally we care about properties of a program besides its type, but the same is not true about proofs.  Any proof of a theorem will do just as well.  As a result, automated proof search is conceptually simpler than automated programming.
 The paradigm of %\index{logic programming}%logic programming%~\cite{LogicProgramming}%, as embodied in languages like %\index{Prolog}%Prolog%~\cite{Prolog}%, is a good match for proof search in higher-order logic.  This chapter introduces the details, attempting to avoid any dependence on past logic programming experience. *)
 (** * Introducing Logic Programming *)
 Example four_plus_three : 4 + 3 = 7.
 (* begin thide *)
 reflexivity.
 Qed.
 (* end thide *)
+(* begin hide *)
+Definition er := @eq_refl.
+(* end hide *)
 Print four_plus_three.
 (** %\vspace{-.15in}%[[
 four_plus_three = eq_refl
 ]]
 Abort.
 (* end thide *)
 (** We see that the two unification variables stand for the two elements of the list.  Indeed, list length is independent of data values.  Paradoxically, we can make the proof search process easier by constraining the list further, so that proof search naturally locates appropriate data elements by unification.  The library predicate [Forall] will be helpful. *)
+(* begin hide *)
+Definition Forall_c := (@Forall_nil, @Forall_cons).
+(* end hide *)
 Print Forall.
 (** %\vspace{-.15in}%[[
 Inductive Forall (A : Type) (P : A -> Prop) : list A -> Prop :=
 Forall_nil : Forall P nil
 | Forall_cons : forall (x : A) (l : list A),
 eauto 9.
 Qed.
 (* end thide *)
 (** We can see which list [eauto] found by printing the proof term. *)
+(* begin hide *)
+Definition conj' := (conj, le_n).
+(* end hide *)
 Print length_is_2.
 (** %\vspace{-.15in}%[[
 length_is_2 =
 ex_intro
 (* begin thide *)
 eauto.
 Qed.
 (* end thide *)
+(* begin hide *)
+Definition e1s := eval1'_subproof.
+(* end hide *)
 Print eval1'.
 (** %\vspace{-.15in}%[[
 eval1' =
 fun var : nat =>
 EvalPlus' (EvalVar var) (EvalPlus (EvalConst var 8) (EvalVar var))
 (** By printing the proof term, it is possible to see the procedure that is used to choose the constants for each input term. *)
 (** * More on [auto] Hints *)
-(** 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].
+(** 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].
 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.
 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. *)
 auto.
 (** A call to [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
 Abort.
+(* begin hide *)
+Definition boool := bool.
+(* end hide *)
 (** It is hard to come up with a [bool]-specific hint that is not just a restatement of the theorem we mean to prove.  Luckily, a simpler form suffices, by appealing to the built-in tactic %\index{tactics!congruence}%[congruence], a complete procedure for the theory of equality, uninterpreted functions, and datatype constructors. *)
 Hint Extern 1 (_ <> _) => congruence.
 (** We see that an [Extern] pattern may bind unification variables that we use in the associated tactic.  The function [proj1] is from the standard library, for extracting a proof of [R] from a proof of [R /\ S]. *)
 End forall_and.
+(* begin hide *)
+Definition noot := (not, @eq).
+(* end hide *)
 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].
 [[
 Hint Extern 1 (?P ?X) =>
 match goal with
 | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
 end.
 ]]
 <<
 User error: Bound head variable
 >>
 Lemma f_f_f : forall x, f (f (f x)) = f x.
 intros; autorewrite with core; reflexivity.
 Qed.
-(** There are a few ways in which [autorewrite] can lead to trouble when insufficient care is taken in choosing hints.  First, the set of hints may define a nonterminating rewrite system, in which case invocations to [autorewrite] may not terminate.  Second, we may add hints that %``%#"#lead [autorewrite] down the wrong path.#"#%''%  For instance: *)
+(** There are a few ways in which [autorewrite] can lead to trouble when insufficient care is taken in choosing hints.  First, the set of hints may define a nonterminating rewrite system, in which case invocations to [autorewrite] may not terminate.  Second, we may add hints that "lead [autorewrite] down the wrong path."  For instance: *)
 Section garden_path.
 Variable g : A -> A.
 Hypothesis f_g : forall x, f x = g x.
 Hint Rewrite f_g.
 ]]
 *)
 Abort.
-(** Our new hint was used to rewrite the goal into a form where the old hint could no longer be applied.  This %``%#"#non-monotonicity#"#%''% of rewrite hints contrasts with the situation for [auto], where new hints may slow down proof search but can never %``%#"#break#"#%''% old proofs.  The key difference is that [auto] either solves a goal or makes no changes to it, while [autorewrite] may change goals without solving them.  The situation for [eauto] is slightly more complicated, as changes to hint databases may change the proof found for a particular goal, and that proof may influence the settings of unification variables that appear elsewhere in the proof state. *)
+(** Our new hint was used to rewrite the goal into a form where the old hint could no longer be applied.  This "non-monotonicity" of rewrite hints contrasts with the situation for [auto], where new hints may slow down proof search but can never "break" old proofs.  The key difference is that [auto] either solves a goal or makes no changes to it, while [autorewrite] may change goals without solving them.  The situation for [eauto] is slightly more complicated, as changes to hint databases may change the proof found for a particular goal, and that proof may influence the settings of unification variables that appear elsewhere in the proof state. *)
 Reset garden_path.
 (** The [autorewrite] tactic also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *)

Mercurial > cpdt > repo

comparison src/LogicProg.v @ 430:610568369aee