blob: 82551fd18536a9f2c27b6aef847d602bd5b3c91d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
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.
|
