Using definitions without specifying ambient variables

Stream: lean4

[Terence Tao]

Consider the following code:

import Mathlib

variable (a b : ℝ)

def c:ℝ := a+b

example : (c a b)*(c a b) = a*a + 2*a*b + b*b := by
  unfold c
  ring

Here I have introduced some ambient variables a, b, and defined a new quantity c in terms of these ambient variables. However, as the example shows, if I want to actually use this new quantity, I have to specify the implicit input variables used to define c. Is there a way to avoid doing this and just refer to a defined quantity like c without specifying inputs? Changing variable (a b : ℝ) to variable {a b : ℝ} doesn't work because Lean cannot fill in the holes when working with c.

In my actual application I have many more variables:

open MeasureTheory ProbabilityTheory

variable {G : Type*} [AddCommGroup G] [Fintype G] [hG : MeasurableSpace G] [ElementaryAddCommGroup G 2]
variable {Ω₀₁ Ω₀₂ : Type*} [MeasurableSpace Ω₀₁] [MeasurableSpace Ω₀₂]
variable (p : ref_package Ω₀₁ Ω₀₂ G)
variable {Ω : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω}
variable (X₁ X₂ X₁' X₂' : Ω → G)
variable (h₁ : IdentDistrib X₁ X₁' μ μ) (h2 : IdentDistrib X₂ X₂' μ μ)
variable (h_indep : iIndepFun ![hG, hG, hG, hG] ![X₁, X₂, X₁', X₂'] μ)
variable (h_min: tau_minimizes p (μ.map X₁) (μ.map X₂))

noncomputable def k : ℝ := d[ X₁; μ # X₂; μ ]
noncomputable def I₁ : ℝ := I[ X₁ + X₂ : X₁' + X₂ | X₁ + X₂ + X₁' + X₂' ; μ ]

lemma first_estimate : I₁ ≤ 2 * η * k := by sorry -- doesn't work because one needs to specify inputs to k, I₁

but as it stands I cannot actually use the defined quantities kand I₁ without explicitly specifying a lot of the input variables, which would clutter up the arguments enormously.

[Kyle Miller]

There's a trick mathlib uses, which is to define a local notation

import Mathlib.Tactic.Ring

section
variable (a b : ℤ)

local notation3 "c" => a + b

example : c * c = a*a + 2*a*b + b*b := by
  ring

end

(I'm using mathlib's notation3 here instead of core Lean's notation because there seems to be a small bug in Lean itself that I'll look into. In any case, notation3 is able to pretty print a + b as c, but notation wouldn't have.)

[Terence Tao]

That works, thanks!

[Pedro Sánchez Terraf]

Hi, I have a similar situation as the above. My declared variables are actually global hypothesis (that are to appear in the main theorem afterwards).

The problem is that I have several lemmas and function definitions (each having other arguments), and my goal is the same as above: Not needing to insert those hypothesis as arguments every time.

Trying to reuse Terence's MWE, I would like to have a more complex c that takes arguments:

import Mathlib

variable (a b : ℝ)

def c (x : ℝ) : ℝ := a + b + x

/-
type mismatch
  0
has type
  ℝ : Type
but is expected to have type
  ℝ → ℝ → ℝ : Type
-/
example : c 0 = (0 : ℝ) := sorry

I could not make notation nor notation3 with the new argument x.

[Richard Copley]

import Mathlib
variable (a b : ℝ)
def c (x : ℝ) : ℝ := a + b + x
local notation3 "c'" => c a b
example : c' 0 = (0 : ℝ) := sorry

or [edit: fixed, sorry]

import Mathlib
variable (a b : ℝ)
local notation3 "c" => fun x => a + b + x
example : c 0 = (0 : ℝ) := sorry

[Pedro Sánchez Terraf]

Thanks! It seems my mistake was trying to add the type signature to the notation3 declaration :man_facepalming: