1 files changed, 45 insertions, 0 deletions
diff --git a/content/zettel/3b5.md b/content/zettel/3b5.md
new file mode 100644
index 0000000..82551fd
--- /dev/null
+++ b/content/zettel/3b5.md
@@ -0,0 +1,45 @@
++++
+title = "Proof search by logic programming"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3b4"]
+forwardlinks = ["3b6", "3b5a"]
+zettelid = "3b5"
++++
+
+Proof search is simpler than automatic programming because any proof is
+good enough for the current goal, whereas not every program is good
+enough for the specification. That is why proof search is useful and
+should be used to find proofs in theorem provers.
+
+The `Hint Constructors` construct can be used to add hints for
+constructors for inductive types, so that auto can solve these
+automatically.
+
+There are two main important functions that are performed during proof
+search, unification and backtracking. Backtracking is performed by
+`auto`, where it will go back and try different values for a tactic.
+However, it does not perform unification. This is done by the `eauto`
+tactic instead, as it can lead to an explosion of proof terms that have
+to be considered. Unifications of variables are, for example, placing a
+unification variable into an existential and then proceeding.
+
+`Hint Immediate` can be used for `auto` to consider lemmas at the leaf
+nodes of a tree. To let `auto` consider them at any level in the search
+tree, `Hint
+Resolve` can be used instead.
+
+One problem that can greatly increase the search tree to find a possible
+solution is the use of transitivity, which can break existing proofs or
+increase the time taken to prove them dramatically.
+
+If hints such as transitivity are needed in `auto` to solve a particular
+proof, they can be added using `eauto with trans`. This way it does not
+pollute the hint database in cases this lemma is not needed.
+
+`Hint Extern` can be used to define custom matching rules with a
+priority in which they are attempted. Lower numbers will be attempted
+before higher numbers. For example,
+`Hint Extern 1 (sum _ = _) => simpl.` will run `simpl` whenever the
+pattern before the `=>` is encountered.