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

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

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

#### 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: Dec 20 2023 at 11:08 UTC