## Stream: new members

### Topic: dependent lift with quotient

#### Yakov Pechersky (Apr 14 2021 at 01:29):

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 (Apr 14 2021 at 01:30): Do I instead use quot.induction_on? #### Yury G. Kudryashov (Apr 14 2021 at 01:39): What's wrong with quot.lift_on? #### Yakov Pechersky (Apr 14 2021 at 01:42): 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 (Apr 14 2021 at 01:46): Could you please post an #mwe that others can copy+paste to make experiments? #### Yury G. Kudryashov (Apr 14 2021 at 01:47): It seems that docs#quot.lift_on is for non-dependent functions. #### Yury G. Kudryashov (Apr 14 2021 at 01:48): There is a docs#quotient.hrec_on' #### Yakov Pechersky (Apr 14 2021 at 01:51): 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 (Apr 14 2021 at 02:01):

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 (Apr 14 2021 at 02:07):

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 (May 07 2021 at 01:15):

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

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 (May 07 2021 at 01:16):

Do I have to use

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


#### Yakov Pechersky (May 07 2021 at 01:17):

And then define another function to extract it?

#### Yakov Pechersky (May 07 2021 at 01:18):

(no pprod.ext =C )

#### Yakov Pechersky (May 07 2021 at 01:25):

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

Last updated: May 12 2021 at 05:19 UTC