## Stream: maths

### Topic: Friday afternoon puzzle -- 37 ∈ 37?

#### Kevin Buzzard (Nov 20 2020 at 15:46):

At Xena yesterday I was too quick with my use of use, accidentally using 37 for a set of reals. But it worked! Shing noted that set \R now has zero, one and add, so numerals work. This reminds me a bit of ZFC, where the corresponding result is false. Puzzle: is it true in Lean?

import tactic

namespace foo

-- all these work fine
instance : has_zero (set ℕ) := by apply_instance
instance : has_one (set ℕ) := by apply_instance
instance : has_add (set ℕ) := by apply_instance
-- so numerals work too

end foo

example : ∃ (a : ℕ) (b : set ℕ), a ∈ b :=
begin
use 37,
use 37,
-- ⊢ 37 ∈ 37
sorry
end


#### Gabriel Ebner (Nov 20 2020 at 15:51):

docs#set.singleton_one also looks scarily non-well-founded.

#### Reid Barton (Nov 20 2020 at 15:53):

Maybe it would make sense to put basically this whole file in a locale?

#### Reid Barton (Nov 20 2020 at 15:53):

e.g. open_locale pointwise to get these instances

#### Eric Wieser (Nov 20 2020 at 15:55):

lemma silly (n : ℕ) : n ∈ (n : set ℕ) :=
begin
induction n,
simp,
convert n_ih,
exact set.one_mem_one,
end

example : ∃ (a : ℕ) (b : set ℕ), a ∈ b :=
begin
use 37,
use 37,
convert silly 37,
simp,
end


#### Damiano Testa (Nov 20 2020 at 15:55):

Also, tidy proves it...

#### Damiano Testa (Nov 20 2020 at 15:56):

here is the proof tidy finds:

use 37,
use 37,
fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, refl } } }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, refl } } }, refl } }, refl } } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, refl } } }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, fsplit, work_on_goal 1 { fsplit, work_on_goal 0 { fsplit, work_on_goal 1 { simp at *, fsplit, work_on_goal 0 { refl }, refl } }, refl } } }, refl } } }, refl } }, refl } } }, refl } } }, refl },

#### Kevin Buzzard (Nov 20 2020 at 15:56):

In ZFC, 37 ∈ 38...

#### Damiano Testa (Nov 20 2020 at 15:57):

or, without following the misleading second use:

example : ∃ (a : ℕ) (b : set ℕ), a ∈ b := ⟨37, _, by solve_by_elim⟩


#### Sebastien Gouezel (Nov 20 2020 at 15:57):

example (n : ℕ) : n ∈ (n : set ℕ) :=
begin
induction n with n hn ih,
{ simp only [nat.cast_zero, set.mem_zero] },
{ exact ⟨n, 1, by simpa using hn⟩,}
end


#### Kevin Buzzard (Nov 20 2020 at 15:58):

I didn't really expect anything beyond entertainment to come from this post, but actually maybe Reid has a point. I remember @Mario Carneiro being a bit concerned about defining addition on set A too (A something with +)

#### Johan Commelin (Nov 20 2020 at 16:04):

lemma mem_bit0 [has_add α] {s : set α} {a : α} (h : a ∈ s) : bit0 a ∈ bit0 s :=
⟨a, a, h, h, rfl⟩

lemma mem_bit1 [has_one α] [has_add α] {s : set α} {a : α} (h : a ∈ s) : bit1 a ∈ bit1 s :=
⟨bit0 a, 1, mem_bit0 h, one_mem_one, rfl⟩

example : ∃ (a : ℕ) (b : set ℕ), a ∈ b :=
begin
use [37, 37],
solve_by_elim only [mem_bit1, mem_bit0, one_mem_one, zero_mem_zero] {max_depth := 6}
end


#### Damiano Testa (Nov 20 2020 at 16:07):

example : ∃ (a : ℕ) (b : set ℕ), a ∈ b := ⟨37, _, rfl⟩


(practicing minimizing skills)

#### Johan Commelin (Nov 20 2020 at 16:07):

I just wanted to post that one

#### Johan Commelin (Nov 20 2020 at 16:07):

@Damiano Testa Yeah, you're getting scary

