Meta-functions: meta programming for everyone

Stream: lean4

[Tomas Skrivan]

I have developed a mechanism to write "functions" that depend on the syntactic structure of their arguments. I'm curious if others would find this useful and what additional applications could be explored.

Here are a few examples:

1. Finding Concrete Bounds for a Function

-- 224
#eval getNaiveBoundOn (fun x : ℤ => (x + 3)*(x - 4)*x) (Icc (-3) 4)

This "function" computes the following:
|(x + 3)*(x - 4)*x| ≤ |x + 3|*|x - 4|*|x| ≤ (4 + 3)*(4 + 4)*4 = 224.

2. Left-Associating Elements of a Product

-- (1, 2, 3)
#eval (lassoc ((1, 2), (), 3))

3. Lifting Elements of a Ring

-- "((#0 * #1) + ((#0 * #0) * #1))"
#eval ringToString [a, b] (a * b + a * a * b)

This is useful as the first step in writing other tactics like ring, module, or polyrith, where you need to transform an element (e.g., from a ring) into a form that other tactics can process.

4. Computing Derivatives

-- (1 * x + x * 1) * x + x * x * 1 + (0 * x + 3 * 1) + (1 * x + x * 1)
#eval_meta_fun derivAt (fun x => x * x * x + 3 * x + x * x) x

---

All these functions evaluate so-called meta-functions during elaboration. For example, getNaiveBoundOn is defined as follows:

def getNaiveBoundOn (f : ℤ → ℤ) (s : Set ℤ) {n} (h : NaiveBoundOn f s n := by data_synth) := n

Here, NaiveBoundOn is the meta-function, and data_synth is the new tactic that solves goals like NaiveBoundOn f s ?n, i.e., it finds n and demonstrates that it bounds f on s. All this is motivated by solving HasFDerivAt f ?f' x as I want to compute derivatives.

I’ve created two new commands, meta_fun_decl and meta_fun_def, to help define these new meta-functions:

meta_fun_decl naiveBoundOn (f : ℤ → ℤ) (s : Set ℤ) : ℤ
satisfying
  (∀ x ∈ s, |f x| ≤ naiveBoundOn)

This declares a "function" NaiveBoundOn : (ℤ → ℤ) → Set ℤ → ℤ → Prop. In reality, NaiveBoundOn f s n is just a Prop structure with a single field ∀ x ∈ s, |f x| ≤ n.

With meta_fun_def, you can define its "values":

meta_fun_def naiveBoundOnIdentity (a b : ℤ) :
  naiveBoundOn (fun x => x) (Icc a b) := max |a| |b|
satisfied_by
  ...

This can be recursively "called":

meta_fun_def naiveBoundOnAdd (f g : ℤ → ℤ) (a b : ℤ) :
  naiveBoundOn (fun x => f x + g x) (Icc a b) :=
    let bf := naiveBoundOn f (Icc a b)
    let bg := naiveBoundOn g (Icc a b)
    bf + bg
satisfied_by
  ...

This definition translates to the theorem:

@[data_synth]
theorem naiveBoundOnAdd (f g : ℤ → ℤ) (a b : ℤ) (bf : ℤ) (hf : NaiveBoundOn f (Icc a b)) (bg : ℤ) (hg : NaiveBoundOn g (Icc a b)) : NaiveBoundOn (f + g) (Icc a b) (bf + bg) := ...

Whether you prefer writing theorems like this or using the meta_fun_def macro is a matter of taste.

Another Example: Left Associating Product Types

This meta-function returns a type along with an equivalence:

meta_fun_decl prodAssoc (X : Type) : Type
satisfying
  X ≃ prodAssoc

When reassociating ((X × Y) × Z), we call prodAssoc on itself:

meta_fun_def (priority := high-1) prodReassocMain (X Y Z : Type) :
  prodAssoc ((X × Y) × Z) := prodAssoc ((prodAssoc X) × Y × Z)
