get R^n from mathlib

Stream: new members

[Mitchell Douglass]

Hello Lean-Prover Community,

I'm very new to Lean. I've completed Kevin Buzzard's Natural Number Game, and the tutorial project exercise files. I'm in the process of reading Theorem Proving in Lean.

As a hands-on learning exercise, I'd like to try formalizing some theorems from a textbook I have; it covers basic real analysis and linear algebra. I want to work at the same level of generality as the book, taking from mathlib anything that the book assumes.

I quickly run up against a roadblock. How does one import/construct a definition for R^n from mathlib?

(side note, are there any beginner resources doing similar formalizations that I might learn from?)

[Adam Topaz]

The standard approach is to use fin n \-> \R (sorry for the lack of unicode... I'm writing this on mobile). With the right imports (some sufficiently deep file from linear_algebra would suffice), this would obtain a structure of a vector space over the reals

[Arien Malec]

Following along b/c I have a similar goal -- would like to do linear algebra done right, and import only the minimum from mathlib -- if there's material for how get the minimums from mathlib without all the proofs that one wants to reconstruct.

[Adam Topaz]

Another useful thing to look at is mathlib's matrix notation, found here file#data/matrix/notation

[Mitchell Douglass]

Thanks @Adam Topaz for the response!

My understanding of fin n /to \R is a function type from fin n to \R, but I have not seen fin. Is it some kind of index type? Where can I learn more?

[Adam Topaz]

fin n is a type with n elements. So functions from fin n to R can be thought of as n-tuples of real numbers.

[Adam Topaz]

I think #tpil covers this?

[Adam Topaz]

Maybe not.

[Arien Malec]

I found https://leanprover-community.github.io/mathlib_docs/data/fin/vec_notation.html (sorry, no idea what magic embeds doc links)

[Kevin Buzzard]

That notation works for concrete numerals like elements of fin 4 -> \R.

[Kevin Buzzard]

Mathematicians would write the type fin n -> \R as $\mathrm{Hom}(\{0,1,\ldots,n-1\},\R).$

[Kevin Buzzard]

That's our "model" in mathlib for $\R^n.$

[Arien Malec]

As an observation, there's a trend where one tries to do undergraduate math using mathlib but one ends up doing category theory

[Kevin Buzzard]

The arrow is not the category theory arrow, it's the function arrow. So it's not category theory yet.

[Patrick Massot]

This has nothing to do with category theory! This is the usual definition of $\R^n$. People often lie to themselves and pretend $\R^n$ is an iterated product of individual copies of $\R$ but they don't mean it. An element of $\R^3$ doesn't look like $((x, y), z)$, it looks like $(x_0, x_1, x_2)$ which is exactly description of a map from $\{0, 1, 2\}$, aka fin 3, to $\R$.

[Kevin Buzzard]

I only wrote the Hom thing to explain another way of thinking about the function type.

[Arien Malec]

I was jokingly referring to the homomorphism.

But it's true, though. The documentation for linear algebra "basic" states that "This file defines the basics of linear algebra. It sets up the "categorical/lattice structure" of modules over a ring, submodules, and linear maps" and the underlying definition of a vector space is in terms of module where the documentation is "A module is a generalization of vector spaces to a scalar semiring. It consists of a scalar semiring R and an additive monoid of "vectors" M, connected by a "scalar multiplication" operation r • x : M (where r : R and x : M) with some natural associativity and distributivity axioms similar to those on a ring."

This isn't quite at the "a monad is a monoid in the category of endofunctors" level, but it's close.

A reasonably rigorous undergraduate linear algebra text like Axler starts with an "ordered list of length n" (which does conform to fin n) and the basic axioms of a vector space.

[Arien Malec]

I wonder whether it's better to discard all that and start with set and define closed addition and scalar multiplication?

[Adam Topaz]

Linear algebra is not linear algebra without linear maps. I suppose that's what the word "category" is referring to in the quote you mentioned.

[Johan Commelin]

Arien Malec said:

I wonder whether it's better to discard all that and start with set and define closed addition and scalar multiplication?

I predict this will be an immense pain.

[Arien Malec]

Johan Commelin said:

Arien Malec said:

I wonder whether it's better to discard all that and start with set and define closed addition and scalar multiplication?

I predict this will be an immense pain.

Probably. I guess I'm asking (from those who have taught or learned theorem proving in undergraduate math) what the the best way to use mathlab without pulling too much in, where the point is to re-derive and prove the same things that mathlib has already proved.

[Eric Wieser]

Arien Malec said:

I wonder whether it's better to discard all that and start with set and define closed addition and scalar multiplication?

Perhaps you already know this, but docs#submodule does exactly that

[Eric Wieser]

But sets aren't the building blocks of Lean, Types are; so you rarely start with sets, instead starting with Types and later specializing to sets.

[Arien Malec]

No, I didn't know that submodule automatizes linear spaces... Mm, so I could start with #mathlib documentation > submodule and then do my own proofs from there & pick up more of mathlib as I've already covered it?

I love @Kevin Buzzard's work on NNG (and I've now redone Complex NG in standard Lean3), and want to recreate that for reasonably undergraduately values of abstract linear algebra.

