Appendix B.1 - using exist statement in def

Stream: Analysis I

[ZhiKai Pong]

I had a go at finishing appendix B.1 and had a question:

the final part

theorem PosintDecimal.sum_eq (p q:PosintDecimal) : ∃ (r:PosintDecimal) (i:ℕ), (r.digit i:ℕ) = p.sum_digit q i ∧ (r:ℕ) = p + q := by

requires us to define a PosintDecimal locally, but the definition itself (the length) requires on another theorem

theorem PosintDecimal.sum_digit_top (p q:PosintDecimal) : ∃ l, p.sum_digit q l ≠ 0 ∧ ∀ i > l, p.sum_digit q l = 0 := by sorry

which is an exists statement. However, I couldn't use the value of l inside the def, and after some debugging I found that stating sum_digit_top as a subtype works. I'm not sure if this is the most idiomatic way though, and would like some clarification/confirmation if anyone knows more about this.

I'm not sure if this counts as a mwe, something I just put together to illustrate:

import Mathlib

theorem exists1 : ∃ (x : ℕ), x + 1 = 2 := by simp

structure abc where
  a : ℕ
  b := a + 1
  c := b + 1

example : ∃ (k : abc), abc.b = abc.a + 1 ∧ abc.a + 1 = 2 := by
  obtain ⟨x, hx⟩ := exists1
  def k : abc := {
    a := x -- Unknown identifier `x`
    b := x + 1
    c := x + 2
  }

[ZhiKai Pong]

I made https://github.com/teorth/analysis/pull/374 for the updated implementation I used eventually

[Aaron Liu]

You can't put a def inside another def or theorem

[Aaron Liu]

try let instead

[ZhiKai Pong]

if I want to make a standalone def outside of tactic mode, is there a way to use the exists statement then?

[Kenny Lau]

Exists.choose and Exists.chooose_spec

[Aaron Liu]

If it's standalone you have to pass in x somehow (for example, as an argument)

[ZhiKai Pong]

old approach:

theorem PosintDecimal.sum_digit_top (p q:PosintDecimal) : ∃ l, p.sum_digit q l ≠ 0 ∧ ∀ i > l, p.sum_digit q l = 0 := by sorry

theorem PosintDecimal.sum_eq (p q:PosintDecimal) : ∃ (r:PosintDecimal) (i:ℕ), (r.digit i:ℕ) = p.sum_digit q i ∧ (r:ℕ) = p + q := by
  sorry

new approach:

def PosintDecimal.sum_digit_top (p q:PosintDecimal) : {l : ℕ // p.sum_digit q l ≠ 0 ∧ (∀ i > l, p.sum_digit q i = 0)} := by sorry

def PosintDecimal.longAddition (p q : PosintDecimal) : PosintDecimal where
  digits := (List.range ((p.sum_digit_top q).val + 1)).reverse.map fun i => Digit.mk (p.sum_digit_lt q i)
  nonempty := by simp
  nonzero := by simp [(p.sum_digit_top q).prop.1]

theorem PosintDecimal.sum_eq (p q:PosintDecimal) (i:ℕ) :
    (((p.longAddition q).digit i):ℕ) = p.sum_digit q i ∧ (p.longAddition q:ℕ) = p + q := by sorry

is there any problem with my new approach, and which will you prefer? Exists.choose makes it noncomputable (although I'm not sure if we care)

[ZhiKai Pong]

for reference this is how the structure is defined:

structure PosintDecimal where
  digits : List Digit
  nonempty : digits ≠ []
  nonzero : digits.head nonempty ≠ 0

[Kenny Lau]

ZhiKai Pong said:

is there any problem with my new approach, and which will you prefer?

I prefer the new approach, but I think you should split the output of PosintDecimal.sum_digit_top, i.e. this function should just return the Nat, and then you can have two theorems below it to state those properties

[ZhiKai Pong]

Kenny Lau said:

ZhiKai Pong said:

is there any problem with my new approach, and which will you prefer?

I prefer the new approach, but I think you should split the output of PosintDecimal.sum_digit_top, i.e. this function should just return the Nat, and then you can have two theorems below it to state those properties

do you mean like this?

def PosintDecimal.sum_digit_top (p q:PosintDecimal) : {l : ℕ // p.sum_digit q l ≠ 0 ∧ (∀ i > l, p.sum_digit q i = 0)} := by sorry

theorem PosintDecimal.leading_nonzero (p q:PosintDecimal) :
    p.sum_digit q (p.sum_digit_top q) ≠ 0 := (p.sum_digit_top q).prop.1

theorem PosintDecimal.out_of_range_eq_zero (p q:PosintDecimal) :
    ∀ i > ↑(p.sum_digit_top q), p.sum_digit q i = 0 := (p.sum_digit_top q).prop.2

or more explicitly define p.sum_digit_top q, then split the proofs under the theorems

[ZhiKai Pong]

nevermind I agree this makes more sense:

def PosintDecimal.sum_digit_top (p q:PosintDecimal) : ℕ := by sorry

theorem PosintDecimal.leading_nonzero (p q:PosintDecimal) :
    p.sum_digit q (p.sum_digit_top q) ≠ 0 := sorry

theorem PosintDecimal.out_of_range_eq_zero (p q:PosintDecimal) :
    ∀ i > ↑(p.sum_digit_top q), p.sum_digit q i = 0 := sorry