swap example with monad tactics

[miriampolzer]

Drafted up tactics and used andres approach from #75 to step through the swap proof rather nicely. The tactics are very drafty, first time I am doing this. I dont want to merge this as is, just wanted to share what I tried out.

[eric-wieser]

Is this the same as let +generalize this := t?

[miriampolzer]

I think so, thank you!

[andres-erbsen]

Here's a difference:

example : (1 + 1) + 1 = 2 + 1 := by
    -- set_simple (2+1) -- works as expected (modifies RHS only)
    let +generalize y := 2+1 -- modifies both sides, new goal is `y = y`

[eric-wieser]

Note that this only happens for Nat, which Lean unifies very agressively even with with_reducible applied.

If the numerals are Int or UInt64 then with_reducible let +generalize y := 2 + 1 behaves in the way you requested.

Lean frequently takes the viewpoint that exact expression matches don't matter, and all that matters is definitional matching up to some reducibility. Typeclasses basically force it to take this viewpoint:

import Mathlib -- for typeclasses

open Lean Elab Tactic Meta

-- as in this PR
def set_simple (mvarId : MVarId) (t : Expr): MetaM MVarId := do
  mvarId.withContext do
    let target ← mvarId.getType
    let type ← inferType t
    let lctx ← getLCtx
    let name := lctx.getUnusedName `x

    let (fvarId, mvarId) ← (← mvarId.define name type t).intro name

    mvarId.withContext do
      let newTarget := target.replace fun e =>
        if e == t then some (mkFVar fvarId) else none -- this line should use `isDefEq` instead
      mvarId.replaceTargetDefEq newTarget

elab "set_simple " t:term : tactic => do
  let mvarId ← getMainGoal
  let term ← elabTerm t none
  let newMvarId ← set_simple mvarId term
  replaceMainGoal [newMvarId]

example : (1 + 2) + 1 = (3 : Int) := by
  rw [add_assoc]  -- Int.add_assoc is ok here, but `add_assoc` introduces `AddSemigroup.toAdd`
  set_simple (2 + 1 : Int)
  -- didn't work, goal doesn't contain `x`

[miriampolzer]

For me to learn: Say we wanted to have a version that doesn't reduce while replacing but can handle the Typeclass issue, would there be a somewhat more limited reduction than isDefEq one could e.g. call on target in the first line of set_simple to avoid this?

Now I am also wondering if the replaceTargetDefEq would blow up on terms that get too large when reduced.