Abstracting away conversions to Real

Stream: new members

[Adomas Baliuka]

Sorry for this very open question, that might be a bit style-based. I hope someone might still have some ideas. It's about about writing Lean code that is as close as possible to LaTeX-style real-number equations (which do not specify types) and make statements about the definitions "when the types are such-and-such" while keeping everything as simple and readable as possible.

Concretely, I have a function which inputs a bunch of (Natural and Rational) numbers and outputs a Natural number. This function is a rather long and cumbersome composition of standard functions such as +, *, /, ^, Real.sqrt, Real.log that work with real numbers. Furthermore, since there are quite many inputs, I group them in (actually two) structures. A toy example might look like this:

import Mathlib
open Real

structure Param where
  x : ℕ
  y : ℚ

noncomputable def f (p : Param) : ℕ := ⌊Real.log (p.x / p.y)⌋₊

def Domf : Set Param := {p | p.x ≠ 0 ∧ p.y ≠ 0}

Imagine that (just for readability) f is defined in terms of a bunch of other functions, which are defined above and fill several pages (all of them in the end reduce to "standard functions").

I would like to state some lemmas about f which effectively (i.e., the code should be as short and easy to understand as possible) convince a reader that f is "well-behaved" on the domain Domf. For example, I might want to say something like

if all inputs were Reals (instead of Naturals or Rationals) then f would be continuous/differentiable/etc. on the real-number version of Domf.

I hope this would also mostly convince a reader that the domain Domf is actually "mathematically valid" (i.e., no junk values are used).

The issue with what I've tried so-far is that the formalization of such statements involves a lot of coercions, which makes the function I'm proving something about quite far away from f.

For example, an approach I've considered would be defining f_Real : ℝ × ℝ → ℝ , prove things about that, and then define f in terms of f_Real. The downside is that I don't see a nice way to relate them (I would basically have to say in a comment "clearly it's the same function with different types") and it makes me have huge tuples everywhere (and also it makes me define duplicates of lots of other auxiliary definitions in terms of real numbers). The definition of fis written to be easy as possible for people to check that I did in fact just type out the exact equations from a certain LaTeX document and all my ideas make this really cumbersome and ugly.

How would you approach this? Thanks in advance for any suggestions!

[Alex Mobius]

You can write a proof that these are the same functions pointwise (i.e. that f_Real takes the same values on all natural points as f_Nat). Then you don't have to define f in terms of fReal, but you still have to write the formula twice.

[Adomas Baliuka]

Alex Mobius said:

You can write a proof that these are the same functions pointwise (i.e. that f_Real takes the same values on all natural points as f_Nat). Then you don't have to define f in terms of fReal, but you still have to write the formula twice.

Right, I have to write all the formulas of almost all of the auxilliary functions twice. (Which might be somewhat OK because a reader who trusts me not to be deceptive on purpose might not have to read those duplicates at all). Also, it still gives me huge tuples everywhere, or I have to define my own product topology for the structures? But maybe there's something better?

[Alex Mobius]

Another approach you might find amusing would be to define your function on "natural-valued reals" {x \in R // \exists n: \N, x = n}, which is about the same as carrying a tuple, but at least it coerces better; and you can prove facts about aux functions a bit easier.