Question: Why does `Series` have a parameter?

[adomasbaliuka]

The type defined in Series.lean

/-- A power series approximation within an interval `[-r,r]` around `0` -/
structure Series (s : Int64) where
  /-- Lower bound on the radius of accuracy -/
  radius : Floating
  /-- Power series coefficients -/
  coeffs : Array (Interval)
  /-- Upper bound on the error within `[-r,r]` -/
  error : Floating

has a parameter s. It is "written to" but does not seem to be read or used anywhere. (I was able to delete it and still build the library with very minor changes).

What is it for? I think it makes sense to document this.

I came across this while trying to figure out why log1p_div_series (defined here) depends on axiom Lean.ofReduceBool even though it seems that neither of the three structure fields depends on it...

[girving]

That’s obsolete: it’s from back when Series used Fixed s. It should definitely be deleted, and that file should have no s variable anywhere.

[adomasbaliuka]

Removed in PR #13

Any idea why log1p_div_series depends on ofReduceBool?

[girving]

I think ofReduceBool is the axiom that says the compiler is correct (and thus that native_decide is correct). So probably there is a native_decide somewhere in the dependencies.

[adomasbaliuka]

I think ofReduceBool is the axiom that says the compiler is correct (and thus that native_decide is correct). So probably there is a native_decide somewhere in the dependencies.

Yes. The compiler isn't completely correct, so I feel avoiding this axiom where possible has its merits (otherwise one needs to be confident everything is correct besides relying on the kernel checking).

The thing that's weird to me about this is that I can define each of the three fields assigned in that definition separately and they do not seem to depend on ofReduceBool. So I wonder where that comes from...

[girving]

These three native_decide calls should probably be removed:

1. https://github.com/girving/interval/blob/eb99034275f3f072cb140b9526de9f8fcd66d8c4/Interval/Floating/Abs.lean#L34
2. https://github.com/girving/interval/blob/eb99034275f3f072cb140b9526de9f8fcd66d8c4/Interval/Floating/Basic.lean#L212
3. https://github.com/girving/interval/blob/eb99034275f3f072cb140b9526de9f8fcd66d8c4/Interval/Floating/Order.lean#L122

[adomasbaliuka]

That fixed it!

I'm still confused why it used (as of eedc7ed31abed73631ef61f4944635f707129793, i.e., before #14) to be like below, but that's just morbid curiosity...

import Interval

def log1p_div_series' (n : ℕ) : Series where
  radius := .ofRat log_series_radius false
  coeffs := (Array.range n).map (fun n : ℕ ↦ .ofRat ((-1)^n / (n + 1)))
  error := .ofRat (log_series_radius ^ n / (1 - log_series_radius)) true

/-
'log1p_div_series'' depends on axioms: [propext, Classical.choice, Lean.ofReduceBool, Quot.sound]
-/
#print axioms log1p_div_series'

-- HOWEVER:

def radius := Floating.ofRat log_series_radius false
def coeffs (n : ℕ) := (Array.range n).map (fun n : ℕ ↦ Floating.ofRat ((-1)^n / (n + 1)))
def error  (n : ℕ) := Floating.ofRat (log_series_radius ^ n / (1 - log_series_radius)) true

/-
'Series' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#print axioms Series
/-
'radius' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#print axioms radius
/-
'coeffs' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#print axioms coeffs
/-
'error' depends on axioms: [propext, Classical.choice, Quot.sound]
-/
#print axioms error

[adomasbaliuka]

The reason for having the axiom was coeffs (which uses Interval.ofRat, which uses ofRat_le, which uses approx_ofRat, which uses approx_ofRat_abs, etc.).

I had mistyped Interval.ofRat to Float.ofRat when testing them separately. In any case, after #14 these things no longer depend on compiler correctness.