Opaque let binding in simp

Stream: lean4

[Tomas Skrivan]

When you turn off zeta reduction in the simplifier the free variable introduced by let becomes completely opaque.

In my use case this is a problem. I want the discharger/typeclass system to see through these free variables.

Here is an example:

set_option trace.Meta.Tactic.simp.discharge true in
example :
  let f := (λ x : Int => 1 + x)
  inv (λ x => f (f x))
  =
  λ x => inv f (inv f x)
  := by simp (config := { zeta := false})  -- [Meta.Tactic.simp.discharge] @comp_inv, failed to synthesize instance HasInv f

The simplifier fails to apply (f ∘ f)⁻¹ = f⁻¹ ∘ f⁻¹ because f is complete opaque with zeta reduction off and it can't prove that f is invertible.

Is there a way to deal with this?

---

My ultimate goal is to have a tactic that turns an expression:

let f := (λ x : Int => 1 + x)
inv (λ x => f (f x))

into:

let f := (λ x : Int => 1 + x)
let inv_f := (λ x : Int => x - 1)
λ x => inv_f (inv_f x)

[Tomas Skrivan]

mwe:

variable {α β γ : Type} [Inhabited α] [Inhabited β] [Inhabited γ]

class HasInv (f : α → β) where
  has_inverse : ∃ g : β → α, (∀ x, f (g x) = x) ∧ (∀ x, g (f x) = x)

def inv (f : α → β) : β → α := sorry

@[simp]
theorem comp_inv (f : β → γ) (g : α → β) [HasInv f] [HasInv g]
  : inv (λ x => f (g x)) = λ y => inv g (inv f y) := sorry

instance (y : Int) : HasInv (λ x => y + x) := sorry
@[simp] theorem add_inv (y : Int) : inv (λ x => y + x) = λ x => x - y := sorry

set_option trace.Meta.Tactic.simp.discharge true in
example :
  let f := (λ x : Int => 1 + x)
  inv (λ x => f (f x))
  =
  λ x => inv f (inv f x)
  := by simp (config := { zeta := false})

[Tomas Skrivan]

Here is an idea how to deal with this problem by modifying the simplifier. However, I would like to know if anyone has a simpler idea before I get into this.

The root of this behavior is the line let bx := b.instantiate1 x which replaces the let free variable with brand new free variable with no value in it.

If I want to have zeta reduction off but allow discharger/typeclass system to see through the free variables introduced by let bindings, I probably have to modify the function synthesizeArgs and restore the original value for all the newly introduced free variables.