giving extra info to `cases` tactic

Stream: new members

[Pedro Sánchez Terraf]

(not a new member, but potentially silly question anyway)
I have this #xy-ed MWE:

import Mathlib.SetTheory.Ordinal.Basic

inductive Sigmo (y : Set α) : ℕ → Set α → Prop
  | basic : Sigmo y 0 x
  | unio (_ : j < i) (_ : Sigmo y j x) : Sigmo y i x

example (h : Sigmo y 1 z) : Sigmo y 0 z := by
  cases h; aesop

cases realizes at once that (1 : ℕ) is indeed different from (0 : ℕ) and only handles the unio case to aesop. But the same def with Ordinal that does not seem to work:

inductive Sigme (y : Set α) : Ordinal → Set α → Prop
  | basic : Sigme y 0 x
  | unio (_ : j < i) (_ : Sigme y j x) : Sigme y i x

example (h : Sigme y 1 z) : Sigme y 0 z := by
  cases h
  /-
  dependent elimination failed, failed to solve equation
    Quot.mk Setoid.r { α := PUnit, r := EmptyRelation, wo := (_ : IsWellOrder PUnit EmptyRelation) } =
      Quot.mk Setoid.r { α := PEmpty, r := EmptyRelation, wo := (_ : IsWellOrder PEmpty EmptyRelation) }
  -/

At least, it seems that the error is about cases trying to equate 0 with 1. How do I tell it that basic does not apply here?

[Eric Rodriguez]

I have got to admit that I have absolutely no clue what is going on here, I assume cases wants to try and eliminate the case that h comes from basic, but I will say that this is solvable using "just" casesOn so maybe that's at least a workaround for your real situation?

example (h : Sigme y 1 z) : Sigme y 0 z := by
  refine h.casesOn ?_ ?_
  apply Sigme.basic
  intros
  apply Sigme.basic

[Kyle Miller]

"dependent elimination" is the thing that deals with type indices, and it's able to automatically handle equations between indices involving constructors of inductive types. The main problem is that Ordinal is not an inductive type (it's a quotient), and a secondary problem is that you can't directly communicate with cases about how to solve (or disprove) additional equations.

An indirect way to communicate with cases is to use generalize to turn certain expressions into variables first, and then that leaves you with the obligations to handle index equalities.

example (h : Sigme y 1 z) : Sigme y 0 z := by
  generalize h1 : (1 : Ordinal) = one at h
  cases h
  · simp at h1
  · cases h1
    /-
    α✝: Type ?u.1317
    yz: Set α✝
    j✝: Ordinal.{?u.1510}
    x✝¹: Sigme y j✝ z
    x✝: j✝ < 1
    ⊢ Sigme y 0 z
    -/

[Kyle Miller]

(I think "dependent elimination" in particular refers to doing cases on inductive types with indices, since these have more complicated dependent types, but I'm not actually sure.)

[Pedro Sánchez Terraf]

Eric Rodriguez said:

I will say that this is solvable using "just" casesOn so maybe that's at least a workaround for your real situation?

Thanks, I had forgotten the naming convention of the low-level theorems on inductive predicates. I tried to apply it to my use case but I couldn't manage to get it through. @Kyle Miller's hack did the trick.

Immediately after the generalization, cases knew that all other cases were unnecessary and right after that I did a rw [←h1] to get back to the original state. (This was actually part of a Lean3 ported proof using induction', and it seems that this tactic knew something about this trick!)