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