sets in lean

Stream: new members

[Alexandre Rademaker]

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]

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

[Alexandre Rademaker]

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]

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

[Mario Carneiro]

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

[Alexandre Rademaker]

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

[Alexandre Rademaker]

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]

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

[Reid Barton]

I'm so confused

[Bryan Gin-ge Chen]

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]

I see

[Reid Barton]

"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]

Anyways, like Mario said, take is assume

[Alexandre Rademaker]

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

[Rob Lewis]

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]

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

[Rob Lewis]

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]

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]

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

[Rob Lewis]

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]

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

[Alexandre Rademaker]

Thank you

[Rob Lewis]

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]

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

[Patrick Massot]

This is now well documented.

[Patrick Massot]

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

[Rob Lewis]

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]

Exactly.

[Rob Lewis]

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

[Rob Lewis]

It's not a huge difference.

[Rob Lewis]

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

[Patrick Massot]

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

[Alexandre Rademaker]

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

[Alexandre Rademaker]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Alexandre Rademaker]

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

[Alexandre Rademaker]

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]

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]

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]

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]

[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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Harsha Nyapathi]

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]

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.

[Alex J. Best]

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.