#### Kevin Buzzard (Nov 20 2020 at 16:08):

example (n : ℕ) : (n : set ℕ) = {n} :=
begin
induction n with n hn,
{ exact set.singleton_zero },
simp [hn],
end


#### Bryan Gin-ge Chen (Nov 20 2020 at 16:31):

Amusing as this is, I agree with Reid that the pointwise instances on set should be hidden in a locale.

#### Kevin Buzzard (Nov 20 2020 at 16:34):

IIRC Mario's objection was that one could imagine a scenario where one has a local definition of addition on subsets of X (e.g. when making them a boolean ring, when you might want + to mean xor), and then you'd have problems if X accidentally also had an addition.

#### Damiano Testa (Nov 20 2020 at 16:43):

With a view towards further developments, the boolean structure on subsets often shows up in explicit representations of 2-torsion points on hyperelliptic curves. In such cases, the underlying set X could very well be a field. Would that be an issue?

#### Damiano Testa (Nov 20 2020 at 16:44):

(in the example of hyperelliptic curves, the 2-torsion points might be subsets of ramification points, or rather 2-set partitions of the ramification points)

#### Eric Wieser (Nov 20 2020 at 16:48):

If we end up not moving these, should we add @Johan Commelin's bit0 lemmas as norm_cast?

#### Gabriel Ebner (Nov 20 2020 at 17:08):

Johann's lemmas do not mention coe, so they can't be norm_cast. But an ↔ version should be simp.

#### Damiano Testa (Nov 20 2020 at 17:17):

To add to the silliness of the Friday afternoon: @Johan Commelin 's first lemma can be proved as follows:

lemma mem_bit0 [has_add α] {s : set α} {a : α} (h : a ∈ s) : bit0 a ∈ bit0 s :=
begin
repeat { fconstructor, exact ‹_›, },
fconstructor,
end


For me, it is the first time that fconstructor closes a goal, I think.

#### Kevin Buzzard (Nov 20 2020 at 17:42):

See if you can get split to close a goal :-)

#### Damiano Testa (Nov 20 2020 at 17:47):

Ahaha! I was wondering whether I was more surprised by fconstructor or split and went for fconstructor!

#### Johan Commelin (Nov 20 2020 at 17:50):

Gabriel Ebner said:

Johann's lemmas do not mention coe, so they can't be norm_cast. But an ↔ version should be simp.

Sadly, the iff version isn't true. For example bit0 2 \mem bit0 {1,3}

#### Kevin Buzzard (Nov 20 2020 at 18:56):

I'd never really internalised this {1}=1 thing but I was just working on valuations this evening and proving lemmas about trivial valuations. I noticed this was missing:

lemma subgroup.closure_eq_bot_iff (G : Type*) [group G] (S : set G) :
closure S = ⊥ ↔ S ⊆ {1} :=
begin
sorry
end


so I tried simp and it changed the RHS to S ⊆ 1. Meh :-/

#### Mario Carneiro (Nov 20 2020 at 20:33):

I was surprised to see that 0 = {0} in that definition. I would have guessed 0 = empty

#### Mario Carneiro (Nov 20 2020 at 20:34):

which for me is enough to suggest that these should not be simp normal form, because they are not universal enough

#### Mario Carneiro (Nov 20 2020 at 20:36):

