Skolem's exponential functions

Stream: new members

[Janitha Aswedige]

I'm trying to formalize a problem of Skolem. Need to define a set $S$ of functions $\mathbb{N} \to \mathbb{N}$ so that $1, id$ are in $S$ and $S$ is closed under addition, multiplication, and exponentiation.

inductive S : (ℕ → ℕ) → Prop
  | one : S (fun _ => 1)
  | id : S (fun n => n)
  | add {f g : ℕ → ℕ} : S f → S g → S (f + g)
  | mul {f g : ℕ → ℕ} : S f → S g → S (f * g)
  | exp {f g : ℕ → ℕ} : S f → S g → S (fun n => f n ^ g n)

Is this the best way to do it?

[Matt Diamond]

Did you mean subtraction or exponentiation? Your description mentions the first but your code implements the second

[Janitha Aswedige]

Sorry. It was a mistake. It's exponentiation. Fixed it.

[Matt Diamond]

All good, thanks for clarifying

[Janitha Aswedige]

I'm having some trouble filling in the last two sorrys. At this point, I'm wondering if the idea of the theorem and its proof is correct at all. Can someone please have a look?

import Mathlib.Data.Real.Basic
import Mathlib.Order.WellFounded
import Mathlib.SetTheory.Ordinal.Arithmetic

open Function

namespace Skolem

/-- S is the set of functions ℕ → ℕ so that 1, id ∈ S, and S is closed under +, *, and exponentiation. -/
inductive S : (ℕ → ℕ) → Prop
  | one : S (fun _ => 1)
  | id : S (fun n => n)
  | add {f g : ℕ → ℕ} : S f → S g → S (f + g)
  | mul {f g : ℕ → ℕ} : S f → S g → S (f * g)
  | exp {f g : ℕ → ℕ} : S f → S g → S (fun n => f n ^ g n)


theorem growth_prop (f : ℕ → ℕ) (h : S f) : (∃ k, ∀ n ≥ k, f n ≥ n) ∨ (∃ c, ∀ n, c ≠ 0 ∧ f n = c):= by
  induction h with
  | one =>
    simp
  | id =>
    simp
  | @add g h sg sh ihg ihh =>
    sorry
  | @mul g h mg mh ihg ihh =>
    sorry
  | @exp g h hg hh ihg ihh =>
    simp
    cases' ihg with kg Hg <;> cases' ihh with kh Hh
    left
    obtain ⟨k₁, gk⟩ := kg
    obtain ⟨k₂, hk⟩ := kh
    let k' := max (max k₁ k₂) 1
    use k'
    intro n H
    have H2 : g n ≥ n := by aesop
    have H3 : h n ≥ n := by aesop
    have H4 : g n ^ h n ≥ n ^ n := by
      refine pow_le_pow H2 ?_ H3
      have : n ≥ 1 := by exact le_of_max_le_right H
      exact Nat.le_trans this H2
    have H5 : n ^ n ≥ n := by
      refine Nat.le_pow ?_
      aesop
    exact Nat.le_trans H5 H4
    left
    obtain ⟨k₁, gk⟩ := kg
    obtain ⟨c, hc⟩ := Hh
    let k := max k₁ 1
    use k
    intro n H
    have H1 : g n ≥ n := by
      have : n ≥ k₁ := by exact le_of_max_le_left H
      exact gk n this
    have H2 : h n = c := by aesop
    have H3 : c ≥ 1 := by
      have : c ≠ 0 := by aesop
      omega
    have H4 : h n ≥ 1 := by omega
    have H5 : g n ^ h n ≥ n ^ 1 := by
      refine pow_le_pow H1 ?_ H4
      have : g n ≥ k := by exact Nat.le_trans H H1
      aesop
    aesop
    left
    sorry
    sorry

[Aaron Liu]

these seem solvable to me

[Vlad]

Proof

import Mathlib.Tactic

inductive S : (ℕ → ℕ) → Prop
| one : S (fun _ => 1)
| id : S (fun n => n)
| add {f g : ℕ → ℕ} : S f → S g → S (f + g)
| mul {f g : ℕ → ℕ} : S f → S g → S (f * g)
| exp {f g : ℕ → ℕ} : S f → S g → S (fun n => f n ^ g n)

theorem eq_zero_of_fn_eq_zero {f n} (hf : S f) (h : f n = 0) : n = 0 := by
  induction hf with
  | one => simp at h
  | id => exact h
  | @add f g hf hg ih₁ ih₂ => simp at h; exact ih₁ h.1
  | @mul f g hf hg ih₁ ih₂ =>
    simp at h; rcases h with h | h; exact ih₁ h; exact ih₂ h
  | @exp f g hf hg ih₁ ih₂ => simp at h; exact ih₁ h.1

theorem le_exp₁ {a b : ℕ} (h : 2 ≤ b) : a ≤ b ^ a := by
  induction a; simp; rename_i a ha; simp [pow_succ]
  replace ha := Nat.add_le_add_right ha 1; apply ha.trans
  obtain ⟨b, rfl⟩ := Nat.exists_eq_add_of_le h; simp [mul_add, mul_two]
  suffices 1 ≤ (2 + b) ^ a + (2 + b) ^ a * b by linarith
  by_contra h; simp at h

theorem le_exp₂ {a b : ℕ} (h : b ≠ 0) : a ≤ a ^ b := by
  cases b; simp at h; rename_i b; simp [pow_add]; cases a
  simp; rename_i a; cases b; simp; rename_i b
  simp [pow_add]; by_contra h₁; simp at h₁

