Zulip Chat Archive

Stream: general

Topic: Help a mathematician learn Lean?

Béranger Seguin (Oct 23 2022 at 18:41):

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,

Riccardo Brasca (Oct 23 2022 at 18:44):

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

Riccardo Brasca (Oct 23 2022 at 18:46):

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 (Oct 23 2022 at 18:46):

What is the mathematical result you are trying to formalize?

Béranger Seguin (Oct 23 2022 at 18:56):

Here is a definition : a (unital, associative, not assumed commutative) ring RR is weakly fadelian if for every nonzero aa, there exist bb and cc such that 1=ab+ca1 = 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 aa and a proof of a0a \neq 0 and returns elements b,cb,c as well as a proof of 1=ab+ca1=ab+ca?

Béranger Seguin (Oct 23 2022 at 18:59):

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=0xy=yx=0 then x2=0x^2=0 or y2=0y^2=0.

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

Eric Wieser (Oct 23 2022 at 19:06):

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

Béranger Seguin (Oct 23 2022 at 19:07):

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 (Oct 23 2022 at 19:09):

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 (Oct 23 2022 at 19:12):

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 (Oct 23 2022 at 19:13):

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

Ruben Van de Velde (Oct 23 2022 at 19:13):

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

Eric Wieser (Oct 23 2022 at 19:14):

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

Béranger Seguin (Oct 23 2022 at 19:14):

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 (Oct 23 2022 at 19:14):

lem_int_2 has a spurious y argument

Ruben Van de Velde (Oct 23 2022 at 19:15):

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

Last updated: Aug 03 2023 at 10:10 UTC