as for 1 : set A I just have no idea what that should mean. It could mean univ if you treat set A as a boolean algebra and notate the top and bottom with 0 and 1. (We don't, but some books do and this would be a source of confusion)

#### Damiano Testa (Nov 21 2020 at 09:35):

Sorry for beating to death this thread, but I got hung up on the tidy proof and while trying to make sense of it, I realized that Lean either subtracts 1 or divides by 2, when the number is even (see below). Why is that?

example : ∃ (a : ℕ) (b : set ℕ), a ∈ b :=
begin
refine ⟨37, 37, _⟩,
refine ⟨36, ⟨1, _⟩⟩,  --here Lean subtracts 1
rw [eq_self_iff_true, and_true, set.mem_one, eq_self_iff_true, and_true],
refine ⟨18, ⟨18, _⟩⟩,  --here Lean divides by 2
rw [eq_self_iff_true, and_true, and_self],
refine ⟨9, ⟨9, _⟩⟩,
rw [eq_self_iff_true, and_true, and_self],
refine ⟨8, ⟨1, _⟩⟩,
rw [eq_self_iff_true, and_true, set.mem_one, eq_self_iff_true, and_true],
refine ⟨4, ⟨4, _⟩⟩,
rw [eq_self_iff_true, and_true, and_self],
refine ⟨2, ⟨2, _⟩⟩,
rw [eq_self_iff_true, and_true, and_self],
refine ⟨1, ⟨1, _⟩⟩,
rw [eq_self_iff_true, and_true, and_self],
exact set.mem_one.mpr rfl,
end


I would have imagined that Lean would have subtracted 1 all the way.

#### Kevin Buzzard (Nov 21 2020 at 09:37):

set_option pp.numerals false

#check 37 -- bit1 (bit0 (bit1 (bit0 (bit0 has_one.one)))) : ℕ


Lean stores numerals internally as binary.

#### Damiano Testa (Nov 21 2020 at 09:38):

Ah! So this proof is a more clunky version of Johan's, right? Thanks for the explanation!

#### Damiano Testa (Nov 21 2020 at 09:39):

Btw, Lean tells me

#check 37  -- 37 : ℕ


I do not see the binaries...

#### Kevin Buzzard (Nov 21 2020 at 09:39):

example : 1000000000 + 1000000000 = 2000000000 := rfl -- works
example : 1000000 + 2000000 = 3000000 := rfl -- times out


I was surprised the first time I saw this.

#### Kevin Buzzard (Nov 21 2020 at 09:40):

Damiano Testa said:

Btw, Lean tells me

#check 37  -- 37 : ℕ


I do not see the binaries...

That's because you didn't do what I did.

#### Damiano Testa (Nov 21 2020 at 09:41):

Sorry, I missed the first line of your code... :face_palm:

#### Kevin Buzzard (Nov 21 2020 at 09:41):

The pp. options just control what the pretty printer outputs (the infoview).

#### Kevin Buzzard (Nov 21 2020 at 09:41):

The elaborator turns 37 into some internal representation, and the pretty printer turns it back into the 37.

#### Damiano Testa (Nov 21 2020 at 09:42):

Thanks for the explanation!

#### Kevin Buzzard (Nov 21 2020 at 09:44):

I think that at some point in my Lean education someone told me about set_option pp.all true, which means "print out what Lean is really thinking", and the realisation that I could do this suddenly taught me a lot about what was going on internally. Sometimes you think "Lean why are you so slow", but then when you turn on pp.all you discover that it is manipulating gigantic terms.

#### Kevin Buzzard (Nov 21 2020 at 09:45):

set_option pp.all true

example : 37 = 37 :=
begin
sorry
end


#### Damiano Testa (Nov 21 2020 at 09:45):

I had a similar realization when I found out about show_term and started using it on all the lines of my code!

#### Damiano Testa (Nov 21 2020 at 09:45):

I will explore set_option pp.all true now!

#### Kevin Buzzard (Nov 21 2020 at 09:45):

Try it in the middle of a commutative algebra proof and you might get a bit of a shock!

#### Damiano Testa (Nov 21 2020 at 09:47):

Already I can see that I no longer have to guess how many _ I have to use in a refine ⟨_, _, ...⟩ expression!

#### Kevin Buzzard (Nov 21 2020 at 09:47):

PS re pp.all -- the infoview actually makes things a bit worse here. In the old days when we just had text output, the pp.alloutput was really nicely formatted.

set_option pp.all true

example : 37 = 37 :=
begin

end


The error here has really nice spacing (especially if you make the infoview window big).

#### Damiano Testa (Nov 21 2020 at 09:49):

This set_option really seems to clarify lots of things that were obscure in the "digested" view on the right

#### Kevin Buzzard (Nov 21 2020 at 09:50):

Try #help options .

#### Damiano Testa (Nov 21 2020 at 09:50):

I now need to look back at all the code that I wrote, turning this on!

#### Kevin Buzzard (Nov 21 2020 at 09:51):

Those give you all the options you can play with. I have never used 95% of them :-) Many are just for people debugging Lean.

#### Damiano Testa (Nov 21 2020 at 09:51):

