Python To Lean4 Translator Agent Skill

Python to Lean4 Translator

Translate Python programs into equivalent, executable Lean4 code while preserving program semantics and ensuring type safety.

Overview

This skill provides systematic guidance for translating Python code to Lean4, handling type inference, function translations, data structures, control flow, and ensuring well-typed, executable output.

Translation Workflow

Python Input → Analyze Structure → Map Types → Translate Constructs → Verify → Output Lean4
    ├─ Identify types and signatures
    ├─ Map Python constructs to Lean4 equivalents
    ├─ Handle type conversions
    ├─ Ensure totality and termination
    └─ Validate executability

Core Translation Principles

1. Type Safety First

Lean4 is strongly typed. Every translation must:

• Infer or specify explicit types for all variables
• Ensure type consistency across operations
• Handle Python's dynamic typing by choosing appropriate Lean4 types
• Use Option for nullable values, Except for error handling

2. Preserve Semantics

The translated code must maintain the same computational behavior, preserve function input-output relationships, keep the same algorithmic complexity, and handle edge cases equivalently.

3. Ensure Executability

Generated Lean4 code must compile without errors, be executable (use #eval to verify), terminate (prove termination for recursive functions), and follow Lean4 syntax and conventions.

Type Mapping Reference

Basic Types

| Python Type | Lean4 Type | Notes |

|------------|-----------|-------|

| int | Int or Nat | Use Nat for non-negative integers |

| float | Float | Lean4's floating point type |

| bool | Bool | Direct mapping |

| str | String | Direct mapping |

| None | Option α | Use none for None, some x for values |

| list | List α | Homogeneous lists |

| tuple | Product types α × β or custom structure | |

| dict | Std.HashMap or List (α × β) | Requires import |

| set | Std.HashSet or List α | Requires import |

For detailed type system information, see references/type_mappings.md.

Translation Patterns

Functions

Simple function:

def add(a: int, b: int) -> int:
    return a + b

Lean4:

def add (a : Int) (b : Int) : Int :=
  a + b

Recursive function:

def factorial(n: int) -> int:
    if n <= 1:
        return 1
    else:
        return n * factorial(n - 1)

Lean4:

def factorial (n : Nat) : Nat :=
  if n ≤ 1 then
    1
  else
    n * factorial (n - 1)

Control Flow

If-else:

if condition:
    result = value1
else:
    result = value2

Lean4:

let result := if condition then value1 else value2

For loops (list iteration):

total = 0
for x in items:
    total += x

Lean4 (using fold):

let total := items.foldl (· + ·) 0

List Operations

List comprehension:

squares = [x * x for x in range(10)]

Lean4:

let squares := (List.range 10).map (fun x => x * x)

Filter:

evens = [x for x in numbers if x % 2 == 0]

Lean4:

let evens := numbers.filter (fun x => x % 2 == 0)

Classes and Structures

Python class:

class Rectangle:
    def __init__(self, width: int, height: int):
        self.width = width
        self.height = height

    def area(self) -> int:
        return self.width * self.height

Lean4:

structure Rectangle where
  width : Int
  height : Int

def Rectangle.area (r : Rectangle) : Int :=
  r.width * r.height

Handling Common Challenges

1. Dynamic Typing

Analyze usage to infer types, use sum types for multiple possible types, use Option for nullable values, and document type assumptions.

2. Mutability

Use immutable bindings with let, thread state through function parameters, or use monadic state (StateM) if needed.

3. Exceptions

Convert Python exceptions to Except or Option:

def divide(a: int, b: int) -> float:
    if b == 0:
        raise ValueError("Division by zero")
    return a / b

Lean4:

def divide (a b : Int) : Except String Float :=
  if b = 0 then
    Except.error "Division by zero"
  else
    Except.ok (a.toFloat / b.toFloat)

4. Recursion and Termination

Use structural recursion when possible, add termination_by clause for complex recursion:

def fibonacci (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | n + 2 => fibonacci n + fibonacci (n + 1)
termination_by n

5. Side Effects and I/O

Use IO monad for I/O operations:

def greet(name: str):
    print(f"Hello, {name}!")

Lean4:

def greet (name : String) : IO Unit :=
  IO.println s!"Hello, {name}!"

Translation Process

Step 1: Analyze Python Code

Identify all functions, classes, and global variables. Infer types from usage and annotations. Identify dependencies and imports. Note any dynamic behavior or side effects.

Step 2: Plan Type Mappings

Map Python types to Lean4 types. Identify where Option, Except, or sum types are needed. Plan structure definitions for classes. Determine function signatures.

Step 3: Translate Constructs

Start with data structures (classes → structures). Translate pure functions first. Handle control flow (convert loops to recursion). Translate functions with side effects using IO. Add necessary imports.

Step 4: Ensure Well-Typedness

Add explicit type annotations. Resolve type mismatches. Handle implicit conversions. Add termination proofs for recursive functions.

Step 5: Verify Executability

Check syntax with Lean4 compiler. Test with #eval for simple cases. Verify output matches Python behavior. Document any semantic differences.

Required Imports

Common imports for translated code:

import Std.Data.HashMap
import Std.Data.HashSet
import Init.Data.List.Basic
import Init.Data.Option.Basic

Example Translation

Python:

def is_prime(n: int) -> bool:
    if n < 2:
        return False
    for i in range(2, int(n ** 0.5) + 1):
        if n % i == 0:
            return False
    return True

def primes_up_to(limit: int) -> list[int]:
    return [n for n in range(2, limit + 1) if is_prime(n)]

Lean4:

def isPrime (n : Nat) : Bool :=
  if n < 2 then
    false
  else
    let rec checkDivisors (i : Nat) : Bool :=
      if i * i > n then
        true
      else if n % i = 0 then
        false
      else
        checkDivisors (i + 1)
    checkDivisors 2

def primesUpTo (limit : Nat) : List Nat :=
  (List.range (limit + 1)).drop 2 |>.filter isPrime

-- Test
#eval primesUpTo 20  -- [2, 3, 5, 7, 11, 13, 17, 19]

Best Practices

• Start Simple: Translate simple functions first, then build up to complex ones
• Test Incrementally: Use #eval to test each function as you translate
• Document Assumptions: Note any assumptions about types or behavior
• Preserve Structure: Keep similar code organization when possible
• Use Lean4 Idioms: Prefer pattern matching over if-else chains
• Handle Errors Explicitly: Use Option or Except instead of exceptions
• Prove Termination: Add termination proofs for recursive functions
• Comment Differences: Note where Lean4 behavior differs from Python

Verification Checklist

Before finalizing translation:

• [ ] All types are explicitly specified or correctly inferred
• [ ] Code compiles without errors
• [ ] #eval produces expected results for test cases
• [ ] Recursive functions have termination proofs
• [ ] Error handling uses Option or Except appropriately
• [ ] Side effects are properly wrapped in IO
• [ ] Imports are included
• [ ] Comments explain non-obvious translations

Additional Resources

For complex translations, refer to:

• Type Mappings - Comprehensive type conversion guide
• Common Patterns - Frequently used translation patterns
• Advanced Features - Monads, type classes, and advanced Lean4 features