## 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 :=
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 (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!!!)

#### 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?

Metavariables?

#### 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

Last updated: May 09 2021 at 20:11 UTC