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 failsclarify-- makes as much progress as possible while not leaving more than one goalsafe-- 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.)
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
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.
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).)
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)]
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))]
Eliminate existential quantifiers
eliminate all existential quantifiers, fails if there aren't any
Substitute if there is a hypothesis x = t or t = x
Split all conjunctions
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
- force : auto.case_option
- at_most_one : auto.case_option
- accept : auto.case_option
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
optiscase_option.force) fail if it does not close the goal, - (if
optiscase_option.at_most_one) fail if it produces more than one goal, and - (if
optiscase_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.
iclarify is like clarify, but only uses intuitionistic logic.
isafe is like safe, but only uses intuitionistic logic.
ifinish is like finish, but only uses intuitionistic logic.