squeeze_simp times out

Stream: general

[Sebastien Gouezel]

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?

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Kevin Buzzard]

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

[Jalex Stark]

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]

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

[Sebastien Gouezel]

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]

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]

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

[Jalex Stark]

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

[Patrick Massot]

This could be true (using simp attributes).

[Reid Barton]

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

[Simon Hudon]

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

[Gabriel Ebner]

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

[Simon Hudon]

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]

@Gabriel Ebner thanks for the correction

[Simon Hudon]

squeeze_simp does not consider this

[Jalex Stark]

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]

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]

Simon Hudon said:

squeeze_simp does not consider this

Filed as #3097.

[Jalex Stark]

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]

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

[Simon Hudon]

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

[Gabriel Ebner]

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]

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

[Simon Hudon]

No it does literally rerun simp in that way

[Simon Hudon]

I'm not sure why it strips useful lemmas.

[Jalex Stark]

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]

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]

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]

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]

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

Metavariables?

[Simon Hudon]

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

[Gabriel Ebner]

What else is reverted? tactic.ref?

[Simon Hudon]

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

[Arthur Paulino]

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]

Actually this is not the issue :thinking:

[Arthur Paulino]

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]

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]

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