getting `aesop` to use cases with custom cases eliminators

Stream: lean4

[Robin Carlier]

Consider this #mwe (which is probably not as minimal as it could be)

import Mathlib.Logic.Unique
import Aesop

inductive CustomType
  | left
  | right

attribute [local aesop safe cases] CustomType -- works

def CustomHom : CustomType → CustomType → Type
  | .left, .left => PUnit
  | .right, .left => PEmpty
  | .left, .right => PUnit
  | .right, .right => PUnit
instance : Unique (CustomHom .left .left) := inferInstanceAs (Unique PUnit)
instance : Unique (CustomHom .left .right) := inferInstanceAs (Unique PUnit)
instance : Unique (CustomHom .right .right) := inferInstanceAs (Unique PUnit)

@[elab_as_elim, cases_eliminator, induction_eliminator]
def customHomInduction
    {P : {x y : CustomType} → (CustomHom x y) → Sort*}
    (left : P (default : CustomHom .left .left))
    (right : P (default : CustomHom .right .right))
    (left_right : P (default : CustomHom .left .right))
    {x y : CustomType} (f : CustomHom x y) : P f :=
  match x, y, f with
  | .left, .left, _ => left
  | .right, .right, _ => right
  | .left, .right, _ => left_right

attribute [local aesop safe cases] CustomHom -- fails

Are there some aesop magic words to get aesop to call cases on hypotheses of the form f : CustomHom x y?

[Jannis Limperg]

This works:

import Mathlib.Logic.Unique
import Aesop

inductive CustomType
  | left
  | right

attribute [local aesop safe cases] CustomType -- works

def CustomHom : CustomType → CustomType → Type
  | .left, .left => PUnit
  | .right, .left => PEmpty
  | .left, .right => PUnit
  | .right, .right => PUnit
instance : Unique (CustomHom .left .left) := inferInstanceAs (Unique PUnit)
instance : Unique (CustomHom .left .right) := inferInstanceAs (Unique PUnit)
instance : Unique (CustomHom .right .right) := inferInstanceAs (Unique PUnit)

@[elab_as_elim, cases_eliminator, induction_eliminator]
def customHomInduction
    {P : {x y : CustomType} → (CustomHom x y) → Sort*}
    (left : P (default : CustomHom .left .left))
    (right : P (default : CustomHom .right .right))
    (left_right : P (default : CustomHom .left .right))
    {x y : CustomType} (f : CustomHom x y) : P f := by
  aesop (add norm unfold CustomHom)

The issue is that Aesop needs to be told to reduce CustomHom .right .left to PEmpty; after that it does cases on PEmpty via a built-in rule.

[Jannis Limperg]

Another way:

import Mathlib.Logic.Unique
import Aesop

inductive CustomType
  | left
  | right

attribute [local aesop safe cases] CustomType -- works

def CustomHom : CustomType → CustomType → Type
  | .left, .left => PUnit
  | .right, .left => PEmpty
  | .left, .right => PUnit
  | .right, .right => PUnit
instance : Unique (CustomHom .left .left) := inferInstanceAs (Unique PUnit)
instance : Unique (CustomHom .left .right) := inferInstanceAs (Unique PUnit)
instance : Unique (CustomHom .right .right) := inferInstanceAs (Unique PUnit)

@[aesop norm forward]
theorem customHom_right_left_false : CustomHom .right .left → False := nofun

@[elab_as_elim, cases_eliminator, induction_eliminator]
def customHomInduction
    {P : {x y : CustomType} → (CustomHom x y) → Sort*}
    (left : P (default : CustomHom .left .left))
    (right : P (default : CustomHom .right .right))
    (left_right : P (default : CustomHom .left .right))
    {x y : CustomType} (f : CustomHom x y) : P f := by
  aesop

[Robin Carlier]

I am a bit confused, I was not asking how I could get aesop to prove customHomInduction, but rather how to tell aesop to use customCaseInduction as a cases rule in other goals for other lemmas once it’s proven. Are you telling me that this is in fact what aesop norm forward or aesop norm unfold achieves?

[Jannis Limperg]

Ah, I see. Registering custom eliminators as cases rules is currently not supported (unfortunately). But if you use the proposed Aesop rules, they should be equivalent to registering customHomInduction: for any hypothesis f : CustomHom x y, the rules will perform cases on x and y, then close the resulting subgoal for x = right and y = left, leaving you with the three cases that would have been generated by customHomInduction.

The only downside of this approach is that cases will also be run on any hypotheses x : CustomType that don't appear in a CustomHom hyp.

[Robin Carlier]

Given that I am fine with attribute [local aesop safe cases] CustomType, I’m okay with aesop callin cases on every x : CustomType in context, thanks!