Zulip Chat Archive

Stream: new members

Topic: sets in lean


view this post on Zulip 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 ∈ ∅?

view this post on Zulip Alexandre Rademaker (Oct 01 2019 at 01:26):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 01 2019 at 02:15):

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

view this post on Zulip Mario Carneiro (Oct 01 2019 at 02:16):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (Oct 01 2019 at 03:19):

I'm so confused

view this post on Zulip 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.

view this post on Zulip Reid Barton (Oct 01 2019 at 03:27):

I see

view this post on Zulip 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."

view this post on Zulip Reid Barton (Oct 01 2019 at 03:29):

Anyways, like Mario said, take is assume

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Alexandre Rademaker (Oct 01 2019 at 10:20):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Alexandre Rademaker (Oct 01 2019 at 11:17):

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

view this post on Zulip 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.

view this post on Zulip Alexandre Rademaker (Oct 01 2019 at 11:24):

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

view this post on Zulip Alexandre Rademaker (Oct 01 2019 at 11:24):

Thank you

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 01 2019 at 11:28):

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

view this post on Zulip Patrick Massot (Oct 01 2019 at 11:28):

This is now well documented.

view this post on Zulip Patrick Massot (Oct 01 2019 at 11:28):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 01 2019 at 11:28):

Exactly.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Oct 01 2019 at 11:30):

It's not a huge difference.

view this post on Zulip Rob Lewis (Oct 01 2019 at 11:31):

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

view this post on Zulip Patrick Massot (Oct 01 2019 at 11:31):

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

view this post on Zulip 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)

view this post on Zulip Alexandre Rademaker (Oct 01 2019 at 11:38):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Oct 01 2019 at 11:39):

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

view this post on Zulip Alexandre Rademaker (Oct 01 2019 at 11:40):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Oct 16 2019 at 21:40):

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

view this post on Zulip 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...

view this post on Zulip Marc Huisinga (Oct 16 2019 at 21:45):

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

view this post on Zulip Kevin Buzzard (Oct 16 2019 at 21:46):

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

view this post on Zulip 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.

view this post on Zulip 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) :=
begin
  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

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.

view this post on Zulip 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: May 18 2021 at 16:25 UTC