Custom recursor in term mode

Stream: new members

[Jakub Nowak]

Writing custom recursor lets you use it with cases or induction. Is there a way to use custom recursor in term mode other than just calling it? Afaik, it's not possible to use custom recursor with match, are there plans to make it possible?

import Mathlib

variable {V : Type*} [Fintype V] {G : SimpleGraph V}
open SimpleGraph

@[elab_as_elim]
def SimpleGraph.Walk.IsPath.rec₂ {motive : {u v : V} → (p : G.Walk u v) → p.IsPath → Sort*}
    (nil : {u : V} → motive (.nil (u := u)) .nil)
    (cons : {u v : V} → (w : V) → (p : G.Walk w v) → (hp : p.IsPath) → (hu : u ∉ p.support) → (h : G.Adj u w) →
      motive (.cons h p) (.cons hp hu))
    {u v : V} {p : G.Walk u v} (hp : p.IsPath) : motive p hp := by
  cases p with
  | nil => exact nil
  | cons h p =>
    have := (cons_isPath_iff h p).mp hp
    exact cons _ p this.1 this.2 h

example {u v : V} {p : G.Walk u v} (hp : p.IsPath) : p.IsPath := by
  cases hp using Walk.IsPath.rec₂ with
  | nil => sorry
  | cons w p hp hu h => sorry

example {u v : V} {p : G.Walk u v} (hp : p.IsPath) : p.IsPath :=
  Walk.IsPath.rec₂ sorry (fun w p hp hu h ↦ sorry) hp

example {u v : V} {p : G.Walk u v} (hp : p.IsPath) : p.IsPath :=
  -- Made-up syntax.
  match hp using Walk.IsPath.rec₂ with
  | nil => sorry
  | cons w p hp hu h => sorry

[Aaron Liu]

match is a lot more complicated than just finding the right recursor so you can't exactly just plug in a different one

[Jakub Nowak]

Can you show an example of what makes match more complicated than cases?

[Aaron Liu]

hmmm.. but cases is complicated too and you can feed it some other recursor

[Aaron Liu]

I guess I don't know then

[Jakub Nowak]

I think the difference is that match allows you to use more complicated patterns, and it can also automatically prove that some cases are impossible. But I don't think that any of that makes it harder to add custom recursor support for match.

[Aaron Liu]

Jakub Nowak said:

Can you show an example of what makes match more complicated than cases?

You can simultaneously match on multiple discriminants
You can have complicated patterns
You can feed it disequalities to eliminate impossible branches
You get a splitter

[Jakub Nowak]

What's "splitter"?

[Aaron Liu]

Well cases does some HEq stuff to solve equations I wonder does that just go away when you use a custom eliminator?

[Aaron Liu]

Jakub Nowak said:

What's "splitter"?

It's what the split tactic uses when splitting a match

[Jakub Nowak]

So if you're using match in its simplest form then splitter is just recursor for the type?

[Aaron Liu]

I guess yeah

[Aaron Liu]

so the match maker is a way to generate recursors?

[Jakub Nowak]

Aaron Liu said:

Well cases does some HEq stuff to solve equations I wonder does that just go away when you use a custom eliminator?

I'm not sure if we're thinking about the same thing. When cases isn't able to replace the matched-on expression in the context because of dependant types, then it just doesn't. That's probably the difference with match, because match I think would error in this case.

[Aaron Liu]

no I mean when it's doing equations

[Aaron Liu]

I feel like you're talking about generalizing the variable

[Aaron Liu]

look at all that heq

/--
info: Try this:
  [apply] Eq.casesOn (motive := fun a t => y = a → h ≍ t → y = x) h
    (fun h_1 =>
      Eq.ndrec (motive := fun {y} => ∀ (h : x = y), h ≍ Eq.refl x → y = x) (fun h h_2 => Eq.refl x) (Eq.symm h_1) h)
    (Eq.refl y) (HEq.refl h)
-/
#guard_msgs in
example {α : Sort u} {x y : α} (h : x = y) : y = x := by?
  cases h
  rfl

[Aaron Liu]

Well this time it didn't end up doing anything with it

[Aaron Liu]

But you can see it present

[Jakub Nowak]

Aaron Liu said:

Well cases does some HEq stuff to solve equations I wonder does that just go away when you use a custom eliminator?

I think it doesn't? It's the same as cases h using Eq.casesOn, but HEq stuff didn't came from Eq.casesOn.

[Aaron Liu]

Here's a slightly more complicated one?

/--
info: Try this:
  [apply] Nat.le.casesOn (motive := fun a t => 1 = a → h ≍ t → h ≠ h) h
    (fun h_1 => Nat.elimOffset 0 (0 + 2) 1 h_1 fun x => False.elim (noConfusion_of_Nat Nat.ctorIdx x))
    (fun {m} a h_1 =>
      Nat.elimOffset 0 m 1 h_1 fun x =>
        Eq.ndrec (motive := fun {m} => ∀ (a : Nat.le 3 m), h ≍ Nat.le.step a → h ≠ h)
          (fun a h_2 =>
            Eq.symm (eq_of_heq h_2) ▸
              Nat.le.casesOn (motive := fun a_1 t => 0 = a_1 → a ≍ t → Nat.le.step a ≠ Nat.le.step a) a
                (fun h => False.elim (noConfusion_of_Nat Nat.ctorIdx h))
                (fun {m} a_1 h => False.elim (noConfusion_of_Nat Nat.ctorIdx h)) (Eq.refl 0) (HEq.refl a))
          x a)
    (Eq.refl 1) (HEq.refl h)
-/
#guard_msgs in
example (h : 3 ≤ 1) : h ≠ h := by?

[Aaron Liu]

I think I can see the pattern now