Zulip Chat Archive

Stream: Lean for teaching

Topic: by { ... } vs. begin ... end


Jasmin Blanchette (Jun 19 2020 at 17:16):

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 (Jun 19 2020 at 17:49):

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 (Jun 19 2020 at 17:50):

and it's less characters so :thumbs_up:

Johan Commelin (Jun 20 2020 at 05:28):

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 (Jun 20 2020 at 05:32):

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 (Jun 20 2020 at 08:17):

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 (Jun 20 2020 at 08:21):

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

Mario Carneiro (Jun 20 2020 at 08:23):

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 (Jun 20 2020 at 08:32):

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 (Jun 20 2020 at 08:33):

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 (Jun 20 2020 at 08:34):

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

Mario Carneiro (Jun 20 2020 at 08:35):

even

do tac1,
   tac2

drives me nuts because it screws up all the tab stops

Jasmin Blanchette (Jun 20 2020 at 08:56):

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

Jasmin Blanchette (Jun 20 2020 at 08:58):

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 (Jun 20 2020 at 09:14):

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


Last updated: Dec 20 2023 at 11:08 UTC