change at

Stream: mathlib4

[Eric Wieser]

When I hover over change, I get a docstring that suggests change t at h is supported:
image.png

But the definition is

/-- `change` is a synonym for `show`,
and can be used to replace a goal with a definitionally equal one. -/
macro_rules
  | `(tactic| change $e:term) => `(tactic| show $e)

Where is this incorrect docstring coming from?

[Eric Wieser]

Ah, I see this came up earlier in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/why.20show.2E.2Efrom.20.3F/near/340489181

[Ruben Van de Velde]

It's definitely not supported. You can use replace h : xxx := h

[Eric Wieser]

Where's the docstring coming from that claims it is supported?

[Eric Wieser]

Ah, it's in core as

/--
* `change tgt'` will change the goal from `tgt` to `tgt'`,
  assuming these are definitionally equal.
* `change t' at h` will change hypothesis `h : t` to have type `t'`, assuming
  assuming `t` and `t'` are definitionally equal.
-/
syntax (name := change) "change " term (location)? : tactic

[Kevin Buzzard]

This keeps coming up. Is it really anything more than a few lines of tactic code to just do "revert h, change [what_you_want_h_to_be] -> [old goal], intro h"? I have no clue about tactic-writing but this looks like something which could easily be added to mathlib by someone who does.

[Eric Wieser]

I have no idea how to write Lean4 tactics, but my initial attempt is

elab_rules : tactic
  | `(tactic| change $e:term $[$l:location]?) => do
    let l := expandOptLocation l
    match l with
    | wildcard => fail
    | targets ts include_goal => do
      for t in ts
        skip -- TODO: `have $t : $e = $t, clear $t`
        -- let hId? := (← getLCtx).findFromUserName? name |>.map fun d ↦ d.fvarId
        -- evalTactic $ ← `(tactic| have $[$n?]? $[: $t?]? := $v)

      if include_goal
        evalTactic $ ← `(tactic| show $e)

[Eric Wieser]

The actual tactic work is trivial, I just have no idea how to process a location, or write a for loop

[Eric Wieser]

And I have no idea what I should be reading to learn about this

[Michael Stoll]

Eric Wieser said:

Ah, it's in core as

/--
* `change tgt'` will change the goal from `tgt` to `tgt'`,
  assuming these are definitionally equal.
* `change t' at h` will change hypothesis `h : t` to have type `t'`, assuming
  assuming `t` and `t'` are definitionally equal.
-/
syntax (name := change) "change " term (location)? : tactic

If you copied it correctly, then the second part has a double "assuming"...

[Eric Wieser]

I assume you meant to say "assuming
assuming I copied it correctly"...

[Adam Topaz]

for the for loop, I think you're missing a do

[Adam Topaz]

BTW, why don't we use TSyntax ident for the targets constructor of docs4#Lean.Elab.Tactic.Location ?

[Arien Malec]

Ruben Van de Velde said:

It's definitely not supported. You can use replace h : xxx := h

I clarified the section on the porting wiki on this.

[Adam Topaz]

I don't know how to clear the old fvar, but here's something that kinda works:

import Lean

open Lean Elab Tactic

#check Location
elab_rules : tactic
  | `(tactic| change $e:term $[$l:location]?) => do
    match l with
    | some l =>
        match expandLocation l with
        | .wildcard => throwError "Wildcards are not supported."
        | .targets ts incl =>
          let allowed : Bool := (ts.size == 0 && incl) || (ts.size == 1 && !incl)
          if !allowed then throwError "Changing in more than one location is not supported"
          if incl then evalTactic <| ← `(tactic| show $e)
          else
            let t := ts[0]!
            evalTactic <| ← `(tactic| have $(TSyntax.mk t) : $e := $(TSyntax.mk t))
    | none => evalTactic <| ← `(tactic| show $e)


example (n m : Nat) (h : n+2 = m) : n+1+1 = m := by
  change n+1+1 = m at h
  sorry

[Adam Topaz]

well change at \goal doesn't work.

[Adam Topaz]

I think I'm just misunderstanding what expandLocation actually does

[Adam Topaz]

Adam Topaz said:

I don't know how to clear the old fvar, but here's something that kinda works:

I forgot about replace... here's a (hacky) approximation:

import Mathlib.Tactic.Replace
import Lean

open Lean Elab Tactic

#check Location
elab_rules : tactic
  | `(tactic| change $e:term $[$l:location]?) => do
    match l with
    | some l =>
        match expandLocation l with
        | .wildcard => throwError "Wildcards are not supported."
        | .targets ts incl =>
          let allowed : Bool := (ts.size == 0 && incl) || (ts.size == 1 && !incl)
          if !allowed then throwError "Changing in more than one location is not supported"
          if incl then evalTactic <| ← `(tactic| show $e)
          else
            let t := ts[0]!
            evalTactic <| ← `(tactic| replace $(TSyntax.mk t) : $e := $(TSyntax.mk t))
    | none => evalTactic <| ← `(tactic| show $e)

example (n m : Nat) (h : n+2 = m) : n+1+1 = m := by
  change n+1+1 = m at h
  change n+2 = m
  sorry

[Kyle Miller]

@Kevin Buzzard It's a little tricker than just revert/change/intro because the revert might revert multiple hypotheses. It's also a bit tricky because change needs to be able to handle _'s (Edit: in the implementation a few messages down, the pre-existing function docs4#Lean.MVarId.changeLocalDecl handles the whole revert/change/intro for us, which is great)

