Working with `equiv.swap`

Stream: new members

[Eric Wieser]

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.

[Mario Carneiro]

mwe?

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

people will thank you later

[Mario Carneiro]

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]

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]

Kevin Buzzard said:

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

depends on the computer scientist

[Marc Huisinga]

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]

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]

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

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]

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]

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

[Mario Carneiro]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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