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

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

meta def auto.add_simps  :

@[instance]

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
@[instance]

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

meta def auto.normalize_hyp  :

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

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

meta def auto.split_hyps_aux  :

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  :

Eagerly apply all the preprocessing rules

### Terminal tactic

meta def auto.mk_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  :

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

@[instance]

@[instance]

meta def auto.case_hyp  :
expr

meta def auto.case_some_hyp  :

### The main tactics

meta def auto.safe_core  :

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  :

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

meta def auto.safe  :

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

meta def auto.finish  :

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

meta def auto.iclarify  :

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

meta def auto.isafe  :

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

meta def auto.ifinish  :

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.