Zulip Chat Archive

Stream: new members

Topic: Working with `equiv.swap`


view this post on Zulip Eric Wieser (Dec 06 2020 at 12:56):

This seemingly trivial statement is proving painful for me to prove:

@[simp] lemma sum_congr_swap_left {α β : Type*} [decidable_eq α] [decidable_eq β] (i j : α) :
  equiv.sum_congr (equiv.swap i j) (1 : equiv.perm β) = equiv.swap (sum.inl i) (sum.inl j) :=
begin
  by_cases h : i = j,
  { simp [h, swap_self _], erw [sum_congr_refl], },
  ext,
  simp [sum_congr_apply],
  cases x,
  { simp,
    rw swap_eq_update,
    rw swap_eq_update,
    rw function.update_comm (ne.symm h),
    revert x,
    rw function.funext_iff,
    rw function.update_comp_eq_of_injective' _ (sum.injective_inl),
    rw function.update_comp_eq_of_injective' _ (sum.injective_inl),
    simp,
    sorry,  -- help!
    -- not sure where these come from
    apply_instance, apply_instance },
  { simp,
    rw swap_eq_update,
    revert x,
    rw function.funext_iff,
    rw function.update_comp_eq_of_not_mem_range',
    rw function.update_comp_eq_of_not_mem_range',
    { refl },
    { simp },
    { simp }, },
end

I could probably get there by completely unfolding swap to ites and case-bashing, but I thought I ought to try and "use the API". Have I missed a crucial piece of the API?

It doesn't help here that I have to juggle the 1 and refl spellings of the identity permutation.

view this post on Zulip Mario Carneiro (Dec 06 2020 at 14:49):

mwe?

view this post on Zulip Mario Carneiro (Dec 06 2020 at 14:59):

There is an unavoidable bit of case bashing, because I don't think we have any theorem about what swap (f x) (f y) does for general injections f, but otherwise it's not too bad:

import data.equiv.basic

namespace equiv

@[simp] lemma sum_congr_swap_left {α β : Type*} [decidable_eq α] [decidable_eq β] (i j : α) :
  equiv.sum_congr (equiv.swap i j) (1 : equiv.perm β) = equiv.swap (sum.inl i) (sum.inl j) :=
begin
  refine (mul_left_inj (equiv.swap (sum.inl i) (sum.inl j))).1 _,
  rw swap_mul_self,
  apply equiv.ext, rintro (x|x); simp [sum.map],
  { simp [swap_apply_def]; split_ifs; simp [sum.map, *, swap_apply_of_ne_of_ne] },
  { simp [swap_apply_of_ne_of_ne] },
end

end equiv

view this post on Zulip Eric Wieser (Dec 06 2020 at 16:07):

I guess this is a symptom of a more general issue I have, where I want lemmas to exist to "swap" or "commute" f and g in some way (to push terms together that match other lemmas), but there are sometimes O(n²) of those pairs so inevitably many aren't in mathlib

view this post on Zulip Mario Carneiro (Dec 06 2020 at 16:48):

My approach to API design is to do the full O(n^2)

view this post on Zulip Mario Carneiro (Dec 06 2020 at 16:48):

people will thank you later

view this post on Zulip Mario Carneiro (Dec 06 2020 at 16:49):

but it does explain why I often try to discourage unnecessary new definitions, because they come with significant overhead in terms of API surface area

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 17:08):

O(n^2) might sound scary to a computer scientist, but they are typically thinking of n=10,000. When n=4, O(n^2) is something which you might want to just bite the bullet and do.

view this post on Zulip Marc Huisinga (Dec 06 2020 at 17:08):

Kevin Buzzard said:

O(n^2) might sound scary to a computer scientist

depends on the computer scientist

view this post on Zulip Marc Huisinga (Dec 06 2020 at 17:09):

it sounds scary to algorithm researchers. cryptography people will be satisfied with it being polynomial, and ITP researchers will be delighted to hear that there's a decision algorithm :grinning_face_with_smiling_eyes:

view this post on Zulip Kevin Buzzard (Dec 06 2020 at 17:10):

My model of a computer scientist is based on my son, who is 18 and does these informatics olympiad problems where often the question is "here's a problem with an obvious O(n^2) algorithm; here are 10,000 pieces of data. Now go find the O(n log n) algorithm"

view this post on Zulip Marc Huisinga (Dec 06 2020 at 17:17):

"algorithm engineering" is a pretty prominent topic here, where time complexity isn't good enough, it also needs to perform good in practice!
i guess they might be happy with O(n^2) if it's fast on the problem sets they care about.

view this post on Zulip Julian Berman (Dec 06 2020 at 17:41):

Kevin Buzzard said:

My model of a computer scientist is based on my son, who is 18 and does these informatics olympiad problems where often the question is "here's a problem with an obvious O(n^2) algorithm; here are 10,000 pieces of data. Now go find the O(n log n) algorithm"

this sounds also like the "programming job interview" model of algorithmic complexity and optimization

view this post on Zulip Mario Carneiro (Dec 06 2020 at 17:48):

In reality it's less than O(n^2) because the network of connections between mathematical concepts is not the complete graph, and is probably on the sparse end of the spectrum

view this post on Zulip Mario Carneiro (Dec 06 2020 at 17:50):

What is the edge density of graphs like social networks? It's probably somewhere around that

view this post on Zulip Mario Carneiro (Dec 06 2020 at 17:51):

For example, how does list.modify_nth commute with T1_space?

view this post on Zulip Eric Wieser (Dec 06 2020 at 18:12):

Does lean give us for free how function composition commutes with recursors for inductive types?

view this post on Zulip Eric Wieser (Dec 06 2020 at 18:14):

Eg, f ° sum.rec g h = sum.rec f°g f°h, but for all inductive types?

view this post on Zulip Eric Wieser (Dec 06 2020 at 21:59):

#5260 makes a start on some of the missing n² lemmas


Last updated: May 15 2021 at 00:39 UTC