Solvers for logic and equality¶

Tactic
tauto
¶ This tactic implements a decision procedure for intuitionistic propositional calculus based on the contractionfree sequent calculi LJT* of Roy Dyckhoff [Dyc92]. Note that
tauto
succeeds on any instance of an intuitionistic tautological proposition.tauto
unfolds negations and logical equivalence but does not unfold any other definition.Example
The following goal can be proved by
tauto
whereasauto
would fail: Goal forall (x:nat) (P:nat > Prop), x = 0 \/ P x > x <> 0 > P x.
 1 goal ============================ forall (x : nat) (P : nat > Prop), x = 0 \/ P x > x <> 0 > P x
 intros.
 1 goal x : nat P : nat > Prop H : x = 0 \/ P x H0 : x <> 0 ============================ P x
 tauto.
 No more goals.
Moreover, if it has nothing else to do,
tauto
performs introductions. Therefore, the use ofintros
in the previous proof is unnecessary.tauto
can for instance for:Example
 Goal forall (A:Prop) (P:nat > Prop), A \/ (forall x:nat, ~ A > P x) > forall x:nat, ~ A > P x.
 1 goal ============================ forall (A : Prop) (P : nat > Prop), A \/ (forall x : nat, ~ A > P x) > forall x : nat, ~ A > P x
 tauto.
 No more goals.
Note
In contrast,
tauto
cannot solve the following goalGoal forall (A:Prop) (P:nat > Prop), A \/ (forall x:nat, ~ A > P x) >
forall x:nat, ~ ~ (A \/ P x).
because(forall x:nat, ~ A > P x)
cannot be treated as atomic and an instantiation ofx
is necessary.

Tactic
intuition ltac_expr?
¶ Uses the search tree built by the decision procedure for
tauto
to generate a set of subgoals equivalent to the original one (but simpler than it) and appliesltac_expr
to them [Mun94]. Ifltac_expr
is not specified, it defaults toauto with *
Ifltac_expr
fails on some goals thenintuition
fails. In fact,tauto
is simplyintuition fail
.intuition
recognizes inductively defined connectives isomorphic to the standard connectivesand
,prod
,or
,sum
,False
,Empty_set
,unit
andTrue
.Example
For instance, the tactic
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
auto
which completes the proof.
Tactic
dintuition ltac_expr?
¶ In addition to the inductively defined connectives recognized by
intuition
,dintuition
also recognizes all inductive types with one constructor and no indices, i.e. recordstyle connectives.

Tactic

Tactic
rtauto
¶ Solves propositional tautologies similarly to
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
rtauto
might not solve goals thattauto
would be able to solve (e.g. goals involving universal quantifiers).Note that this tactic is only available after a
Require Import Rtauto
.

Tactic
firstorder ltac_expr? using qualid+,? with ident+?
¶ An experimental extension of
tauto
to firstorder reasoning. It is not restricted to usual logical connectives but instead can reason about any firstorder class inductive definition.ltac_expr
Tries to solve the goal with
ltac_expr
when no logical rule applies. If unspecified, the tactic uses the default from theFirstorder Solver
option.using qualid+,
Adds the lemmas
qualid+,
to the proof search environment. Ifqualid
refers to an inductive type, its constructors are added to the proof search environment.with ident+
Adds lemmas from
auto
hint basesident+
to the proof search environment.

Option
Firstorder Solver ltac_expr
¶ The default tactic used by
firstorder
when no rule applies inauto with core
. It can be set locally or globally using this option.

Command
Print Firstorder Solver
¶ Prints the default tactic used by
firstorder
when no rule applies.

Tactic
congruence natural? with one_term+?
¶ 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.
with one_term+?
Adds
one_term+
to the pool of terms used bycongruence
. 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
injection
anddiscriminate
). If the goal is a nonquantified equality, congruence tries to prove it with nonquantified 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.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
assert
to add some lemmas as hypotheses so thatcongruence
can use them.Example
 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.
 1 goal A : Type f : A > A g : A > A > A a, b : A ============================ a = f a > g b (f a) = f (f a) > g a b = f (g b a) > g a b = a
 intros.
 1 goal A : Type f : A > A g : A > A > A a, b : A H : a = f a H0 : g b (f a) = f (f a) H1 : g a b = f (g b a) ============================ g a b = a
 congruence.
 No more goals.
 Qed.
 Theorem inj (A:Type) (f:A > A * A) (a c d: A) : f = pair a > Some (f c) = Some (f d) > c=d.
 1 goal A : Type f : A > A * A a, c, d : A ============================ f = pair a > Some (f c) = Some (f d) > c = d
 intros.
 1 goal A : Type f : A > A * A a, c, d : A H : f = pair a H0 : Some (f c) = Some (f d) ============================ c = d
 congruence.
 No more goals.
 Qed.

Error
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 dependentlytyped functions.

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

Flag
Congruence Verbose
¶ Makes
congruence
print debug information.

Tactic
btauto
¶ The tactic
btauto
implements a reflexive solver for boolean tautologies. It solves goals of the formt = u
wheret
andu
are constructed over the following grammar:truefalseWhenever the formula supplied is not a tautology, it also provides a counterexample.
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
.