Trying to formulate Goodstein's sequence

Stream: new members

[Bbbbbbbbba]

As one of my first exercises, I wrote two functions to convert a hereditary base-b notation (represented as an ordinal) to the natural number it represents, and vice versa. The former was easy enough, but the latter turned out to be quite tricky due to the need to prove termination.

Could someone experienced take a look and see if there is any easy way to improve my code (in terms of code style and/or readability)?

import mathlib

def ord_to_nat (b : ℕ) (o : ONote) :=
  match o with
  | 0 => 0
  | ONote.oadd e n a => b^(ord_to_nat b e) * n + (ord_to_nat b a)

def nat_to_ord_rec (e : ℕ) (b : ℕ) (x : ℕ) :=
  if h : 1 < b ∧ 0 < x then
    have h0 : x / b < x := by
      refine Nat.div_lt_self ?hLtN ?hLtK
      exact h.right
      exact h.left
    have h1 : (x / b) * b ^ (e + 1) ≤ x * b ^ e := by
      conv => lhs; rhs; rw [Nat.pow_add]; rw[Nat.mul_comm]; lhs; rw [Nat.pow_one]
      conv => lhs; rw[← Nat.mul_assoc];
      refine Nat.mul_le_mul_right (b ^ e) ?ha
      exact Nat.div_mul_le_self x b
    have h2 : e < b ^ e := by
      refine Nat.lt_pow_self ?hb e
      exact h.left
    have h3 : e < x * b ^ e := by
      refine Nat.lt_of_lt_of_le h2 ?hc
      refine Nat.le_mul_of_pos_left (b ^ e) ?hc.h
      exact Nat.zero_lt_of_lt h0
    (nat_to_ord_rec (e + 1) b (x / b)) + ONote.omega ^ (nat_to_ord_rec 0 b e) * (ONote.ofNat (x % b))
  else
    0
  termination_by (x * b ^ e, x)
  decreasing_by
    all_goals simp_wf
    all_goals refine (Prod.lex_def (fun a₁ a₂ ↦ a₁ < a₂) fun a₁ a₂ ↦ a₁ < a₂).mpr ?_
    all_goals simp
    . if h4 : (x / b) * b ^ (e + 1) < x * b ^ e then
        exact Or.intro_left (x / b * b ^ (e + 1) = x * b ^ e ∧ x / b < x) h4
      else
        refine Or.inr ?h
        refine ⟨?h.left, h0⟩
        refine Eq.symm (Nat.le_antisymm ?h.left.h₁ h1)
        exact Nat.le_of_not_lt h4
    . exact Or.intro_left (e = x * b ^ e ∧ e < x) h3

def nat_to_ord := nat_to_ord_rec 0

#eval ord_to_nat 3 (ONote.omega ^ (ONote.omega + 1) + ONote.omega ^ (2 : ONote) * 2 + 1)
#eval nat_to_ord 3 1234567
#eval ord_to_nat 3 (nat_to_ord 3 1234567)

[Bbbbbbbbba]

Incidentally the linter complains that h1 and h3 are unused, but I guess it's not seeing the decreasing_by block?

[Luigi Massacci]

Well you could definitely compactify your proof

[Luigi Massacci]

The have h0 can be a single line, etc

[Bbbbbbbbba]

Oh, I see, it can be have h0 : x / b < x := Nat.div_lt_self h.right h.left. I was using apply? a lot and never really thought about what refine meant :joy:

[Bbbbbbbbba]

Is there a good convention for naming all those ?h things? (I know that I could get rid of them all at the cost of making my code more nested)

[Bbbbbbbbba]

Oh I guess I could just name them all ?_ and then the compiler won't complain about duplicate names :joy:

[Patrick Massot]

If you don’t need to refer to those names then ?_ is definitely fine.

[Bbbbbbbbba]

Another silly thing caused by apply? is things like exact Or.intro_left (x / b * b ^ (e + 1) = x * b ^ e ∧ x / b < x) h4 when I could just use exact Or.inl h4 :rolling_on_the_floor_laughing:

[Bbbbbbbbba]

