Zulip Chat Archive

Stream: general

Topic: squeeze_simp times out

Sebastien Gouezel (Jun 17 2020 at 12:31):

I just encountered a strange behavior while working on a cleanup of manifolds. I have a proof with simp that succeeds, but takes a little bit long. So I replaced the simp with squeeze_simp, but squeeze_simp times out. I have no MWE for this, the code looks like

/-- Smooth manifold structure on the total space of a basic smooth bundle -/
instance to_smooth_manifold :
  smooth_manifold_with_corners (I.prod (model_with_corners_self 𝕜 F))
  Z.to_topological_fiber_bundle_core.total_space :=
  /- We have to check that the charts belong to the smooth groupoid, i.e., they are smooth on their
  source, and their inverses are smooth on the target. Since both objects are of the same kind, it
  suffices to prove the first statement in A below, and then glue back the pieces at the end. -/
  let J := model_with_corners.to_local_equiv (I.prod (model_with_corners_self 𝕜 F)),
  have A :  (e e' : local_homeomorph M H) (he : e  atlas H M) (he' : e'  atlas H M),
    times_cont_diff_on 𝕜 
    (J  ((Z.chart he).symm.trans (Z.chart he'))  J.symm)
    (J.symm ⁻¹' ((Z.chart he).symm.trans (Z.chart he')).source  range J),
  { assume e e' he he',
    have : J.symm ⁻¹' ((chart Z he).symm.trans (chart Z he')).source  range J =
      (I.symm ⁻¹' (e.symm.trans e').source  range I).prod univ,
    { ext p,
      squeeze_simp [-mem_range, J, chart, model_with_corners.prod],
      sorry },

Is there a way to investigate what is going on?

Sebastien Gouezel (Jun 17 2020 at 12:36):

Update: I just needed to be more patient to get the result of squeeze_simp, which is

