12
$\begingroup$

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?

$\endgroup$
5
  • 1
    $\begingroup$ You can use the so-called finishing tactics to do trivial work for you. $\endgroup$
    – Trebor
    Feb 10, 2022 at 17:05
  • $\begingroup$ Pretty new to it all, so haven't run into that one yet! I'm slowly learning those shortcuts (like using anonymous constructors and such) and making sure that I know how they translate to a more verbose proof. I suspect that there's a good reason why certain tactic states don't automatically close, though, which is why I asked this question, just to see if I can get some insight into how lean works/was designed. $\endgroup$
    – march
    Feb 10, 2022 at 17:12
  • $\begingroup$ The assumption tactic will effectively try exact h for each h 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 calls try {assumption} after each tactic. This would have a significant performance penalty in some parts of the library. $\endgroup$
    – Rob Lewis
    Feb 10, 2022 at 18:32
  • $\begingroup$ @RobLewis That's an interesting take on it, that it's about performance. I guess in order for goals to automatically close, it really would have to check$-$after *every* step$-$to see if the goal matched a hypothesis. I can see how that would significantly reduce performance. $\endgroup$
    – march
    Feb 10, 2022 at 18:40
  • $\begingroup$ @RobLewis That mode could do try { assumption } at the very end of the block, which is more modest of a change. $\endgroup$ Feb 20, 2022 at 23:25

1 Answer 1

15
$\begingroup$

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.

$\endgroup$
5
  • 2
    $\begingroup$ I think that the idea that tactics are used to form terms (in a more verbose and readable/understandable way) is probably the important point here, and it's one that I'm still thinking about, since most of what I've done is go through a bunch of tutorials, where I've only used tactics so far, and I haven't written any pure term proofs. Thanks! $\endgroup$
    – march
    Feb 10, 2022 at 17:37
  • 2
    $\begingroup$ To build on this answer and the comment, while it is generally not advisable, it is possible (and actually done by advanced users) to produce definitions using tactic mode. If you have multiple terms of a given type in context, it's important to be able to choose precisely which one you want to use in the given definition. The exact tactic lets you do precisely this. (Of course, for proofs this distinction doesn't matter.) $\endgroup$
    – Adam Topaz
    Feb 10, 2022 at 18:28
  • 2
    $\begingroup$ Whether it's "advisable" to use tactics to produce definitions depends on what you're doing. In HoTT we do this all the time and it would be very difficult to do without. Of course, Lean 3+ isn't HoTT-compatible, but I don't see any reason to avoid it in principle. $\endgroup$ Feb 10, 2022 at 18:38
  • $\begingroup$ Adam, isn’t that exactly my example, building the fst function? $\endgroup$ Feb 10, 2022 at 18:54
  • 1
    $\begingroup$ Yes, of course Joachim! Sorry, I should have clarified. And to respond to Mike's comment, the same is true in Lean, but we do tend to advise new users against making definitions using tactics. $\endgroup$
    – Adam Topaz
    Feb 10, 2022 at 19:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.