pattern matching with 'cases' and 'match'

Stream: lean4

[Paul Chisholm]

Consider the following nine proofs:

theorem case₁ (n : Nat) : n = 0 ∨ (∃m : Nat, n = m+1) := by
  cases n with
  | zero   => apply Or.inl rfl
  | succ x => apply Or.inr
              exact Exists.intro x rfl

theorem case₂ (n : Nat) : n = 0 ∨ (∃m : Nat, n = m+1) := by
  cases n with
  | Nat.zero   => apply Or.inl rfl
  | Nat.succ x => apply Or.inr
                  exact Exists.intro x rfl

theorem case₃ (n : Nat) : n = 0 ∨ (∃m : Nat, n = m+1) := by
  cases n with
  | 0   => apply Or.inl rfl
  | x+1 => apply Or.inr
           exact Exists.intro x rfl

theorem match₁ (n : Nat) : n = 0 ∨ (∃m : Nat, n = m+1) := by
  match n with
  | zero   => apply Or.inl (by simp)
  | succ x => apply Or.inr
              exact Exists.intro x rfl

theorem match₂ (n : Nat) : n = 0 ∨ (∃m : Nat, n = m+1) := by
  match n with
  | Nat.zero   => apply Or.inl (by simp)
  | Nat.succ x => apply Or.inr
                  exact Exists.intro x rfl

theorem match₃ (n : Nat) : n = 0 ∨ (∃m : Nat, n = m+1) := by
  match n with
  | 0   => apply Or.inl (by simp)
  | x+1 => apply Or.inr
           exact Exists.intro x rfl

theorem term₁ : (n : Nat) → n = 0 ∨ (∃m : Nat, n = m+1)
  | zero   => Or.inl rfl
  | succ x => Or.inr (Exists.intro x rfl)

theorem term₂ : (n : Nat) → n = 0 ∨ (∃m : Nat, n = m+1)
  | Nat.zero   => Or.inl rfl
  | Nat.succ x => Or.inr (Exists.intro x rfl)

theorem term₃ : (n : Nat) → n = 0 ∨ (∃m : Nat, n = m+1)
  | 0   => Or.inl rfl
  | x+1 => Or.inr (Exists.intro x rfl)

Of these, case₁, match₂, match₃, term₂ and term₃ are successful. case₂, case₃, match₁ and term₁ fail.

If I precede the proofs with open Nat then match₁ and term₁ succeed. I can see why this would be the case, by opening Nat you get access to the unqualified names. But if that is the case, why does case₁ succeed without open Nat.

Also, why can I pattern match on 0 and +1 in match₃ and term₃ but not in case₃.

[Mario Carneiro]

cases does not take a term, it takes an identifier followed by a list of names. The identifier refers to the bare constructor name (without the namespace) because it's actually coming from the name of one of the binders in the T.recOn recursor

[Mario Carneiro]

That's why you have to write zero, not Nat.zero or 0 (the latter is a syntax error because it's not an identifier, and the former just doesn't match the expected name which is unqualified zero).

[Mario Carneiro]

I agree that this syntax is a bit inconsistent with pattern matching elsewhere

[Sebastian Ullrich]

Mario Carneiro said:

I agree that this syntax is a bit inconsistent with pattern matching elsewhere

I had this discussion with @Leonardo de Moura quite early. Leo's stance is that cases should be internally consistent with and without using. I tend to agree with you that external consistency with regular pattern matching is more important, especially since using using is not all that common.

[Sebastian Ullrich]

Note that it gets more complicated if we also consider induction, which adds induction hypotheses on top of the constructor parameters, so it really isn't a regular pattern anymore. One proposal I had was to introduce the IH for a parameter x unhygienically as x.ih. But again this begs the question what it should look like with using. It could be resolved using a naming convention, e.g. if your custom recursor has parameters x and x_ih and only bind the former as y, the latter will be auto-introduced as y.ih. We didn't continue the discussion after that I believe though. If someone is motivated to resolve this, a comprehensive RFC would be great I'd say.

[Paul Chisholm]

Thanks for the info. That makes sense. For tactical proofs, from a style perspective is one of match or cases preferred over the other?

[Sebastian Ullrich]

Whichever fits your use case better. match can do nested pattern matching. cases can do case analysis without listing all constructors.

[Reinier van der Gronden]

One proposal I had was to introduce the IH for a parameter x unhygienically as x.ih

This is what I'm currently using in my poc of 'autocomplete cases/induction statements'. Why would that be unhygienic?

[Sebastian Ullrich]

If you can access a name that you didn't literally introduce as such, that's unhygienic according to the usual definition for macro systems

[Sebastian Ullrich]

But you're talking about synthesizing syntax, right? Then that doesn't apply.

[Reinier van der Gronden]

Yeah I was talking about syntax. While I'm still a little new, I would think that if you had

induction n with
| succ n n.ih => sorry

that you have literally introduced it right? Or did you mean what to name those hypotheses if you only use induction n as a tactic?

[Sebastian Ullrich]

Yes, if you insert that on the user's behalf, everything is fine

[Sebastian Ullrich]

The hygiene-bending implementation would be

induction n with
| n + 1 => apply n.ih; ...