# Library Cpdt.LogicProg

# Introducing Logic Programming

Print plus.

plus =

fix plus (n m : nat) : nat := match n with

| 0 => m

| S p => S (plus p m)

end

Inductive plusR : nat -> nat -> nat -> Prop :=

| PlusO : forall m, plusR O m m

| PlusS : forall n m r, plusR n m r

-> plusR (S n) m (S r).

Intuitively, a fact plusR n m r only holds when plus n m = r. It is not hard to prove this correspondence formally.

Hint Constructors plusR.

Theorem plus_plusR : forall n m,

plusR n m (n + m).

induction n; crush.

Qed.

Theorem plusR_plus : forall n m r,

plusR n m r

-> r = n + m.

induction 1; crush.

Qed.

With the functional definition of plus, simple equalities about arithmetic follow by computation.

four_plus_three = eq_refl

At this point the proof is completed. It is no doubt clear that a simple procedure could find all proofs of this kind for us. We are just exploring all possible proof trees, built from the two candidate steps apply PlusO and apply PlusS. The built-in tactic auto follows exactly this strategy, since above we used Hint Constructors to register the two candidate proof steps as hints.

four_plus_three' = PlusS (PlusS (PlusS (PlusS (PlusO 3))))

This time, auto is not enough to make any progress. Since even a single candidate step may lead to an infinite space of possible proof trees, auto is parameterized on the maximum depth of trees to consider. The default depth is 5, and it turns out that we need depth 6 to prove the goal.

auto 6.

Sometimes it is useful to see a description of the proof tree that auto finds, with the info tactical. (This tactical is not available in Coq 8.4 as of this writing, but I hope it reappears soon. The special case info_auto tactic is provided as a chatty replacement for auto.)

Restart.

info auto 6.

Qed.

The two key components of logic programming are

*backtracking*and*unification*. To see these techniques in action, consider this further silly example. Here our candidate proof steps will be reflexivity and quantifier instantiation.
For explanatory purposes, let us simulate a user with minimal understanding of arithmetic. We start by choosing an instantiation for the quantifier. Recall that ex_intro is the constructor for existentially quantified formulas.

apply ex_intro with 0.

reflexivity.

Error: Impossible to unify "7" with "0 + 3".

*backtrack*to the point where we ran apply and make a better alternate choice.

Restart.

apply ex_intro with 4.

reflexivity.

Qed.

The above was a fairly tame example of backtracking. In general, any node in an under-construction proof tree may be the destination of backtracking an arbitrarily large number of times, as different candidate proof steps are found not to lead to full proof trees, within the depth bound passed to auto.
Next we demonstrate unification, which will be easier when we switch to the relational formulation of addition.

We could attempt to guess the quantifier instantiation manually as before, but here there is no need. Instead of apply, we use eapply, which proceeds with placeholder

*unification variables*standing in for those parameters we wish to postpone guessing.eapply ex_intro.

1 subgoal

============================

plusR ?70 3 7

============================

plusR ?71 3 6

============================

plusR ?74 3 3

The auto tactic will not perform these sorts of steps that introduce unification variables, but the eauto tactic will. It is helpful to work with two separate tactics, because proof search in the eauto style can uncover many more potential proof trees and hence take much longer to run.

Restart.

info eauto 6.

Qed.

This proof gives us our first example where logic programming simplifies proof search compared to functional programming. In general, functional programs are only meant to be run in a single direction; a function has disjoint sets of inputs and outputs. In the last example, we effectively ran a logic program backwards, deducing an input that gives rise to a certain output. The same works for deducing an unknown value of the other input.

By proving the right auxiliary facts, we can reason about specific functional programs in the same way as we did above for a logic program. Let us prove that the constructors of plusR have natural interpretations as lemmas about plus. We can find the first such lemma already proved in the standard library, using the SearchRewrite command to find a library function proving an equality whose lefthand or righthand side matches a pattern with wildcards.

SearchRewrite (O + _).

plus_O_n: forall n : nat, 0 + n = n

Hint Immediate plus_O_n.

The counterpart to PlusS we will prove ourselves.

The command Hint Resolve adds a new candidate proof step, to be attempted at any level of a proof tree, not just at leaves.

Now that we have registered the proper hints, we can replicate our previous examples with the normal, functional addition plus.

Example seven_minus_three'' : exists x, x + 3 = 7.

eauto 6.

Qed.

Example seven_minus_four : exists x, 4 + x = 7.

eauto 6.

Qed.

This new hint database is far from a complete decision procedure, as we see in a further example that eauto does not finish.

A further lemma will be helpful.

