Week 5: Logic programming

Author: Adam Chlipala, with modifications by CS-428 staff.
License: No redistribution allowed (usage by permission in CS-428).

Introduction to logic programming

Recall the definition of addition from the standard library.

Print Nat.add.Nat.add =
fix add (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S p => S (add p m)
  end
     : nat -> nat -> nat

Arguments Nat.add (n m)%nat_scope

This is a recursive definition, in the style of functional programming. We might also follow the style of logic programming, which corresponds to the inductive relations we have defined in previous lectures.

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.

Theorem plus_plusR : forall n m,
  plusR n m (n + m).forall n m : nat, plusR n m (n + m)
Proof.forall n m : nat, plusR n m (n + m)
  induction n; simpl.forall m : nat, plusR 0 m m
n: nat
IHn: forall m : nat, plusR n m (n + m)
forall m : nat, plusR (S n) m (S (n + m))
  -forall m : nat, plusR 0 m m constructor.
  -n: nat
IHn: forall m : nat, plusR n m (n + m)
forall m : nat, plusR (S n) m (S (n + m)) constructor.n: nat
IHn: forall m : nat, plusR n m (n + m)
m: nat
plusR n m (n + m)
    apply IHn.
Qed.

We see here another instance of the very mechanical proof pattern that came up before: keep trying constructors and hypotheses. The tactic auto will automate searching through sequences of that kind, when we prime it with good suggestions of single proof steps to try, as with this command:

Local Hint Constructors plusR : core.

That is, every constructor of plusR should be considered as an atomic proof step, from which we enumerate step sequences.

Theorem plus_plusR_snazzy : forall n m,
  plusR n m (n + m).forall n m : nat, plusR n m (n + m)
Proof.forall n m : nat, plusR n m (n + m)
  induction n; simpl; auto.
Qed.

Theorem plusR_plus : forall n m r,
  plusR n m r
  -> r = n + m.forall n m r : nat, plusR n m r -> r = n + m
Proof.forall n m r : nat, plusR n m r -> r = n + m
  induction 1; lia.
Qed.

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

Example four_plus_three : 4 + 3 = 7.4 + 3 = 7
Proof.4 + 3 = 7
  reflexivity.
Qed.

Print four_plus_three.four_plus_three = eq_refl
     : 4 + 3 = 7

With the relational definition, the same equalities take more steps to prove, but the process is completely mechanical. For example, consider this simple-minded manual proof search strategy. The steps prefaced by Fail are intended to fail; they're included for explanatory value, to mimic a simple-minded try-everything strategy.

Example four_plus_three' : plusR 4 3 7.
Proof.plusR 4 3 7
  apply PlusO.Unable to unify "plusR 0 ?M1368 ?M1368" with
 "plusR 4 3 7".
  apply PlusS.plusR 3 3 6
  apply PlusO.Unable to unify "plusR 0 ?M1372 ?M1372" with
 "plusR 3 3 6".
  apply PlusS.plusR 2 3 5
  apply PlusO.Unable to unify "plusR 0 ?M1376 ?M1376" with
 "plusR 2 3 5".
  apply PlusS.plusR 1 3 4
  apply PlusO.Unable to unify "plusR 0 ?M1380 ?M1380" with
 "plusR 1 3 4".
  apply PlusS.plusR 0 3 3
  apply PlusO.

At this point the proof is complete. 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. Thus, auto is another great match!

Restart.plusR 4 3 7
  auto.
Qed.

Print four_plus_three'.four_plus_three' =
PlusS 3 3 6
  (PlusS 2 3 5 (PlusS 1 3 4 (PlusS 0 3 3 (PlusO 3))))
     : plusR 4 3 7

Let us try the same approach on a slightly more complex goal.

Example five_plus_three : plusR 5 3 8.plusR 5 3 8
Proof.plusR 5 3 8
  auto.plusR 5 3 8

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_auto variant.

Restart.plusR 5 3 8
  info_auto 6.(* info auto: *)
simple apply PlusS (in core).
 simple apply PlusS (in core).
  simple apply PlusS (in core).
   simple apply PlusS (in core).
    simple apply PlusS (in core).
     simple apply PlusO (in core).
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.

Example seven_minus_three : exists x, x + 3 = 7.exists x : nat, x + 3 = 7
Proof.exists x : nat, x + 3 = 7

For explanatory purposes, let us simulate a user with minimal understanding of arithmetic. We start by choosing an instantiation for the quantifier. It is relevant that ex_intro is the proof rule for existential-quantifier instantiation.

  apply ex_intro with 0.0 + 3 = 7
  Fail reflexivity.The command has indeed failed with message:
Unable to unify "7" with "0 + 3".
0 + 3 = 7

This seems to be a dead end. Let us backtrack to the point where we ran apply and make a better alternative choice.

Restart.exists x : nat, x + 3 = 7
  apply ex_intro with 4.4 + 3 = 7
  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.

Example seven_minus_three' : exists x, plusR x 3 7.exists x : nat, plusR x 3 7
Proof.exists x : nat, plusR x 3 7

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.plusR ?x 3 7

Now we can finish the proof with the right applications of plusR's constructors. Note that new unification variables are being generated to stand for new unknowns.

  apply PlusS.plusR ?n 3 6
  apply PlusS.plusR ?n 3 5 apply PlusS.plusR ?n 3 4 apply PlusS.plusR ?n 3 3
  apply PlusO.

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.exists x : nat, plusR x 3 7
  info_eauto 6.(* info eauto: *)
simple eapply ex_intro.
simple apply PlusS.
simple apply PlusS.
simple apply PlusS.
simple apply PlusS.
simple apply PlusO.
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.

Example seven_minus_four' : exists x, plusR 4 x 7.exists x : nat, plusR 4 x 7
Proof.exists x : nat, plusR 4 x 7
  eauto 6.
Qed.

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 Search command to find a library function proving an equality whose lefthand or righthand side matches a pattern with wildcards.

Search (O + _).Nat.add_0_l: forall n : nat, 0 + n = n
plus_O_n: forall n : nat, 0 + n = n

The command Hint Immediate asks auto and eauto to consider this lemma as a candidate step for any leaf of a proof tree, meaning that all premises of the rule need to match hypotheses.

Local Hint Immediate plus_O_n : core.

The counterpart to PlusS we will prove ourselves.

Lemma plusS : forall n m r,
  n + m = r
  -> S n + m = S r.forall n m r : nat, n + m = r -> S n + m = S r
Proof.forall n m r : nat, n + m = r -> S n + m = S r
  lia.
Qed.

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

Local Hint Resolve plusS : core.

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.exists x : nat, x + 3 = 7
Proof.exists x : nat, x + 3 = 7
  eauto 6.
Qed.

Example seven_minus_four : exists x, 4 + x = 7.exists x : nat, 4 + x = 7
Proof.exists x : nat, 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 solve.

Example seven_minus_four_zero : exists x, 4 + x + 0 = 7.exists x : nat, 4 + x + 0 = 7
Proof.exists x : nat, 4 + x + 0 = 7
  info_eauto 6.(* info eauto: *)
idtac.
exists x : nat, 4 + x + 0 = 7
Fail Qed.The command has indeed failed with message:
 (in proof seven_minus_four_zero): Attempt to save an incomplete proof
(there are remaining open goals).
exists x : nat, 4 + x + 0 = 7
Abort.

A further lemma will be helpful.

Lemma plusO : forall n m,
  n = m
  -> n + 0 = m.forall n m : nat, n = m -> n + 0 = m
Proof.forall n m : nat, n = m -> n + 0 = m
  lia.
Qed.

Local Hint Resolve plusO : core.

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.

Example seven_minus_four_zero : exists x, 4 + x + 0 = 7.exists x : nat, 4 + x + 0 = 7
Proof.exists x : nat, 4 + x + 0 = 7
  eauto 7.
Qed.

Note

Instead of adding plusO to the core database explicitly, we could configure it to allow more flexibility in unification:

Section AllowUnfold.
  Remove Hints plusO : core.
  Remove Hints plus_n_O : core.

  Example seven_minus_four_zero' : exists x, 4 + x + 0 = 7.exists x : nat, 4 + x + 0 = 7
  Proof.exists x : nat, 4 + x + 0 = 7
    solve [eauto 10].No applicable tactic.
  Abort.

  Hint Constants Transparent : core.

  Example seven_minus_four_zero' : exists x, 4 + x + 0 = 7.exists x : nat, 4 + x + 0 = 7
  Proof.exists x : nat, 4 + x + 0 = 7
    info_eauto 9.(* info eauto: *)
simple eapply ex_intro.
simple apply plusS.
simple apply plusS.
simple apply plusS.
simple apply plusS.
simple apply plusS.
simple apply plusS.
simple apply plusS.
simple apply plus_O_n ; trivial.
  Qed.

This works because 4 + x simplifies to S (S (S (S x))), which allows plusS to apply; should the term have been written as x + 4 instead, it would not have helped:

  Example seven_minus_four_zero'' : exists x, x + 4 + 0 = 7.exists x : nat, x + 4 + 0 = 7
  Proof.exists x : nat, x + 4 + 0 = 7
    Fail solve [eauto 10].The command has indeed failed with message:
No applicable tactic.
exists x : nat, x + 4 + 0 = 7
  Abort.
End AllowUnfold.

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

Hints are scoped over sections, so let us enter a section to contain the effects of an unfortunate hint choice.

Section slow.
  Hint Resolve eq_trans : core.

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.

  Example zero_minus_one : exists x, 1 + x = 0.exists x : nat, 1 + x = 0
    Time eauto 1.Finished transaction in 0. secs (0.u,0.s) (successful)
exists x : nat, 1 + x = 0
    Time eauto 2.Finished transaction in 0. secs (0.u,0.s) (successful)
exists x : nat, 1 + x = 0
    Time eauto 3.Finished transaction in 0.001 secs (0.001u,0.s) (successful)
exists x : nat, 1 + x = 0
    Time eauto 4.Finished transaction in 0.018 secs (0.017u,0.s) (successful)
exists x : nat, 1 + x = 0
    Time eauto 5.Finished transaction in 0.554 secs (0.548u,0.006s) (successful)
exists x : nat, 1 + x = 0

We see worrying exponential growth in running time, and the debug tactical helps us see where eauto is wasting its time, outputting a trace of every proof step that is attempted. The rule eq_trans applies at every node of a proof tree, and eauto tries all such positions.

    debug eauto 3.(* debug eauto: *)
1 depth=3 
1.1 depth=2 simple eapply ex_intro
1.1.1 depth=1 simple apply plusO
1.1.1.1 depth=0 simple eapply eq_trans
1.1.2 depth=1 simple eapply eq_trans
1.1.2.1 depth=1 simple apply plus_n_Sm
1.1.2.1.1 depth=0 simple eapply eq_trans
1.1.2.2 depth=1 simple apply @eq_refl
1.1.2.2.1 depth=0 simple apply plusO
1.1.2.2.2 depth=0 simple eapply eq_trans
1.1.2.3 depth=1 simple apply plus_n_O
1.1.2.3.1 depth=0 simple apply plusO
1.1.2.3.2 depth=0 simple eapply eq_trans
1.1.2.4 depth=1 simple apply eq_add_S ; trivial
1.1.2.4.1 depth=0 simple eapply eq_trans
1.1.2.5 depth=1 simple apply eq_sym ; trivial
1.1.2.5.1 depth=0 simple eapply eq_trans
1.1.2.6 depth=0 simple apply plusO
1.1.2.7 depth=0 simple apply plusS
1.1.2.8 depth=0 simple apply f_equal_nat
1.1.2.9 depth=0 simple apply f_equal2_nat
1.1.2.10 depth=0 simple eapply eq_trans
  Abort.
End slow.

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.

Local Hint Resolve eq_trans : slow.

Example from_one_to_zero : exists x, 1 + x = 0.exists x : nat, 1 + x = 0
Proof.exists x : nat, 1 + x = 0
  Time eauto.Finished transaction in 0. secs (0.u,0.s) (successful)
exists x : nat, 1 + x = 0

This eauto fails to prove the goal, but at least it takes substantially less than the 2 seconds required above!

Abort.

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

Example seven_minus_three_again : exists x, x + 3 = 7.exists x : nat, x + 3 = 7
Proof.exists x : nat, x + 3 = 7
  Time eauto 6.Finished transaction in 0. secs (0.u,0.s) (successful)
Qed.

When we do need transitivity, we ask for it explicitly.

Example needs_trans : forall x y, 1 + x = y
  -> y = 2
  -> exists z, z + x = 3.forall x y : nat,
1 + x = y -> y = 2 -> exists z : nat, z + x = 3
Proof.forall x y : nat,
1 + x = y -> y = 2 -> exists z : nat, z + x = 3
  info_eauto with slow.(* info eauto: *)
intro.
intro.
intro.
intro.
simple eapply ex_intro.
simple 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.

Searching for Underconstrained Values

Recall the definition of the list length function.

Print Datatypes.length.Datatypes.length =
fun A : Type =>
fix length (l : list A) : nat :=
  match l with
  | nil => 0
  | _ :: l' => S (length l')
  end
     : forall [A : Type], list A -> nat

