conv tactic `change _ by _`

Stream: new members

[Tomas Skrivan]

Is there a version of conv tactic change that can replace goal with a term that is propositionally equal?

I couldn't find it and here is a quick implementation

import Lean

open Lean Parser Tactic Conv

syntax (name := change_by) "change " term " by " tacticSeq : conv

open Meta Elab Tactic Conv
@[tactic change_by] def evalChange : Tactic := fun stx => do
  match stx with
  | `(conv| change $e by $tac) => withMainContext do
    let lhs ← getLhs
    let lhs' ← elabTermEnsuringType e (← inferType lhs)
    let eq ← mkEq lhs lhs'
    let proof ← elabTermEnsuringType (← `(by $tac)) eq
    updateLhs lhs' proof
  | _ => throwUnsupportedSyntax

example (n : Nat)
  : 0 + n = n :=
by
  conv => lhs; change n by simp

[Alex J. Best]

This reminds me of convert_to , which doesn't have a conv version as far as I'm aware.

[Damiano Testa]

I'm on mobile, so this may be less relevant, but recently there was a conv equals tactic

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/New.20conv.20.3D.3E.20.E2.80.A6.20equals.20tactic

Is this related?

[Tomas Skrivan]

Yup works exactly the same :)

[Kyle Miller]

In case you're not aware of it, hidden in the mathlib documentation there's a list of all conv tactics, at least as of a few months ago: https://leanprover-community.github.io/mathlib4_docs/docs/Conv/Guide.html

[Tomas Skrivan]

Yeah I just discovered it from the original thread about equals