cases exposes type

Stream: mathlib4

[Matthew Ballard]

Is this behavior expected?

import Mathlib.Tactic

variable (α : Type*)

def Mozzy : Type _ := Option α

namespace Mozzy

@[match_pattern] def some {α} : α → Mozzy α := Option.some

@[match_pattern] def none {α} : Mozzy α := Option.none

instance : Coe α (Mozzy α) := ⟨some⟩

open Mozzy

example {α} (p : Mozzy α → Prop) (hn : p none) (hs : ∀ (a : α), p a) (a : Mozzy α) : p a := by
  cases a
  · simp [hn]  -- simp made no progress, we see Option.none
  · simp [hs] -- simp made no progress, we see Option.some

example {α} (p : Mozzy α → Prop) (hn : p none) (hs : ∀ (a : α), p a) (a : Mozzy α) : p a := by
  match a with
  | none => simp [hn]  -- done
  | some _ => simp [hs] -- done

[Adam Topaz]

I don't know if it's expected, but if you change the two defs to abbrev, then it works as expected. Looking at two examples from mathlib where match_pattern is used, they were both reducible. Is reducability a requirement for matchpattern?

[Adam Topaz]

Or perhaps it's an issue with cases?

[Adam Topaz]

I think it might be an issue with the cases tactic.

[Eric Wieser]

What if you write a custom recursors?

[Eric Wieser]

(like docs#WithTop.recTopCoe/

[Matthew Ballard]

I got this from docs#WithBot.unbot'_le_iff. rintro behaves similarly

[Matthew Ballard]

Is there an argument this behavior is desirable?

[Alex J. Best]

I think one should add custom eliminators like

@[eliminator]
def casesOn  {α : Type u} {motive : Mozzy α → Sort u_1} (t : Mozzy α) (none : motive Mozzy.none)
  (some : (val : α) → motive (Mozzy.some val)) : motive t := Option.casesOn t none some

in cases like this, otherwise lean tries to whnf the type and match that with an inductive, and then uses that eliminator instead.

I'm not sure what to do about the cases / rec (cases / induction) distinction though in cases where it matters

[Matthew Ballard]

I assume we don't have an attribute that generates this and the match patterns automatically?