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:

finish -- solves the goal or fails
clarify -- makes as much progress as possible while not leaving more than one goal
safe -- splits freely, finishes off whatever subgoals it can, and leaves the rest

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

meta def tactic.interactive.revert_all :

Utilities #

meta def auto.whnf_reducible (e : expr) :

meta def auto.add_simps :

simp_lemmas → list name → tactic simp_lemmas

@[protected, instance]

def auto.auto_config.inhabited :

inhabited auto.auto_config

structure auto.auto_config :

Type

use_simp : bool
max_ematch_rounds : ℕ

Configuration information for the auto tactics.

(use_simp := tt): call the simplifier
(max_ematch_rounds := 20): for the "done" tactic

@[protected, instance]

def auto.auto_config.decidable_eq :

decidable_eq auto.auto_config

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) (h : ∀ (f : Prop), (p → f) → f) :

p

meta def auto.preprocess_goal :

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

def auto.common_normalize_lemma_names :

Equations

auto.common_normalize_lemma_names = [name.mk_string "bex_def" name.anonymous, name.mk_string "forall_and_distrib" name.anonymous, name.mk_string "exists_imp_distrib" name.anonymous, name.mk_string "assoc" (name.mk_string "or" name.anonymous), name.mk_string "comm" (name.mk_string "or" name.anonymous), name.mk_string "left_comm" (name.mk_string "or" name.anonymous), name.mk_string "assoc" (name.mk_string "and" name.anonymous), name.mk_string "comm" (name.mk_string "and" name.anonymous), name.mk_string "left_comm" (name.mk_string "and" name.anonymous)]

def auto.classical_normalize_lemma_names :

Equations

auto.classical_normalize_lemma_names = auto.common_normalize_lemma_names ++ [name.mk_string "implies_iff_not_or" (name.mk_string "classical" (name.mk_string "auto" name.anonymous))]

meta def auto.normalize_negations (cfg : auto.auto_config) (h : expr) :

meta def auto.normalize_hyp (cfg : auto.auto_config) (simps : simp_lemmas) (h : expr) :

meta def auto.normalize_hyps (cfg : auto.auto_config) :

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

meta def auto.do_substs :

Split all conjunctions #

meta def auto.add_conjuncts :

expr → expr → tactic bool

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 (h : expr) :

return tt if any progress is made

meta def auto.split_hyps_aux :

list expr → tactic bool

return tt if any progress is made

meta def auto.split_hyps :

fail if no progress is made

Eagerly apply all the preprocessing rules #

meta def auto.preprocess_hyps (cfg : auto.auto_config) :

Eagerly apply all the preprocessing rules

Terminal tactic #

meta def auto.mk_hinst_lemmas :

list expr → smt_tactic hinst_lemmas

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?

meta def auto.done (ps : list pexpr) (cfg : auto.auto_config := {use_simp := tt, max_ematch_rounds := 20}) :

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

force : auto.case_option
at_most_one : auto.case_option
accept : auto.case_option

@[protected, instance]

def auto.case_option.inhabited :

inhabited auto.case_option

@[protected, instance]

def auto.case_option.decidable_eq :

decidable_eq auto.case_option

meta def auto.case_hyp (h : expr) (s : auto.case_option) (cont : auto.case_option → tactic unit) :

meta def auto.case_some_hyp_aux (s : auto.case_option) (cont : auto.case_option → tactic unit) :

list expr → tactic bool

meta def auto.case_some_hyp (s : auto.case_option) (cont : auto.case_option → tactic unit) :

The main tactics #

meta def auto.safe_core (s : simp_lemmas × list name) (ps : list pexpr) (cfg : auto.auto_config) :

auto.case_option → tactic unit

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.

meta def auto.clarify (s : simp_lemmas × list name) (ps : list pexpr) (cfg : auto.auto_config := {use_simp := tt, max_ematch_rounds := 20}) :

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

meta def auto.safe (s : simp_lemmas × list name) (ps : list pexpr) (cfg : auto.auto_config := {use_simp := tt, max_ematch_rounds := 20}) :

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

meta def auto.finish (s : simp_lemmas × list name) (ps : list pexpr) (cfg : auto.auto_config := {use_simp := tt, max_ematch_rounds := 20}) :

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

interactive versions #

meta def tactic.interactive.clarify (hs : interactive.parse tactic.simp_arg_list) (ps : interactive.parse (lean.parser.tk "using" *> interactive.types.pexpr_list_or_texpr)?) (cfg : auto.auto_config := {use_simp := tt, max_ematch_rounds := 20}) :

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.

meta def tactic.interactive.safe (hs : interactive.parse tactic.simp_arg_list) (ps : interactive.parse (lean.parser.tk "using" *> interactive.types.pexpr_list_or_texpr)?) (cfg : auto.auto_config := {use_simp := tt, max_ematch_rounds := 20}) :

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.

meta def tactic.interactive.finish (hs : interactive.parse tactic.simp_arg_list) (ps : interactive.parse (lean.parser.tk "using" *> interactive.types.pexpr_list_or_texpr)?) (cfg : auto.auto_config := {use_simp := tt, max_ematch_rounds := 20}) :

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.