Solvers for logic and equality¶
- Tactic tauto¶
This tactic implements a decision procedure for intuitionistic propositional calculus based on the contraction-free 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 toTauto.intuition_solver
.The initial value of
intuition_solver
is equivalent toauto with *
but prints warningintuition-auto-with-star
when it solves a goal thatauto
cannot solve. In a future version it will be changed to justauto
. Useintuition tac
locally orLtac Tauto.intuition_solver ::= tac
globally to silence the warning in a forward compatible way with your choice of tactictac
(auto
,auto with *
,auto with
your prefered databases, or any other tactic).If
ltac_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. record-style connectives.
- 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 first-order reasoning. It is not restricted to usual logical connectives but instead can reason about any first-order 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
. This command supports the same locality attributes asObligation Tactic
.
- Command Print Firstorder Solver¶
Prints the default tactic used by
firstorder
when no rule applies.
- Tactic gintuition ltac_expr?¶
An extension of
intuition
to first-order reasoning (similar to howfirstorder
extendstauto
).
- 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 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.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.- Tactic simple congruence natural? with one_term+?¶
Behaves like
congruence
, but does not unfold definitions.
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 dependently-typed 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.
Setting
Debug
"congruence"
makescongruence
print debug information.
- Tactic btauto¶
The tactic
btauto_termbtauto
implements a reflexive solver for boolean tautologies. It solves goals of the formt = u
wheret
andu
are constructed over the following grammar:::=
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_termWhenever 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
.