Help a mathematician learn Lean?

Stream: new members

[Béranger Seguin]

Hello !
I'm a classical mathematician, mostly working on questions of number theory.
I had the "fun" idea to formalize results from a recent preprint of mine on noncommutative ring theory, because these results seemed simple enough to be formalized. I'm having a lot of trouble, especially to not write spaghetti code. I don't want to flood this channel, so would anyone be interested in reviewing my code and helping me figure out what I should do better?
With love for this wonderful community,
Béranger

[Riccardo Brasca]

You can certainly post your code here, don't worry!

[Riccardo Brasca]

You can for example start posting the definitions (make sure to post a #mwe), these are the hardest for a beginner, and a mistake there means a lot of pain later

[Riccardo Brasca]

What is the mathematical result you are trying to formalize?

[Béranger Seguin]

Here is a definition : a (unital, associative, not assumed commutative) ring $R$ is weakly fadelian if for every nonzero $a$, there exist $b$ and $c$ such that $1 = ab+ca$. I formalized it as :

definition is_wfad (R : Type*) [ring R] : Prop :=
  ∀(a:R), (a ≠ 0) → (∃(b:R), ∃(c:R), 1=a*b+c*a)

Maybe I should rather have this as structure rather than property? Like a ring equipped with a map that takes an element $a$ and a proof of $a \neq 0$ and returns elements $b,c$ as well as a proof of $1=ab+ca$?

[Béranger Seguin]

One of the first results I prove in my preprint is that such a ring is necessarily integral. The proof probably requires LEM (the definition of integral rings feels weird constructively). The proof uses two lemmas, the first one is :

lemma lem_int_1 {R :Type*} [ring R] [is_wfad R] (x:R) (y:R):
  (x*y=0) → (y*x=0) → (x*x=0) ∨ (y*y=0) :=
-- there goes a proof

i.e. if $xy=yx=0$ then $x^2=0$ or $y^2=0$.

Then later I prove a second lemma, for which at some point I need to apply lem_int_1 with specific $x$ and $y$. And I don't know how to do that!

[Eric Wieser]

Note you need @[class] on your definition if you want [is_wfad R] to work properly

[Béranger Seguin]

If you are really interested in the details, here is what I came up with:
link to a pastebin page
The code is really spaghetti-ish, and I wonder how much easier this can be done.
My main question at the moment is: how to remove the sorry's that I have used: they seem to result formally from a simple beta-reduction (I am at ease with lambda-calculus and thought Lean would be closer, but the whole concept of proving things "from the bottom up" is weird to my mind which likes constructing lambda-terms)

[Béranger Seguin]

A thing you can do if you're (and that's the most understandable thing ever) not interested in reading the crappiest code ever written, is recommend me some really basic stuff for mathematicians trying to learn Lean. I, of course, did the natural number game and stuff, looked at the flashy YouTube videos, but there seems to be a big gap between this and the doc, and I don't know what kind of resources fit in exactly the middle spot. Actually, since I know natural deduction proofs, lambda-calculus, etc., I think at the moment I'd like a clear explanation of Lean's syntax and what exactly tactics are, etc. Because I'm confused. For example, your @{class] remark makes sense, but that's the kind of things I'm unaware of.

[Eric Wieser]

On the subject of typeclasses, you should also write

instance is_fad.to_iswfad {R : Type*} [ring R] [is_fad R] : is_wfad R :=

instead of your fad_to_wfad,
which will make typeclass search apply the lemma automatically

[Ruben Van de Velde]

I suspect currently the best way is to get people to review your code

[Ruben Van de Velde]

Instead of [0 ≠ (1:R)], use [nontrivial R]

[Eric Wieser]

https://leanprover.github.io/theorem_proving_in_lean/type_classes.html is probably the relevant tutorial information here

[Béranger Seguin]

Ok so that's like inheritance but that doesn't have to be "definitionally true", but can be proven a posteriori? Like constructing a forgetful functor?

[Ruben Van de Velde]

lem_int_2 has a spurious y argument

[Ruben Van de Velde]

And then apply lem_int_2 (y*x) yxyx_zero seems to work

[Eric Wieser]

Yes, it is indeed like inheritance; but only because class foo extends bar generates a foo.to_bar instance automatically in the obvious way. It's not inheritance that's special, it's instance (aka @[instance] lemma).

