# Zulip Chat Archive

## Stream: new members

### Topic: decidable surjectivity over fintypes

#### Yakov Pechersky (Sep 22 2020 at 18:46):

I'm trying to get decidable surjectivity to work, over fintypes with provided `decidable_eq`

instances. I think I am misunderstanding something about how decidability is inferred. Here is mwe.

```
import data.fintype.basic
variables {m n : Type}
variables {ι : Type}
def playfield (X Y : Type) (R : Type) : Type* := X × Y → option R
instance : has_mem ι (playfield m n ι) :=
⟨λ ix p, ∃! pos, p pos = some ix⟩
namespace playfield
variables (M : playfield m n ι)
variables [decidable_eq m] [decidable_eq n]
variables [decidable_eq ι]
def occupied_positions' : Type :=
{pos // (M pos).is_some}
example : decidable_eq M.occupied_positions' := by apply_instance
instance coe_occ_t : has_coe_t M.occupied_positions' (m × n) := ⟨subtype.val⟩
def occupied_positions : Type :=
{pos : M.occupied_positions' // option.get pos.property ∈ M}
example : decidable_eq M.occupied_positions' := by apply_instance
instance coe_occ_trans : has_coe M.occupied_positions M.occupied_positions' := ⟨λ pos, pos.val⟩
variables (pos pos' : M.occupied_positions)
def index_at := option.get pos.val.property
example (ix : ι) : decidable (M.index_at pos = ix) := by apply_instance
example : decidable (function.surjective M.index_at) := by { sorry }
end playfield
```

#### Yakov Pechersky (Sep 22 2020 at 18:46):

I'm not sure how to make the definitions work for the sorry at the end.

#### Yakov Pechersky (Sep 22 2020 at 18:47):

Relatedly, if anyone has suggestions for how to avoid the double subtype here, that'd be great too.

#### Yakov Pechersky (Sep 22 2020 at 18:48):

I'd like to avoid using `classical`

because the idea is to prove things about explicit `playfield`

s using `dec_trivial`

.

#### Anne Baanen (Sep 22 2020 at 19:17):

I think you're missing some `fintype`

instances:

```
example : decidable (function.surjective M.index_at) := fintype.decidable_surjective_fintype _
/-
failed to synthesize type class instance for
m n ι : Type,
M : playfield m n ι,
_inst_1 : decidable_eq m,
_inst_2 : decidable_eq n,
_inst_3 : decidable_eq ι
⊢ fintype ι
failed to synthesize type class instance for
m n ι : Type,
M : playfield m n ι,
_inst_1 : decidable_eq m,
_inst_2 : decidable_eq n,
_inst_3 : decidable_eq ι
⊢ fintype M.occupied_positions
-/
```

#### Yakov Pechersky (Sep 22 2020 at 19:19):

Ah, makes sense!

#### Anne Baanen (Sep 22 2020 at 19:19):

I don't think there is a smarter generic decision algorithm than "enumerate `y : Y`

, enumerate `x : X`

, if`f x = y`

continue with next `y`

".

#### Yakov Pechersky (Sep 22 2020 at 19:21):

OK, so this will preclude me from using infinite boards. That's alright for now.

Last updated: May 11 2021 at 00:31 UTC