Unexpected eliminator resulting type

Stream: lean4

[Robert Maxton]

So, I'm looking at trying to build proper quotient categories (as the current structure only allows quotients of morphisms), and that has led me to doing lots of induction on paths of type Path ⟦X⟧ ⟦Y⟧.

However, directly trying to case or induction on such paths doesn't work; you can't use induction on them because ⟦X⟧ isn't a variable, and you can't use case on them because ... I don't know, it seems like case goes too far trying to unify the type with its eliminators because it ends up getting stuck trying to prove injectivity of a quotient constructor? That's how I'm parsing the error, anyway.

You can work around this by reverting/generalizing your statement to Path qX qYs for qX qY : Quotient s, but doing that every time is kind of a pain, so I wrote a custom recursor that does it for you. And it ... almost works!

notation:max s ".⟦" x "⟧" => @Quotient.mk _ s x

def pathOfEq {X Y X' Y' : V}
    (p : Path X Y) (hX : X = X') (hY : Y = Y') : Path X' Y' :=
  cast (congrArg₂ Path hX hY) p

/--Helper recursor for returning from explicit `Path ⟦X⟧ ⟦Y⟧` to general `Path qX qY`,
as `cases` can't handle the former directly.-/
@[elab_as_elim]
def recOn_quot' {X Y : V} {s : Setoid V} {motive : {X Y : V} → Path s.⟦X⟧ s.⟦Y⟧ → Sort*}
    (p : Path s.⟦X⟧ s.⟦Y⟧)
    (generalize : ∀ {qX qY : Quotient s} (p : Path qX qY) (hX : qX = s.⟦X⟧) (hY : qY = s.⟦Y⟧),
      motive (pathOfEq p hX hY)) : motive p := generalize p rfl rfl


@[elab_as_elim]
def recOn_quot {X Z : V} {s : Setoid V} {motive : {qY : Quotient s} → Path s.⟦X⟧ qY → Sort*}
    (p : Path s.⟦X⟧ s.⟦Z⟧) (nil : ∀ {Y} (h : s.⟦X⟧ = s.⟦Y⟧), motive (pathOfEq nil rfl h))
    (cons : ∀ (qY qZ : Quotient s) (p : Path s.⟦X⟧ qY) (f : qY ⟶ qZ),
      motive p → motive (p.cons f)) : motive p := by
  induction' p using recOn_quot' with qX qZ p hX hZ
  cases p with
  | nil => cases hX; exact nil hZ
  | @cons qY _ p f =>
      subst hX hZ
      refine qY.hrecOn
        (motive := fun qY' ↦ ∀ (h : qY = qY'), motive <| (pathOfEq p rfl h).cons (homOfEq f h rfl))
        (fun Y hY ↦
          cons _ _ (pathOfEq p _ hY) (homOfEq f hY _)
            ((pathOfEq p _ hY).recOn (nil rfl) (cons _ _))) ?h rfl
      intro Y₁ Y₂ hY
      replace hY := Quotient.sound hY
      simp
      rw [hY]

[Robert Maxton]

However, I've got two problems with this code.

[Robert Maxton]

One is a performance problem: compiling this recursor really makes the compiler chug, it will eat all my CPU and set my fan speed to max for a solid few seconds, and when I used it to build a recOn₂_quot (not shown), I often ended up waiting 30s+ for simps forto finish. That's a hefty enough performance issue for me to be somewhat concerned about it; if possible I'd like to fix that.

[Robert Maxton]

More pressingly, it also still doesn't work with the tactic -- it does what I need it to do, I can manually write a convert or refine statement using it , but if I try to use it with cases or induction, it throws Unexpected eliminator resulting type.

(Tbf, I'm not actually sure it should work with induction since induction doesn't want to handle indices that aren't variables, but it doesn't work in cases either.)

[Robert Maxton]

The above is the core of the code, but here's a #mwe:

import Mathlib.Combinatorics.Quiver.Path
import Mathlib.Tactic.Cases

open Quiver

universe v u
variable {V : Type u} [Quiver.{v} V]

