lifting into quotient

Stream: new members

[Yakov Pechersky]

I'm trying to learn more about how to lift definitions into quotients. I've proved that if two lists are equivalent up to rotation, then so are their inverses. How can I use this to define a reverse for my cycle, which is the quotient of a list by rotation?

import data.list.rotate
import data.list.erase_dup
import group_theory.perm.basic
import data.finset.basic

variables {α : Type*}

namespace list

lemma reverse_rotate (l : list α) (n : ℕ) :
  (l.rotate n).reverse = l.reverse.rotate (l.length - (n % l.length)) :=
begin
  rw [←length_reverse l, ←rotate_eq_iff],
  induction n with n hn generalizing l,
  { simp },
  { cases l with hd tl,
    { simp },
    { rw [rotate_cons_succ, nat.succ_eq_add_one, ←rotate_rotate, hn],
      simp [rotate_cons_succ] } }
end

def is_rotated (l l' : list α) : Prop := ∃ n, l.rotate n = l'

infixr ` ~r `:1000 := is_rotated

def is_rotated.setoid : setoid (list α) :=
{ r := is_rotated, iseqv := sorry }

lemma is_rotated.reverse {l l' : list α} (h : l ~r l') : l.reverse ~r l'.reverse :=
begin
  rw is_rotated_iff at h ⊢,
  obtain ⟨n, rfl⟩ := h,
  exact ⟨_, (reverse_rotate _ _).symm⟩
end

end list

open list

def cycle (α : Type*) : Type* := quotient (@is_rotated.setoid α)

namespace cycle

instance : has_coe (list α) (cycle α) := ⟨quot.mk _⟩

def reverse (s : cycle α) : cycle α :=
sorry

end cycle

[Kevin Buzzard]

docs#quotient.map maybe?

[Kevin Buzzard]

Or docs#quotient.map' if you're not using setoid as a typeclass

[Yakov Pechersky]

Amazing, thank you!

[Kevin Buzzard]

You can thank @Bhavik Mehta who told me about this trick when I was writing my class on quotients last month :-)

[Yakov Pechersky]

Is there a reason to use the primed quotient methods over the underlying quot methods?

[Kevin Buzzard]

The primed methods attempt to find the setoids using the {} system, and the unprimed ones attempt to find it using the [] system. In your example you didn't make the setoids an instance so the unprimed methods might not work.

[Kevin Buzzard]

I think those systems have got fancier names but I forgot them. Oh [] is type class inference system.

[Kevin Buzzard]

{} is unification

[Yakov Pechersky]

Right, that's the difference between quotient.map and quotient.map'. But quotient.map' is just quot.map. So why not just use quot.map?

[Yakov Pechersky]

Someone remarked at some point about the philosophical difference in the purpose between quot and quotient and I guess that's what I'm wondering about here too.

[Adam Topaz]

They're defeq, but if you have a stetoid, you may as well use the quotient API in case you run into docs#quotient.exact which is better than docs#quot.exact