Zulip Chat Archive

Stream: new members

Topic: Lean not recognising extensions implicitly


view this post on Zulip Pim Spelier (Jul 23 2020 at 10:31):

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?

view this post on Zulip Anne Baanen (Jul 23 2020 at 10:49):

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

view this post on Zulip Anne Baanen (Jul 23 2020 at 10:51):

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

view this post on Zulip Pim Spelier (Jul 23 2020 at 11:14):

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!


Last updated: May 16 2021 at 20:13 UTC