How to call a simp lemma within a simproc?

Stream: metaprogramming / tactics

[George Pîrlea]

This doesn't work, and I'm not sure why. Any clue what I'm doing wrong?

import Lean
open Lean Meta Elab Tactic

def elim_exists_eq_impl : Simp.Simproc := fun e => do
  let thms := (← (simpOnlyBuiltins ++ [``exists_eq_left]).foldlM (·.addConst ·) ({} : SimpTheorems))
  let ctx : Simp.Context := {
    config := (← Simp.getContext).config
    simpTheorems := #[thms]
    congrTheorems := (← getSimpCongrTheorems)
  }
  let (res, _stats) ← Simp.main e ctx
  trace[debug] "Result: {res.expr}"
  return .continue res

#check exists_eq_left

-- I'm not sure if this (pattern declaration) is needed
simproc_decl elim_exists_eq (∃ _, _) := elim_exists_eq_impl

set_option trace.debug true

theorem xx (s' : Nat): ∃ s, s = s' ∧ True := by
  -- simp only [exists_eq_left] -- this works
  simp only [elim_exists_eq] -- this doesn't; WHY?

To give some context of what I'm trying to accomplish:

I have a larger simproc to eliminate redundant existential quantifiers in goals by "pushing" the quantified variable to the right (such that it's the right-most quantifier) and then "pushing" the equality involving that quantifier to the left over conjunction in the quantified formula (such that's it's the left-most conjunct). After this transformation (and potentially using and_assoc), exists_eq_left should get rid of the quantifier. I'd want to call exists_eq_left within my larger simproc, but I don't know how.

[George Pîrlea]

"Manually" recreating the behaviour of exists_eq_left as a simproc works, but is quite unwieldly:

import Lean
open Lean Meta Elab Tactic

theorem exists_eq_left_thm : ∀ {α : Sort u_1} {p : α → Prop} {a' : α}, (∃ a, a = a' ∧ p a) = p a' :=
  propext exists_eq_left

def elim_exists_manual : Simp.Simproc := fun e => do
  let_expr Exists t eBody := e | return .continue
  -- the body of an `∃` is a lambda
  let step ← lambdaBoundedTelescope eBody (maxFVars := 1) (fun ks lBody => do
      let #[k] := ks
        | throwError "Expected exactly one variable in the lambda telescope"
      let_expr And l r ← lBody | return .continue
      let_expr Eq _ lhs rhs ← l | return .continue
      if ← isDefEq lhs k then
        let r' ← mkLambdaFVars #[lhs] r
        let newBody ← Core.betaReduce $ mkAppN r' #[rhs]
        let proof ← mkAppOptM ``exists_eq_left_thm #[t, r', rhs]
        return .done { expr := newBody, proof? := proof }
      else
        return .continue
  )
  return step

simproc_decl elim_exists_eq (∃ _, _) := elim_exists_manual

theorem xx (s' : Nat): ∃ s, s = s' ∧ True := by
  simp only [elim_exists_eq] -- this works