(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
  * Supplementary Coq material: unification and logic programming
  * Author: Adam Chlipala
  * License: https://creativecommons.org/licenses/by-nc-nd/4.0/
  * Much of the material comes from CPDT <http://adam.chlipala.net/cpdt/> by the same author. *)

Require Import Frap.

Set Implicit Arguments.


(** * Introducing Logic Programming *)

(* Recall the definition of addition from the standard library. *)

Definition real_plus := Eval compute in plus.
Print real_plus.

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

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

(* Recall that Coq will automatically derive the induction principle for 
 * inductives. For example: *)
 
Check nat_ind.
Check list_ind.

(* Similarly we have a induction principle for plusR. *)

Check plusR_ind.

(* 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).
Proof.
  induct n; simplify.

  constructor.

  constructor.
  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: *)

Hint Constructors plusR.

(* 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).
Proof.
  induct n; simplify; auto.
Qed.

Theorem plusR_plus : forall n m r,
  plusR n m r
  -> r = n + m.
Proof.
  induct 1;
  (* [induct 1] instructs Coq to perform induction on the first hypothesis of the theorem, which is [plusR n m r]. *) 
  simplify; linear_arithmetic.
Qed.

(* With the functional definition of [plus], simple equalities about arithmetic
 * follow by computation. *)

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

Print four_plus_three.

(* 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.
  Fail apply PlusO.
  apply PlusS.
  Fail apply PlusO.
  apply PlusS.
  Fail apply PlusO.
  apply PlusS.
  Fail apply PlusO.
  apply PlusS.
  apply PlusO.

  (* 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].  Thus, [auto] is another great match! *)
Restart.
  auto.
Qed.

Print four_plus_three'.

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

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

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

Example seven_minus_three : exists x, x + 3 = 7.
Proof.
  (* 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.
  Fail reflexivity.

  (* This seems to be a dead end.  Let us _backtrack_ to the point where we ran
   * [apply] and make a better alternative 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. *)

Example seven_minus_three' : exists x, plusR x 3 7.
Proof.
  (* 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.
  (* [eapply H]: like [apply], but works when it is not obvious how to
   * instantiate the quantifiers of theorem/hypothesis [H].  Instead,
   * placeholders are inserted for those quantifiers, to be determined
   * later. *)

  (* 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.
  apply PlusS. apply PlusS. apply PlusS.
  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.
  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. *)

Example seven_minus_four' : exists x, plusR 4 x 7.
Proof.
  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 [SearchRewrite] command to find a library function proving
 * an equality whose lefthand or righthand side matches a pattern with
 * wildcards. *)

SearchRewrite (O + _).

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

Hint Immediate plus_O_n.

(* The counterpart to [PlusS] we will prove ourselves. *)

Lemma plusS : forall n m r,
  n + m = r
  -> S n + m = S r.
Proof.
  linear_arithmetic.
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. *)

Hint Resolve plusS.

(* 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.
Proof.
  eauto 6.
Qed.

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

Example seven_minus_four_zero : exists x, 4 + x + 0 = 7.
Proof.
  eauto 6.
Abort.

(* A further lemma will be helpful. *)

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

Hint Resolve plusO.

(* 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.
Proof.
  eauto 7.
Qed.

(* 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.

(* 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.

  (* 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.
    Time eauto 1.
    Time eauto 2.
    Time eauto 3.
    Time eauto 4.
    Time eauto 5.

    (* 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.
  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]. *)

Hint Resolve eq_trans : slow.

Example from_one_to_zero : exists x, 1 + x = 0.
Proof.
  Time eauto.
  (* 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.
Proof.
  Time eauto 6.
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.
Proof.
  info_eauto with slow.
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.

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

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

Print length_1_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.
Proof.
  simplify; equality.
Qed.

Theorem length_S : forall A (h : A) t n,
  length t = n
  -> length (h :: t) = S n.
Proof.
  simplify; equality.
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.) *)

Example length_is_2 : exists ls : list nat, length ls = 2.
Proof.
  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, 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.
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.

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

(* We can see which list [eauto] found by printing the proof term. *)

Print length_is_2.

(* 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.
Proof.
  linear_arithmetic.
Qed.

Hint Resolve plusO'.

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

Hint Extern 1 (sum _ = _) => simplify.

(* 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.
Proof.
  eauto 7.
Qed.

Print length_and_sum.

(* 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.
Proof.
  eauto 15.
Qed.

Print length_and_sum'.

(* 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.
Proof.
  eauto 11.
Qed.

Print length_and_sum''.

(* We could continue through exercises of this kind, but even more interesting
 * than finding lists automatically is finding _programs_ automatically. *)


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

Hint Constructors eval.

(* 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)).
Proof.
  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).
Proof.
  eauto.
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.
Proof.
  simplify; subst; auto.
Qed.

Hint Resolve EvalPlus'.

(* 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.

  (* 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).
  Proof.
    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).
  Proof.
    eauto.
  Qed.

  Print synthesize1.

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

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

  Print synthesize2.

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

  Print synthesize3.
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.
Proof.
  simplify; subst; auto.
Qed.

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

Hint Resolve EvalConst' EvalVar'.

(* 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.
  Proof.
    linear_arithmetic.
  Qed.

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

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

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

  Hint Resolve zero_times plus_0 times_1 combine.

  Theorem linear : forall e, exists k n,
    forall var, eval var e (k * var + n).
  Proof.
    induct e; first_order; 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 (mult_comm Z X)
           end
         end.

(* This tactic is pretty expensive, but let's try it eventually whenever the
 * goal is an equality. *)
Hint Extern 5 (_ = _) => robust_ring_simplify.

(* 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. *)
Hint Extern 1 (exists n : nat, _) => exists 0.
Hint Extern 1 (exists n : nat, _) => exists 1.
Hint Extern 1 (exists n : nat, _) => eexists (_ + _).
(* 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).
Proof.
  induct e; first_order; 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]. *)

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

Theorem linear_computable : forall e, sigT (fun k => sigT (fun n =>
  forall var, eval var e (k * var + n))).
Proof.
  induct e; first_order; 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))).


(* 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.
  Proof.
    eexists; propositional.
    eauto.
    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.
  Proof.
    eexists; propositional.
    eauto.
    eauto.
    (* Oh no!  The second subgoal isn't true anymore, because the first [eauto]
     * now matched [Pz] instead of [Px]. *)
  Restart.
    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.
Proof.
  auto.
  (* 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. *)

Hint Extern 1 (_ <> _) => equality.

Theorem bool_neq : true <> false.
Proof.
  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.
  Proof.
    auto.

    (* 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.

    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]. *)
Fail 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 _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. *)

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

(* 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.
  Proof.
    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.
    Proof.
      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. *)

  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.
    Proof.
      intros; autorewrite with core.
    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.
    Proof.
      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.
    Proof.
      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)).
  Proof.
    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]. *)