Zulip Chat Archive

Stream: new members

Topic: sets in lean

Alexandre Rademaker (Oct 01 2019 at 01:23):

In https://leanprover.github.io/logic_and_proof/sets_in_lean.html, why

example :   A  :=
assume x,
assume h : x  ( : set U),
show x  A, from false.elim h

Why do we need x ∈ (∅ : set U) instead of only x ∈ ∅?

Alexandre Rademaker (Oct 01 2019 at 01:26):

ops! Answer in few lines below!! Sorry ;-)

Alexandre Rademaker (Oct 01 2019 at 02:06):

Almost all theorems from https://leanprover.github.io/logic_and_proof/sets_in_lean.html are from Lean2. What is the Lean3 version for take? I suppose that with the definition of ext we could easily redefine the theorems used in this chapter.

Reid Barton (Oct 01 2019 at 02:15):

But that page doesn't contain take...?

Mario Carneiro (Oct 01 2019 at 02:16):

take was merged with assume (or fun or \lam)

Alexandre Rademaker (Oct 01 2019 at 03:12):

take is used in the lean2 libraries. I need to adapt Chapter 12 from Logic and Proofs to Lean3.

Alexandre Rademaker (Oct 01 2019 at 03:15):

https://github.com/leanprover/lean2/blob/227fcad22ab2bc27bb7471be7911075d101ba3f9/library/data/set/basic.lean#L21-L22 seems to be very fundamental for all theorems in this file.

Reid Barton (Oct 01 2019 at 03:18):

But the book you linked to looks like it is already Lean 3. Why are you looking at the Lean 2 libraries?

Reid Barton (Oct 01 2019 at 03:19):

I'm so confused

Bryan Gin-ge Chen (Oct 01 2019 at 03:24):

This example relies on eq_of_subset_of_subset which is in data.set.basic in mathlib. From Alexandre's link above it looks like it was part of core in Lean 2.

Reid Barton (Oct 01 2019 at 03:27):

I see

Reid Barton (Oct 01 2019 at 03:27):

"Basic set-theoretic notions like these are defined in Lean’s core library, but additional theorems and notation are available in an auxiliary library that we have loaded with the command import data.set, which has to appear at the beginning of a file."

Reid Barton (Oct 01 2019 at 03:29):

Anyways, like Mario said, take is assume

Alexandre Rademaker (Oct 01 2019 at 10:03):

In Lean3 this import doesn’t work. Replaced by import init.data.set it works but those theorems are not available.

Rob Lewis (Oct 01 2019 at 10:11):

Logic and Proofs is entirely in Lean 3. Every example should work if you click on the "try it!" link, which loads a browser version of Lean 3.4.1 and a very old mathlib. The examples won't work with a current mathlib.

Alexandre Rademaker (Oct 01 2019 at 10:20):

Ah , so is it already based on mathlib? The book doesn’t mention it

Rob Lewis (Oct 01 2019 at 11:02):

The "auxiliary library" in Reid's quote refers to mathlib. It's not mentioned by name, because the book isn't supposed to be about Lean and mathlib. It's about logic and mathematical reasoning and uses Lean to explain these things.

Rob Lewis (Oct 01 2019 at 11:04):

I believe the web editor is running off of this repo: https://github.com/leanprover/lean-web-editor

You can see in the .toml file which mathlib commit is being used. I'm guessing it's current as of April 30, 2018. https://github.com/leanprover/lean-web-editor/blob/master/combined_lib/leanpkg.toml

Alexandre Rademaker (Oct 01 2019 at 11:17):

I wonder how hard it be to update the book examples for the last mathlib version

Rob Lewis (Oct 01 2019 at 11:21):

It shouldn't be hard. Most of the text doesn't depend on mathlib. Fixing the import statements will take care of a lot of the breakage.

Alexandre Rademaker (Oct 01 2019 at 11:24):

Good, if mathlib didn’t change too much, I will try to update the examples

Alexandre Rademaker (Oct 01 2019 at 11:24):

Thank you

Rob Lewis (Oct 01 2019 at 11:27):

There are complications though. The web editor would have to be updated too. We could point things to the community version at https://leanprover-community.github.io/lean-web-editor but that one updates mathlib periodically, and in theory these updates could break the L&P examples.

Patrick Massot (Oct 01 2019 at 11:28):

You could host a Lean web editor alongside Logic and Proof;

Patrick Massot (Oct 01 2019 at 11:28):

This is now well documented.

Patrick Massot (Oct 01 2019 at 11:28):

And it has the added benefit that you can use a stripped down mathlib.

Rob Lewis (Oct 01 2019 at 11:28):

mathlib has grown a ton since the web editor version and will take much longer to load. The ideal would be to carve out the small part of mathlib that's needed and just put that in a web editor.

Patrick Massot (Oct 01 2019 at 11:28):


Rob Lewis (Oct 01 2019 at 11:30):

But what's the motivation for updating at all? Some imports will match current mathlib instead of mathlib from 18 months ago.

Rob Lewis (Oct 01 2019 at 11:30):

It's not a huge difference.

Rob Lewis (Oct 01 2019 at 11:31):

If and when we add more Lean sections to L&P, we'll definitely upgrade.

Patrick Massot (Oct 01 2019 at 11:31):

I guess the only benefit is for readers who want to try those examples at home.

