Combining instances

Stream: general

[Newell Jensen]

Suppose I have

import Mathlib.Tactic

open List

def isPrefixSublist [DecidableEq α] (s t : List α) := s <+: t ∧ s <+ t

#eval isPrefixSublist [1,3] [1,3,1,3,4] -- failed to synthesize Decidable (isPrefixSublist [1, 3] [1, 3, 1, 3, 4])

In general, a sublist is not necessarily a prefix of a list but every prefix is a sublist of a list.

Now, both prefix and sublist have Decidable instance definitions and I am wondering if there is a simpler way to combine this in some manner rather than having to define an entierly new Decidable instance that combines them for the definition given above?

[Yakov Pechersky]

I think using abbrev instead of def would work.

[Newell Jensen]

Ah, indeed it does. Thanks. Will go and read up on abbrev

[Adomas Baliuka]

@Newell Jensen Did you find where to read up on that? I've been struggling to find documentation on the exact behaviour of these keywords.

[Newell Jensen]

@ab The best documentation I found, which doesn't really go into the inner workings of why abbrev works here and its differences with def, was in the lean 4 functional programming manual. Hence my understanding of this is still lacking as I haven't taken the time to try and dig through the code.

[Kyle Miller]

abbrev makes a definition "reducible" (vs the default "semireducible"), which means that various processes in Lean are willing to unfold it automatically, for example typeclass inference or simp.

[Shreyas Srinivas]

Newell Jensen said:

ab The best documentation I found, which doesn't really go into the inner workings of why abbrev works here and its differences with def, was in the lean 4 functional programming manual. Hence my understanding of this is still lacking as I haven't taken the time to try and dig through the code.

abbrev something := something else is equivalent to @[reducible] def something := something else.

[Shreyas Srinivas]

You usually want to have some control over whether certain definitions unfold or not when you apply certain tactics.

[Kyle Miller]

@Newell Jensen By the way, here's how I'd probably set this up:

def isPrefixSublist (s t : List α) := s <+: t ∧ s <+ t

instance [DecidableEq α] (s t : List α) : Decidable (isPrefixSublist s t) :=
  inferInstanceAs <| Decidable (_ ∧ _)

#eval isPrefixSublist [1,3] [1,3,1,3,4]
-- true

This inferInstanceAs is convenient for unfolding definitions. I'm using a trick that _ ∧ _ causes Lean to unfold isPrefixSublist, and then typeclass search can find the decidable instances for everything involved.

[Newell Jensen]

Thanks @Shreyas Srinivas and @Kyle Miller

@Kyle Miller are there any advantages of doing it the way you showed versus just using abbrev or just two different ways to do the same thing? Curious if there are any pros/cons for the different approaches.

[Kyle Miller]

I think a good rule of thumb is that in an abbrev each argument should appear at most once in the body. There are some exceptions I believe like type arguments or instance arguments. The problem is that abbrev can cause exponential blowup if you're not paying attention. For example if you have

abbrev ohno (n : Nat) : Nat := n + n + n + n

then ohno (ohno (ohno (onno n))) is already 256 copies of n added together.

[Kyle Miller]

If you define your own instance with a plain def then you don't have to worry about this (but you did need to spend a little of your own time to define an instance).

[Newell Jensen]

@Kyle Miller understood. Thanks for the clarification and example.