Note that, if we consider the inputs to plus as the inputs of a corresponding logic program, the new rule plusO introduces an ambiguity. For instance, a sum 0 + 0 would match both of plus_O_n and plusO, depending on which operand we focus on. This ambiguity may increase the number of potential search trees, slowing proof search, but semantically it presents no problems, and in fact it leads to an automated proof of the present example.

Just how much damage can be done by adding hints that grow the space of possible proof trees? A classic gotcha comes from unrestricted use of transitivity, as embodied in this library theorem about equality:

Check eq_trans.

eq_trans

: forall (A : Type) (x y z : A), x = y -> y = z -> x = z

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 Time command to measure how long a proof step takes to run. None of the following steps make any progress.

Finished transaction in 0. secs (0.u,0.s)

Time eauto 2.

Finished transaction in 0. secs (0.u,0.s)

Time eauto 3.

Finished transaction in 0. secs (0.008u,0.s)

Time eauto 4.

Finished transaction in 0. secs (0.068005u,0.004s)

Time eauto 5.

Finished transaction in 2. secs (1.92012u,0.044003s)

debug eauto 3.

1 depth=3

1.1 depth=2 eapply ex_intro

1.1.1 depth=1 apply plusO

1.1.1.1 depth=0 eapply eq_trans

1.1.2 depth=1 eapply eq_trans

1.1.2.1 depth=1 apply plus_n_O

1.1.2.1.1 depth=0 apply plusO

1.1.2.1.2 depth=0 eapply eq_trans

1.1.2.2 depth=1 apply @eq_refl

1.1.2.2.1 depth=0 apply plusO

1.1.2.2.2 depth=0 eapply eq_trans

1.1.2.3 depth=1 apply eq_add_S ; trivial

1.1.2.3.1 depth=0 apply plusO

1.1.2.3.2 depth=0 eapply eq_trans

1.1.2.4 depth=1 apply eq_sym ; trivial

1.1.2.4.1 depth=0 eapply eq_trans

1.1.2.5 depth=0 apply plusO

1.1.2.6 depth=0 apply plusS

1.1.2.7 depth=0 apply f_equal (A:=nat)

1.1.2.8 depth=0 apply f_equal2 (A1:=nat) (A2:=nat)

1.1.2.9 depth=0 eapply eq_trans

Sometimes, though, transitivity is just what is needed to get a proof to go through automatically with eauto. For those cases, we can use named

*hint databases*to segregate hints into different groups that may be called on as needed. Here we put eq_trans into the database slow.Finished transaction in 0. secs (0.004u,0.s)

Abort.

One simple example from before runs in the same amount of time, avoiding pollution by transitivity.

Finished transaction in 0. secs (0.004001u,0.s)

Qed.

When we

*do*need transitivity, we ask for it explicitly.== intro x; intro y; intro H; intro H0; simple eapply ex_intro;

apply plusS; simple eapply eq_trans.

exact H.

exact H0.

Qed.

The info trace shows that eq_trans was used in just the position where it is needed to complete the proof. We also see that auto and eauto always perform intro steps without counting them toward the bound on proof tree depth.
Recall the definition of the list length function.

# Searching for Underconstrained Values

Print length.

length =

fun A : Type =>

fix length (l : list A) : nat :=

match l with

| nil => 0

| _ :: l' => S (length l')

end

length_1_2 = eq_refl

Theorem length_O : forall A, length (nil (A := A)) = O.

crush.

Qed.

Theorem length_S : forall A (h : A) t n,

length t = n

-> length (h :: t) = S n.

crush.

Qed.

Hint Resolve length_O length_S.

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

No more subgoals but non-instantiated existential variables: Existential 1 = ?20249 : [ |- nat] Existential 2 = ?20252 : [ |- nat]

*any*value of type nat (for instance, 0) can be plugged in for either variable! However, for more complex types, finding their inhabitants may be as complex as theorem-proving in general.

Show Proof.

Proof: ex_intro (fun ls : list nat => length ls = 2) (?20249 :: ?20252 :: nil) (length_S ?20249 (?20252 :: nil) (length_S ?20252 nil (length_O nat)))

Abort.

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.

Print Forall.

Inductive Forall (A : Type) (P : A -> Prop) : list A -> Prop :=

Forall_nil : Forall P nil

| Forall_cons : forall (x : A) (l : list A),

P x -> Forall P l -> Forall P (x :: l)

Example length_is_2 : exists ls : list nat, length ls = 2

/\ Forall (fun n => n >= 1) ls.

eauto 9.

Qed.

We can see which list eauto found by printing the proof term.

length_is_2 =

ex_intro

(fun ls : list nat => length ls = 2 /\ Forall (fun n : nat => n >= 1) ls)

(1 :: 1 :: nil)

(conj (length_S 1 (1 :: nil) (length_S 1 nil (length_O nat)))

(Forall_cons 1 (le_n 1)

(Forall_cons 1 (le_n 1) (Forall_nil (fun n : nat => n >= 1)))))

Another basic lemma will be helpful to guide proof search.

Finally, we meet Hint Extern, the command to register a custom hint. That is, we provide a pattern to match against goals during proof search. Whenever the pattern matches, a tactic (given to the right of an arrow =>) is attempted. Below, the number 1 gives a priority for this step. Lower priorities are tried before higher priorities, which can have a significant effect on proof search time.

Now we can find a length-2 list whose sum is 0.

Printing the proof term shows the unsurprising list that is found. Here is an example where it is less obvious which list will be used. Can you guess which list eauto will choose?

We will give away part of the answer and say that the above list is less interesting than we would like, because it contains too many zeroes. A further constraint forces a different solution for a smaller instance of the problem.

Example length_and_sum'' : exists ls : list nat, length ls = 2

/\ sum ls = 3

/\ Forall (fun n => n <> 0) ls.

eauto 11.

Qed.

We could continue through exercises of this kind, but even more interesting than finding lists automatically is finding
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.

*programs*automatically.# Synthesizing Programs

An inductive relation specifies the semantics of an expression, relating a variable value and an expression to the expression value.

Inductive eval (var : nat) : exp -> nat -> Prop :=

| EvalConst : forall n, eval var (Const n) n

| EvalVar : eval var Var var

| EvalPlus : forall e1 e2 n1 n2, eval var e1 n1

-> eval var e2 n2

-> eval var (Plus e1 e2) (n1 + n2).

Hint Constructors eval.

We can use auto to execute the semantics for specific expressions.

Unfortunately, just the constructors of eval are not enough to prove theorems like the following, which depends on an arithmetic identity.

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.

Theorem EvalPlus' : forall var e1 e2 n1 n2 n, eval var e1 n1

-> eval var e2 n2

-> n1 + n2 = n

-> eval var (Plus e1 e2) n.

crush.

Qed.

Hint Resolve EvalPlus'.

Further, we instruct eauto to apply 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.

Hint Extern 1 (_ = _) => abstract omega.

Now we can return to eval1' and prove it automatically.

Example eval1' : forall var, eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8).

eauto.

Qed.

Print eval1'.

eval1' =

fun var : nat =>

EvalPlus' (EvalVar var) (EvalPlus (EvalConst var 8) (EvalVar var))

(eval1'_subproof var)

: forall var : nat,

eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8)

synthesize1 =

ex_intro (fun e : exp => forall var : nat, eval var e (var + 7))

(Plus Var (Const 7))

(fun var : nat => EvalPlus (EvalVar var) (EvalConst var 7))

Example synthesize2 : exists e, forall var, eval var e (2 * var + 8).

eauto.

Qed.

Example synthesize3 : exists e, forall var, eval var e (3 * var + 42).

eauto.

Qed.

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.
We prove a series of lemmas and add them as hints. We have alternate eval constructor lemmas and some facts about arithmetic.

Theorem EvalConst' : forall var n m, n = m

-> eval var (Const n) m.

crush.

Qed.

Hint Resolve EvalConst'.

Theorem zero_times : forall n m r,

r = m

-> r = 0 * n + m.

crush.

Qed.

Hint Resolve zero_times.

Theorem EvalVar' : forall var n,

var = n

-> eval var Var n.

crush.

Qed.

Hint Resolve EvalVar'.

Theorem plus_0 : forall n r,

r = n

-> r = n + 0.

crush.

Qed.

Theorem times_1 : forall n, n = 1 * n.

crush.

Qed.

Hint Resolve plus_0 times_1.

We finish with one more arithmetic lemma that is particularly specialized to this theorem. This fact happens to follow by the axioms of the

*semiring*algebraic structure, so, since the naturals form a semiring, we can use the built-in tactic ring.Require Import Arith Ring.

Theorem combine : forall x k1 k2 n1 n2,

(k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2).

intros; ring.

Qed.

Hint Resolve combine.

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.

Theorem linear : forall e, exists k, exists n,

forall var, eval var e (k * var + n).

induction e; crush; eauto.

Qed.