Arguments Datatypes.length [A]%type_scope _%list_scope

This function is easy to reason about in the forward direction, computing output from input.

Example length_1_2 : length (1 :: 2 :: nil) = 2.Datatypes.length (1 :: 2 :: nil) = 2
Proof.Datatypes.length (1 :: 2 :: nil) = 2
  auto.
Qed.

Print length_1_2.length_1_2 =
eq_refl
     : Datatypes.length (1 :: 2 :: nil) = 2

As in the last section, we will prove some lemmas to recast length in logic-programming style, to help us compute inputs from outputs.

Theorem length_O : forall A, length (nil (A := A)) = O.forall A : Type, Datatypes.length nil = 0
Proof.forall A : Type, Datatypes.length nil = 0
  reflexivity.
Qed.

Theorem length_S : forall A (h : A) t n,
  length t = n
  -> length (h :: t) = S n.forall (A : Type) (h : A) (t : list A) (n : nat),
Datatypes.length t = n ->
Datatypes.length (h :: t) = S n
Proof.forall (A : Type) (h : A) (t : list A) (n : nat),
Datatypes.length t = n ->
Datatypes.length (h :: t) = S n
  simpl; congruence.
Qed.

Local Hint Immediate length_O : core.
Local Hint Resolve length_S : core.

Let us apply these hints to prove that a list nat of length 2 exists.

Example length_is_2 : exists ls : list nat, length ls = 2.exists ls : list nat, Datatypes.length ls = 2
Proof.exists ls : list nat, Datatypes.length ls = 2
  eauto.

Coq leaves for us two subgoals to prove... nat?! We are being asked to show that natural numbers exists. Why? Some unification variables of that type were left undetermined, by the end of the proof. Specifically, these variables stand for the 2 elements of the list we find. Of course it makes sense that the list length follows without knowing the data values. In Coq 8.6 and up, the Unshelve command brings these goals to the forefront, where we can solve each one with exact O, but usually it is better to avoid getting to such a point.

To debug such situations, it can be helpful to print the current internal representation of the proof, so we can see where the unification variables show up.

  Show Proof.(ex_intro
   (fun ls : list nat => Datatypes.length ls = 2)
   (?h :: ?h0 :: nil)
   (length_S nat ?h (?h0 :: nil) 1
      (length_S nat ?h0 nil 0 (length_O nat))))
Abort.

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

Arguments Forall [A]%type_scope P%function_scope
  _%list_scope
Arguments Forall_nil [A]%type_scope P%function_scope
Arguments Forall_cons [A]%type_scope
  [P]%function_scope x [l]%list_scope _ _

Example length_is_2 : exists ls : list nat, length ls = 2
  /\ Forall (fun n => n >= 1) ls.exists ls : list nat,
  Datatypes.length ls = 2 /\
  Forall (fun n : nat => n >= 1) ls
Proof.exists ls : list nat,
  Datatypes.length ls = 2 /\
  Forall (fun n : nat => n >= 1) ls
  eauto 9.
Qed.

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