[Béranger Seguin]

Does it? I get "failed to synthesize type class instance for [...]" :( I'm using Lean 3 btw, should I not?

[Ruben Van de Velde]

Another tip: it's best practice to provide a name for the hypothesis created by by_contradiction, like by_contradiction h (because the autogenerated name may change between lean versions)

[Ruben Van de Velde]

Béranger Seguin said:

Does it? I get "failed to synthesize type class instance for [...]" :( I'm using Lean 3 btw, should I not?

Did you apply the @[class] suggestion from Eric?

[Béranger Seguin]

Ok! I was wondering what was up with these _inst_n thingies too.

[Béranger Seguin]

Yup, I did !

[Eric Wieser]

Can you update the pastebin with the previous suggestions so we can see what you missed?

[Béranger Seguin]

I didn't manage to, but I created an account so next times I will be able to. Here is the new link pastebin link

[Eric Wieser]

Note that here we tend to prefer https://gist.github.com since that support lean syntax highlighting

[Ruben Van de Velde]

Ruben Van de Velde said:

Instead of [0 ≠ (1:R)], use [nontrivial R]

This means you'll also need to change exact _inst_2 H66 to exact zero_ne_one H66

[Riccardo Brasca]

I am moving this conversation to the new members stream

[Notification Bot]

This topic was moved here from #general > Help a mathematician learn Lean? by Riccardo Brasca.

[Béranger Seguin]

Ruben Van de Velde said:

Ruben Van de Velde said:

Instead of [0 ≠ (1:R)], use [nontrivial R]

This means you'll also need to change exact _inst_2 H66 to exact zero_ne_one H66

I didn't make that change because I get "unknown identifier 'nontrivial'". Is something wrong with my Lean installation?

[Notification Bot]

This topic was moved here from #general > Help a mathematician learn Lean? by Riccardo Brasca.

[Eric Wieser]

Realistically you probably want

class is_fad (R : Type*) [ring R] : Prop :=
(prop : ∀(x:R), ∀(a:R), (a ≠ 0) → (∃(b:R), ∃(c:R), x=a*b+c*a))

class is_wfad (R : Type*) [ring R] : Prop :=
(prop : ∀(a:R), (a ≠ 0) → (∃(b:R), ∃(c:R), 1=a*b+c*a))

instead of

@[class] definition is_fad (R : Type*) [ring R] : Prop :=
  ∀(x:R), ∀(a:R), (a ≠ 0) → (∃(b:R), ∃(c:R), x=a*b+c*a)

@[class] definition is_wfad (R : Type*) [ring R] : Prop :=
  ∀(a:R), (a ≠ 0) → (∃(b:R), ∃(c:R), 1=a*b+c*a)

That way you can write apply is_wfad.prop instead of apply _inst_1

[Notification Bot]

This topic was moved here from #general > Help a mathematician learn Lean? by Riccardo Brasca.

[Riccardo Brasca]

Béranger Seguin said:

Does it? I get "failed to synthesize type class instance for [...]" :( I'm using Lean 3 btw, should I not?

You are right in using Lean 3.

[Riccardo Brasca]

Béranger Seguin said:

One of the first results I prove in my preprint is that such a ring is necessarily integral. The proof probably requires LEM (the definition of integral rings feels weird constructively). The proof uses two lemmas, the first one is :

lemma lem_int_1 {R :Type*} [ring R] [is_wfad R] (x:R) (y:R):
  (x*y=0) → (y*x=0) → (x*x=0) ∨ (y*y=0) :=
-- there goes a proof

i.e. if $xy=yx=0$ then $x^2=0$ or $y^2=0$.

Then later I prove a second lemma, for which at some point I need to apply lem_int_1 with specific $x$ and $y$. And I don't know how to do that!

Instead of writing (x*y=0) → (y*x=0) → (x*x=0) ∨ (y*y=0) we usually name the hypothesis x*y=0 and y*x=0 and we only keep (x*x=0) ∨ (y*y=0) as conclusion.

[Eric Wieser]

Béranger Seguin said:

Does it? I get "failed to synthesize type class instance for [...]" :( I'm using Lean 3 btw, should I not?

You should tell us the whole error message! It was

failed to synthesize type class instance for
R : Type u_1,
_inst_1 : ring R,
_inst_2 : 0 ≠ 1,
_inst_3 : is_wfad R,
x y : R,
xy_zero : x * y = 0,
yxyx_zero : y * x * (y * x) = 0
⊢ 0 ≠ 1

which is failing because 0 ≠ 1 is not a typeclass!

Using nontrivial R will fix this

[Eric Wieser]

If nontrivial R really doesn't work for you, perhaps you're on a very old version of lean 3?

[Béranger Seguin]

I have Lean 3.4.2

[Riccardo Brasca]

That's very old

[Eric Wieser]

You should be on Lean 3.48.0

[Béranger Seguin]

Alright, I took what the AUR had.

[Riccardo Brasca]

Have you followed the installation instructions?

[Eric Wieser]

AUR?

[Béranger Seguin]

I'm doing that now. Thanks for all the precious help!!! You've gotten me out of many questions I had.

[Mauricio Collares]

If you want to use the AUR, use https://aur.archlinux.org/packages/elan-lean instead of installing Lean directly

[Riccardo Brasca]

The tool you want is leanproject, doing something like leanproject new wfad will create a folder with the latest mathlib already compiled for you

[Mauricio Collares]

(That's https://aur.archlinux.org/packages/python-mathlibtools in the AUR)

[Eric Wieser]

Looking at AUR, I can't even find a download link to 3.4.2. What was the package name you used?

[Béranger Seguin]

I am using leanproject already, I think it's really my Lean version that sucks. It was lean3-bin.

[Riccardo Brasca]

I had a (very quick look at your code), it seems very reasonable! You can write rw [h1, h2...] on a single line to save lines. Also, using calc mode is probably a good idea when doing computation (at the beginning it seems a pain to use, but it improves readability a lot).

[Riccardo Brasca]

Also, try to not introduce too many sublemmas in a proof (using have). Just prove these lemmas separately (even if they're very technical and they become useless once one has the final result). In this way proofs are much shorter and much easier to read.

[Béranger Seguin]

Thanks to everyone, I updated the pastebin and now everything typechecks ! I'll check out calc mode. Thanks for the rw tip.
I use all these have because I don't know how to do otherwise! rw seems to only act on the ultimate goal and if I don't create intermediate goals I don't know how to do. Can you give an example of how it should be done ?

[Riccardo Brasca]

I mean that if I am proving that n = 2 and I say have : n < 5 := ... I'd rather write an explicit lemma lemma lt_5 ... : n < 5 := ...

[Eric Wieser]

Here's a much shorter spelling of one of your declarations:

instance is_fad.to_is_wfad {R : Type*} [ring R] [is_fad R] :
  is_wfad R :=
{ prop := is_fad.prop 1 }

[Riccardo Brasca]

And use this in the proof that n = 2. Of course nobody else will ever use it again, since I've proved that n = 2. but it doesn't matter.

[Eric Wieser]

Another trick:

    have C : ∃b, ∃c, 1=x*b+c*x := begin
      apply is_wfad.prop,
      exact x_nonzero,
    end,
    cases C with b C',
    cases C' with c d,

can be written

   obtain ⟨b, c, d⟩ := is_wfad.prop _ x_nonzero,

[Eric Wieser]

(tactic#obtain / docs#tactic.interactive.obtain)

[Béranger Seguin]

Awesome! That's exactly the kind of things that I didn't know how to do!

[Riccardo Brasca]

In any case rw [h] at h1 rewrites... well, h at h1, not at the final goal.

[Béranger Seguin]

Riccardo Brasca said:

In any case rw [h] at h1 rewrites... well, h at h1, not at the final goal.

This changes everything !

[Ruben Van de Velde]

Well no, just the hypothesis :)

[Riccardo Brasca]

Also, if your proof is a combination of associativity/distributivity and similar triviality in a ring, you can try the ring tactic

[Riccardo Brasca]

It essentially means "do the computation"

[Patrick Massot]

Béranger, where did you learn how to use Lean? I find it hard to understand how you can write Lean code without knowing some of the stuff you don't know. You must have had a very weird learning path.

[Patrick Massot]

I don't know how to phrase it in a way that I'm sure isn't unpleasant. I'm genuinely curious, and impressed you managed to write all that with a strange learning path.

[Matt Diamond]

As someone also self-taught, it doesn't seem so strange to me (I assume we're talking about the code in the pastebin link)... it looks like he understands very basic tactics (specifically intro, rw, apply, and exact), and those are all covered in the Natural Number Game. You can get pretty far with those alone (as demonstrated by the code in question). The code definitely seems like something you could write after playing NNG.

[Patrick Massot]

This was my first thought, but NNG definitely covers rw ... at ... and ring.

[Matt Diamond]

Well, I guess all I can say is that when one is a newbie it can be hard to remember everything one has learned. :)

[Béranger Seguin]

Patrick Massot said:

Béranger, where did you learn how to use Lean? I find it hard to understand how you can write Lean code without knowing some of the stuff you don't know. You must have had a very weird learning path.

I might have gotten overenthusiastic too soon. But the current version of the code is probably way better !

[Patrick Massot]

There is no problem at all with enthusiasm here!

[Béranger Seguin]

One thing I don't know how to deal with: in the text, I handle the case $(xb)^2=0$ and then the case $(cx)^2=0$ is similar because it is exactly symmetric. I don't find an easy way to avoid rewriting everything twice.

[Patrick Massot]

I really hope my curiosity won't lower your enthusiasm

[Patrick Massot]

Can you point out where exactly is your code this symmetry issue arise?

[Patrick Massot]

There is no silver bullet here, but there are some tricks

[Béranger Seguin]

Patrick Massot said:

I really hope my curiosity won't lower your enthusiasm

Have no worries. I received so much help here! Great community! My enthusiasm is safe

[Béranger Seguin]

Patrick Massot said:

Can you point out where exactly is your code this symmetry issue arise?

In current version, this starts at "cases H44 with xbxb_zero cxcx_zero," line 100 and then the two cases are in the distinct paragraphs that follow.

[Béranger Seguin]

But obviously this is clearer in maths:
We have shown either $(xb)^2=0$ or $(cx)^2=0$. We know $cx+xb=1$ and $x^2=0$. But then since one of the terms in $cx+xb=1$ is zero, $x$ has a (right or left, depending on the case) inverse which contradicts its square being $0$. The argument is one sentence in natural language but 26 lines in my code.

[Yaël Dillies]

You can state it as an auxiliary lemma foo and obtain the other statement by applying foo to the docs#mul_opposite of your ring.

[Riccardo Brasca]

You can probably use the opposite ring

[Riccardo Brasca]

Ops, Yael was faster

[Matt Diamond]

On a side note (and apologies if someone already mentioned this) but I noticed you used by exact X a number of times. This is actually unnecessary... you can delete by exact and simply write X. (This is because by transitions from term mode to tactic mode while exact transitions back into term mode, so they essentially cancel each other out.)

[Riccardo Brasca]

You can surely save a lot of lines using ring.

[Riccardo Brasca]

But I am catching a plane, enjoy Lean!

[Patrick Massot]

I'm not sure ring will buy him much since this is all non-commutative ring theory.

[Riccardo Brasca]

Oh you're right! That's sad

[Patrick Massot]

Non-commutative rings are really painful because nobody worked long enough with them to get us nice tactics. I just tried to do that little computation and the first try ends up at

example {R : Type*} [ring R] [nontrivial R]
  (x : R) (xx_zero : x * x = 0) (b c : R) (d : 1 = x * b + c * x)
  (H2 : x * b = x * (b * x) * b)
  (H : x * b * (x * b) = 0) : false :=
begin
  rw [show x*b = 0, by rw [H2, ← H, mul_assoc, mul_assoc, mul_assoc], zero_add] at d,
  have d' : c * 1 * x = c * (c * x) * x := congr_arg (λ y, c*y*x) d,
  rw [mul_one, mul_assoc, mul_assoc, xx_zero, mul_zero, mul_zero, ← d] at d',
  exact zero_ne_one.symm d'
end

[Patrick Massot]

All this handling of associativity is really a pain.

[Eric Wieser]

We have tactic#noncomm_ring but it's not very clever

[Patrick Massot]

I forgot about that one. At least it can be used to write a proof that doesn't invoke any ring axiom explicitly:

example {R : Type*} [ring R] [nontrivial R]
  (x : R) (xx_zero : x * x = 0) (b c : R) (d : 1 = x * b + c * x)
  (H2 : x * b = x * (b * x) * b)
  (H : x * b * (x * b) = 0) : false :=
begin
  replace d : 1 = c * x, by simpa [show x*b = 0, by { rw [H2, ← H], noncomm_ring }] using d,
  have d' : c * 1 * x = c * (c * x) * x := congr_arg (λ y, c*y*x) d,
  replace d' : c * 1 * x = c * c * (x * x), by { rw d', noncomm_ring },
  simpa [xx_zero, ← d] using d'
end

[Bryan Gin-ge Chen]

The associativity pain in Patrick's first proof can be alleviated slightly using tactic#assoc_rewrite, but of course the proof with noncomm_ring is much better:

import algebra.ring

example {R : Type*} [ring R] [nontrivial R]
  (x : R) (xx_zero : x * x = 0) (b c : R) (d : 1 = x * b + c * x)
  (H2 : x * b = x * (b * x) * b)
  (H : x * b * (x * b) = 0) : false :=
begin
  rw [show x*b = 0, by assoc_rw [H2, ← H], zero_add] at d,
  have d' : c * 1 * x = c * (c * x) * x := congr_arg (λ y, c*y*x) d,
  assoc_rw [mul_one, xx_zero] at d',
  -- trying to combine the following line with the previous one results in an app_builder exception
  rw [←d, mul_zero] at d',
  exact zero_ne_one.symm d'
end

[Béranger Seguin]

Patrick Massot said:

Non-commutative rings are really painful because nobody worked long enough with them to get us nice tactics. I just tried to do that little computation and the first try ends up at

example {R : Type*} [ring R] [nontrivial R]
  (x : R) (xx_zero : x * x = 0) (b c : R) (d : 1 = x * b + c * x)
  (H2 : x * b = x * (b * x) * b)
  (H : x * b * (x * b) = 0) : false :=
begin
  rw [show x*b = 0, by rw [H2, ← H, mul_assoc, mul_assoc, mul_assoc], zero_add] at d,
  have d' : c * 1 * x = c * (c * x) * x := congr_arg (λ y, c*y*x) d,
  rw [mul_one, mul_assoc, mul_assoc, xx_zero, mul_zero, mul_zero, ← d] at d',
  exact zero_ne_one.symm d'
end

--

This is so much more beautiful than my spaghetticode though.

[Béranger Seguin]

This is all so much fun! I even formalized the next theorem in the paper in a matter of minutes (a left Ore weakly fadelian ring is fadelian). I don't think the rest of the paper is as easy to formalize as it requires to define algebras of differential operators.

[Kevin Buzzard]

But it will be just as much fun!

[Patrick Johnson]

Can you share the preprint?

[Béranger Seguin]

Patrick Johnson said:

Can you share the preprint?

Submitted to the arXiv this week-end, so should only be there this week. This is really silly stuff though (absolutely no motivation or context, we were just playing around with rings and found weird results which we deemed shareable).

[Béranger Seguin]

Kevin Buzzard said:

But it will be just as much fun!

Honestly, the funniest thing for me would be formalizing results from my field (number theory stuff, Galois representations, inverse Galois theory, arithmetic geometry, etc., you know all of that better than me), but I think I'll have to get a liiiiittle better x)

[Kevin Buzzard]

This is one of my primary motivations for doing lean. As of quite recently we can now talk about things like a continuous representation $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to GL_n(\mathbb{Z}_p)$ and modular forms are on the way.

[Béranger Seguin]

Kevin Buzzard said:

This is one of my primary motivations for doing lean. As of quite recently we can now talk about things like a continuous representation $\mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})\to GL_n(\mathbb{Z}_p)$ and modular forms are on the way.

Awesome! My master's thesis dealt with (uni)versal deformation rings so I love them! Have things like Schlessinger's criterion already been formalized? It sounds like a cool project!

[Kevin Buzzard]

No, but we probably have all the machinery for Schlessinger now.

[Adam Topaz]

That (Schlessinger) would be a really nice project!

[Béranger Seguin]

Adam Topaz said:

That (Schlessinger) would be a really nice project!

If I didn't have a PhD thesis to finish I'd be doing all-nighters trying to learn Lean for this kind of stuff x)

[Béranger Seguin]

Patrick Johnson said:

Can you share the preprint?

It's on the arXiv now: https://arxiv.org/abs/2210.13078