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?
assumption
tactic will effectively tryexact h
for eachh
in the local context, until one works. It could be an interesting experiment to modify the tactic monad (or introduce a new interactive tactic mode) that callstry {assumption}
after each tactic. This would have a significant performance penalty in some parts of the library. $\endgroup$try { assumption }
at the very end of the block, which is more modest of a change. $\endgroup$