Kevin Buzzard said:

Try #help options .

This means that I can do set_option and then any one of the things that this outputs, right?

#### Damiano Testa (Nov 21 2020 at 09:51):

Kevin Buzzard said:

Those give you all the options you can play with. I have never used 95% of them :-) Many are just for people debugging Lean.

Ok, thanks!

#### Kevin Buzzard (Nov 21 2020 at 09:51):

Right. But for the mathematician end user, most of these are not helpful.

#### Kevin Buzzard (Nov 21 2020 at 09:52):

Things like pp.all help a huge amount when you can't close x = x with rfl though. You can find out yourself exactly what went wrong.

#### Kevin Buzzard (Nov 21 2020 at 09:53):

If you see that one side has an _inst_1 in and the other side an _inst_5 that's when you realise that you have two abelian group structures on something.

#### Damiano Testa (Nov 21 2020 at 09:53):

Yes, I can see exactly where this would have helped with the order_dual stuff

#### Damiano Testa (Nov 21 2020 at 09:54):

When lean is computing max and I have no idea if it means max or min!

#### Kevin Buzzard (Nov 21 2020 at 09:54):

Oh yeah, then you would have been able to see exactly what was going on. I'm sorry I didn't look at that issue more carefully.

#### Damiano Testa (Nov 21 2020 at 09:55):

Do not worry: this way I used alone convert refl _ for the first time!

#### Kevin Buzzard (Nov 21 2020 at 09:56):

My feeling is that this sort of thing might be solved best by making stuff irreducible. But I didn't think too carefully. If order_dual X = X then that's fine, but then if some tactic manages to actually _change_ order_dual X back to X then that's when you're in trouble.

#### Kevin Buzzard (Nov 21 2020 at 09:59):

When I was working with valuations and groups with 0, we would be working with with_zero X and sometimes this would magically change to option X because with_zero X is defined to be option X but of course you want it to always stay as with_zero X to remind both you and Lean that it's $X\cup\{0\}$ rather than $X$ plus some arbitrary extra thing. But sometimes a tactic like simp might change with_zero X to option X and suddenly things are confusing (especially if you are also using with_bot or with_top or whatever). I fixed this by making with_zero irreducible and then things were much better, but also a bunch of proofs broke so I had to fix them :-)

#### Damiano Testa (Nov 21 2020 at 10:01):

When I will have some time, I will look into irreducible: what you describe seems very relevant!

#### Kevin Buzzard (Nov 21 2020 at 10:01):

But once we'd got things working again, stuff was better because Lean wasn't doing this incorrect unfolding.

def order_dual (α : Type*) := α


This definition is fine, but the problem is that when later on Lean is trying to guess what a type is, the elaborator might guess wrong, and think you mean alpha instead of order_dual alpha. Because they are definitionally equal, an order_dual X might accidentally turn back into an X and now all of a sudden max = min and things become impossible to work with. Marking order_dual irreducible will stop this happening.

#### Kevin Buzzard (Nov 21 2020 at 10:04):

import tactic

#print order_dual -- def order_dual :

#print with_zero -- @[irreducible] def with_zero : ...


order_dual isn't irreducible. It was only relatively recently we realised that this sort of thing could really help. The reals weren't irreducible for a while, and then occasionally Lean would think "I know, let's consider this real as an equivalence class of Cauchy sequences of rationals", which is 100% never what you want to do. Probably more things should be irreducible -- it guides Lean in the right direction.

#### Kevin Buzzard (Nov 21 2020 at 10:06):

The idea is that you make the definition, make the API with it not irreducible (so e.g. you can prove transitivity of < on order_dual X from transitivity of > on X) and then make it irreducible at the end of the file. Then in other files making API, you temporarily make it semireducible so you can do these tricks again if you need them.

#### Kevin Buzzard (Nov 21 2020 at 10:07):

But end users shouldn't be needing to unfold it, they should have all the lemmas they need from the API, and should be imagining order_dual X as in some sense being a completely different object to X -- even the map from X to order_dual X should have a name which isn't id.

#### Damiano Testa (Nov 21 2020 at 10:07):

Ok, I am not at the computer right now, but will look into this as soon as I am! Thanks!