notation:max s ".⟦" x "⟧" => @Quotient.mk _ s x

attribute [symm] Setoid.symm

namespace Quotient

variable {s : Setoid V}

@[ext]
structure Hom (qX qY : Quotient s) where
  src : {X // ⟦X⟧ = qX}
  tgt : {Y // ⟦Y⟧ = qY}
  hom : src.1 ⟶ tgt.1

initialize_simps_projections Hom --(src_property → src_class, tgt_property → tgt_class)

-- #check Hom.recOn
lemma Hom.src_class {qX qY : Quotient s} (f : Hom qX qY) : ⟦f.src.1⟧ = qX := f.src.2
lemma Hom.src_class' {qX qY : Quotient s} (f : Hom qX qY) : f.src.1 ≈ qX.out := by
  simp_rw [←f.src_class]; symm; exact Quotient.mk_out _
lemma Hom.src_class'' {X Y : V} (f : Hom s.⟦X⟧ s.⟦Y⟧) : f.src.1 ≈ X :=
  Quotient.exact f.src.2

lemma Hom.tgt_class {qX qY : Quotient s} (f : Hom qX qY) : ⟦f.tgt.1⟧ = qY := f.tgt.2
lemma Hom.tgt_class' {qX qY : Quotient s} (f : Hom qX qY) : f.tgt.1 ≈ qY.out := by
  simp_rw [←f.tgt_class]; symm; exact Quotient.mk_out _
lemma Hom.tgt_class'' {X Y : V} (f : Hom s.⟦X⟧ s.⟦Y⟧) : f.tgt.1 ≈ Y :=
  Quotient.exact f.tgt.2



noncomputable scoped instance : Quiver (Quotient s) where
  Hom qX qY := Hom qX qY

end Quotient
open Quotient
def pathOfEq {X Y X' Y' : V}
    (p : Path X Y) (hX : X = X') (hY : Y = Y') : Path X' Y' :=
  cast (congrArg₂ Path hX hY) p

/--Helper recursor for returning from explicit `Path ⟦X⟧ ⟦Y⟧` to general `Path qX qY`,
as `cases` can't handle the former directly.-/
@[elab_as_elim]
def recOn_quot' {X Y : V} {s : Setoid V} {motive : {X Y : V} → Path s.⟦X⟧ s.⟦Y⟧ → Sort*}
    (p : Path s.⟦X⟧ s.⟦Y⟧)
    (generalize : ∀ {qX qY : Quotient s} (p : Path qX qY) (hX : qX = s.⟦X⟧) (hY : qY = s.⟦Y⟧),
      motive (pathOfEq p hX hY)) : motive p := generalize p rfl rfl


@[elab_as_elim]
def recOn_quot {X Z : V} {s : Setoid V} {motive : {qY : Quotient s} → Path s.⟦X⟧ qY → Sort*}
    (p : Path s.⟦X⟧ s.⟦Z⟧) (nil : ∀ {Y} (h : s.⟦X⟧ = s.⟦Y⟧), motive (pathOfEq .nil rfl h))
    (cons : ∀ (qY qZ : Quotient s) (p : Path s.⟦X⟧ qY) (f : qY ⟶ qZ),
      motive p → motive (p.cons f)) : motive p := by
  induction' p using recOn_quot' with qX qZ p hX hZ
  cases p with
  | nil => cases hX; exact nil hZ
  | @cons qY _ p f =>
      subst hX hZ
      refine qY.hrecOn
        (motive := fun qY' ↦ ∀ (h : qY = qY'), motive <| (pathOfEq p rfl h).cons (homOfEq f h rfl))
        (fun Y hY ↦
          cons _ _ (pathOfEq p _ hY) (homOfEq f hY _)
            ((pathOfEq p _ hY).recOn (nil rfl) (cons _ _))) ?h rfl
      intro Y₁ Y₂ hY
      replace hY := Quotient.sound hY
      simp
      rw [hY]


example {X Y : V} (p : Path s.⟦X⟧ s.⟦Y⟧) : False := by
  induction p using recOn_quot
--unexpected eliminator resulting type
--  motive p