by { ... } vs. begin ... end

Stream: Lean for teaching

[Jasmin Blanchette]

I'm using Lean to teach interactive theorem proving. Lean is a vehicle, not an end, so I'm working had to keep the fragment minimal.

We cover by ..., begin ... end, and { ... } (for multiple subgoals). I'm thinking we could kill begin ... end by using by { ... } instead. Would there be any practical disadvantages to that, beyond the fact that this might be a bit unidiomatic Lean? I can't see any difference in VS Code, but maybe I'm missing something?

[Mario Carneiro]

Under the hood there is an extra unnecessary call to solve1, but other than that I can't think of any way to distinguish the two

[Mario Carneiro]

and it's less characters so :thumbs_up:

[Johan Commelin]

When I give talks, the audience usually knows latex already, so sometimes I tell them that they need to translate as follows

lemma foobar (X : _) : blabla :=

-- \begin{lemma} \label{foobar}
-- Let $X$ be a ...
-- Then blabla

begin
  tac1
end

-- \begin{proof}
-- blabla
-- \end{proof}

I think the begin ... end is actually somewhat comforting for people with a LaTeX background. But of course this is a vague feeling on my side, and a very minor issue anyways.

[Alex J. Best]

Yeah I'd rather go the other way personally and kill {...} in favour of begin ... end but I guess it depends on the audience!

[Jasmin Blanchette]

Well I need to teach { ... } anyway for focusing on one of multiple subgoals, so there would be a slight economy in killing begin ... end as opposed to avoiding by { ... } (which has been my policy so far).

[Mario Carneiro]

You can use begin end in place of { } for focusing on subgoals btw

[Mario Carneiro]

Obviously we need to start writing proofs like this:

begin
  split,
  begin cases x with y,
        cases y,
        refl end
  begin cases x with y,
        cases y,
        begin cases x with y,
              cases y,
              refl end end
end

[Kevin Buzzard]

Trust me, you don't need { } to solve a subgoal :-) In NNG I just tell them "tactics work on the top goal" :-) . In experiments with mathematicians, I found that even getting them to remember to put commas at the end of tactics was an achievement. Every time sometime failed at this I'd add another "don't forget the comma" comment in NNG and we ended up with me saying it about ten times. Perhaps your users are more sophisticated though :-)

[Kevin Buzzard]

The style Mario suggested is also suggested in TPIL and when I mentioned it here before, the community's reaction was rather disdainful

[Mario Carneiro]

I have a lot of disdain for indentation styles where the indent depends on the length of words

[Mario Carneiro]

even

do tac1,
   tac2

drives me nuts because it screws up all the tab stops

[Jasmin Blanchette]

We use structured induction a lot and case works well in tandem with { ... }. Computer scientists have no problems with braces I think.

[Jasmin Blanchette]

As for the "community's reaction", well, I'm not trying to teach idiomatic Lean anyway. I'm sure the community's reaction would be negative if I told them I don't teach rfl, I use fix as an alias for assume (for data), etc. But they're not my audience. If by { ... } works as well as begin ... end, I think I'll embrace it.

[Kevin Buzzard]

An alternative fix for Mario's objection is to only use 5 letter tactics