Multiples of 3, you say?

Stream: general

[Donald Sebastian Leung]

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]

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]

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

[Mario Carneiro]

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]

that's the meta version if you wanna be pedantic

[Mario Carneiro]

what do you mean?

[Kenny Lau]

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

[Kenny Lau]

but your translation is the easiest to work with

[Mario Carneiro]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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