Benefits (or not?) of avoiding division and subtraction

Stream: new members

[J. J. Issai (project started by GRP)]

I am still at the beginning of doing Lean proofs, and am trying to balance clarity and brevity. I am also trying to make things performant, so that if other portions need to use the code I write, my code should not be the bottleneck.

With $n$ of type Natural, the statement I am using for practice is $(4/3)^n > n+1$ when $n>7$. What would be more clear (more performant): trying to prove this statement, or trying to prove the (visibly) equivalent statement $4^n > (n+1)3^n$ for $n>7$? Also, how would a proof that the statements are equivalent look in Lean? (My primary use case would involve the former statement,
but I can be persuaded to modify my use case to use the latter.)

As an aside, is there a proof of these statements "not using induction", meaning the induction is buried in a library somewhere and that one can reference a tool like "This exponential function h(n) eventually gets and stays bigger than this linear function g(n), and a computable witness is n0", so that the tool can return n0 (and a proof that h(n)>g(n) when n>= n0) given simple exponential expression for h and simple linear expression for g." I am aware of (but not familiar with) linarith for certain comparisons involving linear functions, and I am not expecting a high powered tool that can handle an arbitrary exponential expression.

[Weiyi Wang]

I prefer 4/3 here given it is all constants. I might consider it differently if variables are inside the fraction

[Kyle Miller]

import Mathlib

example (n : Nat) (h : 7 < n) : (4 / 3 : ℚ) ^ n > n + 1 := by
  sorry

[Kyle Miller]

If you want to stick with Nat instead of using the rationals, then 4^n > (n + 1)*3^n is a better statement. To go back and forth, there are tools such as qify to make this Nat statement into a rational one and then perhaps field_simp to clear denominators.

[Kyle Miller]

import Mathlib

example (n : Nat) :
    n + 1 < (4 / 3 : ℚ) ^ n ↔ (n + 1) * 3 ^ n < 4 ^ n := by
  qify
  rw [div_pow, lt_div_iff₀]
  positivity

[Kyle Miller]

J. J. Issai (project started by GRP) said:

so that the tool can return n0

This sort of tool usually doesn't exist (yet). There are theorems sometimes that give that such numbers exist, but not what the number is. If the number exists, sometimes you can have Lean exhaustively find such a number, in very concrete situations.

[J. J. Issai (project started by GRP)]

For biconditionals, the examples I have seen were split into forward and backward implications. Where can I learn about handling both at the same time? I guess I am asking for a library of equivalences to use.

[Kyle Miller]

The tactics I suggested rewrote both sides of the biconditional until they were the same. Yes, you can prove forwards and backwards implications, and that's the definition of biconditionals (so it's a proof technique you can always rely on), but tactics like rw can rewrite anything in the goal.

[J. J. Issai (project started by GRP)]

Thanks @Kyle Miller and @Weiyi Wang . I shall study this further.

[Anthony Wang]

J. J. Issai (project started by GRP) said:

As an aside, is there a proof of these statements "not using induction", meaning the induction is buried in a library somewhere and that one can reference a tool like "This exponential function h(n) eventually gets and stays bigger than this linear function g(n), and a computable witness is n0", so that the tool can return n0 (and a proof that h(n)>g(n) when n>= n0) given simple exponential expression for h and simple linear expression for g." I am aware of (but not familiar with) linarith for certain comparisons involving linear functions, and I am not expecting a high powered tool that can handle an arbitrary exponential expression.

I think grind can do most of that, but only for Nat-valued exponential and linear functions. For instance:

example (n : Nat) (h : 4 < n) : 69 * n + 42 < 2 * 3 ^ n + 4 := by
  induction h
  · trivial
  · grind

However, this short proof no longer works if you change the exponential function to something like (3 : ℚ) ^ n.

[J. J. Issai (project started by GRP)]

Anthony Wang said:

J. J. Issai (project started by GRP) said:

As an aside, is there a proof of these statements "not using induction", meaning the induction is buried in a library somewhere and that one can reference a tool like "This exponential function h(n) eventually gets and stays bigger than this linear function g(n), and a computable witness is n0", so that the tool can return n0 (and a proof that h(n)>g(n) when n>= n0) given simple exponential expression for h and simple linear expression for g." I am aware of (but not familiar with) linarith for certain comparisons involving linear functions, and I am not expecting a high powered tool that can handle an arbitrary exponential expression.

I think grind can do most of that, but only for Nat-valued exponential and linear functions. For instance:

example (n : Nat) (h : 4 < n) : 69 * n + 42 < 2 * 3 ^ n + 4 := by
  induction h
  · trivial
  · grind

However, this short proof no longer works if you change the exponential function to something like (3 : ℚ) ^ n.

I will give this a try. How do I extract the proof from the results of using trivial and grind? (I want to produce a specific set of steps based on tactics like rw and calc and have, and I certainly don't mind having Lean give me these steps.)

[Kyle Miller]

You can prefix tactics with show_term to see exactly what low-level proof they generated. (You can also use by? to see that for an entire tactic script.)

However, tactics like grind do not create very interpretable proofs. That tactic in particular is optimized to prove things quickly and produce proofs that can be efficiently verified by the Lean kernel.

[Kyle Miller]

The calcify tactic is able to try to convert proofs generated by rw and simp into calc proofs. To use it you have to include it in your project. (You can either add it to your lakefile, or I think you might be able to copy the single file https://github.com/nomeata/lean-calcify/blob/master/Calcify.lean somewhere in your project and import it; it doesn't have any dependencies.)