enforcing structured proofs

Stream: Lean for teaching

[Mike Shulman]

Is there any way to force the use of braces when there are multiple subgoals, similar to Coq's Set Default Goal Selector "!"? I find some of my students neglect to use braces and then get completely lost in what part of their proof is supposed to be proving what, and if they'd been forced to use braces from the start they would have a much easier time and develop good habits of structuring their tactics.

[Mario Carneiro]

Can you explain what that command does?

[Mario Carneiro]

According to my reading of https://coq.inria.fr/refman/proof-engine/ltac.html#goal-selectors, this makes every tactic fail if it is called on a state with multiple goals. Syntactically this could be done by a set_option, but there are a few exceptions which make it difficult to implement generically as part of the glue code holding tactics together: you don't want a proof like

example : True /\ True := by
  constructor
  . trivial
  . trivial

to fail because the first . trivial was called on a state with two subgoals

[Mike Shulman]

Yes, that's right (about Coq). What does . do there?

[Mike Shulman]

In any case, isn't constructor . trivial . trivial a single tactic (it has no commas)?

[Mario Carneiro]

that's lean 4 syntax

[Mario Carneiro]

the dots are like * and - in coq

[Mike Shulman]

Oh, well in that case the . plays a role similar to { of focusing on a single goal, so it should be allowed.

[Mario Carneiro]

they are actually center dots · but I was being lazy (regular dots also work though)

[Mario Carneiro]

yes, in lean 3 we would use braces to the same effect

[Mario Carneiro]

and I agree that we want to strongly encourage that style

[Mario Carneiro]

It wouldn't be too hard to write a linter to detect structured proof patterns

[Mike Shulman]

My point is, since . is like { I wouldn't regard it as an "exception".

[Mario Carneiro]

and IMO that makes a bit more sense from a PL design standpoint compared to changing the semantics of tactics (which makes things like try change behavior)

[Mike Shulman]

To be honest, I've never understood why Coq or Lean even permits unstructured tactic scripts in the first place. I can understand that maybe it seemed like a good idea decades ago when Coq was first written and now they have a lot of legacy code to support, but why did Lean follow suit?

[Mario Carneiro]

I mean that . / { is an exception to the rule that tactics only take one goal

[Mike Shulman]

Oh, so { and . are themselves "tactics" rather than ways of structuring a tactic script?

[Mario Carneiro]

yes

[Mario Carneiro]

and that might answer your other question too

[Mike Shulman]

Mmm... not really?

[Mike Shulman]

Are you saying the answer is that unstructured tactics are easier to implement?

[Mario Carneiro]

they are certainly more uniform

[Mario Carneiro]

but I am in complete agreement with you that it's not a great base to build on

[Mario Carneiro]

In HOL I think they lean more heavily on the ML type system to express tactics as functions with the appropriate signatures

[Mario Carneiro]

but I guess that means you have to either manipulate goal variables a lot or make a DSL out of fancy combinators

[Mario Carneiro]

I think lean 4 offers some more flexibility in having arbitrary syntax structures as tactic input, and it is leaning more heavily in the direction of structured proofs. The list-of-goals mechanism looks a lot more like a backward compatibility feature now

[Mike Shulman]

Okay, thanks. Anyway, it sounds like the answer to my original question is no, at present.

[Johan Commelin]

I can certainly imagine a tactic pretty_smart that looks at 5 goals, of which 2 are real number metavariables, and it figures out which real numbers to assign to those metavariables in such a way that it can prove the other 3 goals.
Such a tactic needs to operate on multiple goals.

[Patrick Massot]

The first year I taught using Lean, I explained braces, and after two weeks I promised myself I would hide this piece of syntax to students forever. In principle focusing on one goal is nice. But the huge issue is that Lean 3 gets super confused and displays either nothing or an incomprehensible error message as soon as braces are not balanced or a comma is missing between a closing brace and an opening one.

[Kevin Buzzard]

With the natural number game I just said "tactics act on the top goal" and actively encouraged bad style; I have been in two minds about whether this was a good idea ever since! I think it does make it easier to get started (precisely for the incomprehensible error message reasons Patrick mentioned above -- in testing I had enough trouble with people forgetting commas and this already caused enough problems) but for those that go on to write more lean their code is often hard to read until I teach them out of this bad habit.

[Mike Shulman]

@Johan Commelin I'm not against tactics that operate on multiple goals. What I object to is tactics that operate on the first goal only but without explicitly focusing on it.

[Mario Carneiro]

One way to do this that would have pretty uniform impact would be to replace the getMainGoal function with getTheGoal which acts like getMainGoal if the allowUnstructuredProof option is disabled and does your proposed behavior (gets the single goal else fails) when it is enabled

[Sebastian Ullrich]

I believe one reason not to ban unstructured proofs by default is that they are sometimes helpful for a first draft that can then be refactored, especially when heavy automation is involved. But that means we could still make them opt-out warnings instead of errors, which is easy to do with a custom linter in Lean 4 minus edge cases I probably didn't think of

register_builtin_option linter.unstructuredProof : Bool := {
  defValue := true,
  descr := "enable the 'unstructured proof' linter"
}
open Lean Linter

def unstructuredProofLinter : Linter := fun _ => do
  for tree in (← get).infoState.trees do
    tree.visitM' fun
      | _, i@(.ofTacticInfo ti), _ => do
        if i.range?.isSome && -- ignore macros
           ti.goalsBefore.length > 1 && ti.goalsAfter.length > 0 &&
           ti.goalsBefore != ti.goalsAfter then  -- ignore no-op helper tactics
          logLint linter.unusedVariables ti.stx "unstructured proof step"
      | _, _, _ => pure ()

initialize addLinter unstructuredProofLinter

(edit: ah... find the typo)
image.png

[Jon Eugster]

To add to @Patrick Massot and @Kevin Buzzard 's thoughts about their teaching, completely unstructured proofs are also really helpful to create more interactive learning resources. Been thinking about having a drag'n'drop like feature in our project where the Lean4-code is hidden behind an interface, and for this I'd sometimes wish all (or most) tactics worked without enforcing structure. (Lean4-cases is an example that doesn't really work well without structure (when the new variables should be named), but there's still rcases or even cases' around to avoid it.)

[Jon Eugster]

Having a linter telling you how to write nicer code sounds like a good idea though, would love to see that added to the default linters

[Sebastian Ullrich]

You can use rename_i for unstructured cases proofs, for what it's worth

[Mike Shulman]

Sounds to me a lot like the arguments people make for "dynamic typing"... (-:O