Loogle missing equations

Stream: new members

[Snir Broshi]

Loogle has entries which are equations for definitions:

@loogle eq_1

but I noticed a few are missing. For example, I can't find-

@loogle Sym2.eq_1
@loogle Sym2.fromRel.eq_1
@loogle SimpleGraph.ConnectedComponent.eq_1

even though I can find-

@loogle Magma.AssocQuotient.eq_1
@loogle AddMagma.FreeAddSemigroup.eq_1

What makes certain definitions appear and not others? (for example, maybe different universe levels?)

Can you point me towards a way to debug this, for example by pointing to the part of Loogle's code that extracts definitions from the current env, or a MWE of Lean code that extracts definitions from the current env and finds Magma.AssocQuotient.eq_1 but not Sym2.eq_1?

[Snir Broshi]

(deleted)

[Snir Broshi]

(deleted)

[Aaron Liu]

these equations are generated on first use

[Aaron Liu]

if loogle can't find it, that means it wasn't used (so it wasn't generated)

[Snir Broshi]

So using it as defeq doesn't count? e.g. when Quot.lift is applied to a Sym2 term it uses the equation of Sym2 to typecheck.

Mathlib's docs contain more equations than Loogle, is there a way to list unused equations like the docs do?

[Aaron Liu]

the unfolding equation is different from just unfolding

[Aaron Liu]

it's used when, for example, you rw [Sym2], that will use Sym2.eq_1

[Aaron Liu]

but when you're in a typechecking problem that's not using the unfolding equation

[Aaron Liu]

and sometimes this unfolding equation is a lot more complicated than Eq.refl _

[Aaron Liu]

and sometimes it can unexpectedly fail, so you get an error generating the equational lemma

[Snir Broshi]

So it's when "casting" a defeq into a term of Eq?

[Aaron Liu]

Snir Broshi said:

So it's when "casting" a defeq into a term of Eq?

not sure what you mean by this

[Aaron Liu]

can you provide some context

[Aaron Liu]

Snir Broshi said:

Mathlib's docs contain more equations than Loogle, is there a way to list unused equations like the docs do?

what docs does is it just generates all the equational lemmas in contrast to loogle which only looks at existing ones

[Snir Broshi]

Aaron Liu said:

Snir Broshi said:

So it's when "casting" a defeq into a term of Eq?

not sure what you mean by this

You said that the equation is generated when trying to rw [Sym2], so what I understood from that is that the name Sym2 refers to a definition and not a term of type Eq Type, and the rw tactic generates this eq_1 using rfl which uses the defeq of the definition.

[Aaron Liu]

well it's not rw that's doing the generating

[Aaron Liu]

rw triggers the generating but the generating is done by something else

[Snir Broshi]

do you know how the mathlib docs are able to get all the equations, even unused (maybe they trigger the generation)?

[Aaron Liu]

specifically, rw calls docs#Lean.Meta.getEqnsFor? which does all the logic to figure out if it needs to generate some lemmas

[Aaron Liu]

maybe docs does something similar?

[Aaron Liu]

found it https://github.com/leanprover/doc-gen4/blob/31cc380418e01263dad34aff8c7ae7980c14f427/DocGen4/Process/DefinitionInfo.lean#L30-L39

[Snir Broshi]

Nice! If I understand correctly, Loogle uses Batteries to get a list of all the theorems, specifically DeclCache.mk

[Snir Broshi]

so now the question becomes how to give both these pieces of code the PPAP treatment

[Snir Broshi]

#batteries > Generating equations in `DeclCache`