Try this: simp only [J, chart, model_with_corners.prod, local_homeomorph.prod_to_local_equiv, local_equiv.trans_source,
 topological_fiber_bundle_core.local_triv_fst, local_homeomorph.coe_coe_symm, mem_inter_eq, and_true,
 local_equiv.prod_symm, local_homeomorph.coe_coe, id.def, mem_univ, local_equiv.coe_mk,
 local_homeomorph.trans_to_local_equiv, mem_prod, local_equiv.prod_coe, local_equiv.refl_target,
 topological_fiber_bundle_core.mem_local_triv_target, mem_preimage, topological_fiber_bundle_core.mem_local_triv_source,
 local_equiv.symm_source, local_homeomorph.symm_to_local_equiv, local_equiv.trans_target,
 local_homeomorph.refl_local_equiv, base_set, local_equiv.refl_source, and_self, local_equiv.prod_source,
 model_with_corners_self_coe, local_equiv.coe_trans_symm, local_equiv.coe_symm_mk, local_equiv.prod_target,

With simp, the proof takes 8s. With squeeze_simp, it takes 87s (yes, eighty-seven seconds!!!)

Sebastien Gouezel (Jun 17 2020 at 12:37):

And after pasting the output of squeeze_simp, it goes down to less than one second.

Kevin Buzzard (Jun 17 2020 at 12:41):

So I hope you run this code more than about ten times, then you are getting your money's worth

Jalex Stark (Jun 17 2020 at 12:42):

maybe part of your response should be to write more simp lemmas? there might be nontrivial things that get "proven" multiple times during the simp run

Sebastien Gouezel (Jun 17 2020 at 12:43):

The output of simp only is so ugly that I wouldn't want to see this in a (user-editable) file.

Sebastien Gouezel (Jun 17 2020 at 12:43):

Writing more simp lemmas wouldn't be a solution: simp lemmas that can be deduced from other simp lemmas are redundant (we have a linter to warn about them) and only make the search space bigger.

Patrick Massot (Jun 17 2020 at 12:44):

There is something special here. Sébastien's manifold theory is simp-heavy in a way that no other area of mathlib ever heard of. It comes from using very bundled stuff that would be impossible to steer without simp.

Patrick Massot (Jun 17 2020 at 12:44):

And by very bundled I really mean towers of very bundled things.

Jalex Stark (Jun 17 2020 at 12:46):

maybe you can get some mileage out of specialized simp sets? like
meta def manifold_simp := `[simp only [...]]

Patrick Massot (Jun 17 2020 at 12:47):

This could be true (using simp attributes).

Reid Barton (Jun 17 2020 at 12:58):

Does the order of lemmas passed to simp mean anything? Or does the order of lemmas produced by squeeze_simp mean anything?

Simon Hudon (Jun 17 2020 at 13:01):

The order doesn't matter because the simp lemmas are kept in head-indexed tables

Gabriel Ebner (Jun 17 2020 at 13:01):

The order matters very much because for each head symbol, the simp lemmas are stored in a list.

Simon Hudon (Jun 17 2020 at 13:02):

The situation is that squeeze_simp runs simp many times. It tries one set of simp lemmas and it checks if each one in the list is necessary by removing one at a time

Simon Hudon (Jun 17 2020 at 13:02):

@Gabriel Ebner thanks for the correction

Simon Hudon (Jun 17 2020 at 13:02):

squeeze_simp does not consider this

Jalex Stark (Jun 17 2020 at 13:07):

so a successful squeeze_simp runs quadratically in the number of lemmas it outputs, and it provides the guarantee that this set is minimal?

Sebastien Gouezel (Jun 17 2020 at 13:08):

Jalex Stark said:

maybe you can get some mileage out of specialized simp sets? like
meta def manifold_simp := `[simp only [...]]

The problem is that these lemmas typically interact with standard lemmas that are not specific to manifolds. For instance, lemmas on products, or and_self.

Gabriel Ebner (Jun 17 2020 at 13:08):

Simon Hudon said:

squeeze_simp does not consider this

Filed as #3097.

Jalex Stark (Jun 17 2020 at 13:10):

ah, so one invocation of manifold_simp just won't make very much progress. if you tried this you would end up more or less doing repeat {manifold_simp <|> simp} and at that point you should just simp instead

Simon Hudon (Jun 17 2020 at 13:10):

@Gabriel Ebner thanks! I have no idea how to fix this without trying a lot of permutations

Simon Hudon (Jun 17 2020 at 13:11):

@Jalex Stark it is not guaranteed to be minimal. It is just an effort to shrink the list.

Gabriel Ebner (Jun 17 2020 at 13:11):

It's not just the order that is wrong in that example. It outputs simp only [k] even though simp uses both k and l.

Jalex Stark (Jun 17 2020 at 13:12):

so it doesn't literally run simp only once with each lemma removed?

Simon Hudon (Jun 17 2020 at 13:24):

No it does literally rerun simp in that way

Simon Hudon (Jun 17 2020 at 13:24):

I'm not sure why it strips useful lemmas.

Jalex Stark (Jun 17 2020 at 14:21):

I'm still confused. Does squeeze_simp have a guarantee that if you remove any one of the lemmas in the list, it will no longer close the goal? (This is what I call "minimal")

Reid Barton (Jun 17 2020 at 14:22):

Well apparently it doesn't even guarantee what I would consider to be a presupposition of that question, namely that the output list does close the goal in the first place.

Simon Hudon (Jun 17 2020 at 14:23):

because, as @Gabriel Ebner pointed out, the order makes a difference, it's possible that you could reorder the lemmas and remove them and get the same result. squeeze_simp won't find that solution because it doesn't try multiple permutations

Sebastien Gouezel (Jun 17 2020 at 14:25):

I don't think minimality is really important for squeeze_simp. What you really want is a reasonably sized simp set that closes the goal (in reasonable time).

Simon Hudon (Jun 17 2020 at 14:39):

@Gabriel Ebner there's an interaction with retrieve that was unforeseen. When restoring the tactic state, it seems to affect the value of the packaged_goal which is basically only an expression. Do you understand that part of the API? It seems like there is a table of expressions that gets modified and those changes get reversed when reverting to a previous proof state. Does that make sense?

Gabriel Ebner (Jun 17 2020 at 14:39):


Simon Hudon (Jun 17 2020 at 14:42):

yeah, I checked those, there's supposed to be none left

Gabriel Ebner (Jun 17 2020 at 14:45):

What else is reverted? tactic.ref?

Simon Hudon (Jun 17 2020 at 14:48):

I think they get reverted too. I'm not sure how that would affect the value of an expression though

Arthur Paulino (Jan 27 2022 at 00:20):

Continuing from here, why would squeeze_simp suggest something that doesn't work? Should we check if it works first so in the worst case scenario it just fails instead of hinting something invalid?

Then making it try harder with other permutations would become a separated problem in itself.

Arthur Paulino (Jan 27 2022 at 01:23):

Actually this is not the issue :thinking:

Arthur Paulino (Jan 27 2022 at 12:14):

Okay I was able to understand part of the issue. This line builds a name_set from g and it's scrambling the order of appearance of the constants.

If, instead, I use this other (similar) function (that's not in mathlib yet):

meta def list_constant' (e : expr) : list name :=
(e.fold [] (λ e' _ es, if e'.is_constant then es.insert e'.const_name else es)).reverse

I can retrieve the constants in the right order. Note that it returns list name instead. And this time squeeze_simp is suggesting something that works. But there's a catch!

I'm using the example that @Gabriel Ebner provided in #3097. This new squeeze_simp is suggesting:

Try this: simp only [k, l, eq_self_iff_true]

However, eq_self_iff_true is not really essential there and could be dropped. So filter_simp_set doesn't seem to accomplish the goal described in its docstring yet. And some insight from its author(s) might speed up the investigation.

Any idea why this could be happening?

Arthur Paulino (Jan 27 2022 at 13:05):

I'm trying to fix it on this (draft) PR: #11696
Or maybe we should get away with the unnecessary suggestions for now?

Arthur Paulino (Jan 27 2022 at 14:35):

Alright, I figured it out. Will commit a test case too.

Last updated: Aug 03 2023 at 10:10 UTC