Print length_is_2.length_is_2 =
ex_intro
  (fun ls : list nat =>
   Datatypes.length ls = 2 /\
   Forall (fun n : nat => n >= 1) ls) (1 :: 1 :: nil)
  (conj
     (length_S nat 1 (1 :: nil) 1
        (length_S nat 1 nil 0 (length_O nat)))
     (Forall_cons 1 (le_n 1 : 1 >= 1)
        (Forall_cons 1 (le_n 1 : 1 >= 1)
           (Forall_nil (fun n : nat => n >= 1)))))
     : exists ls : list nat,
         Datatypes.length ls = 2 /\
         Forall (fun n : nat => n >= 1) ls

Let us try one more, fancier example. First, we use a standard higher-order function to define a function for summing all data elements of a list.

Definition sum := fold_right plus O.

Another basic lemma will be helpful to guide proof search.

Lemma plusO' : forall n m,
  n = m
  -> 0 + n = m.forall n m : nat, n = m -> 0 + n = m
Proof.forall n m : nat, n = m -> 0 + n = m
  lia.
Qed.

Local Hint Resolve plusO' : core.

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, i.e. when we manage to give lower priorities to the cheaper rules.

Local Hint Extern 1 (sum _ = _) => simpl : core.

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

Example length_and_sum : exists ls : list nat, length ls = 2
  /\ sum ls = O.exists ls : list nat,
  Datatypes.length ls = 2 /\ sum ls = 0
Proof.exists ls : list nat,
  Datatypes.length ls = 2 /\ sum ls = 0
  eauto 7.
Qed.

Print length_and_sum.length_and_sum =
ex_intro
  (fun ls : list nat =>
   Datatypes.length ls = 2 /\ sum ls = 0)
  (0 :: 0 :: nil)
  (conj
     (length_S nat 0 (0 :: nil) 1
        (length_S nat 0 nil 0 (length_O nat)))
     (plusO' (0 + 0) 0 (plus_O_n 0)
      :
      sum (0 :: 0 :: nil) = 0))
     : exists ls : list nat,
         Datatypes.length ls = 2 /\ sum ls = 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?

Example length_and_sum' : exists ls : list nat, length ls = 5
  /\ sum ls = 42.exists ls : list nat,
  Datatypes.length ls = 5 /\ sum ls = 42
Proof.exists ls : list nat,
  Datatypes.length ls = 5 /\ sum ls = 42
  eauto 15.
Qed.

Print length_and_sum'.length_and_sum' =
ex_intro
  (fun ls : list nat =>
   Datatypes.length ls = 5 /\ sum ls = 42)
  (0 :: 0 :: 0 :: 0 :: 42 :: nil)
  (conj
     (length_S nat 0 (0 :: 0 :: 0 :: 42 :: nil) 4
        (length_S nat 0 (0 :: 0 :: 42 :: nil) 3
           (length_S nat 0 (0 :: 42 :: nil) 2
              (length_S nat 0 (42 :: nil) 1
                 (length_S nat 42 nil 0 (length_O nat))))))
     (plusO' (0 + (0 + (0 + (42 + 0)))) 42
        (plusO' (0 + (0 + (42 + 0))) 42
           (plusO' (0 + (42 + 0)) 42
              (plusO' (42 + 0) 42
                 (eq_sym (plus_n_O 42)))))
      :
      sum (0 :: 0 :: 0 :: 0 :: 42 :: nil) = 42))
     : exists ls : list nat,
         Datatypes.length ls = 5 /\ sum ls = 42

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.exists ls : list nat,
  Datatypes.length ls = 2 /\
  sum ls = 3 /\ Forall (fun n : nat => n <> 0) ls
Proof.exists ls : list nat,
  Datatypes.length ls = 2 /\
  sum ls = 3 /\ Forall (fun n : nat => n <> 0) ls
  eauto 11.
Qed.

Print length_and_sum''.length_and_sum'' =
ex_intro
  (fun ls : list nat =>
   Datatypes.length ls = 2 /\
   sum ls = 3 /\ Forall (fun n : nat => n <> 0) ls)
  (1 :: 2 :: nil)
  (conj
     (length_S nat 1 (2 :: nil) 1
        (length_S nat 2 nil 0 (length_O nat)))
     (conj
        (plusS 0 (2 + 0) 2
           (plusO' (2 + 0) 2 (eq_sym (plus_n_O 2)))
         :
         sum (1 :: 2 :: nil) = 3)
        (Forall_cons 1 (not_eq_sym (n_Sn 0))
           (Forall_cons 2 (not_eq_sym (O_S 1))
              (Forall_nil (fun n : nat => n <> 0))))))
     : exists ls : list nat,
         Datatypes.length ls = 2 /\
         sum ls = 3 /\
         Forall (fun n : nat => n <> 0) ls

Revisiting `eval`

The same techniques apply to the eval function that we studied in previous weeks:

Module Simple.
  Notation var := string.
  Open Scope string_scope.

  Inductive arith : Set :=
  | Const (n : nat)
  | Var (x : var)
  | Plus (e1 e2 : arith)
  | Minus (e1 e2 : arith)
  | Times (e1 e2 : arith).

  Coercion Const : nat >-> arith.
  Coercion Var : var >-> arith.
  Infix "+" := Plus : arith_scope.Declaring a scope implicitly is deprecated; use in
advance an explicit "Declare Scope arith_scope.".
[undeclared-scope,deprecated-since-8.10,deprecated,default]
  Infix "-" := Minus : arith_scope.
  Infix "*" := Times : arith_scope.
  Delimit Scope arith_scope with arith.

  Definition valuation := var -> option nat.

  Definition empty : valuation := fun _ => None.

  Definition get (x:var) (v:valuation) : option nat := v x.

  Definition set (x:var) (n:nat) (v:valuation) : valuation :=
    fun y =>
      match string_dec x y with
      | left H => Some n
      | right H' => get y v
      end.

Unlike previously, we define interp as a relation, for maximum eauto-friendliness.

  Inductive interp (v: valuation): forall (e : arith) (n: nat), Prop :=
  | InterpConst (n: nat) : interp v (Const n) n
  | InterpVarNotFound (x: var) (n: nat) :
    get x v = None ->
    interp v (Var x) 0
  | InterpVarFound (x: var) (n: nat) :
    get x v = Some n ->
    interp v (Var x) n
  | InterpPlus (e1 e2: arith) n1 n2:
    interp v e1 n1 -> interp v e2 n2 ->
    interp v (Plus e1 e2) (n1 + n2)
  | InterpMinus (e1 e2: arith) n1 n2:
    interp v e1 n1 -> interp v e2 n2 ->
    interp v (Minus e1 e2) (n1 - n2)
  | InterpTimes (e1 e2: arith) n1 n2:
    interp v e1 n1 -> interp v e2 n2 ->
    interp v (Times e1 e2) (n1 * n2).

  Inductive cmd :=
  | Skip
  | Assign (x : var) (e : arith)
  | Sequence (c1 c2 : cmd)
  | If (e : arith) (then_ else_ : cmd)
  | While (e : arith) (body : cmd).

  Notation "x <- e" := (Assign x e%arith) (at level 75).
  Infix ";;" := (* This one changed to avoid parsing clashes. *)
    Sequence (at level 76).
  Notation "'when' e 'then' then_ 'else' else_ 'done'" :=
    (If e%arith then_ else_) (at level 75, e at level 0).Identifier 'when' now a keyword
Identifier 'done' now a keyword
  Notation "'while' e 'loop' body 'done'" :=
    (While e%arith body) (at level 75).Identifier 'while' now a keyword
Identifier 'loop' now a keyword

  Example factorial :=
    "output" <- 1;;
    while "input" loop
      "output" <- "output" * "input";;
      "input" <- "input" - 1
    done.

  Inductive eval : valuation -> cmd -> valuation -> Prop :=
  | EvalSkip : forall v,
    eval v Skip v
  | EvalAssign : forall v x e n,
    interp v e n ->
    eval v (Assign x e) (set x n v)
  | EvalSeq : forall v c1 v1 c2 v2,
    eval v c1 v1
    -> eval v1 c2 v2
    -> eval v (Sequence c1 c2) v2
  | EvalIfTrue : forall v e then_ else_ v' n,
    interp v e n
    -> n <> 0
    -> eval v then_ v'
    -> eval v (If e then_ else_) v'
  | EvalIfFalse : forall v e then_ else_ v' n,
    interp v e n
    -> n = 0
    -> eval v else_ v'
    -> eval v (If e then_ else_) v'
  | EvalWhileTrue : forall v e body v' v'' n,
    interp v e n
    -> n <> 0
    -> eval v body v'
    -> eval v' (While e body) v''
    -> eval v (While e body) v''
  | EvalWhileFalse : forall v e body n,
    interp v e n
    -> n = 0
    -> eval v (While e body) v.

Our first proof is not the most satisfying:

  Theorem factorial_2 : exists v, eval (set "input" 3 empty) factorial v
                             /\ get "output" v = Some 6.exists v : valuation,
  eval (set "input" 3 empty) factorial v /\
  get "output" v = Some 6
  Proof.exists v : valuation,
  eval (set "input" 3 empty) factorial v /\
  get "output" v = Some 6
    unfold factorial.exists v : valuation,
  eval (set "input" 3 empty)
    ("output" <- 1;;
     while "input"
     loop "output" <- "output" * "input";;
          "input" <- "input" - 1 done) v /\
  get "output" v = Some 6

econstructor simply loops, repeatedly applying EvalWhileTrue:

    Timeout 2 repeat econstructor.Timeout!

The manual alternative does not look great:

    eapply ex_intro.eval (set "input" 3 empty)
  ("output" <- 1;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v /\
get "output" ?v = Some 6
    split.eval (set "input" 3 empty)
  ("output" <- 1;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
get "output" ?v = Some 6
    -eval (set "input" 3 empty)
  ("output" <- 1;;
   while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v eapply EvalSeq.eval (set "input" 3 empty) ("output" <- 1) ?v1
eval ?v1
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
      +eval (set "input" 3 empty) ("output" <- 1) ?v1 apply EvalAssign.interp (set "input" 3 empty) 1 ?n
        apply InterpConst.
      +eval (set "output" 1 (set "input" 3 empty))
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v eapply EvalWhileTrue.interp (set "output" 1 (set "input" 3 empty)) "input"
  ?n
?n <> 0
eval (set "output" 1 (set "input" 3 empty))
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v'
eval ?v'
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
        *interp (set "output" 1 (set "input" 3 empty)) "input"
  ?n apply InterpVarFound; reflexivity.
        *3 <> 0 congruence.
        *eval (set "output" 1 (set "input" 3 empty))
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v' eapply EvalSeq.eval (set "output" 1 (set "input" 3 empty))
  ("output" <- "output" * "input") ?v1
eval ?v1 ("input" <- "input" - 1) ?v'
          --eval (set "output" 1 (set "input" 3 empty))
  ("output" <- "output" * "input") ?v1 apply EvalAssign.interp (set "output" 1 (set "input" 3 empty))
  ("output" * "input")%arith ?n
             apply InterpTimes.interp (set "output" 1 (set "input" 3 empty)) "output"
  ?n1
interp (set "output" 1 (set "input" 3 empty)) "input"
  ?n2
             ++interp (set "output" 1 (set "input" 3 empty)) "output"
  ?n1 apply InterpVarFound.get "output" (set "output" 1 (set "input" 3 empty)) =
Some ?n1
                reflexivity.
             ++interp (set "output" 1 (set "input" 3 empty)) "input"
  ?n2 apply InterpVarFound.get "input" (set "output" 1 (set "input" 3 empty)) =
Some ?n2
                reflexivity.
          --eval
  (set "output" (1 * 3)
     (set "output" 1 (set "input" 3 empty)))
  ("input" <- "input" - 1) ?v' apply EvalAssign.interp
  (set "output" (1 * 3)
     (set "output" 1 (set "input" 3 empty)))
  ("input" - 1)%arith ?n
             apply InterpMinus.interp
  (set "output" (1 * 3)
     (set "output" 1 (set "input" 3 empty))) "input"
  ?n1
interp
  (set "output" (1 * 3)
     (set "output" 1 (set "input" 3 empty))) 1 ?n2
             ++interp
  (set "output" (1 * 3)
     (set "output" 1 (set "input" 3 empty))) "input"
  ?n1 apply InterpVarFound.get "input"
  (set "output" (1 * 3)
     (set "output" 1 (set "input" 3 empty))) =
Some ?n1
                reflexivity.
             ++interp
  (set "output" (1 * 3)
     (set "output" 1 (set "input" 3 empty))) 1 ?n2 apply InterpConst.
        *eval
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty))))
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v eapply EvalWhileTrue.interp
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty))))
  "input" ?n
