Rewriting in a let-body

Stream: lean4

[Wojciech Nawrocki]

Is it possible to rewrite in the value (not the type) of a let binding in the local context? I couldn't get this to work in Lean 3 either. For example

def f (a b : Nat) : Nat := a + b
example : f 1 2 = f 2 1 := by
  let x := f 1
  have : f 1 = fun x => 1 + x := rfl
  /- tactic 'rewrite' failed, did not find instance of the pattern in the target expression
    f 1
  x : ℕ → ℕ := f 1
  this : f 1 = fun x => 1 + x
  ⊢ f 1 2 = f 2 1 -/
  rw [this] at x

[Mac]

Could you elaborate on your use case a bit more (i.e., what your goal is)? Is there a reason why a solution like the following is insufficient?

def f (a b : Nat) : Nat := a + b
example : f 1 2 = f 2 1 := by
  let x := f 1
  have h : x = f 1 := rfl
  have : f 1 = fun x => 1 + x := rfl
  rw [this] at h
  /-
  x : Nat → Nat := f 1
  h : x = fun x => 1 + x
  this : f 1 = fun x => 1 + x
  ⊢ f 1 2 = f 2 1
  -/

[Wojciech Nawrocki]

I am using let-bindings in the context to represent auxiliary functions in a tactic which will then be encoded by a further tactic. However I want to control how this encoding goes by rewriting the the bodies of these auxiliaries. Basically I can go with the let-equals solution you propose or even a custom data structure, it's just that using the let-bodies was very convenient, which is why I wondered if I can rewrite in them.

[Tomas Skrivan]

I would be also quite interested in doing the rewrites directly in the let bindings. My application would be to do source code transformation in the tactic mode.

Currently I'm doing something vaguely similar and to do the rewriting I encode the value in the type.
Define an auxiliary type

def Aux {α : Type u} (a : α) := α

Then you can have the value f 1 in the type Aux (f 1) and do the rewrites.

An example:

def Aux {α : Type u} (a : α) := α
def aux {α} (a : α) : Aux a := a

def f (a b : Nat) : Nat := a + b

example : f 1 2 = f 2 1 := by
  have h : f 1 = fun x => x + 1 := by conv => rhs; enter[x]; rw [Nat.add_comm];
  let x : Aux (f 1) := by
    rw[h];      -- desired rewrite
    apply aux _ -- finish definition of Aux

  have test_rewrite : x = fun x => x + 1 := rfl
  admit

So the general idea is to instead of writing:

let x := <x definition>
rw [<x rewrite>] at x

write

let x : Aux <x definition> := by rw [<x rewrite>]; apply aux _

That is ugly though. We can define a macro of the form term "rewrite_by" convSeq and write ((f 1) rewrite_by rw[h]) instead.

Full code

open Lean.Parser.Tactic.Conv

syntax term "rewrite_by" convSeq : term

macro_rules
  | `($x rewrite_by $rw:convSeq) =>
    `((by (conv => enter[1]; $rw) (apply aux _) : Aux $x))

def f' (a b : Nat) : Nat := a + b

example : f' 1 2 = f' 2 1 := by
  have h : f' 1 = fun x => x + 1 := by conv => rhs; enter[x]; rw [Nat.add_comm];
  let x := ((f' 1) rewrite_by rw[h])

  have test_rewrite : x = fun x => x + 1 := rfl
  admit

[Tomas Skrivan]

(I have modified the statement from f 1 = fun x => 1 + x to f 1 = fun x => x + 1 such that it is not solvable by rfl and the test_rewrite fails if the rewrite rw[h]is not done)

[Tomas Skrivan]

The unfortunate thing is that the resulting definition of x looks rather ugly in the goal view:

x : Aux (f 1) := Eq.mpr (_ : Aux (f 1) = Aux fun x => x + 1) (aux fun x => x + 1)

Not sure what to do about it. To make sense of this definition I would suggest looking at the intermediate stages of(paste it to the code above)

have test_rewrite : x = fun x => x + 1 := by simp only [Eq.mpr]; unfold aux; rfl

[Sebastian Ullrich]

Perhaps we should default pp.proofs.withType to false in the info view, assuming hover gives the same information

[Tomas Skrivan]

I do not have a strong opinion about that and I do not think this is a strong case for or against. For example, if you make the a argument in aux implicit then the the goal view shows x : Aux (f 1) := Eq.mpr _ aux. You completely loose the information about the actual definition fun x => x + 1.

I think this case needs a custom tailored solution to force Lean to show something nice an useful.