Exclude variables when `subst_vars`

Stream: lean4

[Clément Blaudeau]

I'd like to do subst_vars but keeping some of the variables. Looking at the manual, it does not seems like it's a built-in option of subst_vars. Is there a workaround/trick ?

Typically, with the following example:

theorem foo a b c :
  a = 7189283767892987637829987 -- very long expression that I don't want to duplicate
  → b = (a + a) * a + a -- intermediate variable that I want to substitute
  → c = b * a + b * b * b
  → c + 1 = 0
  := by
  intros
  subst b c -- works, but unsatisfactory
  sorry

I would like to subst b and c but without naming them (I have 30+ variables to subst, and their names are not exposed)
Is there some equivalent to subst_vars [-a] ?
Thank for your help!

[Kim Morrison]

Could you use revert/intro?

[František Silváši 🦉]

I am not sure how resilient this version is (e.g. it doesn't bother with HEq) but it works for this example and can be extended for your use case :).

import Lean
import Qq

open Lean Qq

def substEqsSed (reject : Array Name) (mvarId : MVarId) : MetaM (Option MVarId) := do
  let mvarIds ← mvarId.casesRec fun ldecl ↦ do
    let type ← instantiateMVarsQ (α := q(Prop)) ldecl.type
    let ~q($lhs = _) := type | return false
    let Expr.fvar name := lhs | return false
    return !reject.contains (←name.getUserName)
  Meta.ensureAtMostOne mvarIds

elab "subst_but" reject:ident* : tactic =>
  Elab.Tactic.liftMetaTactic1 ∘ substEqsSed <| reject.map (·.getId)

theorem foo a b c :
  a = 7189283767892987637829987 -- very long expression that I don't want to duplicate
  → b = (a + a) * a + a -- intermediate variable that I want to substitute
  → c = b * a + b * b * b
  → c + 1 = 0
  := by
  intros
  subst_but a -- same result as `subst b c`
  sorry

[Clément Blaudeau]

Thank you for the macro! I'll try it out on my non-minimized example and report how it went!