[Kyle Miller]

@Adam Topaz One problem with using replace is that when there are dependencies it creates a new local variable that shadows the old one.

[Kyle Miller]

I think I got an implementation, but it's hacky in a different way:

import Lean

open Lean Elab Tactic Meta

elab_rules : tactic
  | `(tactic| change $newType:term $[$loc:location]?) => do
    let ofNewType : Syntax ← `(term| (_ : $newType))
    withLocation (expandOptLocation (Lean.mkOptionalNode loc))
      (atLocal := fun h ↦ do
        let (e, gs) ← elabTermWithHoles ofNewType (← h.getType) (← getMainTag)
          (allowNaturalHoles := true)
        liftMetaTactic fun mvarId => do
          guard (← isDefEq e (.fvar h))
          if not (← e.mvarId!.isAssigned) then
            e.mvarId!.assign (.fvar h)
          return (← mvarId.changeLocalDecl h (← inferType e)) :: gs)
      (atTarget := withMainContext do
        let (e, gs) ← elabTermWithHoles ofNewType (← getMainTarget) (← getMainTag)
          (allowNaturalHoles := true)
        liftMetaTactic fun mvarId => do
          guard (← isDefEq e (.mvar mvarId))
          if not (← e.mvarId!.isAssigned) then
            e.mvarId!.assign (.mvar mvarId)
          return (← mvarId.change (← inferType e)) :: gs)
      (failed := fun _ ↦ throwError "change failed")

example  (n m : Nat)  (p : n + 2 = m → Type) (h : n+2 = m) (x : p h) : n + 2 = m := by
  change n+1+1 = _ at h
  change n+1+1 = _
  exact h

[Adam Topaz]

Yeah I know that was a problem with using replace.

[Kyle Miller]

The main part of the implementation is mvarId.changeLocalDecl and mvarId.change (and using withLocation to drive things)

[Kyle Miller]

I'm using elabTermWithHoles but I found I kept getting defeq errors when there were placeholders if I tried to work with the types directly

[Kyle Miller]

The workaround I'm using is to run elabTermWithHoles on (_ : $newType) instead, because somehow this creates the right kind of placeholders(?), but I also need to assign the metavariable directly since isDefEq won't do that when the terms are Props (at least I think that's the issue)

[Kyle Miller]

There's a function withAssignableSyntheticOpaque that changes isDefEq to be able to assign to the metavariables that elabTermWithHoles seems to produce, and that appears to be the right thing to do here, giving a cleaner implementation.

import Lean

open Lean Elab Tactic Meta

elab_rules : tactic
  | `(tactic| change $newType:term $[$loc:location]?) => do
    withLocation (expandOptLocation (Lean.mkOptionalNode loc))
      (atLocal := fun h ↦ do
        let hTy ← h.getType
        let (e, gs) ← elabTermWithHoles newType (← inferType hTy) (← getMainTag)
                        (allowNaturalHoles := true)
        liftMetaTactic fun mvarId ↦ do
          unless ← withAssignableSyntheticOpaque (isDefEq e hTy) do
            let h' ← h.getUserName
            throwTacticEx `change mvarId
              m!"given type{indentExpr e}\nis not definitionally equal at {h'} to{indentExpr hTy}"
          return (← mvarId.changeLocalDecl h e) :: gs)
      (atTarget := withMainContext do
        let tgt ← getMainTarget
        let (e, gs) ← elabTermWithHoles newType (← inferType tgt) (← getMainTag)
                        (allowNaturalHoles := true)
        liftMetaTactic fun mvarId ↦ do
          unless ← withAssignableSyntheticOpaque (isDefEq e tgt) do
            throwTacticEx `change mvarId
              m!"given type{indentExpr e}\nis not definitionally equal to{indentExpr tgt}"
          return (← mvarId.change e) :: gs)
      (failed := fun _ ↦ throwError "change failed")

[Kyle Miller]

mathlib4#2836

[Kyle Miller]

It turns out elaborating expressions as well as show does is trickier than I'm able to pull off (and show does a very good job at dealing with placeholders). So, for the main goal, it seems you can't do better than evalTactic <| ← `(tactic| show $newType). And then for hypotheses, there's this hack you can use where you elaborate a show expression, copying how the show (and refine) tactics work, but then you throw this expression away and just use some metavariables you get from this. It seems to work fine for creating side-goals with ?_'s too (as unlikely as the use of those may be).

A downside compared to before is that the error messages are a bit confusing since they refer to details of how show ... from ... elaborates.

Here's the code now for reference:

elab_rules : tactic
  | `(tactic| change $newType:term $[$loc:location]?) => do
    withLocation (expandOptLocation (Lean.mkOptionalNode loc))
      (atLocal := fun h ↦ do
        let hTy ← h.getType
        -- This is a hack to get the new type to elaborate in the same sort of way that
        -- it would for a `show` expression for the goal.
        let mvar ← mkFreshExprMVar none
        let (_, mvars) ← elabTermWithHoles
                          (← `(term | show $newType from $(← Term.exprToSyntax mvar))) hTy `change
        liftMetaTactic fun mvarId ↦ do
          return (← mvarId.changeLocalDecl h (← inferType mvar)) :: mvars)
      (atTarget := evalTactic <| ← `(tactic| show $newType))
      (failed := fun _ ↦ throwError "change tactic failed")