Zulip Chat Archive

Stream: general

Topic: squeeze_simp times out


view this post on Zulip 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 :=
begin
  /- 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 },
    sorry
  }
end

Is there a way to investigate what is going on?

view this post on Zulip 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,
 topological_fiber_bundle_core.local_triv_symm_fst]

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

view this post on Zulip Sebastien Gouezel (Jun 17 2020 at 12:37):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Jun 17 2020 at 12:44):

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

view this post on Zulip 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 [...]]

view this post on Zulip Patrick Massot (Jun 17 2020 at 12:47):

This could be true (using simp attributes).

view this post on Zulip 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?

view this post on Zulip Simon Hudon (Jun 17 2020 at 13:01):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jun 17 2020 at 13:02):

@Gabriel Ebner thanks for the correction

view this post on Zulip Simon Hudon (Jun 17 2020 at 13:02):

squeeze_simp does not consider this

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Jun 17 2020 at 13:08):

Simon Hudon said:

squeeze_simp does not consider this

Filed as #3097.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jalex Stark (Jun 17 2020 at 13:12):

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

view this post on Zulip Simon Hudon (Jun 17 2020 at 13:24):

No it does literally rerun simp in that way

view this post on Zulip Simon Hudon (Jun 17 2020 at 13:24):

I'm not sure why it strips useful lemmas.

view this post on Zulip 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")

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip Gabriel Ebner (Jun 17 2020 at 14:39):

Metavariables?

view this post on Zulip Simon Hudon (Jun 17 2020 at 14:42):

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

view this post on Zulip Gabriel Ebner (Jun 17 2020 at 14:45):

What else is reverted? tactic.ref?

view this post on Zulip 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


Last updated: May 09 2021 at 20:11 UTC