Alexandre Rademaker (Oct 01 2019 at 11:37):

Yes. During class I use emacs not the online version. Many students also prefer to work offline (emacs or VSC)

Alexandre Rademaker (Oct 01 2019 at 11:38):

But it is not clear to me why the web interface depend on the lib itself

Patrick Massot (Oct 01 2019 at 11:38):

It doesn't depend on the lib, but it has to load it if you want to use it.

Patrick Massot (Oct 01 2019 at 11:39):

And it wants to load a precompiled version, this is already slow enough.

Alexandre Rademaker (Oct 01 2019 at 11:40):

Ah , I see. I will have to look the code.

Alexandre Rademaker (Oct 01 2019 at 12:14):

Hi @Reid Barton my confusion about lean2 vs lean3. I though that it was based on lean2 given the missing theorems. But @Rob Lewis explained that it uses mathlib.

Bryan Gin-ge Chen (Oct 01 2019 at 13:55):

It wouldn't be difficult to set up a version of the community web editor with a pinned, minimized version of mathlib for use in L&P. I'm already building a few such bundles for use with some of the Observable notebooks that use Lean.

Ideally there would be a way to dynamically load libraries into the web editor, but I haven't figured out a decent way of doing this yet.

Floris van Doorn (Oct 01 2019 at 14:47):

We can just make a branch of mathlib where we remove 80% of the files: a barebones version of mathlib. And the L&P can point to that commit, right?
It might be nice if we could automatically add all L&P snippets as tests for mathlib (either on master or the barebones branch).

Bryan Gin-ge Chen (Oct 01 2019 at 14:51):

We don't even have to make a new branch of mathlib. If you create a lean package with all the L&P files in src/ and with mathlib as a dependency, the bundling script runs lean --make src/ so the only .olean files that are generated are those that are required for src/ to compile.

Kevin Buzzard (Oct 01 2019 at 15:06):

[Just to parenthetically remark that with my current use case (sending hundreds of undergraduates links to problems which they can solve using the Lean 3.5 web editor) I don't care at all about backwards compatibility and I am absolutely loving the fact that we have an up to date mathlib available like this. Thank you everyone who was involved with this]

Alexandre Rademaker (Oct 16 2019 at 21:19):

Still talking about sets. In https://leanprover.github.io/logic_and_proof/sets_in_lean.html, exercise 2 introduces the notation ⦃x⦄ that seems to be related to the magic of having disj and A ⊆ B acting as implications. Am I right? I didn't really understand what ⦃x⦄ means and how/where this magic is defined... Any pointers?

Kevin Buzzard (Oct 16 2019 at 21:40):

This {| x |} thing -- it is nothing to do with sets.

Kevin Buzzard (Oct 16 2019 at 21:41):

It simply means that when you use disj, you don't have to supply the variable x, Lean will supply it for you, except it's a bit more tricky than that...I'll find the reference...

Marc Huisinga (Oct 16 2019 at 21:45):

https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html#more-on-implicit-arguments ;)

Kevin Buzzard (Oct 16 2019 at 21:46):

I'd just found it when you posted ;-)

Harsha Nyapathi (Jan 26 2020 at 20:11):

Given an inductive type with finite elements, I want to make a set of some of the elements based on some property. How would you achieve that using functions (because function maps every element to a different object)? Also, what is the introduction rule for sets? The context is that I want to make a set of adjacent vertices of given vertex in a graph. Ultimately I want to find the connected component of the vertex. I'm stuck as to how to approach this.

Alex J. Best (Jan 26 2020 at 20:54):

I'm not sure this answers your questions but maybe its something:

import data.list.basic
import data.fintype

namespace FiniteGraph
open_locale classical -- to remove these lines one must prove that being in a connected component is decidable
noncomputable theory

structure FiniteGraph (V : Type) [fintype V] :=
(adjacent : set (V × V))

variables {V : Type} [fintype V] (F : FiniteGraph V)
structure path :=
(edges : list (V × V))
(edges_nonempty : edges  [])
(edges_in_graph :  e  edges, F.adjacent e)
(is_a_path :  i  list.range (edges.length - 1), (edges.nth_le _ (sorry : i < edges.length)).2 =
                                                 (edges.nth_le _ (sorry : i + 1 < edges.length)).1)

def connected_component (v : V) : finset V := set.to_finset
  {w |  p : path F, (p.edges.nth_le 0 sorry).1        = v
                    (p.edges.last p.edges_nonempty).2 = w}

def is_connected (C : finset V) : Prop :=  (v  C) (w  C),
        p : path F, (p.edges.nth_le 0 sorry).1        = v
                    (p.edges.last p.edges_nonempty).2 = w

lemma connected_component_is_connected (v : V) : is_connected F (connected_component F v) :=
  induction (connected_component F v) using finset.induction,
  -- this is the wrong way to prove this I suppose but this is the induction principle

end FiniteGraph

I just used a random type V with fintype to assume it is finite, then to define a subset of vertices subject to some condition I make a finset V from the corresponding set, I use classical logic so that I don't have to prove that a subset of a finset is a finset.

I don't think I understand your question about functions.

Alex J. Best (Jan 26 2020 at 20:56):

Also the last lemma is just a demo, its not even true as we have a directed graph here and the way I defined paths goes forwards along edges only.

Last updated: Dec 20 2023 at 11:08 UTC