#### Kevin Buzzard (Nov 21 2020 at 10:07):

(because id won't work any more if order_dual is irreducible). This is the price you pay, but it makes you write more principled code.

#### Damiano Testa (Nov 21 2020 at 10:08):

Yes, what you describe is very close to what I experienced!

#### Patrick Massot (Nov 21 2020 at 11:38):

Damiano, note that pp.all is much less needed now that we have info view widgets. The advantage of widgets is you can choose what to display instead of getting overwhelmed by pp.all. If you don't understand what I mean then you can post a #mwe where you feel pp.all helps you and I'll explain how to get the same information from widgets.

#### Mario Carneiro (Nov 21 2020 at 11:51):

I think it's easier to do diffing on a type mismatch with pp.all than with the goal view

#### Mario Carneiro (Nov 21 2020 at 11:52):

it's also easier to post a pp.all expression in zulip

#### Mario Carneiro (Nov 21 2020 at 11:52):

particularly if you don't know what you are looking for

#### Kenny Lau (Nov 21 2020 at 12:10):

import algebra.pointwise

example : ∃ (a : ℕ) (b : set ℕ), a ∈ b :=
begin
refine ⟨37, 37, _⟩,
have h1 : 1 ∈ (1 : set ℕ) := rfl,
have h2 : 2 ∈ (2 : set ℕ) := ⟨1, 1, h1, h1, rfl⟩,
have h4 : 4 ∈ (4 : set ℕ) := ⟨2, 2, h2, h2, rfl⟩,
have h8 : 8 ∈ (8 : set ℕ) := ⟨4, 4, h4, h4, rfl⟩,
have h9 : 9 ∈ (9 : set ℕ) := ⟨8, 1, h8, h1, rfl⟩,
have h18 : 18 ∈ (18 : set ℕ) := ⟨9, 9, h9, h9, rfl⟩,
have h36 : 36 ∈ (36 : set ℕ) := ⟨18, 18, h18, h18, rfl⟩,
have h37 : 37 ∈ (37 : set ℕ) := ⟨36, 1, h36, h1, rfl⟩,
exact h37
end


#### Kenny Lau (Nov 21 2020 at 14:19):

import algebra.pointwise

example : ∃ (a : ℕ) (b : set ℕ), a ∈ b :=
begin
refine ⟨37, 37, _⟩,
simp_rw [bit1, bit0, ← set.singleton_one, set.singleton_add_singleton, set.mem_singleton]
end


#### Kenny Lau (Nov 21 2020 at 14:20):

import algebra.pointwise

meta def foo : tactic unit :=
[{apply set.add_mem_add; foo} <|> exact set.one_mem_one]

example : ∃ (a : ℕ) (b : set ℕ), a ∈ b :=
begin
refine ⟨37, 37, _⟩,
foo
end


#### Riccardo Brasca (Nov 21 2020 at 15:27):

Sorry for the silly questions, but what are widgets?

#### Riccardo Brasca (Nov 21 2020 at 15:32):

Also... does 37 ∈ 37 mean that sets in lean are not well founded or am I missing something obvious?

#### Ruben Van de Velde (Nov 21 2020 at 15:34):

It's not 37 ∈ 37, it's 37 ∈ \uparrow 37, right?

#### Reid Barton (Nov 21 2020 at 15:35):

The two s mean different things

#### Riccardo Brasca (Nov 21 2020 at 15:35):

Ah OK, that's reassuring :D

#### Kevin Buzzard (Nov 21 2020 at 15:51):

Any type which has a 0, a 1 and an + automatically gets a 37. In this case this was unintentional, and the joke was to work out what this set actually was. Turns out it's {37}.

#### Riccardo Brasca (Nov 21 2020 at 15:55):

I see, set ℕ is a monoid with 1`, it makes sense.

#### Alex J. Best (Nov 21 2020 at 19:52):

Riccardo Brasca said:

Sorry for the silly questions, but what are widgets?

Widgets are a way of viewing arbitrary html in the goal view due to @Edward Ayers. In vscode this is what allows us to click terms in the goal view and repeatedly click on subterms and go to definition, and gives the nice highlighting of subterms.

Last updated: May 10 2021 at 07:15 UTC