rcases vs cases

Stream: new members

[Moti Ben-Ari]

In the example on p. 64 of MiL I replaced obtain with have and rcases

example (m n : ℕ) (coprime_mn : m.Coprime n) : m ^ 2 ≠ 2 * n ^ 2 := by
  intro sqr_eq
  have : 2 ∣ m := by
    sorry
  have h : ∃ c, m = c * 2 := by
    apply dvd_iff_exists_eq_mul_left.mp this
    rcases h with ⟨k, meq⟩

When I try to replace rcases with

    cases h with k meq

following Section 5 of @Kevin Buzzard 's RM where it is listed as the tactic to apply for an existential hypothesis like h: ∃ c, m = c * 2. P. 39 seems to say exactly what I want

5) If you have a hypothesis h : ∃ a, a^3 + a = 37 then cases h with x hx will give you a number x
and a proof [should be hypothesis?] hx : x^3 + x = 37.

[Riccardo Brasca]

In Lean 4 the syntax is

cases h with
  | intro w h => sorry

(you can write cases h and then click on the bulb). The other syntax comes from Lean3, but you can still use cases' h with n hn.

[Riccardo Brasca]

"...will give you a proof..." is correct, even if is't not standard mathematical terminology. It gives you (hx : x^3+x=37), that is a proof that x^3+x=37. Of course this proof comes from your h (that itself is a proof that ∃ a, a^3 + a = 37).

[Mauricio Collares]

I assume "RM" means "reference manual" and refers to https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2023/Part_C/tactics/cases.html, which uses Lean 3 as Riccardo pointed out. Although Lean 4 is standard now, it wasn't in January 2023 when the course was last taught. Maybe the 2024 version of the course, if it exists, will use Lean 4.

[Mario Carneiro]

You can also use let ⟨w, h⟩ := h when it is a single pattern, or obtain ⟨w, h⟩ := h to use the rcases backend

[Moti Ben-Ari]

Thanks for the help. It's rather confusing when there are many ways to implement the same thing; I guess it will become clear when I have more experience.

[Kevin Buzzard]

Mauricio Collares said:

I assume "RM" means "reference manual" and refers to https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2023/Part_C/tactics/cases.html, which uses Lean 3 as Riccardo pointed out. Although Lean 4 is standard now, it wasn't in January 2023 when the course was last taught. Maybe the 2024 version of the course, if it exists, will use Lean 4.

Indeed, my job for December is to rewrite that entire course document and all of the course repo in Lean 4 because the course will be running again in January.

[Utensil Song]

Moti Ben-Ari said:

Thanks for the help. It's rather confusing when there are many ways to implement the same thing; I guess it will become clear when I have more experience.

Personally, I don't like the verbose Lean 4 cases, nor do I need cases' as I can always go with obtain (handles 1 or more cases, plus accepting a proof) and it spells natural.

rintro is another weird spelling that joined the confusions around cases/rcases (if one only looks at their naming and their not-really-new-user-facing doc strings), until I simply see it as intros + obtains:

Understanding "rintro" for 1 pattern

import Std.Tactic.Rcases
import Mathlib.Tactic.Cases
import Mathlib.Tactic.Use

-- using `rintro`
example (p: Nat → Prop) : (∃ a, p a) → (∃ b, p b) → (∃ c, p c) := by
  rintro ⟨a, ha⟩ ⟨b, hb⟩
  use a

-- break `rintro` into `intro`s and `obtain`s
example (p: Nat → Prop) : (∃ a, p a) → (∃ b, p b) → (∃ c, p c) := by
  intro h1
  intro h2
  obtain ⟨a, ha⟩ := h1
  obtain ⟨b, hb⟩ := h2
  use a

-- rewrite `obtain` to `cases'`
example (p: Nat → Prop) : (∃ a, p a) → (∃ b, p b) → (∃ c, p c) := by
  intro h1
  intro h2
  cases' h1 with a ha
  cases' h2 with a ha
  use a

Understanding "rintro" for 1+ patterns

import Std.Tactic.Rcases
import Mathlib.Tactic.Cases
import Mathlib.Tactic.Use

-- using `rintro`
example (p: Nat → Nat → Prop) : (∃ a, (∃ b, p a b)) → (∃ c, (∃ d, p c d)) := by
  rintro ⟨a, ⟨b, hb⟩⟩
  use a
  use b

-- break `rintro` into `intro`s and `cases'`s
example (p: Nat → Nat → Prop) : (∃ a, (∃ b, p a b)) → (∃ c, (∃ d, p c d)) := by
  intro h
  cases' h with a ha
  cases' ha with b hb
  use a
  use b

-- collapse `cases'`s into a single `rcases`
example (p: Nat → Nat → Prop) : (∃ a, (∃ b, p a b)) → (∃ c, (∃ d, p c d)) := by
  intro h
  rcases h with ⟨a, ⟨b, hb⟩⟩
  use a
  use b

-- rewrite `rcases` to `obtain` then look at `rintro` above again
example (p: Nat → Nat → Prop) : (∃ a, (∃ b, p a b)) → (∃ c, (∃ d, p c d)) := by
  intro h
  obtain ⟨a, ⟨b, hb⟩⟩ := h
  use a
  use b

[Moti Ben-Ari]

Utensil Song said:

Personally, I don't like the verbose Lean 4 cases, nor do I need cases' as I can always go with obtain (handles 1 or more cases, plus accepting a proof) and it spells natural.

rintro is another weird spelling that joined the confusions around cases/rcases (if one only looks at their naming and their not-really-new-user-facing doc strings), until I simply see it as intros + obtains:

Most of my career has been in educational aspects of math and computer science, with emphasis on logic. It is rather frustrating that - although the logic and proof methods, as well as programming techniques, are very familiar - I'm having too much difficulty navigating Lean. I want to see if I can find better approaches to learning and teaching Lean. The answers to my questions have been extremely helpful and I will consider them in the light of my educational experience. Thanks!

[Alex J. Best]

Moti Ben-Ari said:

Thanks for the help. It's rather confusing when there are many ways to implement the same thing; I guess it will become clear when I have more experience.

Part of the reason is that there are basic tactics for doing certain things that are defined in Lean core itself. But the system is user extensible so that users can add their own more powerful tactics that in many cases subsume the functionality of the core ones to some extent. Mathlib and Std add many such tactics, but it would be bad style to override the names of the built in ones (as this could be even more confusing if tactics change meaning) so often similar but distinct names are chosen, hence there are many ways of doing the same thing when you build on these libraries.

[Ruben Van de Velde]

I don't see a good reason to have rcases alongside obtain, though

[Alex J. Best]

That is more of a historical artifact right? I must say that I do still think more in terms of rcases than obtain personally, maybe it just flows better left to right in my head that way

[Utensil Song]

If a new user learns rcases from verbose lean or informal , it certainly flows better.

obtain only feels better when one is already used to Lean's way of statement := proofand the idea of destructive style of pattern matching. It doesn't fully feel like "we obtain ... from ...".

[Wrenna Robson]

How does one use obtain, or Lean-4 cases? I really feel the lack of good tactic documentation nowadays!

[Yaël Dillies]

obtain patterns := terms is the syntax, where patterns is the appropriate combination of ⟨_, _⟩ and (_ | _).

[Utensil Song]

Wrenna Robson said:

How does one use obtain, or Lean-4 cases? I really feel the lack of good tactic documentation nowadays!

import Mathlib.Tactic

variable (p q r: Prop)

example (h: p ∨ q) : q ∨ p := by
  obtain (hp | hq) := h
  . exact Or.inr hp
  . exact Or.inl hq

example (h: p ∧ q) : q ∧ p := by
  obtain ⟨hp, hq⟩ := h
  exact ⟨hq, hp⟩

example (h: (p ∨ q) ∧ r) : r ∧ (q ∨ p) := by
  obtain ⟨hp | hq, hr⟩ := h
  . exact ⟨hr, Or.inr hp⟩
  . exact ⟨hr, Or.inl hq⟩

Do this example and these help?

[Ruben Van de Velde]

And for cases, you just type cases x and a little :light_bulb: comes up in Vs code that fills in the rest

[Utensil Song]

Ruben Van de Velde said:

And for cases, you just type cases x and a little :light_bulb: comes up in Vs code that fills in the rest

Or if you are using Cursor as the editor, you can just use Ctrl+. or Cmd+. because the :light_bulb: won't be showing, related: getcursor/cursor#745 .

[Kevin Buzzard]

It's a blue bulb FWIW

[Mario Carneiro]

BTW vscode has both yellow and blue bulbs. The blue one is a bit bigger and comes with a key combination to accept it, and represents code actions that are particularly recommended, like completions and error fixes. (Internally this corresponds to the isPreferred field on the code action.)