In Lean, why is the exact tactic necessary when the goal is the same as a hypothesis?

Question

In Lean, when proving basic theorems, one runs into the following kind of thing:

import tactic
variables (P : Prop)

example : P → P :=
begin
  intro p,
  exact p,
end

After the intro p, step, the tactic state is

P : Prop
p : P
⊢ P

At this point, we need to use the exact tactic to close the goal. All exact seems to do is to tell Lean that the hypothesis p is the same (syntactically? definitionally?) as the target. It seems as if it would be a reasonable design goal (in the interest of efficiency) to have Lean automatically close the goal once the target is at least syntactically identical to one of the hypotheses.

Is this a design choice, or is there some deeper reason why this doesn't happen, and what is it?

Answer 1

My take on that is that, in their first approximation, tactics are just ways to build terms (typically proof terms), so it is expected to have basic tactics that closely correspond to the various term formers. In particular, in your example

• intro x for λ x, …
• exact e for e.

This hopefully justifies the existence of a basic tactic like exact.

And it may also justify why, unless you ask for it, no automation happens. Consider using tactics to build terms, and imagine end would just close goals using any tactic:

def fst {a : Type} : (a,a) → a :=
begin intro x, cases x with x1 x2, end

Now there are two assumptions that can be used, but the choice certainly matters.

But when using more advanced tactics, some of these do have such automation built in, e.g. simpa.