Why does "cases" fail and what to do then? (mismatch motive)

Stream: new members

[Malvin Gattinger]

I am confused about when "cases" works and what I should use when it does not. My vague understanding is that it only works when the goal is a Prop, but I am wondering whether there is a fundamental reason behind this restriction.

import Mathlib.Tactic.Tauto

def splitCases : α → β → (∀ γ ∈ [α, β], γ) := by
  intro a b γ γ_def
  simp at γ_def
  -- The goal here does not yet mention Prop.
  cases γ_def -- this actually restricts α,β,γ to be Prop !!
  · tauto
  · tauto

noncomputable -- I guess this is because we do not have DecidableEq Type?
def splitNoCases {α β : Type} : List α → List β → (∀ γ ∈ [α, β], List γ) := by
  intro a b γ γ_def
  simp at γ_def
  -- cases γ_def -- does not work because the goal is List γ.
  if h : γ = α then
    subst h; exact a
  else
    if h : γ = β then
     subst h; exact b
   else
     exfalso; tauto

def splitNoCases' {α β : Nat} : Fin α → Fin β → (∀ γ ∈ [α, β], Fin γ) := by
  intro a b γ γ_def
  simp at γ_def
  -- cases γ_def -- does not work: type mismatch when assigning motive
  if h : γ = α then
    subst h; exact a
  else
    if h : γ = β then
     subst h; exact b
   else
     exfalso; tauto

What are shorter and more elegant ways to do this if-then-else chaining? I also tried to use "cases (decide ...)" but it seems tedious with disjunctions. How do I do it if instead of [α, β] I have some arbitrary indexing type? Many thanks in advance for any help!

[Kevin Buzzard]

If the goal isn't a Prop then arguably you shouldn't be in tactic mode at all! High-powered tactics like simp will produce horrible terms which will be very hard to work with. They're fine in proofs because proofs are erased.

[Kyle Miller]

Cases uses the casesOn associated to an inductive type, which is specialized to Prop. In this case, I think you're using List.Mem.casesOn, and you can use #check to verify.

[Kyle Miller]

Here's how I would probably write the last function:

def splitNoCases' {α β : Nat} (a : Fin α) (b : Fin β) (γ : Nat) (γ_def : γ ∈ [α, β]) : Fin γ :=
  if h : γ = α then
    Fin.cast h.symm a
  else if h' : γ = β then
    Fin.cast h'.symm b
  else
    by exfalso; simp at γ_def; tauto

[Malvin Gattinger]

Thanks! This also made me learn about ▸ which seems to be a general version of things like Fin.cast.

[Kyle Miller]

It's general, and it's how Fin.cast itself can be implemented, but be aware that it's better to use Fin.cast, and to define functions such as Fin.cast, since you can write better simp lemmas for such functions than ▸.