Zulip Chat Archive

Stream: new members

Topic: sets in lean 4


Shreyas Srinivas (Nov 30 2022 at 09:54):

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 (Nov 30 2022 at 09:55):

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

Kevin Buzzard (Nov 30 2022 at 10:02):

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

Shreyas Srinivas (Nov 30 2022 at 10:13):

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

Kevin Buzzard (Nov 30 2022 at 10:14):

Is your mathlib4 up to date?

Shreyas Srinivas (Nov 30 2022 at 10:20):

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 (Nov 30 2022 at 10:21):

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

Shreyas Srinivas (Nov 30 2022 at 14:44):

@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 (Nov 30 2022 at 14:44):

Have you read the porting instructions on the wiki?

Shreyas Srinivas (Nov 30 2022 at 14:54):

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 (Nov 30 2022 at 14:55):

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

Shreyas Srinivas (Nov 30 2022 at 15:06):

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 (Nov 30 2022 at 15:06):

on the main mathlib repository?

Shreyas Srinivas (Nov 30 2022 at 15:07):

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

Ruben Van de Velde (Nov 30 2022 at 15:10):

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

Shreyas Srinivas (Nov 30 2022 at 15:43):

Right now it says I cannot edit the page

Ruben Van de Velde (Nov 30 2022 at 15:44):

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 (Nov 30 2022 at 15:53):

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

Shreyas Srinivas (Nov 30 2022 at 15:53):

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 (Nov 30 2022 at 16:49):

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 (Nov 30 2022 at 16:51):

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 (Nov 30 2022 at 16:52):

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

Shreyas Srinivas (Nov 30 2022 at 17:01):

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

Shreyas Srinivas (Nov 30 2022 at 17:01):

I am not sure what this means

Shreyas Srinivas (Nov 30 2022 at 17:02):

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

Shreyas Srinivas (Nov 30 2022 at 17:03):

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 (Nov 30 2022 at 17:07):

It is being held up by a linting error


Last updated: Dec 20 2023 at 11:08 UTC