Lean not recognising extensions implicitly

Stream: new members

[Pim Spelier]

Hi,
I'm working together with Daan van Gent on defining problems, in the computability sense (for example, SAT or 3-colorability, or somewhat simpler, is_even).
We came up with the definition

import computability.primrec
import computability.reduce
open function

namespace problem

structure problem (α : Type*) extends primcodable α :=
(yesinstance : α → Prop)

(I.e., we have a type \alpha that should be nicely encodable into the natural numbers (that's what primcodable means), and for each a : \alpha we have yesinstance a which says a is a yes-instance.)

Then we wanted to define reductions between problems, using computable, and we tried

def many_one_reducible {α β : Type*} (P : problem α) (Q : problem β) :=
∃ f : α → β, computable f ∧ ∀ a, P.yesinstance a ↔ Q.yesinstance (f a)

but this fails: computable needs that \alpha and \beta are of the class primcodable, but it can't synthesize the primcodable type class instance on \alpha and \beta, even though problem extends primcodable.

We have the possible fix

def many_one_reducible {α β : Type*} (P : problem α) (Q : problem β) :=
∃ f : α → β, @computable α β P.to_primcodable Q.to_primcodable f ∧ ∀ a, P.yesinstance a ↔ Q.yesinstance (f a)

but this seems a bit ugly; shouldn't lean already know how P and Q are primcodable? Or if not, how should we tell Lean?

[Anne Baanen]

The issue is that the typeclass system doesn't know about your arguments P and Q. If you make problem a class and P and Q typeclass arguments, it will work (but not look as nice perhaps):

import computability.primrec
import computability.reduce
open function

class problem (α : Type*) extends primcodable α :=
(yesinstance : α → Prop)

namespace problem

def many_one_reducible {α : Type*} {β : Type*} [problem α] [problem β] :=
∃ f : α → β, computable f ∧ ∀ a, yesinstance a ↔ yesinstance (f a)

end problem

[Anne Baanen]

The alternative is to change the extends primcodable into a typeclass argument to your structure:

import computability.primrec
import computability.reduce
open function

namespace problem

structure problem (α : Type*) [primcodable α] :=
(yesinstance : α → Prop)

def many_one_reducible {α β : Type*} [primcodable α] [primcodable β] (P : problem α) (Q : problem β) :=
∃ f : α → β, computable f ∧ ∀ a, P.yesinstance a ↔ Q.yesinstance (f a)

end problem

[Pim Spelier]

Ah, that makes sense!
We were already wondering whether class or structure fits best: we chose structure, as there can be many different problem structures on the same type, so we explicitly don't want typeclass inference. So I think we'll go for the second solution, thanks!