theorem growth_prop (f : ℕ → ℕ) (h : S f) :
    (∃ k, ∀ n ≥ k, f n ≥ n) ∨ (∃ c, ∀ n, c ≠ 0 ∧ f n = c):= by
  suffices h₁ : (∃ c, ∀ (n : ℕ), f n = c + 1) ∨ ∃ k, ∀ n, k ≤ n → n ≤ f n by
    symm; rcases h₁ with ⟨c, h₁⟩ | h₁
    left; use c + 1; simpa; right; exact h₁
  induction h with
  | one => left; use 0; simp
  | id => right; use 0; simp
  | @add f g hf hg ih₁ ih₂ =>
    rcases ih₁ with ⟨c₁, hc₁⟩ | ⟨k₁, hk₁⟩
    · rcases ih₂ with ⟨c₂, hc₂⟩ | ⟨k₂, hk₂⟩
      · left; use c₁ + c₂ + 1; simp [hc₁, hc₂]; ring
      right; use k₂; intro n hn; specialize hk₂ n hn
      simp; linarith
    right; use k₁; intro n hn; specialize hk₁ n hn
    simp; linarith
  | @mul f g hf hg ih₁ ih₂ =>
    rcases ih₁ with ⟨c₁, hc₁⟩ | ⟨k₁, hk₁⟩
    · rcases ih₂ with ⟨c₂, hc₂⟩ | ⟨k₂, hk₂⟩
      · left; use (c₁ + 1) * (c₂ + 1) - 1;
        simp [hc₁, hc₂]; rfl
      right; use k₂; intro n hn; specialize hk₂ n hn
      simp [hc₁]; rw [add_comm, add_mul]; simp
      exact Nat.le_add_right_of_le hk₂
    right; use k₁; intro n hn; specialize hk₁ n hn
    simp; by_cases h₁ : g n = 0
    · have h₂ := eq_zero_of_fn_eq_zero hg h₁; simp [h₂]
    obtain ⟨r, hr⟩ := Nat.exists_eq_succ_of_ne_zero h₁
    simp [hr, mul_add]; exact le_add_of_le_right hk₁
  | @exp f g hf hg ih₁ ih₂ =>
    rcases ih₁ with ⟨c₁, hc₁⟩ | ⟨k₁, hk₁⟩
    · rcases ih₂ with ⟨c₂, hc₂⟩ | ⟨k₂, hk₂⟩
      · left; use (c₁ + 1) ^ (c₂ + 1) - 1; simp [hc₁, hc₂]
        rw [Nat.sub_add_cancel]; apply Nat.one_le_pow'
      cases c₁; left; use 0; simp [hc₁]
      rename_i c₁; right; use k₂; intro n hn
      specialize hk₂ n hn; simp [hc₁]; apply hk₂.trans
      apply le_exp₁; linarith
    right; use k₁; intro n hn; specialize hk₁ n hn
    simp; by_cases h₁ : g n = 0
    · have h₂ := eq_zero_of_fn_eq_zero hg h₁; simp [h₂]
    obtain ⟨r, hr⟩ := Nat.exists_eq_succ_of_ne_zero h₁
    simp [hr]; apply hk₁.trans; apply le_exp₂; simp

[Janitha Aswedige]

How do I write that $(S,\preceq)$ is a well-ordering? I want it as a theorem but can't figure out how to write it.

import Mathlib.Tactic
import Mathlib.Order.Defs.Unbundled
import Mathlib.Order.RelClasses

open Function

namespace Skolem

/-- S is the set of functions ℕ → ℕ so that 1, id ∈ S, and S is closed under +, *, and exponentiation. -/
inductive S : (ℕ → ℕ) → Prop
  | one : S (fun _ => 1)
  | id : S (fun n => n)
  | add {f g : ℕ → ℕ} : S f → S g → S (f + g)
  | mul {f g : ℕ → ℕ} : S f → S g → S (f * g)
  | exp {f g : ℕ → ℕ} : S f → S g → S (fun n => f n ^ g n)

def EventuallyLT (f g : ℕ → ℕ) : Prop := ∃ n₀, ∀ n ≥ n₀, f n < g n

infix:50 " ≺ " => EventuallyLT

def EventuallyLE (f g : ℕ → ℕ) : Prop := f ≺ g ∨ f = g

infix:50 " ≼ " => EventuallyLE

[Aaron Liu]

Probably IsWellOrder S (· ≺ ·)

[Janitha Aswedige]

IsWellOrder S (· ≼ ·) gives an error; unexpected token '·'; expected '_' or identifier.

[Yaël Dillies]

Are you using the correct central dot?

[Janitha Aswedige]

I think so, used \ .

[Aaron Liu]

Then IsWellOrder S EventuallyLT should work

[Janitha Aswedige]

Still no :( theorem well_order : IsWellOrder S EventuallyLT := by sorry gives the error

application type mismatch
IsWellOrder S
argument
S
has type
(ℕ → ℕ) → Prop : Type
but is expected to have type
Type ?u.5733 : Type (?u.5733 + 1)

[Yaël Dillies]

Ah sorry, IsWellOrder {f // S f} (· ≺ ·) will do

[Janitha Aswedige]

That worked. I don't understand the goal state ⊢ IsWellOrder ↑{f | S f} fun x1 x2 => ↑x1 ≺ ↑x2 though. Could you please explain?

[Yaël Dillies]

What do you not understand about it? Also note I have edited my message above :wink:

[Janitha Aswedige]

Noted :) I don't get what it says.

[Yaël Dillies]

"$(S,\preceq)$ is a well-ordering"

[Yaël Dillies]

There are some extra complications due to the fact that S isn't a type. That means you need to make it into a type (this is what {f // S f} does) AND you need to tweak the relation as ≺ alone has the wrong type

[Janitha Aswedige]

Okay, I think I understand it a little now, though not fully. Thanks! :)