mathlib documentation

tactic.finish

The finish family of tactics

These tactics do straightforward things: they call the simplifier, split conjunctive assumptions, eliminate existential quantifiers on the left, and look for contradictions. They rely on ematching and congruence closure to try to finish off a goal at the end.

The procedures do split on disjunctions and recreate the smt state for each terminal call, so they are only meant to be used on small, straightforward problems.

Main definitions

We provide the following tactics:

All accept an optional list of simplifier rules, typically definitions that should be expanded. (The equations and identities should not refer to the local context.)

Implementation notes

The variants ifinish, iclarify, and isafe try to restrict to intuitionistic logic. But the done tactic leaks classical logic:

example {P : Prop} : ¬¬P  P :=
by using_smt (do smt_tactic.intros, smt_tactic.close)

They also do not work well with the current heuristic instantiation method used by ematch. So they are left here mainly for reference.

Utilities

structure auto.auto_config  :
Type
  • use_simp : bool
  • classical : bool
  • max_ematch_rounds :

Configuration information for the auto tactics.

  • (use_simp := tt): call the simplifier
  • (classical := tt): use classical logic
  • (max_ematch_rounds := 20): for the "done" tactic

Preprocess goal.

We want to move everything to the left of the sequent arrow. For intuitionistic logic, we replace the goal p with ∀ f, (p → f) → f and introduce.

theorem auto.by_contradiction_trick (p : Prop) :
(∀ (f : Prop), (p → f) → f) → p

Normalize hypotheses

Bring conjunctions to the outside (for splitting), bring universal quantifiers to the outside (for ematching). The classical normalizer eliminates a → b in favor of ¬ a ∨ b.

For efficiency, we push negations inwards from the top down. (For example, consider simplifying ¬ ¬ (p ∨ q).)

theorem auto.not_not_eq (p : Prop) :
(¬¬p) = p

theorem auto.not_and_eq (p q : Prop) :
(¬(p q)) = (¬p ¬q)

theorem auto.not_or_eq (p q : Prop) :
(¬(p q)) = (¬p ¬q)

theorem auto.not_forall_eq {α : Type u} (s : α → Prop) :
(¬∀ (x : α), s x) = ∃ (x : α), ¬s x

theorem auto.not_exists_eq {α : Type u} (s : α → Prop) :
(¬∃ (x : α), s x) = ∀ (x : α), ¬s x

theorem auto.not_implies_eq (p q : Prop) :
(¬(p → q)) = (p ¬q)

theorem auto.classical.implies_iff_not_or (p q : Prop) :
p → q ¬p q

Eliminate existential quantifiers

meta def auto.eelim  :

eliminate an existential quantifier if there is one

meta def auto.eelims  :

eliminate all existential quantifiers, fails if there aren't any

Substitute if there is a hypothesis x = t or t = x

meta def auto.do_subst  :

carries out a subst if there is one, fails otherwise

Split all conjunctions

meta def auto.add_conjuncts  :

Assumes pr is a proof of t. Adds the consequences of t to the context and returns tt if anything nontrivial has been added.

meta def auto.split_hyp  :

return tt if any progress is made

return tt if any progress is made

meta def auto.split_hyps  :

fail if no progress is made

Eagerly apply all the preprocessing rules

Eagerly apply all the preprocessing rules

Terminal tactic

The terminal tactic, used to try to finish off goals:

  • Call the contradiction tactic.
  • Open an SMT state, and use ematching and congruence closure, with all the universal statements in the context.

TODO(Jeremy): allow users to specify attribute for ematching lemmas?

done first attempts to close the goal using contradiction. If this fails, it creates an SMT state and will repeatedly use ematch (using ematch lemmas in the environment, universally quantified assumptions, and the supplied lemmas ps) and congruence closure.

Tactics that perform case splits

inductive auto.case_option  :
Type

The main tactics

safe_core s ps cfg opt negates the goal, normalizes hypotheses (by splitting conjunctions, eliminating existentials, pushing negations inwards, and calling simp with the supplied lemmas s), and then tries contradiction.

If this fails, it will create an SMT state and repeatedly use ematch (using ematch lemmas in the environment, universally quantified assumptions, and the supplied lemmas ps) and congruence closure.

safe_core is complete for propositional logic. Depending on the form of opt it will:

  • (if opt is case_option.force) fail if it does not close the goal,
  • (if opt is case_option.at_most_one) fail if it produces more than one goal, and
  • (if opt is case_option.accept) ignore the number of goals it produces.

clarify is safe_core, but with the (opt : case_option) parameter fixed at case_option.at_most_one.

safe is safe_core, but with the (opt : case_option) parameter fixed at case_option.accept.

finish is safe_core, but with the (opt : case_option) parameter fixed at case_option.force.

iclarify is like clarify, but in some places restricts to intuitionistic logic. Classical logic still leaks, so this tactic is deprecated.

isafe is like safe, but in some places restricts to intuitionistic logic. Classical logic still leaks, so this tactic is deprecated.

ifinish is like finish, but in some places restricts to intuitionistic logic. Classical logic still leaks, so this tactic is deprecated.

interactive versions

clarify [h1,...,hn] using [e1,...,en] negates the goal, normalizes hypotheses (by splitting conjunctions, eliminating existentials, pushing negations inwards, and calling simp with the supplied lemmas h1,...,hn), and then tries contradiction.

If this fails, it will create an SMT state and repeatedly use ematch (using ematch lemmas in the environment, universally quantified assumptions, and the supplied lemmas e1,...,en) and congruence closure.

clarify is complete for propositional logic.

Either of the supplied simp lemmas or the supplied ematch lemmas are optional.

clarify will fail if it produces more than one goal.

safe [h1,...,hn] using [e1,...,en] negates the goal, normalizes hypotheses (by splitting conjunctions, eliminating existentials, pushing negations inwards, and calling simp with the supplied lemmas h1,...,hn), and then tries contradiction.

If this fails, it will create an SMT state and repeatedly use ematch (using ematch lemmas in the environment, universally quantified assumptions, and the supplied lemmas e1,...,en) and congruence closure.

safe is complete for propositional logic.

Either of the supplied simp lemmas or the supplied ematch lemmas are optional.

safe ignores the number of goals it produces, and should never fail.

finish [h1,...,hn] using [e1,...,en] negates the goal, normalizes hypotheses (by splitting conjunctions, eliminating existentials, pushing negations inwards, and calling simp with the supplied lemmas h1,...,hn), and then tries contradiction.

If this fails, it will create an SMT state and repeatedly use ematch (using ematch lemmas in the environment, universally quantified assumptions, and the supplied lemmas e1,...,en) and congruence closure.

finish is complete for propositional logic.

Either of the supplied simp lemmas or the supplied ematch lemmas are optional.

finish will fail if it does not close the goal.