import hierarchy

Stream: general

[Kenny Lau]

Suppose I want to state the lemma that if A is nonempty and R is a ring of char p then A -> R is a ring of char p.

[Kenny Lau]

The "char p" involves the file algebra.char_p and the A -> R involves the file algebra.ring.pi

[Kenny Lau]

currently I believe the two files do not import each other

[Kenny Lau]

so is there a way to put this lemma in mathlib without messing up the import hierarchy? or does this not matter at all?

[Kevin Buzzard]

My impression is that the way this sort of thing is handled is you just make a new file and import them both, or dump it in a file which imports both.

[Johan Commelin]

@Kenny Lau I think in this case it's ok to import alg.ring.pi in alg.char_p

[Kenny Lau]

@Johan Commelin then we're making alg.char_p depend on more files

[Kenny Lau]

I think this is a bigger problem than we think, in the sense that we might need an entirely new approach to dealing with hierarchy

[Kenny Lau]

I'm sure issues like this is hidden everywhere in mathlib

[Kenny Lau]

Maybe more segmentation (dividing files into multiple files) is the solution

[Johan Commelin]

content addressable declarations

[Kenny Lau]

For example, ring_theory.principal_ideal_domain imports ring_theory.noetherian and ring_theory.unique_factorization_domain

[Kenny Lau]

I'm pretty sure you don't need those imports to define PID

[Adam Topaz]

what about smaller files, more directories, and more default.lean files?

[Kenny Lau]

Sounds like a good idea to me

[Adam Topaz]

This way you could have the option to import giant things (by importing the default file), or little things by importing individual files

[Johan Commelin]

I would still love to see a version of Lean that is similar to unisonweb.org
Every declaration is hashed, and the hash is its stable name. (Before hashing, you also replace all names in the declaration by the hashes that they point to.)

[Johan Commelin]

You dump everything into a database, and you no longer really have directories or files.

[Adam Topaz]

Says the nixos user :wink:

[Johan Commelin]

But they do have tooling to "extract files" that you can then edit, and push back to the db

[Johan Commelin]

The reason this might be tricky for Lean / mathlib is that we have proof search going on. If all simp and tidy proofs would be replaced by the stable output of squeeze_simp and tidy?, then we might be a lot closer to making this work.

[Johan Commelin]

But then we would get really long and ugly proofs (e.g. in category theory). So I feel like maybe you would need to store multiple layers of proofs.

[Johan Commelin]

And then you quickly go down a rabbit hole of open problems and cute dreams. But nothing that we can actually realise in a short amount of time.

[Johan Commelin]

So probably the more pragmatic solution is what Adam said above: more dirs, more files, more default.lean

[Johan Commelin]

The other pragmatic solution is to ask Mario to make us a Lean layer on top of MM0 so that we have an ITP that compiles mathlib in < 5s, and then we can just dump everything into one file, like set.mm.

[Adam Topaz]

Unison sounds really cool BTW

[Adam Topaz]

Just thinking out loud.... How would this hashing AST a la unison work with typeclasses? E.g. how would I define two different category instances on the same type? Right now I would make an alias, and define a new instance on the alias.

[Johan Commelin]

I think you can make that work, if you have some special type_alias constructor in the language