cases vs casesOn

Stream: new members

[Snir Broshi]

Here's a proof using the cases tactic on an inductive:

import Mathlib.Data.Sym.Sym2
theorem foo {a b a' b' : Nat} (h : Sym2.Rel _ (a, b) (a', b')) :
    (a = a' ∧ b = b') ∨ (a = b' ∧ b = a') := by
  cases h with
  | refl => exact Or.inl ⟨rfl, rfl⟩
  | swap => exact Or.inr ⟨rfl, rfl⟩

I want to instead give a concise proof term, such as:

import Mathlib.Data.Sym.Sym2
theorem foo {a b a' b' : Nat} (h : Sym2.Rel _ (a, b) (a', b')) :
    (a = a' ∧ b = b') ∨ (a = b' ∧ b = a') :=
  h.casesOn (Or.inl ⟨rfl, rfl⟩) (Or.inr ⟨rfl, rfl⟩)

but for some reason h.casesOn takes the goal as is and just adds ∀ (x y : ℕ) before it.
Is casesOn not the correct theorem? Or is the huge proof term unavoidable?

[Robin Arnez]

casesOn is a very simple definition that just splits into cases. cases does something more elaborate, something like:

import Mathlib.Data.Sym.Sym2

theorem foo {a b a' b' : Nat} (h : Sym2.Rel _ (a, b) (a', b')) :
    (a = a' ∧ b = b') ∨ (a = b' ∧ b = a') :=
  h.casesOn (motive := fun x y _ => x = (a, b) → y = (a', b') → _)
    (fun _ _ hx hy => .inl (Prod.mk.inj (hx.symm.trans hy)))
    (fun _ _ hx hy => Prod.noConfusion hx fun h₁ h₂ => .inr (Prod.mk.inj (h₁ ▸ h₂ ▸ hy) |>.symm))
    rfl rfl

In other words, it adds equalities to the motive that we prove using rfl and that we can then use in the body. As you can tell this is neither smaller nor better so here is an alternative:

theorem foo {a b a' b' : Nat} : Sym2.Rel _ (a, b) (a', b') → (a = a' ∧ b = b') ∨ (a = b' ∧ b = a')
  | .refl _ _ => .inl ⟨rfl, rfl⟩
  | .swap _ _ => .inr ⟨rfl, rfl⟩

match, contrasting casesOn, has similar capabilities to cases (actually match uses cases).

[Snir Broshi]

Thanks, I'm thoroughly confused about all this though-
When I used casesOn it had 2 parameters, but when you added a motive it had 4.
Also there's not only cases and casesOn, but there's also match which does something slightly different? And there's also the have ⟨ ... ⟩ := ... tactic, which also sometimes complains about motive, although I'm not sure if it can handle sum types and not just product types.
If I understand correctly, proof irrelevance is the cause of all this?

What I'm asking is: Do you know a good resource to learn this from? Since it all seems to be haunting me no matter what I try to do with Lean.

[Snir Broshi]

By this I mean everything about motive, and the difference between Nonempty and Inhabited, or Exists and Subtype, and Sorts and Types and when I can or can't use cases or casesOn or `have ⟨ ... ⟩ := ....
I'm coming from Rocq, where all of this was simply something like intros a [b c | d [e | f]], and it never complained

[Kyle Miller]

If you're using recursors, the first thing you should be familiar with is its exact type:

#check Sym2.Rel.casesOn
/-
Sym2.Rel.casesOn.{u} {α : Type u} {motive : (a a_1 : α × α) → Sym2.Rel α a a_1 → Prop} {a✝ a✝¹ : α × α}
  (t : Sym2.Rel α a✝ a✝¹) (refl : ∀ (x y : α), motive (x, y) (x, y) ⋯) (swap : ∀ (x y : α), motive (x, y) (y, x) ⋯) :
  motive a✝ a✝¹ t
-/

