Zulip Chat Archive

Stream: general

Topic: Make `simp` more powerful than `dsimp`?


view this post on Zulip Scott Morrison (Sep 05 2020 at 04:08):

Would it be possible to change the behaviour of simp (i.e. the C++ implementation), so that whenever it is trying to use a _refl_lemma, it behaves as dsimp?

view this post on Zulip Scott Morrison (Sep 05 2020 at 04:09):

It would be great to avoid the need for dsimp, simp which we see so often in the category theory library, and explained in this library note:
https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/category/default.lean#L249

view this post on Zulip Scott Morrison (Sep 05 2020 at 04:09):

(I've just found myself writing simp, dsimp, simp.)

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:20):

Ideally, simp should traverse the term, recursing into all subterms, but when the subterm is not one provided by the congr lemma it should switch to "definitional mode" where it only does things dsimp would do. That algorithm yields simp and dsimp as special cases

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:21):

Alternatively, we can just make simp' a wrapper around repeat {simp <|> dsimp} which is a lot easier to do. :)

view this post on Zulip Scott Morrison (Sep 05 2020 at 04:22):

I'd certainly be happy with that. Obviously it's slower.

view this post on Zulip Scott Morrison (Sep 05 2020 at 04:23):

Presumably it would need to support simp' [X, Y, Z] and simp' only [X, Y, Z] and so on.

view this post on Zulip Simon Hudon (Sep 05 2020 at 04:24):

One of the overhead there is building the simp_lemmas lists multiple times which we can skip. Where is the rest of the inefficiency coming from?

view this post on Zulip Scott Morrison (Sep 05 2020 at 04:24):

Multiple traversals of the expression.

view this post on Zulip Simon Hudon (Sep 05 2020 at 04:27):

But that's already part of what simp does. Do we cut down the number if we merge the two tasks? I'm not sure because simp and dsimp have distinct tasks. simp has to be careful not to break the type correctness of the expression while dsimp can be more aggressive.

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:28):

the approach I described doesn't break type correctness

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:28):

two traversals is more expensive than one

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:29):

the repeat actually has more failed traversals than that

view this post on Zulip Simon Hudon (Sep 05 2020 at 04:29):

Your estimate is that you'd roughly cut down the number of traversals by half?

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:30):

at the very least the repeat must do 3 traversals for a successful run

view this post on Zulip Scott Morrison (Sep 05 2020 at 04:30):

Don't simp and dsimp by themselves only ever do a single traverse? Sometimes they act multiple times on the same subexpression, but they never "go back".

view this post on Zulip Simon Hudon (Sep 05 2020 at 04:31):

No, on their own they also repeat. They traverse bottom up and then they try again. They stop when they can't make any more changes

view this post on Zulip Simon Hudon (Sep 05 2020 at 04:31):

(unless you turn on the single_pass option)

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:32):

consider a case where we want to do simp, dsimp, simp:

simp -> succeed
simp -> fail
dsimp -> succeed
simp -> succeed
simp -> fail
dsimp -> fail

that's 6 traversals where 3 were done before and 1 could do the job in principle

view this post on Zulip Scott Morrison (Sep 05 2020 at 04:32):

I thought single_pass just prevented it from rewriting in an already rewritten subexpression

view this post on Zulip Scott Morrison (Sep 05 2020 at 04:33):

I've been trying to read https://github.com/leanprover-community/lean/blob/master/src/library/tactic/simplify.cpp looking for the spot where simp stops looking inwards because it can't find an appropriate congr. And failing. :-)

view this post on Zulip Simon Hudon (Sep 05 2020 at 04:34):

Look for the function visit_app

view this post on Zulip Simon Hudon (Sep 05 2020 at 04:35):

@Mario Carneiro I believe you. I don't have a firm grip on the number of passes that simp performs on average. If you have the time to implement your idea, I'd love to see the difference

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:36):