[Mitchell Douglass]

Reviving this topic ...

I have come across a hurdle in my quest to formalize some undergraduate math.

I am trying to define the standard basis vectors for R^n. Minimally, I have:

variables {n : nat}

def R (n: nat) : Type := fin n -> ℝ

def e (i : fin n) : R n :=
begin
  intro j,
  have H: i = j ∨ ¬i = j,
    from decidable.em (i=j),
  cases H with heq hneq,
  sorry
end

It's this final cases that gives an error: "induction tactic failed, recursor 'or.dcases_on' can only eliminate into Prop". As I understand it, the issue lies in fact of trying to construct a non-Prop value from a Prod inductive type (or). I believe the relevant text is found in 7.8 Axiomatic Details (TPL), where it states "Generally speaking, for an inductive type in Prop, the motive of the elimination rule is required to be in Prop." Please correct me if I'm mistaken.

I guess my question is, what's my alternative? How can I define the standard basis vectors as I've set up above?

[Andrew Yang]

In general it might not be a good idea to construct data in tactic mode.
In this case you can do refine if (h : i = j) then _ else _.

[Mitchell Douglass]

I see, thanks Andrew. Is your suggestion of refine if (h : i = j) then _ else _ for tactic mode or term mode?

[Andrew Yang]

That is in tactic mode. refine is a tactic.

[Andrew Yang]

To elaborate further, tactic modes are generally designed for proofs, so the terms they produce might not be easy to manipulate. The most basic tactics (intro, refine, apply, exact) might be fine, some might be okay if you know what you are doing (dsimp, change, cases, ...), but other tactics will probably give unreadable and unusable terms.

[Mitchell Douglass]

Thanks for the elaboration! Do you mind showing me how you would write this in term mode? Here is my try:

def e (i : fin n) : R n :=
  λ (j : fin n), or.rec_on (decidable.em (i=j)) 1 0

I get a new error ""eliminator" elaborator failed to compute the motive", but I suspect it's the same issue.

Can you explain for me how we are getting around this issue of recursing on "or" (inductively defined Prop) and producing data (a real number) ?

[Mitchell Douglass]

Btw, I am trying not to use classical until I need to

[Andrew Yang]

if i = j then 1 else 0. I believe this doesn't use classical but I might be wrong.

[Mitchell Douglass]

Aha! I found 10.4 Decidable Propositions (TPL) which talks exactly about this if-then-else requiring decidable props. Wonderful!

[Eric Wieser]

You might also want docs#pi.single

[King Crawford]

Try by_cases i = j, as an alternative to have H: i = j ∨ ¬i = j, from decidable.em (i=j).