## Stream: general

### Topic: Multiples of 3, you say?

#### Donald Sebastian Leung (Mar 31 2020 at 09:32):

Perhaps a bit off-topic, but how familiar and/or interested are typical undergraduate mathematicians with the following type of question?

Let S be the smallest set satisfying the following conditions:
- 0 ∈ S
- For any n ∈ S, we have n + 3 ∈ S

Let S' be the smallest set satisfying the following conditions:
- 30 ∈ S'
- 21 ∈ S'
- For any n, m ∈ S', we have n + m ∈ S'
- For any n, m ∈ S' with n ≥ m, we have n - m ∈ S'

Prove that S = S'.

Asking because I am considering translating such an exercise to Lean (for Codewars) once my midterms are over and I get a bit more free time, but I would like to assess the value of such a translation beforehand.

(The official invitation to join Codewars will hopefully be sent in a few weeks, after we have a few Lean challenges available on the site)

#### Kevin Buzzard (Mar 31 2020 at 10:28):

That looks like a pretty cool problem. I think that this could be attacked in tactic mode using the kind of tactics which people will have learnt by playing the natural number game.

#### Donald Sebastian Leung (Mar 31 2020 at 10:41):

Thanks for your input, I will definitely translate the problem into Lean when I have the time then :smile:

#### Mario Carneiro (Mar 31 2020 at 10:49):

Something like this?

inductive S : nat → Prop
| S_21 : S 21
| S_30 : S 30
| S_add {n m} : S n → S m → S (n + m)
| S_sub {n m} : n ≥ m → S n → S m → S (n - m)
open S

inductive S' : nat → Prop
| S'_0 : S' 0
| S'_add3 {n} : S' n → S' (n + 3)
open S'

theorem S'_eq_S : S' = S := sorry


#### Kenny Lau (Mar 31 2020 at 11:11):

that's the meta version if you wanna be pedantic

#### Mario Carneiro (Mar 31 2020 at 11:12):

what do you mean?

#### Kenny Lau (Mar 31 2020 at 11:13):

if you translate it more literally you might get def S : set nat := \bigint ...

#### Kenny Lau (Mar 31 2020 at 11:13):

but your translation is the easiest to work with

#### Mario Carneiro (Mar 31 2020 at 11:13):

I prefer to think that "let S be the smallest set such that ..." is mathematician-speak for inductive

#### Patrick Massot (Mar 31 2020 at 11:48):

This is clearly cheating. But I guess this kind of cheating is allowed on codewars.

#### Kevin Buzzard (Mar 31 2020 at 11:54):

The cheating is in the question isn't it? How do we know there is such a smallest set? Are we supposed to prove that an arbitrary intersection of sets satisfying the axioms used to define S also satisfies the axioms? There will be one tactic which does all of these I guess? obviously?

#### Kevin Buzzard (Mar 31 2020 at 12:15):

Mario's formalisation is wrong. This question has nothing to do with nat subtraction.

#### Kevin Buzzard (Mar 31 2020 at 12:16):

Surely you have to put all that n>=m stuff in and work in integers :-)

#### Kevin Buzzard (Mar 31 2020 at 12:17):

import data.real.basic -- because obviously S is a set of reals
import tactic

-- I'd happily make it an arbitrary ring
def S_like (T : set ℝ) :=
(0 : ℝ) ∈ T ∧
(∀ t ∈ T, t + (3 : ℝ) ∈ T)

example (ι : Type*) (T : ι → set ℝ) (hT : ∀ i, S_like (T i)) :
S_like (⋂(i : ι), T i) :=
begin
-- what tactic am I?
split,
rw set.mem_Inter,
intro i, replace hT := hT i,
exact hT.1,
intros t ht,
rw set.mem_Inter at *,
intro i, replace hT := hT i, replace ht := ht i,
exact hT.2 t ht
end

def S : set ℝ := ⋂₀{T : set ℝ | S_like T}


#### Mario Carneiro (Mar 31 2020 at 12:30):

Kevin Buzzard said:

The cheating is in the question isn't it? How do we know there is such a smallest set? Are we supposed to prove that an arbitrary intersection of sets satisfying the axioms used to define S also satisfies the axioms? There will be one tactic which does all of these I guess? obviously?

The tactic that does all this is called the inductive command and associated equation compiler

#### Mario Carneiro (Mar 31 2020 at 12:31):

I'm confused - I did put n >= m in

#### Mario Carneiro (Mar 31 2020 at 12:32):

yes you could do this in integers too, it's not very different

#### Mario Carneiro (Mar 31 2020 at 12:32):

pretty sure my version literally typechecks if you replace nat with int

#### Mario Carneiro (Mar 31 2020 at 12:33):

I don't appreciate your insinuating that nat subtraction is wrong, particularly when there is an n >= m assumption in the context. That is just as good as actual subtraction, it behaves nicely and should be a nat

#### Kevin Buzzard (Mar 31 2020 at 14:19):

You are implicitly assuming the theorem that $S\subseteq\mathbb{N}$.

#### Mario Carneiro (Mar 31 2020 at 14:58):

Yes I am, because this is type theory and I cannot do otherwise

#### Mario Carneiro (Mar 31 2020 at 15:01):

In order to typecheck the original statement I have to ask the mathematically meaningless question of what type 21 has. It looks like a nat to me, and nothing in the statement suggests otherwise, so nat it is. You could do it with int if you wanted, the statement is the same, or perhaps you could do it in an arbitrary ring if you like. Well, not quite, it has to be an ordered ring, but I think it is still true in that setting

#### Mario Carneiro (Mar 31 2020 at 15:02):

But I cannot just let it be unbounded as in set theory and prove that it is bounded

#### Mario Carneiro (Mar 31 2020 at 15:02):

so it would seem that a satisfactory formulation of the problem is impossible in lean by this standard

Last updated: May 14 2021 at 23:14 UTC