?n <> 0
eval
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty))))
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v'
eval ?v'
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
          --interp
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty))))
  "input" ?n apply InterpVarFound.get "input"
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty)))) =
Some ?n
             reflexivity.
          --3 - 1 <> 0 simpl; congruence.
          --eval
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty))))
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v' eapply EvalSeq.eval
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty))))
  ("output" <- "output" * "input") ?v1
eval ?v1 ("input" <- "input" - 1) ?v'
             ++eval
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty))))
  ("output" <- "output" * "input") ?v1 apply EvalAssign.interp
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty))))
  ("output" * "input")%arith ?n
                apply InterpTimes.interp
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty))))
  "output" ?n1
interp
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty))))
  "input" ?n2
                **interp
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty))))
  "output" ?n1 apply InterpVarFound.get "output"
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty)))) =
Some ?n1
                   reflexivity.
                **interp
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty))))
  "input" ?n2 apply InterpVarFound.get "input"
  (set "input" (3 - 1)
     (set "output" (1 * 3)
        (set "output" 1 (set "input" 3 empty)))) =
Some ?n2
                   reflexivity.
             ++eval
  (set "output" (1 * 3 * (3 - 1))
     (set "input" (3 - 1)
        (set "output" (1 * 3)
           (set "output" 1 (set "input" 3 empty)))))
  ("input" <- "input" - 1) ?v' apply EvalAssign.interp
  (set "output" (1 * 3 * (3 - 1))
     (set "input" (3 - 1)
        (set "output" (1 * 3)
           (set "output" 1 (set "input" 3 empty)))))
  ("input" - 1)%arith ?n
                apply InterpMinus.interp
  (set "output" (1 * 3 * (3 - 1))
     (set "input" (3 - 1)
        (set "output" (1 * 3)
           (set "output" 1 (set "input" 3 empty)))))
  "input" ?n1
interp
  (set "output" (1 * 3 * (3 - 1))
     (set "input" (3 - 1)
        (set "output" (1 * 3)
           (set "output" 1 (set "input" 3 empty))))) 1
  ?n2
                **interp
  (set "output" (1 * 3 * (3 - 1))
     (set "input" (3 - 1)
        (set "output" (1 * 3)
           (set "output" 1 (set "input" 3 empty)))))
  "input" ?n1 apply InterpVarFound.get "input"
  (set "output" (1 * 3 * (3 - 1))
     (set "input" (3 - 1)
        (set "output" (1 * 3)
           (set "output" 1 (set "input" 3 empty))))) =
Some ?n1
                   reflexivity.
                **interp
  (set "output" (1 * 3 * (3 - 1))
     (set "input" (3 - 1)
        (set "output" (1 * 3)
           (set "output" 1 (set "input" 3 empty))))) 1
  ?n2 apply InterpConst.
          --eval
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty))))))
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v eapply EvalWhileTrue.interp
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty))))))
  "input" ?n
?n <> 0
eval
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty))))))
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v'
eval ?v'
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v
             ++interp
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty))))))
  "input" ?n apply InterpVarFound.get "input"
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty)))))) =
Some ?n
                reflexivity.
             ++3 - 1 - 1 <> 0 simpl; congruence.
             ++eval
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty))))))
  ("output" <- "output" * "input";;
   "input" <- "input" - 1) ?v' eapply EvalSeq.eval
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty))))))
  ("output" <- "output" * "input") ?v1
eval ?v1 ("input" <- "input" - 1) ?v'
                **eval
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty))))))
  ("output" <- "output" * "input") ?v1 apply EvalAssign.interp
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty))))))
  ("output" * "input")%arith ?n
                   apply InterpTimes.interp
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty))))))
  "output" ?n1
interp
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty))))))
  "input" ?n2
                   ---interp
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty))))))
  "output" ?n1 apply InterpVarFound.get "output"
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty)))))) =
Some ?n1
                       reflexivity.
                   ---interp
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty))))))
  "input" ?n2 apply InterpVarFound.get "input"
  (set "input" (3 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1))
        (set "input" (3 - 1)
           (set "output" (1 * 3)
              (set "output" 1 (set "input" 3 empty)))))) =