The motive should be a function of three arguments. However, Robin gave it a function of five arguments (that's perfectly fine! A forall is a Prop after all). That means Sym2.Rel.casesOn is returning a function of two arguments in this case.

[Kyle Miller]

Snir said:

If I understand correctly, proof irrelevance is the cause of all this?

No, definitely not. Dependent type theory is the cause.

There's a reason we have all these high-level tactics and elaborators to avoid ever needing to touch recursors by hand. It's a good exercise to write recursor expressions, to see how it works under the hood, but that doesn't need to come before getting familiar first with how the system is actually used.

[Snir Broshi]

Kyle Miller said:

If you're using recursors, the first thing you should be familiar with is its exact type:

I tried checking the type of casesOn, but it complained with a separate cryptic error message:

import Mathlib.Data.Sym.Sym2
theorem foo {a b a' b' : Nat} (h : Sym2.Rel _ (a, b) (a', b')) :
    (a = a' ∧ b = b') ∨ (a = b' ∧ b = a') := by
  #check h.casesOn
  cases h with
  | refl => exact Or.inl ⟨rfl, rfl⟩
  | swap => exact Or.inr ⟨rfl, rfl⟩

failed to elaborate eliminator, expected type is not available

[Snir Broshi]

Kyle Miller said:

No, definitely not. Dependent type theory is the cause.

So why is this never a problem in Rocq, which also uses dependent type theory?
When I asked why I can't destruct an Exists inside a function that returns Nat I was told it's because of proof irrelevance, that's why I suspected it's the cause of all of the motive things.

[Kyle Miller]

That error might be a hint that you shouldn't be using eliminators (aka recursors) by hand :upside_down: (Not everyone agrees with this. I guess I don't even agree, since in my graduate Lean course I had my students write recursor expressions in the first couple weeks!)

[Kyle Miller]

Snir said:

So why is this never a problem in Rocq

I don't understand then what "all this" refers to. Rocq doesn't avoid dependent type issues.

[Kyle Miller]

If you mean "why this complexity with elimination of propositions", then I guess, sure, that's motivated by proof irrelevance, as I understand. But that's such a small part of the discussion — I thought you were talking about working with casesOn, which is going to be about the same difficulty no matter what system you're working in.

[Kyle Miller]

#check h.casesOn doesn't work because you're giving it the term h.casesOn. If you gave it the full name of the identifier, Sym2.Rel.casesOn, you'd get the type signature.

#check has two modes: if you give it an identifier it shows you the type signature, but if you give it a general expression it will try to elaborate that expression and then give you the elaborated expression and its type.

[Kyle Miller]

I lost a draft message; I was going to mention Theorem Proving in Lean

[Snir Broshi]

Kyle Miller said:

Snir said:

So why is this never a problem in Rocq

I don't understand then what "all this" refers to. Rocq doesn't avoid dependent type issues.

Hmm, maybe I'm trying to do things in Lean that I never tried in Rocq, and I just think it works in Rocq

[Snir Broshi]

Kyle Miller said:

I lost a draft message; I was going to mention Theorem Proving in Lean

Looks like they mention all the casesOn and recOn and recursors, thank you!
I'll try to read it, it'll hopefully fix the way I approach Lean theorems :)

[Kyle Miller]

The match expression (according to https://rocq-prover.org/doc/v8.10/refman/language/cic.html#the-match-with-end-construction) appears to have the same universe elimination rules as Lean. It's motivated by program extraction; it causes ex to eliminate only into Prop, since in an extracted program proofs are erased, so getting the witness would amount to getting something from nothing.

Rocq has SProp too, which is analogous to Lean's Prop. That can only eliminate into SProp, just like Lean.

That match limitation is artificial though, since Rocq's eliminator for ex, ex_rec, does allow elimination into Set. Lean only allows the "ex_sind" eliminator for existentials, since Exists is "SProp"-valued.

If you want ex in Lean, you need to work with sigma types instead.

[Kyle Miller]

Snir said:

Kyle Miller said:

If you're using recursors, the first thing you should be familiar with is its exact type:

I tried checking the type of casesOn, but it complained with a separate cryptic error message:

Just to check: was there no type for casesOn when you hovered over it in the source code? That would be surprising. This usually works even if there are errors.

[Snir Broshi]

Kyle Miller said:

Just to check: was there no type for casesOn when you hovered over it in the source code?

There was, but since it both didn't work correctly for me and the #check showed an error I thought I might be seeing the type of a different casesOn or something
There's also no autocompletion for the name casesOn, even when it doesn't error