contextual simp

Stream: general

[Bhavik Mehta]

I find the simp config option (config := {contextual := true}) incredibly helpful. In my experience, there are very few times when turning it on makes my proof worse in any way, except for the fact that it's so much to type and read.

1. Is it possible to have a local config setting in my file so that every simp call automatically has that option turned on?
2. Should this option be turned on by default in simp?

[Bhavik Mehta]

Here's a quick example of the kind of thing it can be used for:

def p : Nat → Prop := sorry
def f : Nat → Nat := sorry
def g : Nat → Nat := sorry
theorem thing {x : Nat} (h : p x) : f x = g x := sorry

example : ∀ x, p x → f x = g x := by
  simp (config := {contextual := true}) [thing]

with the option turned off, simp [thing] can't close the goal, but once it's open simp can look at the context in which f x = g x is meant to be proved, and use hypotheses there to help

[Joachim Breitner]

At least nice syntax (simp contextual …) would be nice. Whenever I see (config := …) it feels like we are in reaching into the guts of the machine, warranty broken, get to keep both pieces territory, and I hope that contextual is more user-facing than that.

[Bhavik Mehta]

I'd go further and ask for simp! to mean that! My rough mnemonic for ! is "try a bit harder", which feels pretty similar to what contextual is doing here

[Joachim Breitner]

Hmm, if there are many different ways a tactic could go harder, like here (less limits! more unfolding! contextual! decide!) then simp! is probably no a good UI choice.

[Joachim Breitner]

With my Isabelle background I also wonder why it isn’t simply the default. Probably performance, or simply backward compat? Or does it sometimes maybe break?

[Bhavik Mehta]

Fair point about simp!. But I also wonder why it isn't the default...

[Tomas Skrivan]

I think caching is harder with contextual on.

[Floris van Doorn]

I also find contextual the most useful simp configuration, and use it regularly. That said, I don't use it that often, so if it's a bit slower, I think we should not turn it on by default.
I think a useful experiment would be to build Mathlib with this option turned on by default.
If we don't turn it on by default, I would also appreciate a shorter syntax

[Bhavik Mehta]

Yes, running this experiment sounds incredibly valuable. How can I turn the option on by default in order to try this? (Or rather, how can I do so in a way that CI can benchmark it rather than me rebuilding Lean + mathlib)

[Floris van Doorn]

Maybe override the simp syntax and elaborate it to a call with the contextual option turned on. Hopefully there are not too many nonterminal simps that now break (or terminal simps that break due to nonconfluence).

[Floris van Doorn]

I'm not exactly sure how to do this if the user also specifies a config option and you have to combine options (then it might be tricky as a purely syntax-level manipulation). This should be doable, but I don't know exactly how.
One option is to not override those simp calls, and then it can be done by an easy macro.

[Joachim Breitner]

Or open a draft PR against lean4, changing the actual default, and then play with the adaption branch

[Bhavik Mehta]

Both of these sound doable but I'm not sure I'm smart enough to figure either one out on my own

[Kyle Miller]

There's a chance that the next Lean release will have simp +contextual syntax and some support for composable config updates. We've been discussing enabling such notation for every tactic that uses Lean.Parser.Tactic.config, with some varying thoughts on what the syntax would be.

I've been thinking syntax like simp +contextual -zeta (etaStruct := .none) (maxSteps := 22222), where +contextual is shorthand for (contextual := true).

[Bhavik Mehta]

Does composable config updates mean chaining +contextual -zeta in the way you did, or having local config settings in a file, or something else? In any case this syntax is nicer already!

[Kyle Miller]

Composability means you would be able to make a macro that takes my_great_tactic $config to simp +contextual $config, maybe with a little bit of extra syntax.

[Floris van Doorn]

This is a partial implementation of the macro:

open Lean Meta Parser Tactic

macro (name := my_simp) (priority := high) "simp"
  -- cfg:(config)?
  dis:(discharger)? args:(" [" ((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
  loc:(location)? : tactic =>
`(tactic| simp (config := {contextual := true}) $(dis)? $(loc)?)

example : ∀ (P Q : Prop), P → (P → Q) → Q := by
  simp -- works

Currently the args argument is ignored in this macro. Maybe one of the metaprogramming wizards can help me with also applying the simp to $(args)?, which doesn't work because that is not an atomic syntax.
I would also be interested to see the implementation with an uncommented $cfg and adding the extra configuration option on the right-hand side. I tried to do that once before with a different tactic, but didn't succeed.

(I do not let the macro apply for simp only since it seems bad to turn contextual on in that case).

[Bhavik Mehta]

Kyle Miller said:

There's a chance that the next Lean release will have simp +contextual syntax and some support for composable config updates. We've been discussing enabling such notation for every tactic that uses Lean.Parser.Tactic.config, with some varying thoughts on what the syntax would be.

I've been thinking syntax like simp +contextual -zeta (etaStruct := .none) (maxSteps := 22222), where +contextual is shorthand for (contextual := true).

I've been playing with this recently, and I really like it. Thanks!

[Kyle Miller]

By the way, here's how you can define "Bhavik's simp":

declare_simp_like_tactic bhavikSimp "bsimp " (contextual := true)

example : ∀ (P Q : Prop), P → (P → Q) → Q := by
  bsimp

[Bhavik Mehta]

Thanks! Have added this to my list of mehtaprogramming tricks :)

[Edward van de Meent]

i seem to recall that now you can also write simp +contextual

[Edward van de Meent]

and apparently, this also works:

declare_simp_like_tactic bhavikSimp "bsimp " +contextual