function.update golf

Stream: new members

[Eric Wieser]

I'm wondering if I can golf the proof in #5091 any further. It feels like I should be one or two steps away from a refl or a congr, rather than having to go case-wise:

import data.equiv.basic

variables {α : Type*} [decidable_eq α]

lemma comp_swap_eq_update {β : Type*} (i j : α) (f : α → β) :
  f ∘ equiv.swap i j = function.update (function.update f j (f i)) i (f j) :=
funext $ λ x,
  if hi : x = i then
    by rw [function.comp_app, hi, equiv.swap_apply_left, function.update_same]
  else if hj : x = j then
    by rw [function.comp_app, hj, equiv.swap_apply_right, function.update_comm (hj ▸ hi : j ≠ i),
      function.update_same]
  else
    by rw [function.comp_app, equiv.swap_apply_of_ne_of_ne hi hj, function.update_noteq hi,
      function.update_noteq hj]

the function composition is somewhat irritating to work with too, as I end up with function.comp_app in every branch

[Reid Barton]

regarding the repeated function.comp_app, how about inserting a second line show f (equiv.swap i j x) = _, from

[Reid Barton]

It's probably cleaner to just use tactic mode from the start since the meat is all rws anyway

[Eric Wieser]

That didn't work, as it introduced a metavariable on the RHS that rw couldn't touch

[Eric Wieser]

It works if I fill out the _ by hand, but that's a big ugly

[Reid Barton]

lemma comp_swap_eq_update {β : Type*} (i j : α) (f : α → β) :
  f ∘ equiv.swap i j = function.update (function.update f j (f i)) i (f j) :=
begin
  ext x,
  rw function.comp_app,
  by_cases hi : x = i,
  { rw [hi, equiv.swap_apply_left, function.update_same] },
  { by_cases hj : x = j,
    { rw [hj, equiv.swap_apply_right, function.update_comm (hj ▸ hi : j ≠ i),
          function.update_same] },
    { rw [equiv.swap_apply_of_ne_of_ne hi hj, function.update_noteq hi,
          function.update_noteq hj] } }
end

[Reid Barton]

simp wizards will probably come up with something shorter

[Eric Wieser]

I can get it with split_ifs using:

lemma comp_swap_eq_update' {β : Type*} (i j : α) (f : α → β) :
  f ∘ equiv.swap i j = function.update (function.update f j (f i)) i (f j) :=
begin
  ext x,
  rw function.comp_apply,
  rw equiv.swap_apply_def,
  rw [function.update, function.update],
  split_ifs,
  rw eq_rec_constant,
  rw eq_rec_constant,
  refl,
end

although that introduces some nasty eq.recs

[Yakov Pechersky]

This is about as good as it can get because you don't have function application on the LHS but you do on the RHS. Also, equiv.swap or function.update doesn't have helpful lemmas for the cases where it isn't applied.

[Eric Wieser]

I think #5093 (which provides function.update f a' b a = if a = a' then b else f a) will make this a little less painful, and eliminate both the function.update unfolding and the eq_rec mess

[Damiano Testa]

I am writing as a complete outsider to this thread, so feel free to disregard my question!

I often face the issue of trying to "minimize" my proofs and I always run into the issue that I do not have a clear idea of what it is that I should minimize. Is there any guidance on what constitutes a "better" proof in this context?

[Johan Commelin]

I think speed is a very important factor. After that, it becomes a question of: how readable do I want my proof to be...

[Johan Commelin]

There only fit so many statements of trivial lemmas on 1 laptop screen. So if you are searching for a trivial lemma that you want to use, then you don't want lengthy proofs taking up screen real estate. Hence we golf those proofs like crazy.

[Johan Commelin]

But for "bigger results", I really don't care whether the proof is 25 lines or 30.

[Johan Commelin]

Then it's more a question: if this breaks, can a maintainer easily fix it? Or is it golfed so much, that they need to spend an hour reconstructing the proof.

[Yakov Pechersky]

I think proof minimization should first focus on combining branches and pruning dead-ends in the proof. That is, if there is something that splits into two or more goals, and then the same tactic step is in both subgoals, then perhaps there is a way to perform that step before the branching.

[Yakov Pechersky]

And also removing branching if it is unnecessary -- if there is a way to prove something without needing to do a case bash, then the tree-structure proof can be simplified into a linear sequence.

[Damiano Testa]

Johan Commelin said:

I think speed is a very important factor. After that, it becomes a question of: how readable do I want my proof to be...

Ok, how do you measure speed? The length of the term produced by show_term does not seem like a good metric...

[Damiano Testa]

(but is the only thing that I can think of...)

[Damiano Testa]

In the specific case at hand, here is a subtly different version of the lemma: is it any better?

lemma comp_swap_eq_update'_n {α : Type*} {β : Type*} (i j : α) (f : α → β) :
  f ∘ equiv.swap i j = function.update (function.update f j (f i)) i (f j) :=
begin
  ext x,
  rw [function.update, function.update],
  split_ifs with h k,
  { rw [eq_rec_constant, h],
    exact congr_arg f (equiv.swap_apply_left _ _), },
  { rw [eq_rec_constant, k],
    exact congr_arg f (equiv.swap_apply_right _ _), },
  { exact congr_arg f (equiv.swap_apply_of_ne_of_ne h k), },
end

[Johan Commelin]

@Damiano Testa set_option profiler true

[Damiano Testa]

Johan Commelin said:

Damiano Testa set_option profiler true

Ah!!! Thanks!! So then one should compare parsing?

[Johan Commelin]

no, just the total time

[Johan Commelin]

and the big time drops are where the most time is spent

[Yakov Pechersky]

Another lemma proof:

lemma comp_swap_eq_update' {β : Type*} (i j : α) (f : α → β) :
  f ∘ equiv.swap i j = function.update (function.update f j (f i)) i (f j) :=
begin
  ext,
  rw [function.comp_apply, equiv.swap_apply_def, function.update, function.update],
  split_ifs;
  rw eq_rec_constant <|> refl,
end

[Damiano Testa]

ok, elaboration of .... So my version is almost 40ms worst than the suggested one! Ahaha

[Damiano Testa]

Thank you! Not all is clear from the output of set_option profiler true but this does indeed satisfy my doubt about measuring "proof lengths"!