Entries in a list must be one of three specific functions

Stream: new members

[Nathan]

I'm working on this problem

image.png

I set things up like this:

import Mathlib.Data.Nat.Totient

def τ : ℕ → ℕ := fun n ↦ n.divisors.card
def σ : ℕ → ℕ := fun n ↦ ∑ d ∈ n.divisors, d
def φ : ℕ → ℕ := Nat.totient
def button : Type := {f : ℕ → ℕ // f = τ ∨ f = σ ∨ f = φ}
def seq : Type := List button

def s₁ : seq := [⟨τ, Or.inl rfl⟩, ⟨φ, Or.inr (Or.inr rfl)⟩]

But the definition of s₁ is cumbersome. I thought I could try something like this

import Mathlib.Data.Nat.Totient

inductive button : (ℕ → ℕ) → Type
| τ : button (fun n ↦ n.divisors.card)
| σ : button (fun n ↦ ∑ d ∈ n.divisors, d)
| φ : button Nat.totient
def seq : Type := List button

open button
def s₂ : seq := [τ, σ]

But the definition of seq is invalid. Any thoughts?

[Robin Arnez]

What about making the button type and its interpretation independent:

import Mathlib.Data.Nat.Totient

inductive Button where
  | τ | σ | φ

def Button.apply : Button → ℕ → ℕ
  | .τ, n => n.divisors.card
  | .σ, n => ∑ d ∈ n.divisors, d
  | .φ, n => Nat.totient n

def s₁ : List Button := [.τ, .φ]

def s₁fun : ℕ → ℕ := s₁.foldl (· ∘ ·.apply) id

[Aaron Liu]

here's how I would write it

import Mathlib

def buttonClosed (s : Set Nat) : Prop :=
  (∀ n ∈ s, n.divisors.card ∈ s) ∧
  (∀ n ∈ s, ∑ d ∈ n.divisors, d ∈ s) ∧
  (∀ n ∈ s, n.totient ∈ s)

theorem day2414 {s : Set Nat} (hs : buttonClosed s)
    {a b : Nat} (ha : 1 < a) (hb : 1 < b) (has : a ∈ s) : b ∈ s := by
  sorry

[Eric Wieser]

I don't think that's a particularly faithful translation, since it doesn't mention sequences or finiteness

[Nathan]

what is the dot doing in [.τ, .φ]?

[Nathan]

something like accessing local namespaces i guess?

[Aaron Liu]

Eric Wieser said:

I don't think that's a particularly faithful translation, since it doesn't mention sequences or finiteness

that's kind of the point, at a first glance this question has nothing to do with sequences or finiteness

[Matt Diamond]

@Nathan Here's the section of the manual that discusses "leading dot" notation:

https://lean-lang.org/doc/reference/latest/Terms/Identifiers/#The-Lean-Language-Reference--Terms--Identifiers--Leading--___

[Matt Diamond]

the TL;DR is that Lean knows that the elements of the list should have type Button, so when you write .τ it's smart enough to interpret that as Button.τ

[Nathan]

thanks :pray:

[Snir Broshi]

FWIW mathlib has definitions for the other two functions as well. Instead of:

def τ : ℕ → ℕ := fun n ↦ n.divisors.card
def σ : ℕ → ℕ := fun n ↦ ∑ d ∈ n.divisors, d

You can write:

def τ : ℕ → ℕ := ArithmeticFunction.sigma 0
def σ : ℕ → ℕ := ArithmeticFunction.sigma 1

See docs#ArithmeticFunction.sigma_zero_apply and docs#ArithmeticFunction.sigma_one_apply.
You can also open scoped ArithmeticFunction.sigma to get the notation σ, so those functions will be σ 0 and σ 1 without introducing any defs.

[Nathan]

nice

[Nathan]

that might even give me some nice lemmas about sigma

[Snir Broshi]

btw for the statement I'd go for something like this:

import Mathlib

inductive ReachableByOneButton : ℕ → ℕ → Prop
| τ {n : ℕ} : ReachableByOneButton n n.divisors.card
| σ {n : ℕ} : ReachableByOneButton n (∑ d ∈ n.divisors, d)
| φ {n : ℕ} : ReachableByOneButton n n.totient

def Reachable := Relation.ReflTransGen ReachableByOneButton

theorem day2414 {a b : ℕ} (ha : 1 < a) (hb : 1 < b) : Reachable a b := by
  sorry

[Nathan]

epic

[Nathan]

Aaron Liu said:

here's how I would write it

import Mathlib

def buttonClosed (s : Set Nat) : Prop :=
  (∀ n ∈ s, n.divisors.card ∈ s) ∧
  (∀ n ∈ s, ∑ d ∈ n.divisors, d ∈ s) ∧
  (∀ n ∈ s, n.totient ∈ s)

theorem day2414 {s : Set Nat} (hs : buttonClosed s)
    {a b : Nat} (ha : 1 < a) (hb : 1 < b) (has : a ∈ s) : b ∈ s := by
  sorry

this makes sense to me, but how do you show that this implies the existence of a button sequence? i guess we have to look at "the smallest closed set containing a" but i'm not sure how to do it

[Robin Arnez]

Take the set of natural numbers reachable from a sequence of button presses starting at a. This set is "button closed" and a is trivially in the set (through the empty sequence), thus b is in the set, i.e. there is a sequence of button presses that get you from a to b.

[Nathan]

thanks

[Nathan]

POTD2414.lean

I did it! This was so difficult, I almost gave up. Couldn't have done it without your guys' help and Ruben who actually updated Mathlib with some theorems I needed :skull: :melting_face:

[suhr]

By the way, which book is this problem from?

[Nathan]

it was posted in the math olympiads discord. apparently it's from "2020 ELMO, P6 of 6"

[metakuntyyy]

Very impressive work, that's a hard problem to start with. The tactics replace and obtain might be useful to you. They clear the hypotheses for you so you don't have to manually clear the context after you've used them.

[Nathan]

thanks, those do seem useful :pray: