Zulip Chat Archive

Stream: Lean for teaching

Topic: enforcing structured proofs

Mike Shulman (Dec 06 2022 at 00:08):

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 (Dec 06 2022 at 00:11):

Can you explain what that command does?

Mario Carneiro (Dec 06 2022 at 00:16):

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
  . trivial
  . trivial

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

Mike Shulman (Dec 06 2022 at 00:27):

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

Mike Shulman (Dec 06 2022 at 00:31):

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

Mario Carneiro (Dec 06 2022 at 00:33):

that's lean 4 syntax

Mario Carneiro (Dec 06 2022 at 00:33):

the dots are like * and - in coq

Mike Shulman (Dec 06 2022 at 00:33):

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

Mario Carneiro (Dec 06 2022 at 00:33):

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

Mario Carneiro (Dec 06 2022 at 00:34):

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

Mario Carneiro (Dec 06 2022 at 00:34):

and I agree that we want to strongly encourage that style

Mario Carneiro (Dec 06 2022 at 00:34):

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

Mike Shulman (Dec 06 2022 at 00:35):

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

Mario Carneiro (Dec 06 2022 at 00:36):

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 (Dec 06 2022 at 00:36):

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 (Dec 06 2022 at 00:36):

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

Mike Shulman (Dec 06 2022 at 00:37):

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

Mario Carneiro (Dec 06 2022 at 00:37):


Mario Carneiro (Dec 06 2022 at 00:37):

and that might answer your other question too

Mike Shulman (Dec 06 2022 at 00:37):

Mmm... not really?

Mike Shulman (Dec 06 2022 at 00:38):

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

Mario Carneiro (Dec 06 2022 at 00:38):

they are certainly more uniform

Mario Carneiro (Dec 06 2022 at 00:39):

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

Mario Carneiro (Dec 06 2022 at 00:39):

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

Mario Carneiro (Dec 06 2022 at 00:40):

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

Mario Carneiro (Dec 06 2022 at 00:42):

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 (Dec 06 2022 at 00:46):

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

Johan Commelin (Dec 06 2022 at 06:48):

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 (Dec 06 2022 at 07:52):

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 (Dec 06 2022 at 08:47):

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 (Dec 06 2022 at 16:45):

@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 (Dec 06 2022 at 16:51):

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 (Dec 06 2022 at 17:21):

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)

Jon Eugster (Dec 07 2022 at 12:27):

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 (Dec 07 2022 at 12:28):

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 (Dec 07 2022 at 12:29):

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

Mike Shulman (Dec 07 2022 at 18:37):

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

Last updated: Dec 20 2023 at 11:08 UTC