Grind Tactic : split/cases for non-inductive type

Stream: metaprogramming / tactics

[Dolores Haze]

Hello,

As I understand, the grind tactic can do case-splitting on inductive types like this

@[grind cases]
inductive IsEven : Nat → Prop
  | zero : IsEven 0
  | step : IsEven n → IsEven (n + 2)

/--
[grind.split] IsEven 5, generation: 0
[grind.split] IsEven n, generation: 1
-/
example (h : IsEven (n := n) 5) : False := by
  grind

Now, If I have a type that is not an inductive type, how can I guide the grind tactic to do case splitting? Say I have this:

def DefEven {n : Nat} : Nat → Prop := IsEven (n := n)

-- this fails as grind can't do case splitting for DefEven
example (h : DefEven (n := n) 5) : False := by
  grind

I understand that I can : 1) make the DefEven definition reducible, or 2) unfold it before running grind in my example. So, I'm wondering if there's another way to provide my own case splitting for grind?

The reason is, in my real use case, my type is defined to be a List, and I'm transferring many nice facts about List while I can still some modifications that suits my own application. However, I lose some nice properties so I was hoping I could find a hack were I provide nil/cons theorems for my custom type and still could benefit from grind.

[Aaron Liu]

you can make it an abbrev

[Dolores Haze]

Aaron Liu said:

you can make it an abbrev

Thanks. Yes I know about abbrev; that's why I mentioned in my original post that I can make the definition reduicible.

But My question is is there a way to not abbrev my type and instead manually guide the grind? (e.g., by providing theorems like DefEven.zero and DefEven.step ?

[Aaron Liu]

you can unfold DefEven at *

[Robin Arnez]

Well you can provide a lemma to the effect of case splitting like:

@[grind →]
theorem DefEven.unstep : DefEven (n + 2) → DefEven n
  | .step h => h

@[grind .]
theorem DefEven.no_one : ¬DefEven 1 := nofun

[Robin Arnez]

Now, my guess is that, in your real application, you should use a one-field structure instead:

@[grind cases]
structure StructEven (n : Nat) where
  ofIsEven ::
  toIsEven : IsEven n

[Robin Arnez]

or well, something like

@[grind cases]
structure MyCustomList where
  ofList :: toList : List Nat

[Dolores Haze]

Robin Arnez said:

Well you can provide a lemma to the effect of case splitting like:

Thank you. This is very close to what I was looking for.

or well, something like

I wasn't aware of the one-field structure. I have to learn more about this.

[Ka Wing Li]

I have a similar question: how to let grind unfold the le/lt instance?

structure Word where
  ofBitVec :: toBitVec : BitVec 64

namespace Word

instance : LE Word where
  le x y := x.toBitVec.toNat ≤ y.toBitVec.toFin

instance : LT Word where
  lt x y := x.toBitVec.toNat < y.toBitVec.toFin

instance : Preorder Word where
  le_refl x := by simp [instLE]
  le_trans x y z := by simp [instLE]; grind
  lt_iff_le_not_ge := by simp [instLE, instLT]; grind

end Word

[Ka Wing Li]

I seems have to unfold the instLE/instLT everywhere before applying grind.

[Aaron Liu]

write a le_def theorem and have grind use that

[Ka Wing Li]

You mean something like this

@[grind =]
theorem le_def {x y : Addr} : x ≤ y ↔ x.toBitVec.toNat ≤ y.toBitVec.toNat := by rfl

[Ka Wing Li]

Thanks! It works like a charm.