satisfied_by
  intro X' f XYZ' g
  constructor
  exact (Equiv.prodAssoc X Y Z
    |>.trans (Equiv.prodCongr f.1 (Equiv.refl _))
    |>.trans g.1)

Traditionally, this kind of function is implemented using a typeclass and a collection of instances. Similarly to instances, we can control which "evaluation" rule is applied using priorities.

You can find more details on how other meta-functions are defined in this file.

---

Naming Help: I currently use the term meta-function and the tactic data_synth, but neither term is perfect. I could rename the tactic to meta_fun_eval, but "meta-function" already refers to a function that operates on Lean.Expr. Suggestions are welcome.

[Aaron Liu]

I don't see how this is any different from writing meta-functions that act on Lean.Expr.

[Tomas Skrivan]

The point is user extensibility, imagine changing simp's code each time you add a new theorem.

[Aaron Liu]

I feel like that can be done the same way simp did it - with attributes. No need for a type class and fake function that don't respect equality.

[Patrick Massot]

Anything that makes it easier to build such tactics seem very useful to me.

[Patrick Massot]

Side-note: the tests in that file again tell us we should really fix that max delaboration issue…

[Tomas Skrivan]

Aaron Liu said:

I feel like that can be done the same way simp did it - with attributes. No need for a type class and fake function that don't respect equality.

The whole thing is based on the tactic data_synth I wrote. You can directly write theorems like:

@[data_synth]
theorem naiveBoundOnAdd (f g : ℤ → ℤ) (a b : ℤ) (bf : ℤ) (hf : NaiveBoundOn f (Icc a b)) (bg : ℤ) (hg : NaiveBoundOn g (Icc a b)) : NaiveBoundOn (f + g) (Icc a b) (bf + bg) := ...

In a way, these theorems are defining a function on Lean.Expr so the meta_fun_decl and meta_fun_defmake it more explicit and a lot easier to use for people not familiar writing meta level code.

[Tomas Skrivan]

Patrick Massot said:

Side-note: the tests in that file again tell us we should really fix that max delaboration issue…

Huh? What are you talking about? I'm not aware of this.

[Mario Carneiro]

max is being printed as \sqcup in the tests

[Kyle Miller]

This is really creative and neat! It's not every day that you see a new (meta)programming idiom

[Mario Carneiro]

Tomas Skrivan said:

Naming Help: I currently use the term meta-function and the tactic data_synth, but neither term is perfect. I could rename the tactic to meta_fun_eval, but "meta-function" already refers to a function that operates on Lean.Expr. Suggestions are welcome.

I think I would call this a (bounded) nondeterministic function instead of a meta-function

[Tomas Skrivan]

Yeah that would be more technically correct but is a bit of a mouthful.

[Aaron Liu]

Tomas Skrivan said:

Aaron Liu said:

I feel like that can be done the same way simp did it - with attributes. No need for a type class and fake function that don't respect equality.

The whole thing is based on the tactic data_synth I wrote. You can directly write theorems like:

@[data_synth]
theorem naiveBoundOnAdd (f g : ℤ → ℤ) (a b : ℤ) (bf : ℤ) (hf : NaiveBoundOn f (Icc a b)) (bg : ℤ) (hg : NaiveBoundOn g (Icc a b)) : NaiveBoundOn (f + g) (Icc a b) (bf + bg) := ...

In a way, these theorems are defining a function on Lean.Expr so the meta_fun_decl and meta_fun_defmake it more explicit and a lot easier to use for people not familiar writing meta level code.

I'm still against getNativeBoundOn and ringToString, because this goes against my model of how typeclasses are meant to be used.

[Asei Inoue]

very nice!!!

[Eric Wieser]

Kyle Miller said:

It's not every day that you see a new (meta)programming idiom

Isn't the "abuse a default argument to fill a metavariable" an old idiom? It's how we wrote reassoc_of and the matrix "simprocs" in Lean 3.