# 6. Writing Automation¶

The goal of this chapter is to provide some examples that illustrate the ways that metaprogramming in Lean can be used to implement automated proof procedures.

## 6.1. A Tableau Prover for Classical Propositional Logic¶

In this section, we design a theorem prover that is complete for classical propositional logic. The method is essentially that of tableaux theorem proving, and, from a proof-theoretic standpoint, can be used to demonstrate the completeness of cut-free sequent calculi.

The idea is simple. If `a`, `b`, `c`, and `d` are formulas of propositional logic, the sequent `a, b, c ⊢ d` represents the goal of proving that `d` follows from `a`, `b` and `c`, and `d`. The fact that they are propositional formulas means that they are built up from variables of type `Prop` and the constants `true` and `false` using the connectives `∧ ∨ → ↔ ¬`. The proof procedure proceeds as follows:

• Negate the conclusion, so that the goal becomes `a, b, c, ¬ d ⊢ false`.
• Put all formulas into negation-normal form. In other words, eliminate `→` and `↔` in terms of the other connectives, and using classical identities to push all equivalences inwards.
• At that stage, all formulas are built up from literals (propositional variables and negated propositional variables) using only `∧` and `∨`. Now repeatedly apply all of the following proof steps:
• Reduce a goal of the form `Γ, a ∧ b ⊢ false` to the goal `Γ, a, b ⊢ false`, where `Γ` is any set of propositional formulas.
• Reduce a goal of the form `Γ, a ∨ b ⊢ false` to the pair of goals `Γ, a ⊢ false` and `Γ, b ⊢ false`.
• Prove any goal of the form `Γ, a, ¬ a ⊢ false` in the usual way.

It is not hard to show that this is complete. Each step preserves validity, in the sense that the original goal is provable if and only if the new ones are. And, in each step, the number of connectives in the goal decreases. If we ever face a goal in which the first two rules do not apply, the goal must consist of literals. In that case, if the last rule doesn’t apply, then no propositional variable appears with its negation, and it is easy to cook up a truth assignment that falsifies the goal.

In fact, our procedure will work with arbitrary formulas at the leaves. It simply applies reductions and rules as much as possible, so formulas that begin with anything other than a propositional connective are treated as black boxes, and act as propositional atoms.

First, let us open the namespaces we will use:

```open expr tactic classical
```

The next step is to gather all the facts we will need to put formulas in negation-normal form.

```section logical_equivalences
local attribute [instance] prop_decidable
variables {a b : Prop}

theorem not_not_iff (a : Prop) : ¬¬a ↔ a :=

theorem implies_iff_not_or (a b : Prop) : (a → b) ↔ (¬ a ∨ b) :=
iff.intro
(λ h, if ha : a then or.inr (h ha) else or.inl ha)
(λ h, or.elim h (λ hna ha, absurd ha hna) (λ hb ha, hb))

theorem not_and_of_not_or_not (h : ¬ a ∨ ¬ b) : ¬ (a ∧ b) :=
assume ⟨ha, hb⟩, or.elim h (assume hna, hna ha) (assume hnb, hnb hb)

theorem not_or_not_of_not_and (h : ¬ (a ∧ b)) : ¬ a ∨ ¬ b :=
if ha : a then
or.inr (show ¬ b, from assume hb, h ⟨ha, hb⟩)
else
or.inl ha

theorem not_and_iff (a b : Prop) : ¬ (a ∧ b) ↔ ¬a ∨ ¬b :=
iff.intro not_or_not_of_not_and not_and_of_not_or_not

theorem not_or_of_not_and_not (h : ¬ a ∧ ¬ b) : ¬ (a ∨ b) :=
assume h₁, or.elim h₁ (assume ha, h^.left ha) (assume hb, h^.right hb)

theorem not_and_not_of_not_or (h : ¬ (a ∨ b)) : ¬ a ∧ ¬ b :=
and.intro (assume ha, h (or.inl ha)) (assume hb, h (or.inr hb))

theorem not_or_iff (a b : Prop) : ¬ (a ∨ b) ↔ ¬ a ∧ ¬ b :=
iff.intro not_and_not_of_not_or not_or_of_not_and_not
end logical_equivalences
```

We can now use Lean’s built-in simplifier to do the normalization:

```meta def normalize_hyp (lemmas : simp_lemmas) (hyp : expr) : tactic unit :=
do try (simp_hyp lemmas [] hyp)

meta def normalize_hyps : tactic unit :=
do hyps ← local_context,
``implies_iff_not_or, ``not_and_iff, ``not_or_iff, ``not_not_iff,
``not_true_iff, ``not_false_iff] >>= simp_lemmas.mk.append),
```

The tactic `normalize_hyp` just simplifies the given hypothesis with the given list of lemmas. The `try` combinator ensures that the tactic is deemed successful even if no simplifications are necessary. The tactic `normalize_hyps` gathers the local context, turns the list of names into a list of expressions by applying the `mk_const` tactic to each one, and then calls `normalize_hyp` on each element of the context with those lemmas. The `for`’ tactic, like the `for` tactic, applies the second argument to each element of the first, but it returns unit rather than accumulate the results in a list.

We can test the result:

