Zulip Chat Archive

Stream: general

Topic: Multiples of 3, you say?


view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 31 2020 at 11:11):

that's the meta version if you wanna be pedantic

view this post on Zulip Mario Carneiro (Mar 31 2020 at 11:12):

what do you mean?

view this post on Zulip Kenny Lau (Mar 31 2020 at 11:13):

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

view this post on Zulip Kenny Lau (Mar 31 2020 at 11:13):

but your translation is the easiest to work with

view this post on Zulip 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

view this post on Zulip Patrick Massot (Mar 31 2020 at 11:48):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 12:15):

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

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 12:16):

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

view this post on Zulip 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}

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 31 2020 at 12:31):

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

view this post on Zulip Mario Carneiro (Mar 31 2020 at 12:32):

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

view this post on Zulip Mario Carneiro (Mar 31 2020 at 12:32):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 31 2020 at 14:19):

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

view this post on Zulip Mario Carneiro (Mar 31 2020 at 14:58):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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