Adding more examples to mathlib

Stream: mathlib4

[metakuntyyy]

I was wondering if it were possible to add more examples or documentation to mathlib. As someone who browses the library I feel that I am missing examples of how to use the theorems or just in general how to apply stuff.

In a different project I am trying to formalise finite fields or algebraic closures, but I am struggling hard to understand how to read the theorems. I was stumbling upon https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/MvPolynomial/Basic.html#MvPolynomial during my research and I would like to add some examples.

For example the polynomial
$f: (x,y) \mapsto 2x\cdot y + y +1$
I would like to show that f(2,2) = 11 in mathlib, so that future users have an idea how to use the api provided by mathlib.

Can someone guide me in adding examples and improving documentation? That would be nice, not only for me, but for future boneheads like myself.

[metakuntyyy]

I tried it a bit with chatgpt's help and this is the best I could come up with

import Mathlib

open MvPolynomial

noncomputable def my_poly : MvPolynomial Nat Nat :=
  2 * (MvPolynomial.X 0 * MvPolynomial.X 1) + MvPolynomial.X 1 + 1



-- Prove that the polynomial evaluated at x = 2 and y = 2 is 11
theorem example_eval :  MvPolynomial.eval_eval₂ my_poly 2 2 = 11 := by
  have h1 :  2 2 = 2 * (2 * 2) + 2 + 1, by simp [eval_poly, mv_polynomial.eval],

[Kim Morrison]

It would be lovely to have a term elaborator so we could just write MvPolynomial.of% fun x y => 2 * (x + y) + y + 1, which would automatically produce an MvPolynomial (Fin 2) Nat (and would be clever about inferring the coefficient type).

[Kim Morrison]

Your theorem statement seems garbled?

[metakuntyyy]

Yeah, sorry, that's as far as I could construct it with chatgpt. I think it used lean3 and mathlib3.
Basically my goal is to add a very simple example to mathlib so that newer users like myself know how to construct a polynomial and prove basic properties.

So far it is not obvious at all, and I think I'd like to fill it with documentation and api's so that it is easy to use by reading the documentation. As the documentation is very hard to read since it is maximally generic, I struggle to construct those types.

[Kim Morrison]

import Mathlib.Algebra.MvPolynomial.Basic

open MvPolynomial

noncomputable def my_poly : MvPolynomial Nat Nat :=
  2 * (MvPolynomial.X 0 * MvPolynomial.X 1) + MvPolynomial.X 1 + 1

-- Prove that the polynomial evaluated at x = 2 and y = 2 is 11
example : my_poly.eval (fun _ => 2) = 11 := by
  simp [my_poly] -- hmm, doesn't work, there's a missing library lemma
  sorry

variable {σ R : Type*} [CommSemiring R]
@[simp] theorem eval_ofNat (f : σ → R) (n : Nat) [n.AtLeastTwo] :
    (no_index (OfNat.ofNat n) : MvPolynomial σ R).eval f = n := by
  rw [map_ofNat]; rfl

example : my_poly.eval (fun _ => 2) = 11 := by
  simp [my_poly] -- :tada:

[Kim Morrison]

Yes, more documentation would be great, and is very welcome.

(There's unfortunately a bit of a chicken and egg problem, that one has to learn how to use a part of the library before it is possible to write good documentation for it!)

[Kim Morrison]

I added this missing lemma in #19356

[Kim Morrison]

How would people feel about adding an example like:

## Examples

We could construct the polynomial `y^2 - x^3 + x - 37` as an `MvPolynomial (Fin 2) ℤ` as follows:
```
import Mathlib.Algebra.MvPolynomial.CommRing

open MvPolynomial

def f : MvPolynomial (Fin 2) ℤ := (X 1)^2 - (X 0)^3 + X 0 - C 37
```
To evaluate it at `x = y = 2`, we could write:
```
example : f.eval (fun _ => 2) = -39 := by simp [f]
```

to a module-doc?

[Kevin Buzzard]

That's a particularly fine choice of elliptic curve I must say

[metakuntyyy]

Glad I could help.

A weird thing is I looked at the PR of yours:

@[simp] theorem eval₂_ofNat (n : Nat) [n.AtLeastTwo] :
    (no_index (OfNat.ofNat n) : MvPolynomial σ R).eval₂ f g = n :=
  (eval₂_C _ _ _).trans (map_natCast f n)

and I don't understand a single thing. Like what does this do is beyond me?

You sure had a good way to learn how to do this but for me I can't even comprehend what's happening.

If I check the docs https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/MvPolynomial/Basic.html#MvPolynomial.eval%E2%82%82_C I see nothing, I assume this does some constant evaluation but I can't really understand it since there is no documentation.

Here I get some docs https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/MvPolynomial/Basic.html#MvPolynomial.eval%E2%82%82 but it's still insufficient to explain what's happening.

Few questions pop up to my mind immediately, Why do I need both $S_1$ and R, are those scalar coefficients and coefficient in the "range". What is $\sigma$, is this an index set? It says g is a map from $\sigma$ to $S_1$, so I assume in

example : f.eval (fun _ => 2) = -39 := by simp [f]

your example g is (fun _ =>2) which is the pair (2,2), how do I get the pair (1,2) I assume pattern matching, something like that
(fun _ => |
1 -> 1,
2 ->2 )

[Ruben Van de Velde]

For the sigma, I'll quote the docs:

Let R be a commutative ring (or a semiring) and let σ be an arbitrary type. This file creates the type MvPolynomial σ R, which mathematicians might denote . It is the type of multivariate (a.k.a. multivariable) polynomials, with variables corresponding to the terms in σ, and coefficients in R.

[Ruben Van de Velde]

And

eval₂ (f : R → S₁) (g : σ → S₁) p : given a semiring homomorphism from R to another semiring S₁, and a map σ → S₁, evaluates p at this valuation, returning a term of type S₁.

[Ruben Van de Velde]

OfNat.ofNat n is how lean works with numeric literals; (3 : MvPolynomial σ R) is interpreted as ((OfNat.ofNat (3 : Nat)) : MvPolynomial σ R)

[Ruben Van de Velde]

So what this says is that if you apply eval₂ to a MvPolynomial that's just a numeric literal, you just get the number itself, but now interpreted as a term of type S₁

[Ruben Van de Velde]

@metakuntyyy Does that help put some of the pieces together?

[Vincent Beffara]

How does such code in a module doc appear in the webpage generated by docgen? Is there fancy access to the proof state and the like, or is it plain html?

One thing that might make sense is a parallel tree, next to Mathlib and MathlibTest and Counterexamples, for examples? With the same structure as the Mathlib tree, and examples for the definitions of Mathlib/Foo/Bar.lean in MathlibExamples/Foo/Bar.lean so that they can be opened in vscode and inspected. But that would likely be a huge maintenance burden...

[Patrick Massot]

@metakuntyyy did you try reading #mil instead of hoping ChatGPT will do everything?

[metakuntyyy]

@Patrick Massot Yeah, I went through all the tutorials/games I could find. I've played the natural numbers game, looked at youtube videos such as there is an infinite number of primes and read all the docs I could find. However that still sadly leaves a gap actually trying to prove things I'd like.

For context I am trying to formalise the AKS primality lemma in metamath. I have made substantial progress in showing that the following statement. Let $n\geq 3$ be a natural number, then there exists a natural number p with

$$p \leq \lceil \log_2^5 n \rceil \textit{~and~} \log_2^2 n < ord_r(n)$$

The metamath proof is found here https://us.metamath.org/mpeuni/aks4d1.html the written proofs by authors I want to formalise/follow are https://www3.nd.edu/~andyp/notes/AKS.pdf and https://www.cse.iitk.ac.in/users/manindra/algebra/primality_v6.pdf.
A somewhat incomplete blueprint is found here https://tirix.github.io/metamath-blueprints/AKS%20(PRIMES%20is%20in%20P)/

Essentially the proof reduces from calculations in $(\mathbb{Z}/n)[X]/(X^r-1)$ to the algebraic closure of $\mathbb{F}_p$ by mapping X to one of the primitive roots $\mu$ of $X^r-1$

The hypothesis now is that for $1\leq a \leq \lfloor \theta(r)\log_2 n\rfloor$ we have

$$(\mu+a)^n=\mu^n+a$$

where a is here interpreted as the element of the canonical isomorphism from $\mathbb{Z}$ to the algebraic closure of $\mathbb{F}_p$
My goals are in multiple steps: First I want to understand the glue that connects the higher level statement to the mathematical primitives, while I understand the theorem that I want to formalise in a higher sense I am still struggling in understanding which of the primitive lemmas I need to formalise to actually connect the theorem to its mathematical axioms. Therefore I want to develop the theory of finite fields in metamath such that I can finish the proof there, while I am unsure which theorems I actually need to formalise. Then I want to redo the proof once more in lean. In the meantime I'm trying to understand what statements I actually need to formalise.

Basically I want to understand this definition

def AlgebraicClosure : Type u :=
  MvPolynomial (AlgebraicClosureAux k) k ⧸
    RingHom.ker (MvPolynomial.aeval (R := k) id).toRingHom

so that I know what api I need to develop in metamath. I assume there will be a plethora of theorem regarding finite fields and its closure that I will need in one way or another.

I am afraid that I am missing certain idiomacies that lean is capable of doing, such as dipping into layered definitions.

I guess a more concrete example would be to just define the hypothesis of theorem 6.1, a second would be to construct the primitive root $\mu$ and show that $\mu^r=1$ and for any $0<s<r, \mu^s\neq 1$, all in the algebraic closure of $\mathbb{F}_p$, in the meantime while I am in the process of understanding definitions I want to improve the docs of mathlib with more clarifying examples such that other people like myself have hopefully a better time understanding what is going on.

@Ruben Van de Velde Thanks for your comment, it helped me a lot. Would you say that Fin n is a "canonical" choice for $\sigma$ in a sense that if I want $R[X,Y,Z]$ instead I can use something of the type MvPolynomial (Fin 3)

[Ruben Van de Velde]

Yes, I think so (though I haven't really done anything in this area)