\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

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 whereas auto 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 of intros 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 goal Goal 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 of x is necessary.

Tactic dtauto: While tauto recognizes inductively defined connectives isomorphic to the standard connectives and, prod, or, sum, False, Empty_set, unit and True, dtauto also recognizes all inductive types with one constructor and no indices, i.e. record-style connectives.

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 applies ltac_expr to them [Mun94]. If ltac_expr is not specified, it defaults to Tauto.intuition_solver.

The initial value of intuition_solver is equivalent to auto with * but prints warning intuition-auto-with-star when it solves a goal that auto cannot solve. In a future version it will be changed to just auto. Use intuition tac locally or Ltac Tauto.intuition_solver ::= tac globally to silence the warning in a forward compatible way with your choice of tactic tac (auto, auto with *, auto with your prefered databases, or any other tactic).

If ltac_expr fails on some goals then intuition fails. In fact, tauto is simply intuition fail.

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

Flag Intuition Negation Unfolding: This flag controls whether intuition unfolds inner negations which do not need to be unfolded. It is on by default.

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 that tauto 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 the Firstorder Solver option.
using qualid+,: Adds the lemmas qualid+, to the proof search environment. If qualid refers to an inductive type, its constructors are added to the proof search environment.
with ident+: Adds lemmas from auto hint bases ident+ to the proof search environment.

Option Firstorder Solver ltac_expr: The default tactic used by firstorder when no rule applies in auto with core. This command supports the same locality attributes as Obligation Tactic.

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

Option Firstorder Depth natural: This option controls the proof search depth bound.

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 by 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 injection and 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.

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 that congruence 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 Rocq 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" makes congruence print debug information.

Tactic btauto

The tactic btauto implements a reflexive solver for boolean tautologies. It solves goals of the form t = u where t and u are constructed over the following grammar:

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.

Error Cannot recognize a boolean equality.: The goal is not of the form t = u. Especially note that btauto doesn't introduce variables into the context on its own.