Zulip Chat Archive

Stream: new members

Topic: dependent lift with quotient


view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Apr 14 2021 at 01:30):

Do I instead use quot.induction_on?

view this post on Zulip Yury G. Kudryashov (Apr 14 2021 at 01:39):

What's wrong with quot.lift_on?

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Apr 14 2021 at 01:46):

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

view this post on Zulip Yury G. Kudryashov (Apr 14 2021 at 01:47):

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

view this post on Zulip Yury G. Kudryashov (Apr 14 2021 at 01:48):

There is a docs#quotient.hrec_on'

view this post on Zulip 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

view this post on Zulip 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 {  })

view this post on Zulip 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 } })

view this post on Zulip 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

@[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

view this post on Zulip 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) α :=

view this post on Zulip Yakov Pechersky (May 07 2021 at 01:17):

And then define another function to extract it?

view this post on Zulip Yakov Pechersky (May 07 2021 at 01:18):

(no pprod.ext =C )

view this post on Zulip 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