Equational Lemmas

Stream: lean4

[Marcus Rossel]

What are the equational lemmas called that are generated for definitions?
In this thread there are examples like @<name>._eq_1, @<name>._eq_2 and @<name>._unfold. When I try this in my project (nightly 2022-09-06) they don't exist though.

[Leonardo de Moura]

In Lean 4, the lemmas are not eagerly generated like in Lean 3.

def fact (n : Nat) :=
  match n with
  | 0 => 1
  | n+1 => (n+1) * fact n

#check fact._eq_1 -- Error

theorem ex : fact 0 = 1 := by
  simp [fact] -- `simp` generates the lemmas here

#check fact._eq_1
#check fact._eq_2

You can also use the API Lean.Meta.getEqnsFor?

import Lean

def fact (n : Nat) :=
  match n with
  | 0 => 1
  | n+1 => (n+1) * fact n

#check fact._eq_1 -- Error

#eval Lean.Meta.getEqnsFor? ``fact  -- generates the lemmas

#check fact._eq_1
#check fact._eq_2

[Mario Carneiro]

How about an attribute to request eager equation generation? @[simp] presumably implies it anyway

[Leonardo de Moura]

Yes, @[simp] def ... also forces the lemmas to be eagerly generated.

[Mario Carneiro]

in fact for mathlib I would probably want to disable lazy equation generation and use that to find missing occurrences of the equation generation attribute. It's a bit of boilerplate though, since we will basically want this on every def. Maybe a set_option?

[Mario Carneiro]

What are the cases where we definitely don't want equations?

[Leonardo de Moura]

Mario Carneiro said:

in fact for mathlib I would probably want to disable lazy equation generation and use that to find missing occurrences of the equation generation attribute. It's a bit of boilerplate though, since we will basically want this on every def. Maybe a set_option?

Yes, we can add an option.

[Leonardo de Moura]

Mario Carneiro said:

What are the cases where we definitely don't want equations?

If you one is using Lean as a programming language, then eager lemma generation is just increasing the compilation time.

[Mario Carneiro]

I guess an option does have the right semantics here: we want to be able to set it globally (to set the "nature" of the project for proving vs programming) and with overrides in certain files (like tactics in mathlib or Init.List.Basic in lean), and users can add a short notation for the single def case if desired. Defaulting to false seems like a good idea since it still basically works even without eager generation, and folks that don't prove anything don't need to pay for it

[Leonardo de Moura]

@Mario Carneiro Here is a relevant feature: https://github.com/leanprover/lean4/issues/14

[Lev Stambler]

Leonardo de Moura said:

In Lean 4, the lemmas are not eagerly generated like in Lean 3.

def fact (n : Nat) :=
  match n with
  | 0 => 1
  | n+1 => (n+1) * fact n

#check fact._eq_1 -- Error

theorem ex : fact 0 = 1 := by
  simp [fact] -- `simp` generates the lemmas here

#check fact._eq_1
#check fact._eq_2

You can also use the API Lean.Meta.getEqnsFor?

import Lean

def fact (n : Nat) :=
  match n with
  | 0 => 1
  | n+1 => (n+1) * fact n

#check fact._eq_1 -- Error

#eval Lean.Meta.getEqnsFor? ``fact  -- generates the lemmas

#check fact._eq_1
#check fact._eq_2

Is there any way to get these equations (like _eq_1) to not be private?

[Lev Stambler]

Lev Stambler said:

Leonardo de Moura said:

In Lean 4, the lemmas are not eagerly generated like in Lean 3.

def fact (n : Nat) :=
  match n with
  | 0 => 1
  | n+1 => (n+1) * fact n

#check fact._eq_1 -- Error

theorem ex : fact 0 = 1 := by
  simp [fact] -- `simp` generates the lemmas here

#check fact._eq_1
#check fact._eq_2

You can also use the API Lean.Meta.getEqnsFor?

import Lean

def fact (n : Nat) :=
  match n with
  | 0 => 1
  | n+1 => (n+1) * fact n

#check fact._eq_1 -- Error

#eval Lean.Meta.getEqnsFor? ``fact  -- generates the lemmas

#check fact._eq_1
#check fact._eq_2

Is there any way to get these equations (like _eq_1) to not be private?

Right now I am trying to access something like fact._eq_1 in after creating it a few lines above within one function.

[James Gallicchio]

private functions should be accessible within the file, and I think you can do open private or something to access private names in other files

[Alex Keizer]

On a related note, if I wanted to customize how simp [Foo] behaves for a spefic kind of definition, then could I do that with registerGetEqnsFn?

[Eric Wieser]

Mathlib4 has an eqns attribute for this (docs4#eqnsAttribute )

[Alex Keizer]

Cool! Do things break if I give an equation lemma which only holds propositionally, not definitionally? I would imagine it does, right?

[Eric Wieser]

I doubt it, many equation lemmas don't hold definitionally

[Eric Wieser]

(especially when using termination_by, IIRC)

[Alex Keizer]

Allright, thanks for the info!