Make `simp` more powerful than `dsimp`?

Stream: general

[Scott Morrison]

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?

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Simon Hudon]

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?

[Scott Morrison]

Multiple traversals of the expression.

[Simon Hudon]

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.

[Mario Carneiro]

the approach I described doesn't break type correctness

[Mario Carneiro]

two traversals is more expensive than one

[Mario Carneiro]

the repeat actually has more failed traversals than that

[Simon Hudon]

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

[Mario Carneiro]

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

[Scott Morrison]

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".

[Simon Hudon]

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

[Simon Hudon]

(unless you turn on the single_pass option)

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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. :-)

[Simon Hudon]

Look for the function visit_app

[Simon Hudon]

@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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Simon Hudon]

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

[Scott Morrison]

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

[Scott Morrison]

that does definitional simplification on arg?

[Mario Carneiro]

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

[Simon Hudon]

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

[Mario Carneiro]

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

[Simon Hudon]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Scott Morrison]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Simon Hudon]

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

[Gabriel Ebner]

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