Friday afternoon puzzle -- 37 ∈ 37?

Stream: maths

[Kevin Buzzard]

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]

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

[Reid Barton]

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

[Reid Barton]

e.g. open_locale pointwise to get these instances

[Eric Wieser]

lemma silly (n : ℕ) : n ∈ (n : set ℕ) :=
begin
  induction n,
  simp,
  rw nat.succ_eq_add_one,
  apply set.add_mem_add,
  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]

Also, tidy proves it...

[Damiano Testa]

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]

In ZFC, 37 ∈ 38...

[Damiano Testa]

or, without following the misleading second use:

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

[Sebastien Gouezel]

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]

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]

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]

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

(practicing minimizing skills)

[Johan Commelin]

I just wanted to post that one

[Johan Commelin]

@Damiano Testa Yeah, you're getting scary

[Kevin Buzzard]

spoiler alert:

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

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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]

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]

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

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

[Gabriel Ebner]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Johan Commelin]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

set_option pp.numerals false

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

Lean stores numerals internally as binary.

[Damiano Testa]

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

[Damiano Testa]

Btw, Lean tells me

#check 37  -- 37 : ℕ

I do not see the binaries...

[Kevin Buzzard]

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

I was surprised the first time I saw this.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Damiano Testa]

Thanks for the explanation!

[Kevin Buzzard]

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]

set_option pp.all true

example : 37 = 37 :=
begin
  sorry
end

[Damiano Testa]

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]

I will explore set_option pp.all true now!

[Kevin Buzzard]

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

[Damiano Testa]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Try #help options .

[Damiano Testa]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Damiano Testa]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

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

[Patrick Massot]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

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]

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]

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]

Sorry for the silly questions, but what are widgets?

[Riccardo Brasca]

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

[Ruben Van de Velde]

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

[Reid Barton]

The two s mean different things

[Riccardo Brasca]

Ah OK, that's reassuring :D

[Kevin Buzzard]

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]

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

[Alex J. Best]

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.