proving an existing theorem as practice?

Stream: Is there code for X?

[JJ]

I'm taking an algebra class and I'd like to set about mechanizing some of the theorems we're covering in class and on homeworks and such in Lean. These are usually already in Mathlib. Is there any way to tell Mathlib "I want to re-prove this theorem, so don't let me use it or anything that depends on it?"

Ideally I'd like to be able to use things like simp and simp? and what not. Right now I've just been porting over my paper proofs to Lean, to make sure I don't have any circularity, but I'd like to try out using Lean for writing the proofs, too.

Are there any features for non-circularity like this that exist already? Do you all have any advice on how to best approach re-mechanizing existing proofs? I was considering taking an approach like what Tao's Analysis does, but this commits me to mechanizing (or at least formulating) everything we cover in the course and I don't know if I'll be able to do all of that in my spare time.

[Kenny Lau]

well it's an exercise to yourself and you could just not use some of the theorems

[JJ]

The problem is that other theorems can depend on the theorem I am proving, and I might accidentally use them. It's fairly easy (though still a pain) to avoid using exactly what I am proving.

[Kenny Lau]

you could also not import Mathlib but rather import some parts

[Kenny Lau]

well simp? tells you what theorems you're using

[JJ]

Yes, I'm aware :smile:

[JJ]

(hm. maybe i should have posted this in #new members or #general ?)

[Robert Maxton]

Unfortunately, no, there's no good way to avoid transitive dependencies on a lemma like that. You can remove individual lemmas from the simp pool by using attribute [-simp], but otherwise, I don't think so.

[Antoine Chambert-Loir]

Not a good and systematic way, but you can always check that the Mathlib lemma you want to use doesn't exist with the set of files that you have imported.

[Rado Kirov]

I was considering taking an approach like what Tao's Analysis does, but this commits me to mechanizing (or at least formulating) everything

It works reasonably well in Tao's Analysis (though there are exceptions like absolute value for some reason is imported from mathlib). Technically, you just need the nearest definition to the theorem you are doing, e.g. if you want to prove something about reals, you can build custom reals from sequences of mathlib rationals (you don't necessarily need custom rationals).