applying a function definition inside a proof

Stream: lean4

[Michael]

I want to complete a proof that for any function of three variables f : α × β × γ → δ, there is a function of a single variable f' : α → β → γ → δ that does the same thing, satisfying (((f' a) b) g) = f ⟨a,b,g⟩ for all a,b,g of types α, β, γ. This feels like it should be straightforward.

I can define the function I want, or I think I can:

let witness := fun a : α => fun b : β => fun g : γ => f ⟨a,b,g⟩

with that and some intros and an invocation of exists, lean tells me my goal is to prove that witness a b g = f (a, b, g). witness exists in the context like so:

witness: α → β → γ → δ := fun a b g => f (a, b, g)

Should I be able to use this in a rewrite somehow? What's going wrong? How do I apply the definition of witness?

[Eric Rodriguez]

Can you put in the full code that is failing for you?

[Eric Rodriguez]

(#mwe)

[Michael]

I'm working inside a MIL installation, so for total completeness I'll include the file header:

import Mathlib.Data.Set.Lattice
import Mathlib.Data.Nat.Prime
import Mathlib.Data.Nat.Parity
import MIL.Common

section
variable {α β γ δ: Type*}

example : ∀ f : α × β × γ → δ,
          ∃ g : α → β → γ → δ,
          ∀ x : α, ∀ y : β, ∀ z : γ,
          (((g x) y) z) = f ⟨x,y,z⟩ := by
  intro f
  let f_prime := fun x : α => (fun y : β => (fun z : γ => f ⟨x,y,z⟩))
  exists f_prime
  intro x y z
  -- where do I go from here?
  done
end

[Eric Rodriguez]

rfl will close it! it's true by definition. if you want to unfold the let you can use unfold_let(s) f_prime or simp only [f_prime]

[Michael]

Thanks!

I feel that rfl is doing some work behind the scenes there that I'd like to know how to do manually. Can I manipulate this into a state where it tells me my goal is f (x, y, z) = f (x, y, z)?

[Eric Rodriguez]

Do the unfold_let or simp calls I mentioned above work? This is a specific rule of equality called zeta-reduction.

[Michael]

1. simp only [f_prime] closes the goal, just like rfl
2. unfold_lets f_prime complains that unfold_lets is an unknown tactic
3. unfold_let f_prime sets the goal to (fun x y z => f (x, y, z)) x y z = f (x, y, z), which is a painfully obvious thing to have to prove, but hasn't quite gotten all the way to f (x, y, z) = f (x, y, z)

[Eric Rodriguez]

I'm surprised the first one closes the goal! simp clearly did not obey the only...

For the second two (sorry, I forgot whether there was an s on the tactic or not): what you then need to do is called eta-reduction. Again, there is a tactic for this somewhere if you want to have control about it, but in most real-life cases you'll use simp and it will eta reduce most things that you can. The correct tactic is eta_reduce in this case.

here are some tactics that do the same sorts of things

[Michael]

Thanks again!

[Ruben Van de Velde]

If you use set rather than let , you can have it create a hypothesis that you can rewrite with

[Yury G. Kudryashov]

Eric Rodriguez said:

I'm surprised the first one closes the goal! simp clearly did not obey the only...

Currently, simp unfolds local definitions unconditionally. See lean4#2682 for a discussion.