By printing the proof term, it is possible to see the procedure that is used to choose the constants for each input term.
Let us stop at this point and take stock of the possibilities for auto and eauto hints. Hints are contained within
The basic hints for auto and eauto are: Hint Immediate lemma, asking to try solving a goal immediately by applying a lemma and discharging any hypotheses with a single proof step each; Resolve lemma, which does the same but may add new premises that are themselves to be subjects of nested proof search; Constructors type, which acts like Resolve applied to every constructor of an inductive type; and 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, to add 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 expressed with a more primitive hint kind, Extern. A few more examples of Hint Extern should illustrate more of the possibilities.

# More on auto Hints

*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.
A call to crush would have discharged this goal, but the default hint database for auto contains no hint that applies.

Abort.

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 congruence, a complete procedure for the theory of equality, uninterpreted functions, and datatype constructors.

A Hint Extern may be implemented with the full Ltac language. This example shows a case where a hint uses a match.

Section forall_and.

Variable A : Set.

Variables P Q : A -> Prop.

Hypothesis both : forall x, P x /\ Q x.

Theorem forall_and : forall z, P z.

crush.

The crush invocation makes no progress beyond what intros would have accomplished. An auto invocation will not apply the hypothesis both to prove the goal, because the conclusion of both does not unify with the conclusion of the goal. However, we can teach auto to handle this kind of goal.

Hint Extern 1 (P ?X) =>

match goal with

| [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))

end.

auto.

Qed.

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 U from a proof of U /\ V.

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.
Coq's auto hint databases work as tables mapping
Fortunately, a more basic form of Hint Extern also applies. We may simply leave out the pattern to the left of the =>, incorporating the corresponding logic into the Ltac script.

Hint Extern 1 (?P ?X) =>

match goal with

| [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))

end.

User error: Bound head variable

*head symbols*to lists of tactics to try. Because of this, the constant head of an Extern pattern must be determinable statically. In our first Extern hint, the head symbol was not, since x <> y desugars to not (eq x y); and, in the second example, the head symbol was P.
Be forewarned that a Hint Extern of this kind will be applied at
Another dimension of extensibility with hints is rewriting with quantified equalities. We have used the associated command Hint Rewrite in many examples so far. The crush tactic uses these hints by calling the built-in tactic autorewrite. Our rewrite hints have taken the form Hint Rewrite lemma, which by default adds them to the default hint database core; but alternate hint databases may also be specified just as with, e.g., Hint Resolve.
The next example shows a direct use of autorewrite. Note that, while Hint Rewrite uses a default database, autorewrite requires that a database be named.

*every*node of a proof tree, so an expensive Ltac script may slow proof search significantly.# Rewrite Hints

Section autorewrite.

Variable A : Set.

Variable f : A -> A.

Hypothesis f_f : forall x, f (f x) = f x.

Hint Rewrite f_f.

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:

Section garden_path.

Variable g : A -> A.

Hypothesis f_g : forall x, f x = g x.

Hint Rewrite f_g.

Lemma f_f_f' : forall x, f (f (f x)) = f x.

intros; autorewrite with core.

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.

The autorewrite tactic also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings.

Section garden_path.

Variable P : A -> Prop.

Variable g : A -> A.

Hypothesis f_g : forall x, P x -> f x = g x.

Hint Rewrite f_g.

Lemma f_f_f' : forall x, f (f (f x)) = f x.

intros; autorewrite with core.

============================

g (g (g x)) = g x

subgoal 2 is:

P x

subgoal 3 is:

P (f x)

subgoal 4 is:

P (f x)

Abort.

The inappropriate rule fired the same three times as before, even though we know we will not be able to prove the premises.

Our final, successful, attempt uses an extra argument to Hint Rewrite that specifies a tactic to apply to generated premises. Such a hint is only used when the tactic succeeds for all premises, possibly leaving further subgoals for some premises.

Section garden_path.

Variable P : A -> Prop.

Variable g : A -> A.

Hypothesis f_g : forall x, P x -> f x = g x.

Hint Rewrite f_g using assumption.

Lemma f_f_f' : forall x, f (f (f x)) = f x.

intros; autorewrite with core; reflexivity.

Qed.

We may still use autorewrite to apply f_g when the generated premise is among our assumptions.

Lemma f_f_f_g : forall x, P x -> f (f x) = g x.

intros; autorewrite with core; reflexivity.

Qed.

End garden_path.

It can also be useful to apply the autorewrite with db in * form, which does rewriting in hypotheses, as well as in the conclusion.

Lemma in_star : forall x y, f (f (f (f x))) = f (f y)

-> f x = f (f (f y)).

intros; autorewrite with core in *; assumption.

Qed.

End autorewrite.

Many proofs can be automated in pleasantly modular ways with deft combinations of auto and autorewrite.