too many semicolons

Stream: general

[Scott Morrison]

I appreciate the desire to be terse, but there are many places where I think we go too far. As an example from linear_combination.lean (I haven't look up who wrote this --- no fingers are being pointed!)

theorem restrict_dom_comp_subtype (s : set β) :
  (restrict_dom α s).comp (submodule.subtype _) = linear_map.id :=
by ext l; apply subtype.coe_ext.2; simp; ext a;
   by_cases a ∈ s; simp [h]; exact (mem_supported'.1 l.2 _ h).symm

This proof broke when I was trying to clean something up. With the semicolons everywhere, it's much harder to debug than a simple begin ... end block.

[Scott Morrison]

Indeed, exactly one of those semicolons is actually serving its real purpose (running a tactic on multiple goals).

[Scott Morrison]

I would have preferred writing this proof as

theorem restrict_dom_comp_subtype (s : set β) :
  (restrict_dom α s).comp (submodule.subtype _) = linear_map.id :=
begin
  ext l,
  apply subtype.coe_ext.2,
  simp,
  ext a,
  by_cases h : a ∈ s; simp [h],
  exact (mem_supported'.1 l.2 _ h).symm
end

[Scott Morrison]

Now you can both see the structure better (simp [h] is acting on both branchs of by_cases --- otherwise the proof is linear),

[Scott Morrison]

and if something goes wrong you can inspect the intermediate states.

[Scott Morrison]

I worry that proofs like this are being written in "semicolon style" solely to reduce the character count (and perhaps that feeling of accomplishment when you get a proof short enough to use by instead of begin ... end)

[Scott Morrison]

What do people think? Could we perhaps add something to the style guide discouraging the use of by A;B;C;...;X;Y;Z for chains beyond some length?

[Simon Hudon]

I'm wondering if simp only wouldn't have done more to make the proof adaptable.

[Johannes Hölzl]

I'm in absolutely agree that we should of avoid by A;B;C;...;X;Y;Z as much as possible. With small exceptions like by c; m where c is something like ext or cases, a predictable method to destruct the goal into simpler forms, and m is simp or similar.

[Johannes Hölzl]

simp only might help when it breaks, but it doesn't help to make the proof understandable

[Scott Morrison]

That's perhaps a stronger argument than I would have made. There are _many_ examples in mathlib of by X; Y which have only been written as that instead of begin X, Y end for the sake of brevity. What do you think of these?

[Johan Commelin]

I have been guilty of golfing proofs down in this way. I wouldn't mind changing the culture.

[Johannes Hölzl]

I sometimes also do it for the sake of brevity, but when I look at it some times later, I dislike it. But two methods have usually the flavour of first apply cases, or add some kind of "marker" which is then pushed through the statement to solve it.

[Kevin Buzzard]

What about by {A, B, C}?

[Johan Commelin]

I think it's a lot better, but it isn't common style.

[Kevin Buzzard]

I remember being quite surprised the first time I saw a semicolon bring used in this way when there was only one goal

[Kevin Buzzard]

The bracket notation only adds about two characters to the proof

[Kevin Buzzard]

And I also had trouble debugging a semicolon proof recently

[Scott Morrison]

Okay -- perhaps I will write a PR to the style guide that goes as far as saying: "don't misuse semicolons: X; Y means that X produces multiple goals, and you want to apply Y to each of them"

[Sebastien Gouezel]

If you just have one semicolon and the two expressions are short, I think it is also acceptable. For instance, by ext; simp looks all right to me.

[Kevin Buzzard]

I would definitely support that change. I would even be happy if people consistently wrote by {ext, blah} instead of by ext; blah.

[Scott Morrison]

Maybe one day we will have a proof-linting tool that actually checks for multiple goals when ; is used.

[Mario Carneiro]

Okay, I'm on board as long as I can still keep the two line compression proof

[Mario Carneiro]

so the example would become

by { ext l, apply subtype.coe_ext.2, simp, ext a,
     by_cases a ∈ s; simp [h], exact (mem_supported'.1 l.2 _ h).symm }

[Mario Carneiro]

and where the internal spaces can be omitted for a one liner like Kevin's style

[Mario Carneiro]

Actually, I would go so far as to say that by should always be used for compression style proofs and begin ... end for multiline proofs

[Mario Carneiro]

i.e. by {tac1, tac2} preferred over begin tac1, tac2 end, and

begin
  tac1,
  tac2,
  tac3...
end

is preferred over

by {
  tac1,
  tac2,
  tac3...
}

or some such thing

[Mario Carneiro]

To clarify on the original example (of which I am the author): I am also against using long strings of tac; tac; tac but my cutoff is about two lines, so that kind of example is around the upper limit

[Kevin Buzzard]

We all have different styles I guess.

[Scott Morrison]

Okay, it sounds like there's a reasonable compromise.

[Scott Morrison]

One complaint I have about semicolons is that VSCode rarely manages to show me the intermediate states, and I really rely on this for parsing proofs.

[Patrick Massot]

I agree with Scott, but this remark obviously don't apply to by ext ; simp or by unfold ... ; apply_instance

[Scott Morrison]

I'm certainly not suggesting we go back and change any existing appearances of by ext; simp, but I think it would be reasonable to encourage everyone to write by { ext, simp } in future (assuming that ext is actually only creating one goal!) But I'm not at all concerned by these single semicolon proofs, themselves.

[Johan Commelin]

#854 tries to adhere to your new style guidelines

[Johan Commelin]

I also wrote some split; { tac1, tac2 } proofs

[Johan Commelin]

Instead of chaining semicolons

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/4ec60c3353e511d094045e80a32a5715760a7603/src/algebra/pointwise.lean#L34-L37 :open_mouth: that's an implicit proof!

[Patrick Massot]

@Simon Hudon what happened to https://github.com/leanprover-community/mathlib/pull/431 ? Johan's PR would be yet another PR needing this bug fix

[Johan Commelin]

Those proofs are superboring. I wish I knew a tactic that would kill them for me.

[Patrick Massot]

You could write it!

[Johan Commelin]

I guess tidy + rw_search + back would blast through all of this. But then we get complaints that this file is too low-level, and it slows things down, etc...

[Johan Commelin]

Anyway, this is going off topic. Maybe we should move it to PR reviews...

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/blob/4ec60c3353e511d094045e80a32a5715760a7603/src/algebra/pointwise.lean#L34-L37 :open_mouth: that's an implicit proof!

It's not quite -- he uses mul_assoc twice :-)

[Kevin Buzzard]

Nice to see ‹_› in there :-)

[Patrick Massot]

I wonder why x, y and z are named

[Kevin Buzzard]

to help the unifier probably :joy:

[Kevin Buzzard]

Maybe calling them _ is a metavariable too far

[Johan Commelin]

I wonder why x, y and z are named

Oops... I forgot to remove them.

[Patrick Massot]

I really think that writing this tactic would be an excellent exercise. Unfortunately I lack time for this. I need to grade proofs written by my students after convincing Lean. I just went through a fundamentalist student who starts by unfolding every single definition he can see. The goal of the assignment was to prove that increasing sequences with an upper bound tend to their supremum...

[Sebastien Gouezel]

Did he unfold real numbers to Cauchy sequences?

[Patrick Massot]

Fortunately, he did not see this definition

[Patrick Massot]

But he never writes "upper bound" or "supremum", only things like x ∈ {x : ℝ | ∀ (a : ℝ), a ∈ A → a ≤ x} and x ∈ {x : ℝ | ∀ (a : ℝ), a ∈ {x : ℝ | ∀ (a : ℝ), a ∈ A → a ≤ x} → x ≤ a} (written like this on paper). I guess I'm punished by my own sins

[Sebastien Gouezel]

Not sure I understand the concept. First, they get a working Lean proof, and then they write a paper proof -- your idea being that the paper proof will be correct since they have been able to convince Lean. But then you get super-formal proofs on paper?

[Patrick Massot]

The goal of the course is to get correct and readable proofs on paper. Lean is only an intermediate step. I never assumed it would be easy to go from Lean to paper. Some students can do it, some can't. The one I quoted is of course an extreme case

[Simon Hudon]

@Patrick Massot to answer your earlier question, I was getting nowhere with that PR so I put it on hold. I can get back to it next week.

[Johan Commelin]

On a somewhat recent mathlib:

git grep ";.*;" | wc -l
977

I agree that we shouldn't purge mathlib just for the sake of it. But I wanted to know this stat anyway (-;