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

### Utilities #

meta def auto.whnf_reducible (e : expr) :
@[instance]
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
@[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) (h : ∀ (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 (cfg : auto.auto_config) (simps : simp_lemmas) (h : expr) :

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

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

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 #

Eagerly apply all the preprocessing rules

### Terminal tactic #

meta def auto.mk_hinst_lemmas  :

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

• 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
@[instance]
@[instance]
meta def auto.case_hyp (h : expr) (s : auto.case_option) (cont : auto.case_option) :

### The main tactics #

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

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 × ) (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 × ) (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 × ) (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 #

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.