angle brackets in tutorial is hard

Stream: general

[Miguel Raz Guzmán Macedo]

Hi!
I'm working on the tutorial levels and I'm at stage 6 of sub_sequences. However, I've done a few of the previous challenges that included destructuring the proof with \< and \> and I still very much struggle to come up with its applications by my own.
@Kenny Lau asked me to post about my experience here - perhaps a cheat sheet of sorts can be put together with some basic examples?

The description of the mathlib docs under rcases wasn't too helpful either.

[Patrick Massot]

It would be easier to help you if you posted a specific example.

[Patrick Massot]

Also, you should know you can do the whole tutorial without ever using a single bracket like this (this is what my students did during the first life of this tutorial). They are used only to compress proofs.

[Heather Macbeth]

Maybe @Miguel Raz Guzmán Macedo is asking about when to use the angle brackets, rather than about how to use them in a particular example?

[Heather Macbeth]

Here are a few use cases, apologies if you already know them:

• rcases with angle brackets can replace several recursive uses of cases;
• rintros with angle brackets can replace intros + cases;
• exact with angle brackets can replace use + exact.

[Miguel Raz Guzmán Macedo]

Thanks @Heather Macbeth , that's more of what I meant. If those examples were in a handy "Lean cheatsheet" or something like that it would be really useful.

What I mean more specifically @Patrick Massot is that you learn them as you go along in the tutorial but there's always like 4 different things going on when they're used, and that can be overwhelming to keep track of.

e.g., they're used like this in 06_sequences:

lemma cluster_limit (hl : seq_limit u l) (ha : cluster_point u a) : a = l :=
begin
  -- sorry
  rcases ha with ⟨φ, φ_extr, lim_u_φ⟩,
  have lim_u_φ' : seq_limit (u ∘ φ) l,
    from subseq_tendsto_of_tendsto' hl φ_extr,
  exact unique_limit lim_u_φ lim_u_φ',
end

But this is the first example use of it in file 00_ first_proofs:

example {x y : ℝ} : (∀ ε > 0, y ≤ x + ε) →  y ≤ x :=
begin
  contrapose!,
  exact assume h, ⟨(y-x)/2, by linarith, by linarith⟩,
end

/-

Which at least to me as a beginner has waaaay too much going on in one line to figure out precisely how they work.

[Bryan Gin-ge Chen]

To be fair, 00_first_proofs only says: "The goal is to demonstrate what it feels like to prove things using Lean and mathlib. [...] Everything is covered again more slowly and with exercises in the next files."

[Bryan Gin-ge Chen]

I do agree it'd be helpful to have a cheatsheet or reference with some examples of angle brackets / anonymous constructor notation. It's mentioned a few times in TPiL, but there's not really a dedicated section on it: 3.3.1 9.1 10.1

[Johan Commelin]

@Miguel Raz Guzmán Macedo Thanks for the feedback! That's very valuable. Particularly with the workshop coming up next week!

[Miguel Raz Guzmán Macedo]

I understand the scope can't be all encompassing. A cheat sheet of idiomatic tactic solutions would be useful.

[Miguel Raz Guzmán Macedo]

@Johan Commelin yup, I'm trying to speedrun the tutorials to get up to speed for next week. See ya there!

[Patrick Massot]

@Miguel Raz Guzmán Macedo you don't have to speedrun the tutorials before next week. Next week won't assume any Lean knowledge. Of course lectures and exercises sessions are always easier when you already know everything about the topic, but if you do the first seven tutorials then it means you won't learn anything before Wednesday.

[Patrick Massot]

About the examples you give. I honestly don't know how we could do better in the zeroth file. You have the uncompressed proof right before, at https://github.com/leanprover-community/tutorials/blob/master/src/exercises/00_first_proofs.lean#L175-L188. The compressed one is exactly the same, gathering five lines into one. Then you can put your cursor at the beginning of this compressed line and slowly move it towards the right while watching the tactic state changing. What else could we do?

[Patrick Massot]

And the cluster limit example from the 6th file is much simpler. You can replace it with cases ha with φ H, cases H with φ_extr, lim_u_φ. If you don't understand the cases version then you need to go back to the second file (explaining the "and" logical connective). Once you understand the double cases solutions, I don't know what to write beyond: you can do it at once using rcases and this bracket syntax (but feel free to PR a new explanation).

[Scott Morrison]

(On the other hand, someone who has done a speedrun will probably be a helpful contributor in the exercise sessions. :-)