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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
|
.. _decisionprocedures:
==============================
Solvers for logic and equality
==============================
.. tacn:: tauto
This tactic implements a decision procedure for intuitionistic propositional
calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff
:cite:`Dyc92`. Note that :tacn:`tauto` succeeds on any instance of an
intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and
logical equivalence but does not unfold any other definition.
.. example::
The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would
fail:
.. coqtop:: reset all
Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x.
intros.
tauto.
Moreover, if it has nothing else to do, :tacn:`tauto` performs introductions.
Therefore, the use of :tacn:`intros` in the previous proof is unnecessary.
:tacn:`tauto` can for instance for:
.. example::
.. coqtop:: reset all
Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) -> forall x:nat, ~ A -> P x.
tauto.
.. note::
In contrast, :tacn:`tauto` cannot solve the following goal
:g:`Goal forall (A:Prop) (P:nat -> Prop), A \/ (forall x:nat, ~ A -> P x) ->`
:g:`forall x:nat, ~ ~ (A \/ P x).`
because :g:`(forall x:nat, ~ A -> P x)` cannot be treated as atomic and
an instantiation of `x` is necessary.
.. tacn:: dtauto
While :tacn:`tauto` recognizes inductively defined connectives isomorphic to
the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``,
``Empty_set``, ``unit`` and ``True``, :tacn:`dtauto` also recognizes all inductive
types with one constructor and no indices, i.e. record-style connectives.
.. todo would be nice to explain/discuss the various types of flags
that define the differences between these tactics. See Tauto.v/tauto.ml.
.. tacn:: intuition {? @ltac_expr }
Uses the search tree built by the decision procedure for :tacn:`tauto`
to generate a set of subgoals equivalent to the original one (but
simpler than it) and applies :n:`@ltac_expr` to them :cite:`Mun94`. If
:n:`@ltac_expr` is not specified, it defaults to :n:`auto with *`
If :n:`@ltac_expr` fails on some goals then :tacn:`intuition` fails. In fact,
:tacn:`tauto` is simply :g:`intuition fail`.
:tacn:`intuition` recognizes inductively defined connectives
isomorphic to the standard connectives ``and``, ``prod``, ``or``, ``sum``, ``False``,
``Empty_set``, ``unit`` and ``True``.
.. example::
For instance, the tactic :g:`intuition auto` applied to the goal::
(forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O
internally replaces it by the equivalent one::
(forall (x:nat), P x), B |- P O
and then uses :tacn:`auto` which completes the proof.
.. tacn:: dintuition {? @ltac_expr }
In addition to the inductively defined connectives recognized by :tacn:`intuition`,
:tacn:`dintuition` also recognizes all inductive
types with one constructor and no indices, i.e. record-style connectives.
.. flag:: Intuition Negation Unfolding
Controls whether :tacn:`intuition` unfolds inner negations which do not need
to be unfolded. The flag is on by default.
.. tacn:: rtauto
Solves propositional tautologies similarly to
:tacn:`tauto`, but the proof term is built using a
reflection scheme applied to a sequent calculus proof of the goal. The search
procedure is also implemented using a different technique.
Users should be aware that this difference may result in faster proof search
but slower proof checking, and :tacn:`rtauto` might not solve goals that
:tacn:`tauto` would be able to solve (e.g. goals involving universal
quantifiers).
Note that this tactic is only available after a ``Require Import Rtauto``.
.. tacn:: firstorder {? @ltac_expr } {? using {+, @qualid } } {? with {+ @ident } }
An experimental extension of :tacn:`tauto` to
first-order reasoning. It is not restricted to
usual logical connectives but instead can reason about any first-order class
inductive definition.
:token:`ltac_expr`
Tries to solve the goal with :token:`ltac_expr` when no logical rule applies.
If unspecified, the tactic uses the default from the :opt:`Firstorder Solver`
option.
:n:`using {+, @qualid }`
Adds the lemmas :n:`{+, @qualid }` to the proof search environment. If :n:`@qualid`
refers to an inductive type, its constructors are
added to the proof search environment.
:n:`with {+ @ident }`
Adds lemmas from :tacn:`auto` hint bases :n:`{+ @ident }` to the proof search
environment.
.. opt:: Firstorder Solver @ltac_expr
The default tactic used by :tacn:`firstorder` when no rule applies in
:g:`auto with core`. It can be set locally or globally using this option.
.. cmd:: Print Firstorder Solver
Prints the default tactic used by :tacn:`firstorder` when no rule applies.
.. opt:: Firstorder Depth @natural
Controls the proof search depth bound.
.. tacn:: congruence {? @natural } {? with {+ @one_term } }
:token:`natural`
Specifies the maximum number of hypotheses stating quantified equalities that may be added
to the problem in order to solve it. The default is 1000.
:n:`{? with {+ @one_term } }`
Adds :n:`{+ @one_term }` to the pool of terms used by :tacn:`congruence`. This helps
in case you have partially applied constructors in your goal.
Implements the standard
Nelson and Oppen congruence closure algorithm, which is a decision procedure
for ground equalities with uninterpreted symbols. It also includes
constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal
is a non-quantified equality, congruence tries to prove it with non-quantified
equalities in the context. Otherwise it tries to infer a discriminable equality
from those in the context. Alternatively, congruence tries to prove that a
hypothesis is equal to the goal or to the negation of another hypothesis.
:tacn:`congruence` is also able to take advantage of hypotheses stating
quantified equalities, but you have to provide a bound for the number of extra
equalities generated that way. Please note that one of the sides of the
equality must contain all the quantified variables in order for congruence to
match against it.
Increasing the maximum number of hypotheses may solve
problems that would have failed with a smaller value. It will make failures slower but it
won't make successes found with the smaller value any slower.
You may want to use :tacn:`assert` to add some lemmas as
hypotheses so that :tacn:`congruence` can use them.
.. example::
.. coqtop:: reset all
Theorem T (A:Type) (f:A -> A) (g: A -> A -> A) a b: a=(f a) -> (g b (f a))=(f (f a)) -> (g a b)=(f (g b a)) -> (g a b)=a.
intros.
congruence.
Qed.
Theorem inj (A:Type) (f:A -> A * A) (a c d: A) : f = pair a -> Some (f c) = Some (f d) -> c=d.
intros.
congruence.
Qed.
.. exn:: I don’t know how to handle dependent equality.
The decision procedure managed to find a proof of the goal or of a
discriminable equality but this proof could not be built in Coq because of
dependently-typed functions.
.. exn:: Goal is solvable by congruence but some arguments are missing. Try congruence with {+ @term}, replacing metavariables by arbitrary terms.
The decision procedure could solve the goal with the provision that additional
arguments are supplied for some partially applied constructors. Any term of an
appropriate type will allow the tactic to successfully solve the goal. Those
additional arguments can be given to congruence by filling in the holes in the
terms given in the error message, using the `with` clause.
:opt:`Debug` ``"congruence"`` makes :tacn:`congruence` print debug information.
.. tacn:: btauto
The tactic :tacn:`btauto` implements a reflexive solver for boolean
tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are
constructed over the following grammar:
.. prodn::
btauto_term ::= @ident
| true
| false
| orb @btauto_term @btauto_term
| andb @btauto_term @btauto_term
| xorb @btauto_term @btauto_term
| negb @btauto_term
| if @btauto_term then @btauto_term else @btauto_term
Whenever the formula supplied is not a tautology, it also provides a
counter-example.
Internally, it uses a system very similar to the one of the ring
tactic.
Note that this tactic is only available after a ``Require Import Btauto``.
.. exn:: Cannot recognize a boolean equality.
The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto`
doesn't introduce variables into the context on its own.
|
