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 playfields 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, iff 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: Dec 20 2023 at 11:08 UTC