```example (p q r : Prop) (h₁ : ¬ (p ↔ (q ∧ ¬ r))) (h₂ : ¬ (p → (q → ¬ r))) : true :=
by do normalize_hyps,
trace_state,
triv
```

The result is as follows:

```p q r : Prop,
h₁ : p ∧ (r ∨ ¬q) ∨ q ∧ ¬p ∧ ¬r,
h₂ : p ∧ q ∧ r
⊢ true
```

The next five tactics handle the task of splitting conjunctions.

```open tactic expr

meta def add_fact (prf : expr) : tactic unit :=
do nh ← get_unused_name `h none,
p ← infer_type prf,
assertv nh p prf,
return ()

meta def is_conj (e : expr) : tactic bool :=
do t ← infer_type e,
return (is_app_of t `and)

meta def add_conjuncts : expr → tactic unit | e :=
do e₁ ← mk_app `and.left [e],
e₂ ← mk_app `and.right [e],

meta def split_conjs_at (h : expr) : tactic unit :=
skip

meta def split_conjs : tactic unit :=
do l ← local_context,
```

The tactic `add_fact prf` takes a proof of a proposition `p`, and adds `p` the the local context with a fresh name. Here, `get_unused_name \`h none` generates a fresh name of the form `h_n`, for a numeral `n`. The tactic `is_conj` infers the type of a given expression, and determines whether or not it is a conjunction. The tactic `add_conjuncts e` assumes that the type of `e` is a conjunction and adds proofs of the left and right conjuncts to the context, recursively splitting them if they are conjuncts as well. The tactic `split_conjs_at h` tests whether or not the hypothesis `h` is a conjunction, and, if so, adds all its conjuncts and then clears it from the context. The last tactic, `split_conjs`, applies this to every element of the context.

We need two more small tactics before we can write our propositional prover. The first reduces the task of proving a statement `p` from some hypotheses to the task of proving falsity from those hypotheses and the negation of `p`.

```meta def deny_conclusion : tactic unit :=
nh ← get_unused_name `h none,
intro nh,
return ()
```

The refine tactic applies the expression in question to the goal, but leaves any remaining metavariables for us to fill. The theorem `classical.by_contradiction` has type `∀ {p : Prop}, (¬p → false) → p`, so applying this theorem proves the goal but leaves us with the new goal of proving `¬p → false` from the same hypotheses, at which point, we can use the introduction rule for implication. If we omit the `return ()`, we will get an error message, because `deny_conclusion` is supposed to have type `tactic unit`, but the `intro` tactic returns an expression.

The next tactic finds a disjunction among the hypotheses, or returns the `option.none` if there aren’t any.

```meta def find_disj : tactic (option expr) :=
do l ← local_context,
(first \$ l.map
(λ h, do t ← infer_type h,
cond (is_app_of t `or)
(return (option.some h)) failed)) <|>
return none
```

Our propositional prover can now be implemented as follows:

```meta def prop_prover_aux : ℕ → tactic unit
| 0            :=  fail "prop prover max depth reached"
| (nat.succ n) :=
do split_conjs,
do (option.some h) ← find_disj |
fail "prop_prover failed: unprovable goal",
cases h,
prop_prover_aux n,
prop_prover_aux n

meta def prop_prover : tactic unit :=
do deny_conclusion,
normalize_hyps,
prop_prover_aux 30
```

The tactic `prop_prover` denies the conclusion, reduces the hypotheses to negation-normal form, and calls `prop_prover_aux` with a maximum splitting depth of 30. The tactic `prop_prover_aux` executes the following simple loop. First, it splits any conjunctions in the hypotheses. Then it tries applying the `contradiction` tactic, which will find a pair of contradictory literals, `p` and `¬ p`, if there is one. If that does not succeed, it looks for a disjunction `h` among the hypotheses. At this stage, if there aren’t any disjunctions, we know that the goal is not propositionally valid. On the other hand, if there is a disjunction, `prop_prover_aux` calls the `cases` tactic to split the disjunction, and then applies itself recursively to each of the resulting subgoals, decreasing the splitting depth by one.

Notice the pattern matching in the `do` notation:

```(option.some h) ← find_disj |
fail "prop_prover failed: unprovable goal"
```

This is shorthand for the use of the `bind` operation in the tactic monad to extract the result of `find_disj`, together with the use of a `match` statement to extract the result. The expression after the vertical bar is the value returned for any other case in the pattern match; in this case, it is the value returned if `find_disj` returns `none`. This is a common idiom when writing tactics, and so the compressed notation is handy.

All this is left for us to do is to try it out:

```section
variables a b c d : Prop

example (h₁ : a ∧ b) (h₂ : b ∧ ¬ c) : a ∨ c :=
by prop_prover

example (h₁ : a ∧ b) (h₂ : b ∧ ¬ c) : a ∧ ¬ c :=
by prop_prover

-- not valid
-- example (h₁ : a ∧ b) (h₂ : b ∧ ¬ c) : a ∧ c :=
-- by prop_prover

example : ((a → b) → a) → a :=
by prop_prover

example : (a → b) ∧ (b → c) → a → c :=
by prop_prover

example (α : Type) (x y z w : α) :
x = y ∧ (x = y → z = w) → z = w :=
by prop_prover

example : ¬ (a ↔ ¬ a) :=
by prop_prover
end
```