Porting category theory

Stream: mathlib4

[Jad Ghalayini]

I would like to port some category theory to Mathlib 4, could I please have branch access? My GitHub is imbrem

[Scott Morrison]

It looks like someone has sent one for you.

[Scott Morrison]

I'm currently working on porting the tidy tactic, which currently handles most of the proofs in the early parts of the category theory development.

[Scott Morrison]

It's fine to go ahead with porting theory files, but it may be slightly more cumbersome as mathport won't have any way to reconstruct these proofs.

[Scott Morrison]

You can do it by hand (e.g. sometimes by opening mathlib3, inserting the missing field, giving it a proof := by tidy? and then translating the output tidy gives you) if you like.

[Scott Morrison]

But in any cases you do so, please leave a comment in some uniform way that says "This is done by tidy", so we can clean it back up again afterwards.

[Scott Morrison]

This won't necessarily happen at the moment of porting, but I would like to change the syntax of tidy so that when you call tidy?, it outputs something like:

tidy says
  intro X
  ext
  cases h
  simp only [foo, bar]

and then tidy says is just a no-op wrapper, but with the possibility of setting an option which causes tidy to check that it would still regenerate this same proof.

I think this gives us best of both worlds: we're not actually running tidy over and over again in CI, which currently is burning lots of CPU resources, but at the same time the proof is clearly marked as "this is all done by automation", and in addition it is possible to keep it up to date, by occasionally setting the "regenerate" option and sanity checking what it says.

Finally, we can probably add code folding in VS Code so that the tidy says block is by default hidden.

[Scott Morrison]

@Jad Ghalayini limits.pdf shows the current import dependencies of the beginning of the category theory library. (At least after #17216; without that we need all the algebra.order hierarchy too.)

[Scott Morrison]

It may be helpful to organise this porting goal.

[Scott Morrison]

It can be regenerated at the command line in the mathlib repository by

cd src
leanproject import-graph --to category_theory.limits.yoneda --exclude-tactics --port-status limits.pdf

[Andrea Laretto]

Hello! I was trying to also to understand the porting mechanism for Category Theory, to which I'd like to contribute, and I stumbled upon this discussion. I would love to start working on CT and even build some new stuff in Lean4 on it, but before that I need to port the basic definitions, starting from Category. So, I started having a look at Combinatorics.Quiver.Basic.lean, but I'm getting a low-level error when declaring the mixfix syntax for Quiver.Hom. The error is the following:

application type mismatch
  pure
    { raw :=
        Lean.Syntax.node2 info✝ `Lean.Parser.Term.app
          (Lean.Syntax.ident info✝ (String.toSubstring' "Quiver.Hom") (Lean.addMacroScope mainModule✝ `Quiver.Hom scp✝)
            [Lean.Syntax.Preresolved.decl `Quiver.Hom []])
          (Lean.Syntax.node2 info✝ `null lhs✝.raw rhs✝.raw) }
argument
  { raw :=
      Lean.Syntax.node2 info✝ `Lean.Parser.Term.app
        (Lean.Syntax.ident info✝ (String.toSubstring' "Quiver.Hom") (Lean.addMacroScope mainModule✝ `Quiver.Hom scp✝)
          [Lean.Syntax.Preresolved.decl `Quiver.Hom []])
        (Lean.Syntax.node2 info✝ `null lhs✝.raw rhs✝.raw) }
has type
  Lean.TSyntax `term : Type
but is expected to have type
  Lean.Syntax : Type

and

IR check failed at '«_aux_Mathbin_Combinatorics_Quiver_Basic___macroRules_term_⟶__1»', error: unknown declaration 'coeDecidableEq'

Using Lean version 4.0.0-nightly-2022-11-21 17b73fa3. Thanks!

[Ruben Van de Velde]

Do you have the code in a branch so people can debug live?

[Andrea Laretto]

Not really, I just cloned mathlib3port and took a look at Combinatorics.Quiver.Basic.lean without adding anything else.

[Moritz Doll]

did you have a look at https://github.com/leanprover-community/mathlib4/wiki#porting-procedure ? cloning mathlib3port is not a thing that you should do

[Henrik Böving]

Also to address the first error. TSyntax is merely a typed wrapper around Syntax you can always access the underlying syntax object with myTstx.raw. We haven't fully ported all the relevant stuff over to TSyntax yet so this is a common-ish issue.

[Sebastian Ullrich]

This really shouldn't happen as there is a coercion between the two types

[Henrik Böving]

Really? I remember having to deal with that a couple of times when it was introduced.

[Sebastian Ullrich]

https://leanprover-community.github.io/mathlib4_docs/Init/Notation.html#Lean.instCoeHeadTSyntaxSyntax

[Sebastian Ullrich]

Note that this is the safe direction

[Sebastian Ullrich]

I assume this is the failing line: https://github.com/leanprover-community/mathlib3port/blob/master/Mathbin/Combinatorics/Quiver/Basic.lean#L46. That really shouldn't break unless the environment was changed in some way infixr doesn't expect.

[Scott Morrison]

@Andrea Laretto, please check out the branch category_theory, where I have already ported about the first half dozen files.

[Scott Morrison]

Please feel free to hack on that branch.

[Scott Morrison]

I will start converting it into PRs soon.

[Scott Morrison]

It's been held up due to some problems with using aesop in mathlib4, and by waiting for some Lean 4 commits to come through.

[Jad Ghalayini]

Hello! It seems I haven't been given branch access since the invitation has expired (got swamped in thesis work, let's try this again...). Could anyone please send a new invitation? Thanks! GitHub is imbrem

[Kevin Buzzard]

@maintainers

[Johan Commelin]

@Jad Ghalayini https://github.com/leanprover-community/mathlib4/invitations

[Jad Ghalayini]

Thanks!