Some ?n2
                       reflexivity.
                **eval
  (set "output" (1 * 3 * (3 - 1) * (3 - 1 - 1))
     (set "input" (3 - 1 - 1)
        (set "output" (1 * 3 * (3 - 1))
           (set "input" (3 - 1)
              (set "output" (1 * 3)
                 (set "output" 1 (set "input" 3 empty)))))))
  ("input" <- "input" - 1) ?v' apply EvalAssign.interp
  (set "output" (1 * 3 * (3 - 1) * (3 - 1 - 1))
     (set "input" (3 - 1 - 1)
        (set "output" (1 * 3 * (3 - 1))
           (set "input" (3 - 1)
              (set "output" (1 * 3)
                 (set "output" 1 (set "input" 3 empty)))))))
  ("input" - 1)%arith ?n
                   apply InterpMinus.interp
  (set "output" (1 * 3 * (3 - 1) * (3 - 1 - 1))
     (set "input" (3 - 1 - 1)
        (set "output" (1 * 3 * (3 - 1))
           (set "input" (3 - 1)
              (set "output" (1 * 3)
                 (set "output" 1 (set "input" 3 empty)))))))
  "input" ?n1
interp
  (set "output" (1 * 3 * (3 - 1) * (3 - 1 - 1))
     (set "input" (3 - 1 - 1)
        (set "output" (1 * 3 * (3 - 1))
           (set "input" (3 - 1)
              (set "output" (1 * 3)
                 (set "output" 1 (set "input" 3 empty)))))))
  1 ?n2
                   ---interp
  (set "output" (1 * 3 * (3 - 1) * (3 - 1 - 1))
     (set "input" (3 - 1 - 1)
        (set "output" (1 * 3 * (3 - 1))
           (set "input" (3 - 1)
              (set "output" (1 * 3)
                 (set "output" 1 (set "input" 3 empty)))))))
  "input" ?n1 apply InterpVarFound.get "input"
  (set "output" (1 * 3 * (3 - 1) * (3 - 1 - 1))
     (set "input" (3 - 1 - 1)
        (set "output" (1 * 3 * (3 - 1))
           (set "input" (3 - 1)
              (set "output" (1 * 3)
                 (set "output" 1 (set "input" 3 empty))))))) =
Some ?n1
                       reflexivity.
                   ---interp
  (set "output" (1 * 3 * (3 - 1) * (3 - 1 - 1))
     (set "input" (3 - 1 - 1)
        (set "output" (1 * 3 * (3 - 1))
           (set "input" (3 - 1)
              (set "output" (1 * 3)
                 (set "output" 1 (set "input" 3 empty)))))))
  1 ?n2 apply InterpConst.
             ++eval
  (set "input" (3 - 1 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1) * (3 - 1 - 1))
        (set "input" (3 - 1 - 1)
           (set "output" (1 * 3 * (3 - 1))
              (set "input" (3 - 1)
                 (set "output" (1 * 3)
                    (set "output" 1
                       (set "input" 3 empty))))))))
  (while "input"
   loop "output" <- "output" * "input";;
        "input" <- "input" - 1 done) ?v eapply EvalWhileFalse.interp
  (set "input" (3 - 1 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1) * (3 - 1 - 1))
        (set "input" (3 - 1 - 1)
           (set "output" (1 * 3 * (3 - 1))
              (set "input" (3 - 1)
                 (set "output" (1 * 3)
                    (set "output" 1
                       (set "input" 3 empty))))))))
  "input" ?n
?n = 0
                **interp
  (set "input" (3 - 1 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1) * (3 - 1 - 1))
        (set "input" (3 - 1 - 1)
           (set "output" (1 * 3 * (3 - 1))
              (set "input" (3 - 1)
                 (set "output" (1 * 3)
                    (set "output" 1
                       (set "input" 3 empty))))))))
  "input" ?n apply InterpVarFound.get "input"
  (set "input" (3 - 1 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1) * (3 - 1 - 1))
        (set "input" (3 - 1 - 1)
           (set "output" (1 * 3 * (3 - 1))
              (set "input" (3 - 1)
                 (set "output" (1 * 3)
                    (set "output" 1
                       (set "input" 3 empty)))))))) =
Some ?n
                   reflexivity.
                **3 - 1 - 1 - 1 = 0 reflexivity.
    -get "output"
  (set "input" (3 - 1 - 1 - 1)
     (set "output" (1 * 3 * (3 - 1) * (3 - 1 - 1))
        (set "input" (3 - 1 - 1)
           (set "output" (1 * 3 * (3 - 1))
              (set "input" (3 - 1)
                 (set "output" (1 * 3)
                    (set "output" 1
                       (set "input" 3 empty)))))))) =
Some 6 reflexivity.

Thankfully, with just a few hints, we can get eauto to do all the work for us!

      Restart.exists v : valuation,
  eval (set "input" 3 empty) factorial v /\
  get "output" v = Some 6

      Hint Constructors interp eval : core.exists v : valuation,
  eval (set "input" 3 empty) factorial v /\
  get "output" v = Some 6
      Hint Extern 1 => (simpl; congruence) : core.exists v : valuation,
  eval (set "input" 3 empty) factorial v /\
  get "output" v = Some 6
      Hint Extern 1 => reflexivity : core.exists v : valuation,
  eval (set "input" 3 empty) factorial v /\
  get "output" v = Some 6

      unfold factorial.exists v : valuation,
  eval (set "input" 3 empty)
    ("output" <- 1;;
     while "input"
     loop "output" <- "output" * "input";;
          "input" <- "input" - 1 done) v /\
  get "output" v = Some 6
      debug eauto 50.(* debug eauto: *)
1 depth=50 
1.1 depth=49 simple eapply ex_intro
1.1.1 depth=48 simple apply conj
1.1.1.1 depth=47 simple eapply EvalSeq
1.1.1.1.1 depth=46 simple apply EvalAssign
1.1.1.1.1.1 depth=46 simple apply InterpConst
1.1.1.1.1.1.1 depth=45 simple eapply EvalWhileFalse
1.1.1.1.1.1.1.1 depth=44 simple apply InterpVarFound
1.1.1.1.1.1.1.1.1 depth=44 (*external*) reflexivity
1.1.1.1.1.1.1.2 depth=44
               simple apply InterpVarNotFound
