Zulip Chat Archive

Stream: new members

Topic: function.update golf


Eric Wieser (Nov 23 2020 at 12:33):

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 (Nov 23 2020 at 12:59):

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

Reid Barton (Nov 23 2020 at 13:00):

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

Eric Wieser (Nov 23 2020 at 13:02):

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

Eric Wieser (Nov 23 2020 at 13:02):

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

Reid Barton (Nov 23 2020 at 13:03):

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 (Nov 23 2020 at 13:09):

simp wizards will probably come up with something shorter

Eric Wieser (Nov 23 2020 at 13:37):

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 (Nov 23 2020 at 14:26):

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 (Nov 23 2020 at 14:28):

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 (Nov 23 2020 at 14:35):

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 (Nov 23 2020 at 14:42):

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 (Nov 23 2020 at 14:43):

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 (Nov 23 2020 at 14:43):

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

Johan Commelin (Nov 23 2020 at 14:44):

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 (Nov 23 2020 at 14:47):

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 (Nov 23 2020 at 14:48):

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 (Nov 23 2020 at 14:49):

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 (Nov 23 2020 at 14:49):

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

Damiano Testa (Nov 23 2020 at 14:50):

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 (Nov 23 2020 at 14:50):

@Damiano Testa set_option profiler true

Damiano Testa (Nov 23 2020 at 14:51):

Johan Commelin said:

Damiano Testa set_option profiler true

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

Johan Commelin (Nov 23 2020 at 14:55):

no, just the total time

Johan Commelin (Nov 23 2020 at 14:55):

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

Yakov Pechersky (Nov 23 2020 at 14:56):

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 (Nov 23 2020 at 14:56):

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

Damiano Testa (Nov 23 2020 at 15:03):

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


Last updated: Dec 20 2023 at 11:08 UTC