Explicit constants/rates

Stream: general

[Josha Dekker]

Hi, I haven't had a lot of time to work on Lean recently because of PhD-duties, but I'm slowly trying to orient myself on possible research topics to proceed from there, and I was wondering what the status is for the following problem, or if anyone has any thoughts on it, as it is something I may consider working on in the future. Let's begin with a hypothetical situation:

Suppose I have a lemma lem1 that establishes f(n) = O(g(n)) and a lemma lem2 that establishes g(n) = O(h(n)). From this, I can derive my my_theorem, f(n) = O(h(n)).

Now suppose that I'm interested in getting explicit constants for f(n) = O(h(n)): I might begin by getting constants for both lemmata, lem1_ex and lem2_ex and then combining them to get a constant for my_theorem_ex, a version of my_theorem with explicit constants. After a while, someone might refine the constant in lem1_ex, which means that I might be able to improve on my constant for my_theorem_ex (and probably breaking its proof). With only few lemmata, we may keep track of any such changes and reasonably expect and breaks to proofs to be fixed, but with many lemmata, it would be nice to have an automated way of doing this.

You could argue that the proof my_theorem_ex would largely follow the proof my_theorem, so I'm wondering if there is a way to use some automation in such a way that 'explicit' versions of results follow easily from their non-explicit versions?

The current picture I have is the following: for any basic 'implicit' theorems, register (with some tagging mechanism) (an) explicit version(s) (such as lem1_ex and lem2_ex above). To then compute a constant for my_theorem_ex, we use an extensible macro (e.g. called explicit) that reads the proof of my_theorem and replaces all implicit versions of results called by explicit versions. I understand that this is still vague, and to make reasoning go through, we will probably need to add some additional information to my_theorem, but I hope I get the message across.

So, my questions are:

1. Do we have this?
2. If we do not have this, do we want this?
3. If we want this, would the above approach (on a very abstract level) be a desirable approach, or would you say alternative methods are preferable?

[Yaël Dillies]

@Bhavik Mehta and I have been experimenting with a slightly different approach, which is to make every single constant that appears in a statement its own def. In your example, it would look like

def lem1Const : ℝ := sorry

lemma lem1 : ∀ᶠ x in atTop, ‖f x‖ ≤ lem1Const * ‖g x‖ := sorry

def lem2Const : ℝ := sorry

lemma lem2 : ∀ᶠ x in atTop, ‖g x‖ ≤ lem2Const * ‖h x‖ := sorry

def myTheoremConst : ℝ := lem1Const * lem2Const

lemma my_theorem : ∀ᶠ x in atTop, ‖f x‖ ≤ myTheoremConst * ‖h x‖ := sorry

[Yaël Dillies]

And now you can prove results about myTheoremConst like myTheoremConst < 1000

[Josha Dekker]

I didn't think about using constants yet, that indeed seems like a very elegant approach to the problem where you would not really need a lot of automation. Perhaps you'd want to have a lemma pretty_myTheoremConst which shows that myTheoremConst = somePrettyExpression (at a given state of lem1Const and lem2Const), where this lemma would now need updating once the constants involved change, but that seems manageable (and perhaps amenable to some automatisation)

[Yaël Dillies]

Josha Dekker said:

Perhaps you'd want to have a lemma pretty_myTheoremConst which shows that myTheoremConst = somePrettyExpression (at a given state of lem1Const and lem2Const), where this lemma would now need updating once the constants involved change

Part of Bhavik and I's approach is that you should not do that, because it exposes the definition of the constant (and encourages downstream users to access it). Instead, you should only prove results of the form const ≤ some_explicit_expr (or ≥, depending on the constant): if ever you lower const, the proof of those results will break, but the statement will remain unchanged (you could change the statement to a stronger form, but I don't think you should. Write a new statement instead)

[Yaël Dillies]

Yaël Dillies said:

it exposes the definition of the constant (and encourages downstream users to access it)

In fact, I would go as far as saying that const should be an irreducible_def

[Bhavik Mehta]

I think this idea came from the Carleson project, actually!

[Bhavik Mehta]

Note that docs#Asymptotics.isBigOWith_iff tells you that docs#Asymptotics.IsBigOWith might give you a nice way to spell your statement