1.1.1.1.1.1.2 depth=45 simple eapply EvalWhileTrue
1.1.1.1.1.1.2.1 depth=44 simple apply InterpVarFound
1.1.1.1.1.1.2.1.1 depth=44 (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1 depth=44
                   simple apply not_eq_sym ; trivial
1.1.1.1.1.1.2.1.1.1.1 depth=43 simple eapply EvalSeq
1.1.1.1.1.1.2.1.1.1.1.1 depth=42
                       simple apply EvalAssign
1.1.1.1.1.1.2.1.1.1.1.1.1 depth=41
                         simple apply InterpTimes
1.1.1.1.1.1.2.1.1.1.1.1.1.1 depth=40
                           simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1 depth=40
                             (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1 depth=39
                               simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1 depth=39
                                 (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1 depth=38
                                   simple apply EvalAssign
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1 depth=37
                                     simple apply InterpMinus
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=36
                                       simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=36
                                         (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=36
                                           simple apply InterpConst
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=35
                                             simple eapply EvalWhileFalse
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=34
                                               simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=34
                                                 (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2 depth=34
                                               simple apply InterpVarNotFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2 depth=35
                                             simple eapply EvalWhileTrue
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1 depth=34
                                               simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1 depth=34
                                                 (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1
 depth=34 (*external*) (simpl; congruence)
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1
 depth=33 simple eapply EvalSeq
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1
 depth=32 simple apply EvalAssign
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1
 depth=31 simple apply InterpTimes
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1
 depth=30 simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1
 depth=30 (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1
 depth=29 simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1
 depth=29 (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1
 depth=28 simple apply EvalAssign
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1
 depth=27 simple apply InterpMinus
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=26 simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=26 (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=26 simple apply InterpConst
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=25 simple eapply EvalWhileFalse
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=24 simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=24 (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2
 depth=24 simple apply InterpVarNotFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2
 depth=25 simple eapply EvalWhileTrue
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1
 depth=24 simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1
 depth=24 (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1
 depth=24 simple apply not_eq_sym ; trivial
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1
 depth=23 simple eapply EvalSeq
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1
 depth=22 simple apply EvalAssign
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1
 depth=21 simple apply InterpTimes
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1
 depth=20 simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1
 depth=20 (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1
 depth=19 simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1
 depth=19 (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1
 depth=18 simple apply EvalAssign
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1
 depth=17 simple apply InterpMinus
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=16 simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=16 (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=16 simple apply InterpConst
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=15 simple eapply EvalWhileFalse
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=14 simple apply InterpVarFound
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=14 (*external*) reflexivity
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=14 simple apply @eq_refl
1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1
 depth=14 simple apply @eq_refl
  Qed.
End Simple.

Backtracking without `auto`

We have now seen two forms of backtracking: eauto, and match goal with. Let us see a third one, with “multiple successes”.

Inductive EasyPeasy :=
| Nope0 (n: nat): n < 0 -> EasyPeasy
| Yep   (n: nat): n = 0 -> EasyPeasy
| Nope1 (n: nat): n < 0 -> EasyPeasy.

Note the order of constructors, chosen to trick constructor into trying Nope before Yep.

Hint Constructors EasyPeasy : core.

Goal EasyPeasy.EasyPeasy

Unsurprisingly, a plain application of econstructor does not solve the goal. In fact, it leaves an unprovable goal instead, because the argument of Nope0 is not satisfiable:

  econstructor.?n < 0

Uh oh.

  Restart.EasyPeasy

Also unsurprisingly, eauto solves the goal (it tries constructors in reverse order, but the order is irrelevant for correctness, since it backtracks after attempting Nope1):

  debug eauto.(* debug eauto: *)
1 depth=5 
1.1 depth=4 simple eapply Nope1
1.1.1 depth=3 unfold lt
1.2 depth=4 simple eapply Yep
1.2.1 depth=4 simple apply @eq_refl

More interesting is what happens if we chain the constructor tactic with another one:

  Restart.EasyPeasy
  econstructor; reflexivity.

The econstructor tactic produces a stream of proof states to attempt (one per applicable constructor, not just one for the first applicable constructor).

When the control flow reaches a period, all candidate states except the first are discarded.

Any time a tactic fails before reaching a period, however, the Ltac engine backtracks: it rewinds execution to the last ; and tries the next available proof state in the stream produced by earlier tactics.

Here reflexivity fails to solve the goal ?n < 0 (the result of applying Nope0), so the Ltac interpreter backtracks to the next state produced by constructor, which is ?n = 0 (the result of applying Yep). At this point, reflexivity completes the proof.

Another way to force backtracking is by inserting explicit failures. The following does not solve the goal, because eauto does not fail if it cannot solve the goal:

  Restart.EasyPeasy
  econstructor; eauto.?n < 0

In contrast, the following works, because the fail tactic forces backtracking:

  Restart.EasyPeasy
  econstructor; eauto; fail.

Or, we can create backtracking points by hand using the + operator:

  Restart.EasyPeasy
  (eapply Nope0 + eapply Yep + eapply Nope1); reflexivity.

… or, should we want to condition the application of any of the branches, we can create backtracking points with multimatch instead:

  Restart.EasyPeasy

  match goal with
       | _ => eapply Nope0
       | _ => eapply Yep
       end; reflexivity.The relation lt is not a declared reflexive relation. Maybe you need to require the Coq.Classes.RelationClasses library

  multimatch goal with
  | _ => eapply Nope0
  | _ => eapply Yep
  end; reflexivity.
Qed.

Note

Observing backtracking

Here is a quick and dirty way to observe the backtracking that Ltac performs: printing the goal with idtac:

Goal EasyPeasy.EasyPeasy
  econstructor;
    match goal with
    | [  |- ?g ] => idtac "The goal is:" g
    end;
    reflexivity.The goal is: (?n < 0)
The goal is: (?n = 0)
Qed.

Other operators that control backtracking, including once, first`, and [> … ], are documented in the reference manual.

Synthesizing Programs

Here is a simple syntax type for arithmetic expressions, similar to those we have used several times before. In this case, we allow expressions to mention exactly one distinguished variable.

Inductive exp : Set :=
| Const (n : nat)
| Var
| Plus (e1 e2 : exp).

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

Local Hint Constructors eval : core.

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

Example eval1 : forall var,
    eval var (Plus Var (Plus (Const 8) Var)) (var + (8 + var)).forall var : nat,
eval var (Plus Var (Plus (Const 8) Var))
  (var + (8 + var))
Proof.forall var : nat,
eval var (Plus Var (Plus (Const 8) Var))
  (var + (8 + var))
  auto.
Qed.

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

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

To help prove eval1', we prove an alternative 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 alternative 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.forall (var : nat) (e1 e2 : exp) (n1 n2 n : nat),
eval var e1 n1 ->
eval var e2 n2 ->
n1 + n2 = n -> eval var (Plus e1 e2) n
Proof.forall (var : nat) (e1 e2 : exp) (n1 n2 n : nat),
eval var e1 n1 ->
eval var e2 n2 ->
n1 + n2 = n -> eval var (Plus e1 e2) n
  intros; subst; auto.
Qed.

Local Hint Resolve EvalPlus' : core.

Further, we instruct eauto to apply ring, via Hint Extern. We should try this step for any equality goal.

Section use_ring.
  Hint Extern 1 (_ = _) => ring : core.

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).forall var : nat,
eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8)
  Proof.forall var : nat,
eval var (Plus Var (Plus (Const 8) Var)) (2 * var + 8)
    eauto.
  Qed.

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.

  Example synthesize1 : exists e, forall var, eval var e (var + 7).exists e : exp, forall var : nat, eval var e (var + 7)
  Proof.exists e : exp, forall var : nat, eval var e (var + 7)
    eauto.
  Qed.

  Print synthesize1.synthesize1 =
ex_intro
  (fun e : exp =>
   forall var : nat, eval var e (var + 7))
  (Plus Var (Const 7))
  (fun var : nat =>
   EvalPlus var Var (Const 7) var 7 (EvalVar var)
     (EvalConst var 7))
     : exists e : exp,
         forall var : nat, eval var e (var + 7)

Here are two more examples showing off our program-synthesis abilities.

  Example synthesize2 : exists e, forall var, eval var e (2 * var + 8).exists e : exp,
  forall var : nat, eval var e (2 * var + 8)
  Proof.exists e : exp,
  forall var : nat, eval var e (2 * var + 8)
    eauto.
  Qed.

  Print synthesize2.synthesize2 =
ex_intro
  (fun e : exp =>
   forall var : nat, eval var e (2 * var + 8))
  (Plus (Plus Var Var) (Const 8))
  (fun var : nat =>
   EvalPlus var (Plus Var Var) (Const 8) (2 * var) 8
     (EvalPlus' var Var Var var var (2 * var)
        (EvalVar var) (EvalVar var)
        (let hyp_list := nil in
         let fv_list := var :: nil in
         natr_ring_lemma1 ring_subst_niter fv_list
           hyp_list
           (Ring_polynom.PEadd
              (Ring_polynom.PEX BinNums.N BinNums.xH)
              (Ring_polynom.PEX BinNums.N BinNums.xH))
           (Ring_polynom.PEmul
              (Ring_polynom.PEc (BinNat.N.of_nat 2))
              (Ring_polynom.PEX BinNums.N BinNums.xH))
           I
           (eq_refl
            <:
            (let lmp :=
               Ring_polynom.mk_monpol_list BinNums.N0
                 (BinNums.Npos BinNums.xH)
                 BinNat.N.add BinNat.N.mul
                 BinNat.N.add (fun x : BinNums.N => x)
                 BinNat.N.eqb BinNat.N.div_eucl
                 hyp_list in
             Ring_polynom.Peq BinNat.N.eqb
               (Ring_polynom.norm_subst BinNums.N0
                  (BinNums.Npos BinNums.xH)
                  BinNat.N.add BinNat.N.mul
                  BinNat.N.add
                  (fun x : BinNums.N => x)
                  BinNat.N.eqb BinNat.N.div_eucl
                  ring_subst_niter lmp
                  (Ring_polynom.PEadd
                     (Ring_polynom.PEX BinNums.N
                        BinNums.xH)
                     (Ring_polynom.PEX BinNums.N
                        BinNums.xH)))
               (Ring_polynom.norm_subst BinNums.N0
                  (BinNums.Npos BinNums.xH)
                  BinNat.N.add BinNat.N.mul
                  BinNat.N.add
                  (fun x : BinNums.N => x)
                  BinNat.N.eqb BinNat.N.div_eucl
                  ring_subst_niter lmp
                  (Ring_polynom.PEmul
                     (Ring_polynom.PEc
                        (BinNat.N.of_nat 2))
                     (Ring_polynom.PEX BinNums.N
                        BinNums.xH)))) = true)))
     (EvalConst var 8))
     : exists e : exp,
         forall var : nat, eval var e (2 * var + 8)

  Example synthesize3 : exists e, forall var, eval var e (3 * var + 42).exists e : exp,
  forall var : nat, eval var e (3 * var + 42)
  Proof.exists e : exp,
  forall var : nat, eval var e (3 * var + 42)
    eauto.
  Qed.

  Print synthesize3.synthesize3 =
ex_intro
  (fun e : exp =>
   forall var : nat, eval var e (3 * var + 42))
  (Plus (Plus Var (Plus Var Var)) (Const 42))
  (fun var : nat =>
   EvalPlus var (Plus Var (Plus Var Var)) (Const 42)
     (3 * var) 42
     (EvalPlus' var Var (Plus Var Var) var (var + var)
        (3 * var) (EvalVar var)
        (EvalPlus var Var Var var var (EvalVar var)
           (EvalVar var))
        (let hyp_list := nil in
         let fv_list := var :: nil in
         natr_ring_lemma1 ring_subst_niter fv_list
           hyp_list
           (Ring_polynom.PEadd
              (Ring_polynom.PEX BinNums.N BinNums.xH)
              (Ring_polynom.PEadd
                 (Ring_polynom.PEX BinNums.N
                    BinNums.xH)
                 (Ring_polynom.PEX BinNums.N
                    BinNums.xH)))
           (Ring_polynom.PEmul
              (Ring_polynom.PEc (BinNat.N.of_nat 3))
              (Ring_polynom.PEX BinNums.N BinNums.xH))
           I
           (eq_refl
            <:
            (let lmp :=
               Ring_polynom.mk_monpol_list BinNums.N0
                 (BinNums.Npos BinNums.xH)
                 BinNat.N.add BinNat.N.mul
                 BinNat.N.add (fun x : BinNums.N => x)
                 BinNat.N.eqb BinNat.N.div_eucl
                 hyp_list in
             Ring_polynom.Peq BinNat.N.eqb
               (Ring_polynom.norm_subst BinNums.N0
                  (BinNums.Npos BinNums.xH)
                  BinNat.N.add BinNat.N.mul
                  BinNat.N.add
                  (fun x : BinNums.N => x)
                  BinNat.N.eqb BinNat.N.div_eucl
                  ring_subst_niter lmp
                  (Ring_polynom.PEadd
                     (Ring_polynom.PEX BinNums.N
                        BinNums.xH)
                     (Ring_polynom.PEadd
                        (Ring_polynom.PEX BinNums.N
                           BinNums.xH)
                        (Ring_polynom.PEX BinNums.N
                           BinNums.xH))))
               (Ring_polynom.norm_subst BinNums.N0
                  (BinNums.Npos BinNums.xH)
                  BinNat.N.add BinNat.N.mul
                  BinNat.N.add
                  (fun x : BinNums.N => x)
                  BinNat.N.eqb BinNat.N.div_eucl
                  ring_subst_niter lmp
                  (Ring_polynom.PEmul
                     (Ring_polynom.PEc
                        (BinNat.N.of_nat 3))
                     (Ring_polynom.PEX BinNums.N
                        BinNums.xH)))) = true)))
     (EvalConst var 42))
     : exists e : exp,
         forall var : nat, eval var e (3 * var + 42)
End use_ring.

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.forall var n m : nat, n = m -> eval var (Const n) m
Proof.forall var n m : nat, n = m -> eval var (Const n) m
  intros; subst; auto.
Qed.

Theorem EvalVar' : forall var n,
  var = n
  -> eval var Var n.forall var n : nat, var = n -> eval var Var n
Proof.forall var n : nat, var = n -> eval var Var n
  intros; subst; auto.
Qed.

Local Hint Resolve EvalConst' EvalVar' : core.

Next, we prove a few hints that feel a bit like cheating, as they telegraph 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.

Section cheap_hints.
  Theorem zero_times : forall n m r,
    r = m
    -> r = 0 * n + m.forall n m r : nat, r = m -> r = 0 * n + m
  Proof.forall n m r : nat, r = m -> r = 0 * n + m
    lia.
  Qed.

  Theorem plus_0 : forall n r,
    r = n
    -> r = n + 0.forall n r : nat, r = n -> r = n + 0
  Proof.forall n r : nat, r = n -> r = n + 0
    lia.
  Qed.

  Theorem times_1 : forall n, n = 1 * n.forall n : nat, n = 1 * n
  Proof.forall n : nat, n = 1 * n
    lia.
  Qed.

  Theorem combine : forall x k1 k2 n1 n2,
    (k1 * x + n1) + (k2 * x + n2) = (k1 + k2) * x + (n1 + n2).forall x k1 k2 n1 n2 : nat,
k1 * x + n1 + (k2 * x + n2) =
(k1 + k2) * x + (n1 + n2)
  Proof.forall x k1 k2 n1 n2 : nat,
k1 * x + n1 + (k2 * x + n2) =
(k1 + k2) * x + (n1 + n2)
    intros; ring.
  Qed.

  Hint Resolve zero_times plus_0 times_1 combine : core.

  Theorem linear : forall e, exists k n,
    forall var, eval var e (k * var + n).forall e : exp,
exists k n : nat,
  forall var : nat, eval var e (k * var + n)
  Proof.forall e : exp,
exists k n : nat,
  forall var : nat, eval var e (k * var + n)
    induction e; firstorder eauto.
  Qed.
End cheap_hints.

Let's try that again, without using those hints that give away the answer. We should be able to coerce Coq into doing more of the thinking for us.

First, we will want to be able to use built-in tactic ring_simplify on goals that contain unification variables, which will be the case at intermediate points in our proof search. We also want a bit more standardization on ordering of variables within multiplications, to increase the odds that different calculations can unify with each other. Here is a tactic that realizes those wishes.

Ltac robust_ring_simplify :=
  (* First, introduce regular names for all unification variables,
     because `ring_simplify` freaks out when it meets a unification
     variable. *)

  repeat match goal with
         | [ |- context[?v] ] => is_evar v; remember v
         end;

  (* Now call the standard tactic. *)

  ring_simplify;

  (* Replace uses of the new variables with the original unification
     variables. *)
  subst;

  (* Find and correct cases where commutativity doesn't agree across
     subterms of the goal. *)
  repeat match goal with
         | [ |- context[?X * ?Y] ] =>
           match goal with
           | [ |- context[?Z * X] ] => rewrite (Nat.mul_comm Z X)
           end
         end.

This tactic is pretty expensive, but let's try it eventually whenever the goal is an equality.

Local Hint Extern 5 (_ = _) => robust_ring_simplify : core.

The only other missing ingredient is priming Coq with some good ideas for instantiating existential quantifiers. These will all be tried in some order, in a particular proof search.

Local Hint Extern 1 (exists n : nat, _) => exists 0 : core.
Local Hint Extern 1 (exists n : nat, _) => exists 1 : core.
Local Hint Extern 1 (exists n : nat, _) => eexists (_ + _) : core.

Note how this last hint uses eexists to provide an instantiation with wildcards inside it. Each underscore is replaced with a fresh unification variable.

Now Coq figures out the recipe for us, and quite quickly, at that!

Theorem linear_snazzy : forall e, exists k n,
  forall var, eval var e (k * var + n).forall e : exp,
exists k n : nat,
  forall var : nat, eval var e (k * var + n)
Proof.forall e : exp,
exists k n : nat,
  forall var : nat, eval var e (k * var + n)
  induction e; firstorder eauto.
Qed.

Here's a quick tease using a feature that we'll explore fully in a later class. Let's use a mysterious construct sigT instead of exists.

Local Hint Extern 1 (sigT (fun n : nat => _)) => exists 0 : core.
Local Hint Extern 1 (sigT (fun n : nat => _)) => exists 1 : core.
Local Hint Extern 1 (sigT (fun n : nat => _)) => eexists (_ + _) : core.

Theorem linear_computable : forall e, sigT (fun k => sigT (fun n =>
  forall var, eval var e (k * var + n))).forall e : exp,
{k : nat &
{n : nat & forall var : nat, eval var e (k * var + n)}}
Proof.forall e : exp,
{k : nat &
{n : nat & forall var : nat, eval var e (k * var + n)}}
  induction e; firstorder eauto.
Defined.

Essentially the same proof search has completed. This time, though, we ended the proof with Defined, which saves it as transparent, so details of the "proof" can be consulted from the outside. Actually, this "proof" is more like a recursive program that finds k and n, given e! Let's add a wrapper to make that idea more concrete.

Definition params (e : exp) : nat * nat :=
  let '(existT _ k (existT _ n _)) := linear_computable e in
  (k, n).

Now we can actually run our proof to get normalized versions of particular expressions.

Compute params (Plus (Const 7) (Plus Var (Plus (Const 8) Var))).= (2, 15)
: nat * nat

With Coq doing so much of the proof-search work for us, we might get complacent and consider that any successful eauto invocation is as good as any other. However, because introduced unification variables may wind up spread across multiple subgoals, running eauto can have a surprising kind of side effect across goals! When a proof isn't solved completely by one eauto call, the cross-subgoal side effects can break proofs that used to work, when we introduce new premises or hints. Here's an illustrative example.

Section side_effect_sideshow.
  Variable A : Set.
  Variables P Q : A -> Prop.
  Variable x : A.

  Hypothesis Px : P x.
  Hypothesis Qx : Q x.

  Theorem double_threat : exists y, P y /\ Q y.A: Set
P, Q: A -> Prop
x: A
Px: P x
Qx: Q x
exists y : A, P y /\ Q y
  Proof.A: Set
P, Q: A -> Prop
x: A
Px: P x
Qx: Q x
exists y : A, P y /\ Q y
    eexists; split.A: Set
P, Q: A -> Prop
x: A
Px: P x
Qx: Q x
P ?y
A: Set
P, Q: A -> Prop
x: A
Px: P x
Qx: Q x
Q ?y
    eauto.A: Set
P, Q: A -> Prop
x: A
Px: P x
Qx: Q x
Q x
    eauto.
  Qed.

That was easy enough. eauto could have solved the whole thing, but humor me by considering this slightly less-automated proof. Watch what happens when we add a new premise.

  Variable z : A.
  Hypothesis Pz : P z.

  Theorem double_threat' : exists y, P y /\ Q y.A: Set
P, Q: A -> Prop
x: A
Px: P x
Qx: Q x
z: A
Pz: P z
exists y : A, P y /\ Q y
  Proof.A: Set
P, Q: A -> Prop
x: A
Px: P x
Qx: Q x
z: A
Pz: P z
exists y : A, P y /\ Q y
    eexists; split.A: Set
P, Q: A -> Prop
x: A
Px: P x
Qx: Q x
z: A
Pz: P z
P ?y
A: Set
P, Q: A -> Prop
x: A
Px: P x
Qx: Q x
z: A
Pz: P z
Q ?y
    eauto.A: Set
P, Q: A -> Prop
x: A
Px: P x
Qx: Q x
z: A
Pz: P z
Q z
    eauto.A: Set
P, Q: A -> Prop
x: A
Px: P x
Qx: Q x
z: A
Pz: P z
Q z

Oh no! The second subgoal isn't true anymore, because the first eauto now matched Pz instead of Px.

  Restart.A: Set
P, Q: A -> Prop
x: A
Px: P x
Qx: Q x
z: A
Pz: P z
exists y : A, P y /\ Q y
    eauto.

eauto can still find the whole proof, though.

  Qed.
End side_effect_sideshow.

Again, the moral of the story is: while proof search in Coq often feels purely functional, unification variables allow imperative side effects to reach across subgoals. That's a tremendously useful feature for effective proof automation, but it can also sneak up on you at times.

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 a proof script using auto or eauto can automatically adapt to presence of new hints.

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
Hint Resolve lemma, which does the same but may add new premises that are themselves to be subjects of nested proof search
Hint Constructors pred, which acts like Resolve applied to every constructor of an inductive predicate
Hint 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.

Theorem bool_neq : true <> false.true <> false
Proof.true <> false
  auto.true <> false

No luck so far.

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 equality tactic.

Local Hint Extern 1 (_ <> _) => congruence : core.

Theorem bool_neq : true <> false.true <> false
Proof.true <> false
  auto.
Qed.

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.A: Set
P, Q: A -> Prop
both: forall x : A, P x /\ Q x
forall z : A, P z
  Proof.A: Set
P, Q: A -> Prop
both: forall x : A, P x /\ Q x
forall z : A, P z
    auto.A: Set
P, Q: A -> Prop
both: forall x : A, P x /\ Q x
forall z : A, P z

The auto invocation makes no progress beyond what intros would have accomplished. An auto call 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 : core.

    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.

End forall_and.

After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates P.

Local Hint Extern 1 (?P ?X) =>
  match goal with
    | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
  end : core.Head pattern or sub-pattern must be a global constant, a section variable, an if, case, or let expression, an application, or a projection.

Coq's auto hint databases work as tables mapping 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 (x = y); and, in the second example, the head symbol was P.

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.

Local Hint Extern 1 =>
  match goal with
    | [ H : forall x, ?P x /\ _ |- ?P ?X ] => apply (proj1 (H X))
  end : core.

Be forewarned that a Hint Extern of this kind will be applied at every node of a proof tree, so an expensive Ltac script may slow proof search significantly.

Rewrite Hints

Another dimension of extensibility with hints is rewriting with quantified equalities. We have used the associated command Hint Rewrite in several examples so far. The simplify 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.

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.A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
forall x : A, f (f (f x)) = f x
  Proof.A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
forall x : A, 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.A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
g: A -> A
f_g: forall x : A, f x = g x
forall x : A, f (f (f x)) = f x
    Proof.A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
g: A -> A
f_g: forall x : A, f x = g x
forall x : A, f (f (f x)) = f x
      intros; autorewrite with core.A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
g: A -> A
f_g: forall x : A, f x = g x
x: A
g (g (g x)) = g x
    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.

  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.

  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.A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
P: A -> Prop
g: A -> A
f_g: forall x : A, P x -> f x = g x
forall x : A, f (f (f x)) = f x
    Proof.A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
P: A -> Prop
g: A -> A
f_g: forall x : A, P x -> f x = g x
forall x : A, f (f (f x)) = f x
      intros; autorewrite with core.A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
P: A -> Prop
g: A -> A
f_g: forall x : A, P x -> f x = g x
x: A
g (g (g x)) = g x
A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
P: A -> Prop
g: A -> A
f_g: forall x : A, P x -> f x = g x
x: A
P x
A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
P: A -> Prop
g: A -> A
f_g: forall x : A, P x -> f x = g x
x: A
P (f x)
A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
P: A -> Prop
g: A -> A
f_g: forall x : A, P x -> f x = g x
x: A
P (f (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.

  Reset garden_path.

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.A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
P: A -> Prop
g: A -> A
f_g: forall x : A, P x -> f x = g x
forall x : A, f (f (f x)) = f x
    Proof.A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
P: A -> Prop
g: A -> A
f_g: forall x : A, P x -> f x = g x
forall x : A, 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.A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
P: A -> Prop
g: A -> A
f_g: forall x : A, P x -> f x = g x
forall x : A, P x -> f (f x) = g x
    Proof.A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
P: A -> Prop
g: A -> A
f_g: forall x : A, P x -> f x = g x
forall x : A, 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)).A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
forall x y : A,
f (f (f (f x))) = f (f y) -> f x = f (f (f y))
  Proof.A: Set
f: A -> A
f_f: forall x : A, f (f x) = f x
forall x y : A,
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.