inverse of quotient.mk

Stream: general

[Yakov Pechersky]

Is there a function that, given a term of a quotient type, gives the (fin)set of all the terms of the parent type that could have produced it? For example, something like

import data.finset.basic
import data.list.perm

open list

-- `decidable_eq α` is needed because proving `nodup l.permutations` is hard
example {α : Type*} [decidable_eq α] : multiset α → finset (list α) :=
λ s, quotient.lift_on s (λ l, l.permutations.to_finset)
(λ l l' (h : l ~ l'),
  begin
    ext sl,
    simp only [mem_permutations, mem_to_finset],
    exact ⟨λ hs, hs.trans h, λ hs, hs.trans h.symm⟩
  end)

[Eric Rodriguez]

isn't that just quotient.mk ⁻¹' {x}?

[Yakov Pechersky]

Is that computable?

[Eric Rodriguez]

i mean lean lets me write it as a def without jamming noncomputable on it, but I guess it probably strongly depends on your setoid instance

[Yakov Pechersky]

quotient.mk ⁻¹' {x} is really a Prop. That's why it doesn't complain about computability. And given that set (list nat) is an uncountable type, I can't imagine a nice decision procedure that will evaluate it. For some fixed x, yes, that set is finite. But set.finite.to_finset _is_ noncomputable:

import data.finset.sort
import data.list.perm
import data.set.finite

open list

variables {α : Type*} [decidable_eq α]

-- `decidable_eq α` is needed because proving `nodup l.permutations` is hard
def quotient.inv : multiset α → finset (list α) :=
λ s, quotient.lift_on s (λ l, l.permutations.to_finset)
(λ l l' (h : l ~ l'),
  begin
    ext sl,
    simp only [mem_permutations, mem_to_finset],
    exact ⟨λ hs, hs.trans h, λ hs, hs.trans h.symm⟩
  end)

#check set.finite.to_finset

#eval (quotient.inv ({1, 2, 3} : finset ℕ).val)
/-
{[1, 2, 3], [1, 3, 2], [2, 1, 3], [2, 3, 1], [3, 1, 2], [3, 2, 1]}
-/


#eval quotient.mk ⁻¹' ({({1, 2, 3} : finset ℕ).val} : set (multiset ℕ))
/-
cannot evaluate function: 0 arguments given but expected 1
-/