If my current goal is p ∨ q, is there a tactic that allows me to add ¬p to the hypotheses, like what I've essentially done with my if block here?

[Patrick Massot]

I don’t think we have a tactic for such a specialized task, but you can use

  rw [Classical.or_iff_not_imp_left]
  intro hnp

[Bbbbbbbbba]

This is where I am, with an error as I try to prove my first lemma.

import mathlib

def ω := ONote.omega

def ord_to_nat (b : ℕ) (o : ONote) :=
  match o with
  | 0 => 0
  | ONote.oadd e n a => b ^ (ord_to_nat b e) * n + (ord_to_nat b a)

def nat_to_ord_rec (e : ℕ) (b : ℕ) (x : ℕ) :=
  if h : 1 < b ∧ 0 < x then
    (nat_to_ord_rec (e + 1) b (x / b)) +
    ω ^ (nat_to_ord_rec 0 b e) * (ONote.ofNat (x % b))
  else 0
  termination_by (x * b ^ e, x)
  decreasing_by
    all_goals simp_wf
    all_goals apply (Prod.lex_def (fun a₁ a₂ ↦ a₁ < a₂) fun a₁ a₂ ↦ a₁ < a₂).mpr
    all_goals simp
    . rw [Classical.or_iff_not_imp_left]
      intro hnp
      constructor
      . apply Nat.le_antisymm
        . show x / b * b ^ (e + 1) ≤ x * b ^ e
          conv => lhs; rhs; rw [Nat.pow_add, Nat.mul_comm, Nat.pow_one]
          rw[← Nat.mul_assoc]
          apply Nat.mul_le_mul_right (b ^ e)
          exact Nat.div_mul_le_self x b
        . exact Nat.le_of_not_lt hnp
      . show x / b < x
        exact Nat.div_lt_self h.right h.left
    . apply Or.inl
      show e < x * b ^ e
      apply Nat.lt_of_lt_of_le
      . exact Nat.lt_pow_self h.left e
      . exact Nat.le_mul_of_pos_left (b ^ e) h.right

def nat_to_ord := nat_to_ord_rec 0

lemma nat_to_ord_rec_eq_zero_iff (hb : 1 < b) : nat_to_ord_rec e b x = 0 ↔ x = 0 := by
  rw [nat_to_ord_rec, ite_eq_right_iff] /- tactic 'rewrite' failed -/
  admit

image.png

[Ted Hwa]

You are probably looking for unfold nat_to_ord_rec in order to replace nat_to_ord_rec by its definition.

[Bbbbbbbbba]

Ted Hwa said:

You are probably looking for unfold nat_to_ord_rec in order to replace nat_to_ord_rec by its definition.

I think for nat_to_ord_rec, unfold does the same thing as rw

[Bbbbbbbbba]

My current problem is with ite_eq_right_iff (as seen in the screenshot)

[Bbbbbbbbba]

For what it's worth, I have an alternative version that uses Nat.log in order to make the recursion more simple (directly using ONote.oadd instead of ordinal arithmetic). However for either version, I think I need to "factor out" the decreasing_by block into a separate lemma (or two?) to avoid heavy code duplication when I try to prove anything, and I'm not exactly sure how to do that (for this version, mainly due to not wanting to expand all the let variables when stating the lemma).

import mathlib

def ω := ONote.omega

def ord_to_nat (b : ℕ) (o : ONote) :=
  match o with
  | 0 => 0
  | ONote.oadd e n a => b ^ (ord_to_nat b e) * n + (ord_to_nat b a)

