## Stream: new members

### Topic: Working with equiv.swap

#### 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.

mwe?

#### 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


#### 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

#### Mario Carneiro (Dec 06 2020 at 16:48):

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

#### Mario Carneiro (Dec 06 2020 at 16:48):

people will thank you later

#### 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

#### 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.

#### 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

#### 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:

#### 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"

#### 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.

#### 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

#### 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

#### Mario Carneiro (Dec 06 2020 at 17:50):

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

#### Mario Carneiro (Dec 06 2020 at 17:51):

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

#### Eric Wieser (Dec 06 2020 at 18:12):

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

#### 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?

#### 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