Add LEAN formula generation support for nrt operation

[Copilot]

The formula generator maps nrt operations to sqrtint (n=2) and sqrtnint (n≥3) functions, but LEAN export failed on programs containing these functions.

Changes

• sqrtint: Maps to LEAN's Nat.sqrt with Int/Nat conversions: Int.ofNat (Nat.sqrt (Int.toNat x))
• sqrtnint: Maps to LEAN's Nat.nthRoot from Mathlib.Data.Nat.NthRoot.Defs: Int.ofNat (Nat.nthRoot (Int.toNat n) (Int.toNat x))

Example

-- Square root
def a (n : Int) : Int := Bool.toInt (((Int.ofNat (Nat.sqrt (Int.toNat n)))^2)==n)

-- Cube root
def a (n : Int) : Int := Bool.toInt (((Int.ofNat (Nat.nthRoot (Int.toNat 3) (Int.toNat n)))^3)==n)

Both functions require provably non-negative inputs, consistent with LODA nrt semantics.

Tests

Added formula tests for nrt operations:

• A010052: Characteristic function of perfect squares - tests sqrtint

• A999998: Characteristic function of perfect cubes - tests sqrtnint

• Fixes loda-lang/loda-cpp#553

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Support "nrt" operation in LEAN formula generation</issue_title> <issue_description>The general FormulaGenerator maps nrt operations to sqrtint or sqrtnint functions. Extend the LEAN formula generator to also support such programs/functions. Figure out whether LEAN has native support for it, or if there are modules for this, or if we can add ad-hoc function definitions to the generated code.</issue_description>

Comments on the Issue (you are @copilot in this section)

• Fixes loda-lang/loda-cpp#553

---

💡 You can make Copilot smarter by setting up custom instructions, customizing its development environment and configuring Model Context Protocol (MCP) servers. Learn more Copilot coding agent tips in the docs.

[ckrause]

@copilot Can you use Nat.nthRoot instead of creating a helper function? Please also add formula tests.

[Copilot]

@copilot Can you use Nat.nthRoot instead of creating a helper function? Please also add formula t...

Done! Changed to use Nat.nthRoot from Mathlib.Data.Nat.NthRoot.Defs instead of the custom helper function. Also added formula tests for A010052 (squares) and A999998 (cubes). Commit: bbf4743

[loader3229]

Please rename A999998 in the check to A010057