def nat_to_ord (b : ℕ+) (x : ℕ) :=
  match x with
  | 0 => 0
  | y + 1 =>
    let x := y + 1;
    let e := Nat.log b x;
    let n := x / b ^ e;
    have lem0 : b ^ e ≤ x := by
      apply Nat.pow_log_le_self ↑b
      simp
    have lem1 : e < b ^ e := by
      if h: b = 1 then
        have : e = 0 := by
          refine Nat.log_of_left_le_one ?_ x
          simp [h]
        simp_arith [this]
      else
        refine Nat.lt_pow_self ?_ e
        apply Nat.one_lt_iff_ne_zero_and_ne_one.mpr
        simp [h]
    have : e < x := Nat.lt_of_lt_of_le lem1 lem0
    have n_pos : 0 < n := by
      refine (Nat.div_pos_iff ?_).mpr lem0
      simp
    have : x - b ^ e * n < x := by
      apply Nat.sub_lt
      . exact Nat.zero_lt_succ y
      . refine Mathlib.Tactic.Ring.mul_exp_pos e ?_ n_pos
        exact PNat.pos b
    ONote.oadd (nat_to_ord b e) (⟨n, n_pos⟩ : ℕ+) (nat_to_ord b (x - b ^ e * n : ℕ))

[Bbbbbbbbba]

This is my current progress. I think I'm starting to get the hang of it, but I assume there should be a way to make the line def dec_lemma {b : ℕ+} {x : ℕ} : 0 < x → Nat.log b x < x ∧ 0 < x / b ^ Nat.log b x ∧ x - b ^ Nat.log b x * (x / b ^ Nat.log b x) < x shorter, right?

import mathlib

def ω := ONote.omega

def ord_to_nat (b : ℕ) (o : ONote) :=
  match o with
  | 0 => 0
  | ONote.oadd e n a => b ^ (ord_to_nat b e) * n + (ord_to_nat b a)

def dec_lemma {b : ℕ+} {x : ℕ} : 0 < x → Nat.log b x < x ∧ 0 < x / b ^ Nat.log b x ∧ x - b ^ Nat.log b x * (x / b ^ Nat.log b x) < x := by
  intro hx
  exact
    let e := Nat.log b x;
    let n := x / b ^ e;
    have lem0 : b ^ e ≤ x := by
      apply Nat.pow_log_le_self ↑b
      exact Nat.not_eq_zero_of_lt hx
    have lem1 : e < b ^ e := by
      if h: b = 1 then
        have : e = 0 := by
          refine Nat.log_of_left_le_one ?_ x
          simp [h]
        simp_arith [this]
      else
        refine Nat.lt_pow_self ?_ e
        apply Nat.one_lt_iff_ne_zero_and_ne_one.mpr
        simp [h]
    have r0: e < x := Nat.lt_of_lt_of_le lem1 lem0
    have n_pos : 0 < n := by
      refine (Nat.div_pos_iff ?_).mpr lem0
      simp
    have r1: x - b ^ e * n < x := by
      apply Nat.sub_lt
      . exact hx
      . refine Mathlib.Tactic.Ring.mul_exp_pos e ?_ n_pos
        exact PNat.pos b
    ⟨r0, n_pos, r1⟩

def nat_to_ord (b : ℕ+) (x : ℕ) :=
  if h : 0 < x then
    let e := Nat.log b x;
    let n := x / b ^ e;
    have ⟨_, n_pos, _⟩ : e < x ∧ 0 < n ∧ x - b ^ e * n < x := dec_lemma h
    ONote.oadd (nat_to_ord b e) (⟨n, n_pos⟩ : ℕ+) (nat_to_ord b (x - b ^ e * n : ℕ))
  else 0
  termination_by x

theorem nat_to_ord_to_nat {b : ℕ+} : ord_to_nat b (nat_to_ord b x) = x := by
  unfold nat_to_ord
  if h : 0 < x then
    let e := Nat.log b x;
    let n := x / b ^ e;
    simp [h, ord_to_nat]
    have ⟨_, _, _⟩ : e < x ∧ 0 < n ∧ x - b ^ e * n < x := dec_lemma h
    repeat rw [nat_to_ord_to_nat]
    apply Nat.add_sub_of_le
    exact Nat.mul_div_le x (b ^ e)
  else
    simp [h, ord_to_nat]
    exact Eq.symm (Nat.eq_zero_of_not_pos h)

[Violeta Hernández]

Hi! I'm just finding this thread

[Violeta Hernández]

It just so happens I've been working with ONote this past week or so

[Violeta Hernández]

Did you finish the Goodstein proof? I think that could make a nice result for Mathlib.

[Violeta Hernández]

If not, I could try and finish it myself :smile: