rintro < equation compiler?

Stream: general

[Kevin Buzzard]

Looking to level up my rintro skills.. Can I do with rintro what I can do with the equation compiler on pnat?

import data.pnat.basic

-- what I want to emulate
example : ℕ+ → true
| ⟨1, _⟩ := trivial
| ⟨n+2, _⟩ := trivial

example : ℕ+ → true :=
begin
  rintro (⟨n0, ⟨⟩⟩ | ⟨n1, h1⟩ | ⟨n, hn⟩),
  -- was hoping for 2 goals N. Want to name `a_property` but can't? No sign of n or hn
  /-
  a_property : 0 < 0
  ⊢ true

  a_property : 0 < 1
  ⊢ true

  a_property : 0 < 2
  ⊢ true

  a_val: ℕ
  a_property: 0 < a_val.succ.succ.succ
  ⊢ true
  -/
  repeat {sorry}
end

example : ℕ+ → true :=
begin
  rintro ⟨(_ | _ | n), hn⟩,
  cases hn, -- can I avoid cases after rintro?
  /-
  hn : 0 < 1
  ⊢ true
  n : ℕ
  hn : 0 < n.succ.succ
  ⊢ true
  -/
  repeat {sorry}
end

[Adam Topaz]

How does the equation compiler know to ignore the ⟨0, _⟩ case?

[Adam Topaz]

For example, lean complains about that case with this:

def foo : ℕ+ → ℕ
| ⟨1,_⟩ := 1
| ⟨n+2, _⟩  := 1

[Adam Topaz]

Looks like the equation compiler has something special for props?

def foo {P : ℕ+ → Sort 0} : Π (n : ℕ+), P n -- lean is happy
| ⟨1,_⟩ := _
| ⟨n+2, _⟩  := _

def bar {P : ℕ+ → Sort 1} : Π (n : ℕ+), P n -- lean complains
| ⟨1,_⟩ := _
| ⟨n+2, _⟩  := _

[Mario Carneiro]

@Kevin Buzzard This is a limitation of the syntax of rcases patterns. Logically, case trees are trees; you split on one thing in the context and then in each of the resulting subgoals you can do different kinds of split. rcases patterns, however, are limited in that in <a | b, pat>, we are saying "split the top level to get l,r, then split l to get two subgoals a and b, then split r with pat in subgoal 1, then split r with pat in subgoal 2", and it is not possible to supply two different values for pat in the two subgoals. It's perfectly within the realm of possibility for rcases to handle this, indeed it would be simpler if it could, but it is a limitation of the tuples-and-alts style pattern syntax.

The equation compiler uses a different syntax, where you instead describe all the subgoals, and all the splits that are needed to get to each of them (possibly containing a lot of redundant splits), and the computer then has to put them back together into a case tree. This is also a bit ambiguous, and you have seen the equation compiler sometimes generate spurious case splits because it reconstructed the wrong case tree. But by writing the patterns many times, you have the opportunity to make the patterns different in each case.

To get a true case tree, you need to use nested cases as in cases a with b c, {cases b with d e}, {cases c, {cases c}, {cases c}}. rcases can remove most of the need to have this, but due to the aforementioned limitation of tuples-and-alts patterns, you may sometimes need to have more than one rcases invocation as well. In short, my recommendation is:

example : ℕ+ → true :=
begin
  rintro ⟨(_ | _ | n), hn⟩, {cases hn},
  { sorry },
  { sorry },
end

[Mario Carneiro]

As a sketch of how one might extend the syntax to support the full range of case trees, we might use [pat1, pat2, pat3] to mean that this pattern will be invoked 3 times as a result of splits to the left of it, and in those 3 invocations it should use pat1, pat2, pat3 respectively. With that, you could write this case split as rintro ⟨(_ | _ | n), [⟨⟩, -, -]⟩, but one thing I don't like about this is that it makes the patterns more contextual than structural, and I think it decreases readability as a result.

[Kevin Buzzard]

Very interesting, thanks! I had not appreciated the difference between the two approaches before.