simp should be able to create new goals

Stream: lean4

[Floris van Doorn]

I just opened this RFC: lean#5994.
This suggest that simp gets the ability to create new goals when using a conditional rewrite rule, just like rw.
I think this would be incredibly useful, especially when rewriting under (nested) sums and integrals.
Please discuss here, and upvote the issue if you agree.
(If you have seen people request this before, please link those discussions, so that I can add them to the RFC)

[Michael Stoll]

I'm a bit wary that this could lead to simp "doing too much" and creating a bunch of side goals that are not all satisfiable, because it tries many lemmas that might apply, but actually don't in the concrete situation.

[Floris van Doorn]

I agree, this option should be off by default (see RFC).

[Floris van Doorn]

We can discuss among Mathlib users whether we want it on by default in simp_rw (I strongly think we should have it on by default).

[Floris van Doorn]

If it still creates undesired side goals even with simp only or simp_rw, you can either set the option singlePass := true or you can give more implicit arguments to your simp-lemma, so that it only rewrites the desired occurrences.

[Michael Stoll]

I agree that it makes sense for simp_rw (so that its behavior is more similar to what rw does).

[Michael Stoll]

Otherwise, I assume the only way to find out if it works in a reasonable way is to try it out.

[Asei Inoue]

I think this is a task of aesop, not simp.

[Frédéric Dupuis]

One possible issue is that the side-goals would appear in whichever order simp applies the lemmas, and this is largely arbitrary and subject to change whenever simp's internals change.

[Joachim Breitner]

I tried to find out if this is maybe possible using the existing API and the ability to set a discharger, but the simplifier doesn’t like mvars being created there:

import Mathlib

open Lean Meta Elab Tactic

axiom f : Bool → Bool
axiom P : Prop
@[simp] axiom odd_id_eq : P → f true = false

set_option trace.Meta.Tactic.simp true in
set_option trace.Meta.Tactic.simp.discharge true in
example : f true = false := by
  run_tac do
    let ctxt ← Simp.Context.mkDefault
    let (result?, _stats) ← simpGoal (← getMainGoal) ctxt (discharge? := some fun t => do
      logInfo m!"Discharging {t}"
      return (some (← mkFreshExprSyntheticOpaqueMVar t)))
    match result? with
    | none => replaceMainGoal []
    | some (_, mvarId) => replaceMainGoal [mvarId]
 ```

[Floris van Doorn]

That might indeed be a way to implement this: make simp compatible with dischargers that create new subgoals.