decidable surjectivity over fintypes

Stream: new members

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

I'd like to avoid using classical because the idea is to prove things about explicit playfields using dec_trivial.

[Anne Baanen]

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]

Ah, makes sense!

[Anne Baanen]

I don't think there is a smarter generic decision algorithm than "enumerate y : Y, enumerate x : X, iff x = y continue with next y".

[Yakov Pechersky]

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