Using `aesop` to perform cases on a non-inductive type

Stream: lean4

[Anand Rao]

As I understand it, aesop uses the cases rule builder to perform proofs by cases on inductive types, which can be further calibrated using the patterns option. Is there currently a way to perform cases on type that is not an inductive type, or will there be support for this in the future?

For context, I am currently dealing with the type Fin 2 × Fin 2, which I would like aesop to learn to split into the four cases (0, 0), (0, 1), (1, 0) and (1, 1).

[Jannis Limperg]

Maybe something roughly like this will work:

@[aesop safe forward]
theorem fin2_split : (x : Fin 2 x Fin 2) -> x = (0, 0) \or x = (0, 1) \or x = (1, 0) \or x = (1, 1)

Then Aesop should split the new hyp into the four cases and substitute the equations.

If this doesn't work, I may need to implement general elimination rules after all...

[Anand Rao]

Thanks a lot for the suggestion! It seems to work perfectly on the test example below. It is failing for the use case that I have in mind, but I think that is only because of my overall configuration of parameters - the error message suggests that the case splitting has already occurred and the error is elsewhere downstream. I do not need this feature crucially in my code, it is just to trim a couple of lines of case matching and delegate the entire proof to aesop. I think that with some experimentation I should be able to get it to work for my main code as it did for the test example.

import Aesop
import Mathlib.Data.Fin.Basic
import Mathlib.Algebra.Group.Prod

declare_aesop_rule_sets [Q]

/-- The Klein Four group. -/
@[aesop safe (rule_sets [Q])]
abbrev Q := Fin 2 × Fin 2

instance : AddCommGroup Q := inferInstance

namespace Q

/-! The elements of the Klein Four group `Q`. -/

/-- The identity element of `Q`. -/
@[aesop norm unfold (rule_sets [Q]), match_pattern]
abbrev e : Q := (⟨0, by decide⟩, ⟨0, by decide⟩)
/-- The first generator of `Q`. -/
@[aesop norm unfold (rule_sets [Q]), match_pattern]
abbrev a : Q := (⟨1, by decide⟩, ⟨0, by decide⟩)
/-- The second generator of `Q`. -/
@[aesop norm unfold (rule_sets [Q]), match_pattern]
abbrev b : Q := (⟨0, by decide⟩, ⟨1, by decide⟩)
/-- The product of the generators of `Q`. -/
@[aesop norm unfold (rule_sets [Q]), match_pattern]
abbrev c : Q := (⟨1, by decide⟩, ⟨1, by decide⟩)

@[aesop safe forward (rule_sets [Q])]
theorem split : ∀ q : Q, q = .e ∨ q = .a ∨ q = .b ∨ q = .c
  | .e | .a | .b | .c => by aesop

end Q

example : ∀ q : Q, q + q = Q.e := by aesop (rule_sets [Q])