How to unwrap a let expression

Stream: general

[Bolton Bailey]

I am in tactic mode, and I have a value defined via let, which appears in my hypothesis list as g': Polynomial (ZMod q) := p % vanishingPoly G. Now I have g' in my goal and I want to see it as the value it's defined as again. How do I do this?

[Kevin Buzzard]

You can use change to do it explicitly, or you can just imagine that it's being translated into its def and things might work fine anyway.

[Bolton Bailey]

The change documentation looks like

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

[Bolton Bailey]

Do I have to rewrite out the whole goal? Why isn't there just a simple tactic where I can say unlet g' and be done?

[Kevin Buzzard]

You need to use set if you want that.

[Kevin Buzzard]

You set g := blah with hg and now you can just rw [hg]

[Kevin Buzzard]

You don't have to rewrite the entire goal, you can just use _s liberally. But set is easier.

[Bolton Bailey]

Wait, so then what is the difference between set and let and why would I ever use let in tactic mode?

[Bolton Bailey]

Actually strike the cross out, I'm definitely confused about why you would use let in tactic mode. Is there ever a reason?

[Bolton Bailey]

Is it that let is not actually a tactic, but a lean built-in that somehow seems like a tactic and has tactic documentation?

[Niels Voss]

let is both a built-in and a tactic. The tactic let is essentially just a wrapper around the let built-in that lets you use it in tactic mode (kind of like how have is both a command and a tactic).
let is very similar to have in tactic mode, with the main difference that let remembers what the term is defined as. If you do let x := 2 then x is now definitionally equal to 2 so you can prove that x = 2 with just rfl. This is not the case when you use have, because if you did have x := 2 then there's no way to prove that x = 2.

[Niels Voss]

set is very similar to let, but if you do set x := some_expression then it will look at all your hypotheses and replace all instances of some_expression with x. Essentially you can use set as a replacement for generalize. As Kevin Buzzard mentioned, another helpful thing about set is that if you do set g := blah with hg then it will also give you a proof that g = blah

[Bolton Bailey]

Thanks Niels, one more question: I see that there is a set! tactic that does not replace the expression. Does this mean that set! behaves identically to let?

[Niels Voss]

I actually don't know. The only difference I can see between set! and let is that set! lets you do set! x := 2 with hx to automatically prove that x = 2. I think this is basically just the same thing as let x := 2, have hx : x = 2 := rfl but there might be some other difference I'm not aware of.

[Bolton Bailey]

Ok, thanks for the explanation and thanks to Kevin for solving my issue, you all have been a great help.

[Niels Voss]

Generally I like to use let to introduce new terms that represent data, and have to introduce new terms that represent proofs. And then I work with let statements by using change quite often. I only started learning lean last year, and when I did I had a lot of trouble with this same thing.

[Bolton Bailey]

My top-level issue is that I have change g' with p % vanishingPoly G in my ported code, and I'm getting the error "tactic 'Lean.Parser.Tactic.changeWith' has not been implemented"

[Niels Voss]

I don't have much experience with lean 4 but from reading the lean 3 documentation it seems that if your goal is something like f g' = something then change g' with p % vanishingPoly G is just a shorter way to accomplish change f (p % vanishingPoly G) = something. Basically you just write change ... where the ... is what you want your goal to become. Do you have a minimum working example?

[Niels Voss]

What I think the change g' with (p % vanishingPoly G) command does is just replace all instances of g' with (p % vanishingPoly G) in the goal (I didn't actually know this existed) but if you can't use that you should just write out change ... where ... is what the goal would look like if you were to just replace all instances of g' with (p % vanishpingPoly G). You could also consider asking about this in the #lean4 stream.

[Bolton Bailey]

Sorry, actually I'm mistaken, the change with issue can be ameliorated by just commenting out the tactic. My issue now is that when I switch let to set to try to fix another part of the code, another part of the code starts timing out at isDefEq, but indeed this seems like a problem for the lean4 stream.

[Kyle Miller]

@Bolton Bailey I couldn't find anything in Lean 4 or mathlib that lets you substitute let bindings, but it's possible to write this unfold_let tactic:

import Mathlib.Tactic.Basic

open Lean Meta Elab.Tactic

/-- Unfold all the fvars from `fvars` in `e` that are local declarations. -/
def unfoldFVars (e : Expr) (fvars : Array FVarId) : MetaM Expr := do
  transform e fun node =>
    match node with
    | .fvar fvarId =>
      if fvars.contains fvarId then
        (TransformStep.continue ·) <$> (fvarId.getValue? >>= Option.mapM instantiateMVars)
      else
        pure TransformStep.continue
    | _ => pure TransformStep.continue

/--
`unfold_let x y z at loc` unfolds the local declarations `x`, `y`, and `z` at the given
location.
-/
syntax "unfold_let" (ppSpace colGt term:max)+ (ppSpace Parser.Tactic.location)? : tactic

elab_rules : tactic
  | `(tactic| unfold_let $hs:term* $[$loc?]?) => withMainContext do
    let fvarIds ← getFVarIds hs
    withLocation (expandOptLocation (Lean.mkOptionalNode loc?))
      (atLocal := fun h => do
        liftMetaTactic1 fun mvarId => do
        let ty ← instantiateMVars (← h.getType)
        mvarId.changeLocalDecl' h (← unfoldFVars ty fvarIds))
      (atTarget := liftMetaTactic1 fun mvarId => do
        let ty ← instantiateMVars (← mvarId.getType)
        mvarId.change (← unfoldFVars ty fvarIds))
      (failed := fun _ => throwError "unfold_let failed")

example : let x := 1; let y := 2; x + y = y + x := by
  intro x y
  /-
  x: Nat := 1
  y: Nat := 2
  ⊢ x + y = y + x
  -/
  unfold_let x
  -- ⊢ 1 + y = y + 1

[Kyle Miller]

Unless there's some other way to substitute this that I'm missing, I can try contributing this to mathlib

[Kyle Miller]

I'll mention that dsimp only will substitute everything defined with let indiscriminately

[Bolton Bailey]

This is helpful to know, there was a simp only [g'] in the ported code which was not working, but dsimp only seems to make this part work.

[Kyle Miller]

This has made it into #5717, among a few other tactics (@Jeremy Salwen it also has eta_reduce)

[Jeremy Salwen]

Kyle Miller said:

This has made it into #5717, among a few other tactics (Jeremy Salwen it also has eta_reduce)

Would an eta for structures tactic belong here as well?