sets in lean 4

Stream: new members

[Shreyas Srinivas]

Hi everyone,

In lean 3 it seems simple enough to use sets finsets etc. However I have not been able to find the equivalents for lean 4 in the Init or Data folders in the installation. I tried to install mathlib4 to use Init.set inside it. I get the following error

./lake-packages/Mathlib/././Mathlib/Data/Prod/Basic.lean:194:78: error: function expected at
  Lex
term has type
  ?m.8926
./lake-packages/Mathlib/././Mathlib/Data/Prod/Basic.lean:195:3: error: invalid field notation, type is not of the form (C ...) where C is a constant
  Lex
has type
  x✝

[Shreyas Srinivas]

Is there any other way I can use sets in lean 4?

[Kevin Buzzard]

You can help to port them! data.set.basic is just about within scope right now.

[Shreyas Srinivas]

okay, but this particular error appears to be in Data/Prod/Basic.lean, where should I begin?

[Kevin Buzzard]

Is your mathlib4 up to date?

[Shreyas Srinivas]

My lean toolchain: leanprover/lean4:nightly-2022-11-30
Lakefile :

import Lake
open Lake DSL

require Mathlib from git "https://github.com/leanprover-community/mathlib4"

package trials_errors {
  -- add package configuration options here
}

lean_lib TrialsErrors {
  -- add library configuration options here
}

@[default_target]
lean_exe trials_errors {
  root := `Main
}

I just created a fresh package today morning

[Shreyas Srinivas]

So I assume this is the version of mathlib on the main or master branch as of the last hour or so

[Shreyas Srinivas]

@Kevin Buzzard I think I now have a successfully building version of mathlib4. What exactly is needed to port data.set.basic ? I already see a Mathlib/Init/Set.Lean file and lake build was successful.

[Ruben Van de Velde]

Have you read the porting instructions on the wiki?

[Shreyas Srinivas]

I read it again. I think I'll follow along until I get stuck. It is confusing to see Init/Set.Lean already in there.

[Ruben Van de Velde]

Init/Set.lean is just a different file than Data/Set/Basic.lean which also covers some results about sets

[Shreyas Srinivas]

There is something I am not sure about. Does one have to send a pull request just to claim that one is working on porting some file?

[Shreyas Srinivas]

on the main mathlib repository?

[Shreyas Srinivas]

and then separately send another pull request to mathlib4 which only contains the lean3 X.lean file as is?

[Ruben Van de Velde]

No, you can just edit the porting status wiki page directly to claim a file

[Shreyas Srinivas]

Right now it says I cannot edit the page

[Ruben Van de Velde]

Oh, I guess that may be included in the push access. I can make the change if you tell me what it should say

[Shreyas Srinivas]

I would like to change the No in front of data.set.basic to No: WIP by Shreyas Srinivas 4e42a9d0a79d151ee359c270e498b1a00cc6fa4e

[Shreyas Srinivas]

This is in accordance with the instruction : if you would like to "claim" that you are working on the file, you can visit the port status page and change No to No: WIP by [your name] [mathlib3 SHA you just found]

[Shreyas Srinivas]

I took a look at the dependencies of data.set.basic. We need to port

1. Mathlib.Order.BooleanAlgebra : Has one dependency Mathlib.Order.Heyting.Basic which is already in mathlib4
2. Mathlib.Order.SymmDiff : Has two dependencies
   a) Mathlib.Order.BooleanAlgebra : See point 1.
   b) Mathlib.Logic.Equiv.Basic : already in mathlib4.
   in that order.

[Shreyas Srinivas]

Perhaps it makes sense for me to claim those two as well? Should these changes be pushed together or are separate pull requests preferred?

[Ruben Van de Velde]

I'd do separate PRs - especially when you're getting started, each file is more work than you'd think

[Shreyas Srinivas]

okay. I just looked up the porting status file for Order.BooleanAlgebra
It says "No please adopt mathlib4#793 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3"

[Shreyas Srinivas]

I am not sure what this means

[Shreyas Srinivas]

Okay now I see that 793 is an issue number thanks to zulip

[Shreyas Srinivas]

Since we do seem to have Mathlib.Order.Heyting.Basic it seems reasonable to change the status of Order.BooleanAlgebra I would not mind finishing it

[Shreyas Srinivas]

It is being held up by a linting error