# Zulip Chat Archive

## Stream: new members

### Topic: Lean not recognising extensions implicitly

#### 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?

#### 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
```

#### 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
```

#### 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