dependent lift with quotient

Stream: new members

[Yakov Pechersky]

What's the right way to have a dependent definition on a quotient? I have defined my own setoid on list which is whether two lists are rotations of one another:

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 := is_rotated.eqv }

so I can define a cycle via a quotient:

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

In fact, properties like nodup can be lifted into the quotient

lemma is_rotated.nodup_iff {l l' : list α} (h : l ~r l') : nodup l ↔ nodup l' :=
h.perm.nodup_iff

def nodup (s : cycle α) : Prop :=
quot.lift_on s nodup (λ l₁ l₂ (e : l₁ ~r l₂), propext $ e.nodup_iff)

I've also defined a cyclical permutation from the list, and shown that it is invariant to rotation

def form_perm : equiv.perm α :=
(zip_with equiv.swap l (l.rotate 1)).tail.prod

lemma form_perm_eq_of_is_rotated {l l' : list α} (hd : nodup l) (h : l ~r l') :
  form_perm l = form_perm l' :=
begin
  obtain ⟨n, rfl⟩ := h.def,
  exact (form_perm_rotate l hd n).symm
end

My question is, what's the right invocation to make this dependent definition:

def perm [decidable_eq α] : Π (s : cycle α) (h : nodup s), equiv.perm α :=
λ s, quot.lift_on s
  _ -- list α → s.nodup → equiv.perm α
  _ -- ∀ (a b : list α), setoid.r a b → ⁇ a = ⁇ b

[Yakov Pechersky]

Do I instead use quot.induction_on?

[Yury G. Kudryashov]

What's wrong with quot.lift_on?

[Yakov Pechersky]

I don't know how to unlift the provided cycle.nodup s to provide me list.nodup with the proof I supply for the last argument of lift_on

[Yury G. Kudryashov]

Could you please post an #mwe that others can copy+paste to make experiments?

[Yury G. Kudryashov]

It seems that docs#quot.lift_on is for non-dependent functions.

[Yury G. Kudryashov]

There is a docs#quotient.hrec_on'

[Yakov Pechersky]

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

variables {α : Type*}

namespace list

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.perm {l l' : list α} (h : l ~r l') : l ~ l' :=
exists.elim h (λ _ hl, hl ▸ (rotate_perm _ _).symm)

lemma is_rotated.nodup_iff {l l' : list α} (h : l ~r l') : nodup l ↔ nodup l' :=
h.perm.nodup_iff

def form_perm [decidable_eq α] (l : list α) : equiv.perm α :=
(zip_with equiv.swap l (l.rotate 1)).tail.prod

lemma form_perm_eq_of_is_rotated [decidable_eq α] {l l' : list α} (hd : nodup l) (h : l ~r l') :
  form_perm l = form_perm l' := sorry

end list

open list

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

namespace cycle

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

def nodup (s : cycle α) : Prop :=
quot.lift_on s nodup (λ l₁ l₂ (e : l₁ ~r l₂), propext $ e.nodup_iff)

def perm [decidable_eq α] : Π (s : cycle α) (h : nodup s), equiv.perm α :=
λ s, quot.lift_on s
  (λ l (h : nodup s), form_perm l)
  (λ l₁ l₂ (e : l₁ ~ l₂), by { ext1 (hd : nodup s), simp only, sorry })

def perm' [decidable_eq α] : Π (s : cycle α) (h : nodup s), equiv.perm α :=
λ s, quot.rec_on s
  (λ l (h : nodup _), form_perm l)
  (λ l₁ l₂ h, by { ext1 hd, sorry })

end cycle

[Yakov Pechersky]

hrec leads to a heq I'm not sure how to discharge:

def perm' [decidable_eq α] : Π (s : cycle α) (h : nodup s), equiv.perm α :=
λ s, quot.hrec_on s (λ l h, form_perm l)
  (λ l₁ l₂ h, by {  })

[Yakov Pechersky]

Thank you Yury! Here's my solution:

def perm [decidable_eq α] : Π (s : cycle α) (h : nodup s), equiv.perm α :=
λ s, quot.hrec_on s (λ l h, form_perm l)
  (λ l₁ l₂ (h : l₁ ~r l₂), by {
    ext,
    { exact is_rotated.nodup_iff h },
    { intros h1 h2 he,
      refine heq_of_eq _,
      rw form_perm_eq_of_is_rotated _ h,
      exact h1 } })

[Yakov Pechersky]

Another quotient problem: what about defining a dependent product on a multiset if I know that the multiplication is commutative within the multiset?

import data.finset.fold

variables {α : Type*} [monoid α]

namespace multiset

@[to_additive]
def noncomm_prod' : Π (s : multiset α) (comm : ∀ ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s), commute x y),
  α :=
λ s, quotient.hrec_on s (λ l h, l.prod) -- how do I build the output to encode `h` as well?
(λ l l' (h : l ~ l'),
  begin
    ext,
    { refine forall_congr (λ x, _),
      refine imp_congr h.mem_iff _,
      refine forall_congr (λ y, _),
      exact imp_congr h.mem_iff iff.rfl },
    { rintros - - -,
      rw heq_iff_eq,
      refine h.prod_eq' _,
      sorry -- no access to `h` here
    },
  end)

end multiset

[Yakov Pechersky]

Do I have to use

  pprod (∀ ⦃x⦄ (hx : x ∈ s) ⦃y⦄ (hy : y ∈ s), commute x y) α :=

[Yakov Pechersky]

And then define another function to extract it?

[Yakov Pechersky]

(no pprod.ext =C )

[Yakov Pechersky]

Oh I guess I threw away the info, didn't need the pprod