Creating a new type

Stream: general

[É Olive]

Alright so I got through the natural number game (skipping powers because I didn't care to do that). I started reading the docs but found them impenetrable, so I switched over to just proving more stuff aimlessly. I'm trying to make my own rings, but I'm running into some issues.

inductive ring
| add_id : ring
| mul_id : ring
| add (a b : ring) : ring
| add_inv (a : ring) : ring
| mul (a b : ring) : ring

axiom add_assoc {a b c : ring} : add a (add b c) = add (add a b) c

To start I used inductive because, having looked some lean source on github, it seems to be the way to make GADTs, however I'm skeptical that this is what I want since if this actually allows induction then I've made the integers, which is not my intention. The inductive declaration compiles at least so I moved on to writing some axioms. Immediately my first axiom add_assoc does not work. It doesn't know what add is, which seems odd to me since I just declared it as one of the constructors. Obviously I have no idea what I'm doing, but if someone could point me in the right way that would be much appreciated.

[Yakov Pechersky]

You need to say "open ring" to make the constructors available, instead of having to say ring.add

[Patrick Massot]

Which doc did you try to read? You won't go anywhere by trying to randomly guess how to use Lean, there are too many possible combinations.

[Yakov Pechersky]

But inductive and axiom isn't really the most flexible way to define rings.

[É Olive]

Patrick Massot said:

Which doc did you try to read? You won't go anywhere by trying to randomly guess how to use Lean, there are too many possible combinations.

I am reading from both "Theorem Proving in Lean" and "The Lean Reference Manual".

[Johan Commelin]

@É Olive I think you didn't even define the integers, to be honest. Because you can't prove 2 + 2 = 2 * 2 in this type.

[Johan Commelin]

docs#ring might give you a peek into how mathlib does rings.

[Johan Commelin]

Also, https://leanprover-community.github.io/learn.html lists a bunch of things that you could do after the natural number game.

[É Olive]

If I were to add the ring axioms I could certainly prove that (1+1) + (1+1) = (1+1) * (1+1). It might be more accurate to say that I would just have a subring of the integers, not necessarily the integers themselves.

[Eric Wieser]

Normally instead of introducing axioms, you would use a quotient type that defines equality such that those properties hold

[Eric Wieser]

If you did that you'd end up with a construction analogous to free_comm_ring empty (docs#free_comm_ring) tofree_ring empty (docs#free_ring) I think

[É Olive]

Well presumably that's commutative right? But if I'm understanding other than commutativity that then that is what I'm shooting for. What is the difference between quotient types and axioms?

[Patrick Massot]

É Olive said:

Patrick Massot said:

Which doc did you try to read? You won't go anywhere by trying to randomly guess how to use Lean, there are too many possible combinations.

I am reading from both "Theorem Proving in Lean" and "The Lean Reference Manual".

The Lean reference manual is not meant for learning (as is clear from its name). Theorem proving in Lean should be much better. If this is too computer sciency for you then you can try Mathematics in Lean (which is far from complete but should keep you busy for some time).

[Eric Wieser]

Whoops, I didn't check to see if you mentioned commutativity, and assumed you had. Edited.

[Eric Wieser]

axioms allow you to create contradictions globally if you screw up, quotients at worst let you create types that are accidently isomorphic to unit.

[Eric Wieser]

IIRC, mathlib contains no uses of axiom

[É Olive]

I appreciate the modularity of matlib when it comes to constructing algebra, but I am really struggling to figure out how it actually builds anything. Is there anywhere I can see some algebra built from first principles?

[Johan Commelin]

docs#semigroup and/or src#semigroup

[Heather Macbeth]

or this tutorial:
https://github.com/leanprover-community/lftcm2020/blob/master/src/exercises_sources/wednesday/algebraic_hierarchy.lean

[Eric Wieser]

Note that docs#ring is not building a semigroup, it's listing the requirements for something built elsewhere to be considered a semigroup.

[É Olive]

Oh! Alright, that makes a lot of sense. Ok I think I was stuck in the wrong sort of open world mindset here. Not that that was the only problem, but I get how mathlib is working a lot better now.

[Notification Bot]

Gabriel Ebner has marked this topic as unresolved.