greetings & where to start?

Stream: new members

[Vasily Nesterov]

Hi everyone! I am a third year student in Math & CS and I really enjoy playing with Lean.

Maybe I can bring some benefit to the community? I have seen the page https://leanprover-community.github.io/undergrad_todo.html about undergraduate topics still uncovered in mathlib, and I want to work on some of them. I have checked the PR list and, for example, the following topics do not seem to be done:

1. Matrices: Jordan normal form
2. Fourier analysis: Dirichlet theorem, Fejer theorem, Plancherel’s theorem.
3. ODE: exit theorem of a compact subspace, stability of equilibrium points (linearisation theorem), linear differential systems, etc

I just want to become more familiar with mathlib and lean and would be happy to pick any of them. I will be grateful if someone would outline the situation in these subjects and give advice on how and where to start.

[Kevin Buzzard]

The undergrad_todo is a place where new members sometimes go to die :-( There is often a reason these things are not yet done, perhaps the community demands that they're done in a specific way and an expert is needed :-/

[Patrick Massot]

Don't listen to Kevin, there are many things that are still doable on this list. Many items are not done because they are boring elementary mathematics.

[Moritz Doll]

There is also a tag on the issue tracker on github for good beginner projects: https://github.com/leanprover-community/mathlib/issues?q=is%3Aissue+is%3Aopen+sort%3Aupdated-desc+label%3Agood-first-project

[Moritz Doll]

From undergrad_todo, the special orthogonal/unitary groups should be rather easy and there are examples of matrix groups that you could follows. Looking at docs#matrix.special_linear_group and docs#matrix.orthogonal_group should suffice to implement matrix.special_orthogonal_group

[Moritz Doll]

btw: why is the special linear group still on the list? there is docs#matrix.special_linear_group

[Moritz Doll]

@Fourier Series: There was the idea to rewrite the Fourier series, but I don't know what became out of that. If you are interested in working on that you should ping Heather Macbeth and you might have to do some refactoring of existing code. So it might take a some time to get to the interesting parts, but if you really want to learn Lean, then it can be worthwhile.

[Yaël Dillies]

Moritz Doll said:

btw: why is the special linear group still on the list? there is docs#matrix.special_linear_group

Probably same answer as here, unless you have more to say, @Heather Macbeth?

[Kevin Buzzard]

I think that the truth is that there might be some items on there which are accessible (as well as some items which are not at all accessible to beginners but which look accessible, which is very disheartening) but there problem is that the more detailed descriptions of what needs doing and how the mathlib community want it done are often described in threads like this which are transient and get lost. My main point is that it's not like 2-3 years ago where people could just say "oh you don't have X, here I can do X" and then they do X and get it merged. It's now much more complicated which is why the list has stagnated.

[Kevin Buzzard]

Newcomers stumble onto the list but not the details of what we know needs actually doing.

[Kevin Buzzard]

There's an undergraduate at Imperial who has essentially done partial factions by the way. Should I record this somewhere as WIP?

[Moritz Doll]

In my opinion the github issue tracker is way better for maintaining a list of "beginner issues". The problem with the undergrad list is as you say that "mathematically easy" != "Lean easy".

[Moritz Doll]

As for the partial fractions: if the student is ok with it, then you could create a WIP PR and tag it with "please-adopt"

[Henrik Böving]

Patrick Massot said:

Don't listen to Kevin, there are many things that are still doable on this list. Many items are not done because they are boring elementary mathematics.

I barely even know the terms on the list /o\

[Vasily Nesterov]

Thank you for answers! OK, I will try to complete the matrix group examples for now.

[Heinrich Apfelmus]

Hello! :wave: I'm Heinrich and I'm new to Lean. I have a background in mathematics and functional programming (Haskell).

I have a question. Is this a good channel to ask this? If not, where would be more appropriate?

Background: I'm interested in proving statements about functional programs (written in Haskell); think Bird-style proofs. I have had success proving that reverse (reverse xs) = xs for any xs : list α in Lean and now I would like to step up my game by proving statements about abstract data types. In Haskell, we typically build new abstract data types by combining old ones.

Question: I'm constructing an abstract data type, let's call it Foo, by using an abstract data type called Set α (where α : Type) which represents a set of values of type α. I expect that Set will be implemented as an inductive type in terms of binary search trees, with some equivalence relation == representing equality of Set. (I don't understand the distinction between computational and noncomputational well enough to force this to =, I'm happy to live with an equivalence relation on inductive terms.) However, I don't really care how Set is implemented — all I care about are some functions that operate on it and some lemmas about how these functions behave (e.g. a complete axiomatization). In other words, when defining my inductive type Foo, I would like to use the Set α type and functions that operate on it, but I don't want to import an actual implementation — all I care about is a structure that holds a collection of operations and theorems about them, i.e. a "module interface" in programming language speak. How would I go about declaring and using such a module interface (without implementing it)? Should I use type classes?

I have tried constant, but then I run into "noncomputational" issues. I have tried declaring a lot of variable, but that does not give me enough control about their namespace — I would like to write Set.insert x (Set.empty) where e.g. empty : Set α is part of the module interface.

Put differently, I'm writing the abstract data type Foo as follows: "Assume that I have a data type Set α with some lemmas. Then, I define Foo as follows … . Now, from the lemmas about Set, I can prove the following lemmas about Foo: … ". I'm looking for a syntactically nice way of specifying "Assume that I have a data typeSet α".

[Johan Commelin]

Welcome! This is certainly the right place to ask your first questions.

[Johan Commelin]

I think that you are looking for structure.

[Heinrich Apfelmus]

Johan Commelin said:

I think that you are looking for structure.

Maybe. :thinking: Ok, so when I extract the Set interface into a structure, I get the following, which does not work:

structure SetAPI :=
  (Set : Type -> Type)
  (empty : ∀{α}, Set α)
  (insert : ∀{α}, α -> Set α -> Set α)
  (member : ∀{α}, α -> Set α -> bool)
  (prop_insert_member : ∀{α} (x : α) (s : Set α),
    member x (insert x s) = tt
  )
  (prop_insert_comm : ∀{α} (x:α) (y:α) (s : Set α),
    insert x (insert y s) = insert y (insert x s)
  )

variable Set : SetAPI

structure Foo :=
   (bar : Set.Set nat)
   (baz : Set.Set nat)

#check Foo
-- Foo : SetAPI → Type

def insertBar (x : nat) (foo : Foo) : Foo :=
  Foo.mk (Set.insert x (foo.bar)) (foo.baz)

Here SetAPI is a structure that represents the API of the module that I want to import. I define a variable Set in order to "import" it into my namespace. However, this does not quite work as I want it, as Foo gets the type Foo : SetAPI -> Type rather than the type Foo : Type. I understand that this is ultimately correct (the type Foo needs to be supplied with an actual implementation in order to make sense; Foo behaves like a "module functor" in the ML programming language), but for the sake of my own sanity, I would like to have Set : SetAPI as an implicit hypothesis of my entire source file rather than an explicit argument. :thinking: Is there a way to do this?

[Johan Commelin]

You can use parameter Set : SetAPI. This is a feature that isn't used so much in the Lean community. But it should do what you want.

[Johan Commelin]

It doesn't do exactly the same as in ML modules, but within one file, the behaviour is roughly the same.

[Heinrich Apfelmus]

Awesome, thank you! :heart_eyes: Using parameter for assuming a module API works for me at this stage. (I can imagine this becoming unwieldy in larger projects, but I can ask more questions if I get to that point. :grinning: )

[Rida Hamadani]

Hi. I think I am starting to understand theorem proving, so I have decided to do my differential calculus homework using lean, and was surprised by how confusing writing a theorem can be. I found an abundance of online guides for theorem proving, but I wasn't able to find a guide on theorem writing. Advice is appreciated, where to start with theorem writing?

[Riccardo Brasca]

What is the theorem are you trying to formalize? One problem can be that mathematics in mathlib is probably written in a very general form and you can be confused by this, especially if you are a student and don't know the general formulation used in mathlib.

[Rida Hamadani]

As a start, I am trying to prove the following statement:
Given a, b ∈ ℝ, E, F normed vector spaces, T ∈ L(E, F), and f: (a,b) → E differentiable at t, then g = T ∘ f is differentiable at t with g'(t)=T∘ f'(t).

[Rida Hamadani]

Here is my code so far:

import analysis.calculus.fderiv
import analysis.normed_space.continuous_linear_map
import linear_algebra.basic

variables {E F : Type*} [normed_add_comm_group E] [normed_space ℝ E]
[normed_add_comm_group F] [normed_space ℝ F] {T : E → F}
{a b : ℝ} {t₀ : set.Ioo a b} {f : set.Ioo a b → E}

def g : set.Ioo a b → F := T ∘ f

Attempting to add a [differentiable_at f t₀] after defining f leads to a type mismatch error, is that because its domain is (a, b) ?
Also, I am confused on whether to add given in variables/def fields, or as hypotheses in the lemma .

[Riccardo Brasca]

docs#differentiable_at wants 𝕜 as is first variable, not f.

[Riccardo Brasca]

But in any case it is not going to work since it is for f : E → F where E is a normed_space 𝕜 E, and set.Ioo a b is not.

[Riccardo Brasca]

I suggest to start with f : ℝ → E. If in some application you have a function that is only defined on an interval you can always extend it by 0.

[Riccardo Brasca]

But there may be better ways, I am not very familiar with this part of the library.

[Riccardo Brasca]

Also, differentiable_at is not a class, so you shouldn't use square brackets. Instead you can write (h : differentiable_at...).

[Rida Hamadani]

I see, in that case, I will try to write a differentiable_at that is compatible with intervals, and if that proved to be too difficult, I'll do as you said. Thank you. If someone has other suggestions for this, please share, it would be appreciated.

[Riccardo Brasca]

Reinventing the wheel seems a bad idea, especially since you have to build all the API. I am sure it's better to use the already existing library.

[Rida Hamadani]

In order to prove the previous statement, I made the following changes:

variables {E F : Type*} [normed_add_comm_group E] [normed_space ℝ E]
[normed_add_comm_group F] [normed_space ℝ F]

lemma lincont_compose_diff_is_diff (T : E →  F) (f : ℝ → E) (t₀ : ℝ)
(f_diff : differentiable_at ℝ f t₀) (T_lincont :  is_bounded_linear_map ℝ T):
differentiable_at ℝ (T ∘ f) t₀ ∧ (deriv (T∘f) t₀ = T ∘ (deriv f t₀)) :=
begin
sorry
end

However, now I am getting this error message:

  deriv f
term
  f
has type
  ℝ → E : Type u_1
but is expected to have type
  ?m_1 → ?m_2 → E : Type (max ? ?)

My current understanding is that, while mathematically the composition T∘f has domain ℝ and image E, Lean is interpreting it as T∘f : ℝ → E → F. I would greatly appreciate any assistance in confirming the cause of this problem and finding a solution.

[Kevin Buzzard]

docs#deriv

[Kevin Buzzard]

T ∘ (deriv f t₀) doesn't make any sense, right? That's your problem I think. It doesn't "typecheck".

[Rida Hamadani]

f t is in E, implying deriv f t is in E too, and T is from E to F. Why wouldn't it typecheck?

[Eric Wieser]

q ∘ p : A → C where p : A → B and q : B → C. You have p as deriv f t : E, which isn't a function

[Kevin Buzzard]

\circ eats a function and you gave it a vector

[Rida Hamadani]

Oh I see! This is easy to fix, thank you!