Help a mathematician learn Lean?

Stream: general

[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