It is possible to get fewer than 6 calls with better state management even if you only treat simp and dsimp as black boxes

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:37):

if you assume that simp never succeeds twice in a row (which is false, but close enough) then you can get it down to 4 calls in the example

view this post on Zulip Simon Hudon (Sep 05 2020 at 04:38):

That would be worth experimenting with. This is something that can be done without going into the C++ code I think

view this post on Zulip Scott Morrison (Sep 05 2020 at 04:38):

So is Mario's suggestion to revert to dsimp mode if congr lemmas aren't available a suggestion to add a line before
https://github.com/leanprover-community/lean/blob/master/src/library/tactic/simplify.cpp#L769

view this post on Zulip Scott Morrison (Sep 05 2020 at 04:39):

that does definitional simplification on arg?

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:40):

I think we want to enhance the defeq_canonize step at the beginning of that function

view this post on Zulip Simon Hudon (Sep 05 2020 at 04:42):

For comparison, you can look at what dsimplify.cpp does in visit_app

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:43):

https://github.com/leanprover-community/lean/blob/master/src/library/tactic/dsimplify.cpp#L188

view this post on Zulip Simon Hudon (Sep 05 2020 at 04:43):

I think you're right Mario, defeq canonize is a good place to look

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:44):

what's not clear to me is whether to basically call dsimp on the expression, or just do a head simplification; the first sounds like it might have exponential blowup but the second is probably incomplete

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:46):

In order to incorporate it in the traversal, we need to analyze the congr lemma to find all arguments that don't change, and dsimp in them before traversing the hypotheses of the congr lemma

view this post on Zulip Scott Morrison (Sep 05 2020 at 04:51):

Is it really necessary to do this analysis? I feel like we'd get most of the benefit just by doing the dsimp on the arg of a dependent function, when simp has fallen back just using congr_fun.

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:52):

It comes up pretty frequently in automatically generated congr lemmas, for example a = b -> c = d -> @add A inst a c = @add A inst b d

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:52):

here if we loop over just the hypotheses we will miss A and inst

view this post on Zulip Mario Carneiro (Sep 05 2020 at 04:55):

We can probably modify try_auto_eq_congr to do something else in the Fixed and FixedNoParam cases

view this post on Zulip Scott Morrison (Sep 05 2020 at 05:15):

Going back to the repeat {simp <|> dsimp} suggestion, I think

import tactic.core

namespace tactic

meta def alternate : tactic unit  tactic unit  tactic unit
| t₁ t₂ := t₁ >> try (alternate t₂ t₁)

meta def alternate' (t₁ t₂ : tactic unit) : tactic unit :=
(t₁ >> try (alternate t₂ t₁)) <|> (t₂ >> try (alternate t₁ t₂))

meta def simp' := alternate' `[dsimp] `[simp]

end tactic

would work.

view this post on Zulip Scott Morrison (Sep 05 2020 at 05:15):

Should I bother dressing this up (e.g. argument handling an interactive simp')?

view this post on Zulip Scott Morrison (Sep 05 2020 at 05:17):

(Of course I'd be perfectly happy if making a PR of this provoked someone into working out how to improve simp in core, thereby making it obsolete!)

view this post on Zulip Scott Morrison (Sep 05 2020 at 05:17):

But on the other hand if people wouldn't want to allow simp' as a valid terminal step in proofs I'm not keen to do the work.

view this post on Zulip Simon Hudon (Sep 05 2020 at 05:26):

That looks like a reasonable workaround to me. Given how prevalent the pattern is in category theory code, that looks like a nice improvement. And we could support it with squeeze_* too

view this post on Zulip Gabriel Ebner (Sep 05 2020 at 10:11):

The hsimp tactic did this in '18: https://github.com/gebner/hott3/blob/7ead7a8a2503049eacd45cbff6587802bae2add2/src/hott/init/meta/simp.lean


Last updated: May 06 2021 at 21:09 UTC