Definition by recursion: introducing variables, etc.

Stream: Is there code for X?

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

I am attempting a definition by recursion, and need to introduce variables inside the definition. Is there an example in the documentation I can follow?

Here is (a snippet from) my attempt:

def my_langg  ( n : @& Nat ) : Nat :=
  if n <= 1 then 1
  else if IsPrimePow n then n.minFac
       else
           if ∃ p q , Prime p  ∧  p ∣ n ∧  Prime q ∧  q ∣ n ∧  ¬ (p = q) --failed to synthesize
                 then if  p^(n.factorization p) < q^(n.factorization q)
                      then my_langg (n/p^(n.factorization p))
                      else my_langg (n/q^(n.factorization q))
          else 1
  termination_by n
  decreasing_by sorry -- p^(n.factorization p) >1 and divides??

After this hurdle is the hurdle of showing decreasing_by; is there an example which uses the list of the factorization of n ?

[Kim Morrison]

#mwe

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

If I could get the example working, I would not have the question. Here is a longer version:

import Mathlib

open scoped Nat

def my_f  ( n :  Nat ) : Nat :=
  if IsPrimePow n then n.minFac
  else
      if ∃ p q , Prime p ∧ p ∣ n ∧  Prime q ∧  q ∣ n ∧  ¬ (p = q)
      then if  p^(n.factorization p) < q^(n.factorization q)
          then my_f (n / p^(n.factorization p))
          else my_f (n / q^(n.factorization q))
      else 1
  termination_by n

This again fails to synthesize at "exists p q ...". There are other issues such as p and q not being defined, but the first line with problems has "exists".

[Robin Arnez]

Do I understand correctly that you are trying to define https://oeis.org/A088387? In that case, why not do something like

import Mathlib

def mostSignificantPrimeFactor (n : ℕ) : ℕ :=
  n.primeFactors.image (fun p => p ^ n.factorization p) |>.max.getD 1 |>.minFac

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

@Robin Arnez , because of ignorance, because I am still at the beginning of my journey, and because I am also concerned about whether Lean can prove termination for me. However, I will try your suggestion. Thanks

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

Also, I am interested in recursive definitions. If you have a similar shorthand for lcmint(n) == least common multiple of integers from [1,n], I would also be interested in that.

[Snir Broshi]

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

If you have a similar shorthand for lcmint(n) == least common multiple of integers from [1,n], I would also be interested in that.

https://alexkontorovich.github.io/PrimeNumberTheoremAnd/docs/PrimeNumberTheoremAnd/Lcm.html#Lcm.L

[Snir Broshi]

btw if you're proving something about how this LCM grows (e.g. ≥ 2^n or Θ(e^O(n))) I'd be interested to know

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

Actually, I am using the lcm as an upper bound for a different argument. However, next on my todo list is product of primes in (j,k] is less than 4^(k-j) (for certain values of k and j).

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

Also, in Alex's (repo containing the) definition of L, why have _root_.id ?

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

If you want a diversion, I am willing to share Aristotle's version of lcmint. (It is quite a bit longer, and I don't want to read its proof that lcmint(n) = lcm(1,...,n).)

[Robin Arnez]

You mean why the _root_? Well, there's a conflict with ArithmeticFunction.id

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

Oh. Why is the .id needed? to resolve the term to a Nat ?

[Robin Arnez]

You mean why there's a function there at all? Well, that's just in the definition of docs#Finset.lcm. Think of it as $\text{lcm}_{x \in \{1, ..., n\}} \text{id}(x)$. You could also write fun x => x but id is shorter.

[Snir Broshi]

This lets you use the set only as an indexing set to what you're actually taking the LCM of, because you may want to have duplicates and a set doesn't allow that

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

AH. Thumbs up since I can't find the emoji for enlightenment. Thanks.

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

Doesn't Mathlib have a nice upper bound for (what I am calling) lcmint(n) ?

[Snir Broshi]

By what expression approximately? You can bound it by a factorial

[Snir Broshi]

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

Also, in Alex's (repo containing the) definition of L, why have _root_.id ?

btw this is Alex's repo but Terry Tao's definition

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

Well I can poorly bound it by $4^{n + c\sqrt{n}}$, and Erd{\o}s can do better with elementary means. However I thought it would have a good bound in MathLib (at least log(lcmint(n)) should be bounded by a constant in Mathlib).

[Aaron Liu]

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

This again fails to synthesize at "exists p q ...".

The error message is:

failed to synthesize instance of type class
  Decidable (∃ p q, Prime p ∧ p ∣ n ∧ Prime q ∧ q ∣ n ∧ ¬p = q)

You have an if-then-else statement. In order to decide which branch to take at runtime, Lean has to have a way of figuring out whether the condition you provided is true or false (it has to synthesize a docs#Decidable instance). But for the condition you provided (∃ p q, ...) Lean was unable to do this automatically.

[Snir Broshi]

Sure you can open Classical in but then you have more errors because that def needs to extract the p and q from the Exists

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

OK. If I wanted to do a recursive definition of my_f, and I needed to introduce p and q, how would that be done?

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

I tried a version using .minFac (to avoid introducing p and q) but it got real ugly real fast.

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

Also, what would be a reason to prefer a recursive approach as opposed to the nice streamlined approaches suggested by you (Snir) and Robin? Would it not be easier to prove (in Lean) properties with a recursive definition?

[Snir Broshi]

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

Well I can poorly bound it by $4^{n + c\sqrt{n}}$, and Erd{\o}s can do better with elementary means. However I thought it would have a good bound in MathLib (at least log(lcmint(n)) should be bounded by a constant in Mathlib).

IIUC bounds on it are related to the prime-number-theory so would live in the PNT+ repo, see #general > livestream announcement @ 💬
I suggest asking for this statement in #PrimeNumberTheorem+

[Snir Broshi]

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

Also, what would be a reason to prefer a recursive approach as opposed to the nice streamlined approaches suggested by you (Snir) and Robin? Would it not be easier to prove (in Lean) properties with a recursive definition?

Personally I strive to avoid adding recursive definitions, since it requires proving a lot of basic API about it manually using induction. It's not hard to do so, but defining it in terms of other definitions leads to a better outcome IMO - it gives you access to more API.

[Rushil Raghavan]

This is not built-in anywhere, but for a relatively simple argument that delivers an explicit constant, you could try the proof of Proposition 12 here. I think it would give log(lcm(1,...,n)) < 4log(2)n.

(Actually, never mind, one still needs to control the error term here. I'm not sure if this would be that easy to do with an explicit constant.)

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

@Rushil Raghavan Thanks. For the current project (SSS) I only need that lcm(1..n) is finite, as well as good bounds for small n (n< 10), which I can compute by hand as needed.