C Cpp To Lean4 Translator

C/C++ to Lean4 Translator

Overview

Transform C or C++ programs into equivalent Lean4 code that preserves the original semantics while leveraging Lean4's functional programming paradigm, strong type system, and proof capabilities.

Translation Workflow

Step 1: Analyze Input Code

Understand the C/C++ program structure and semantics:

1. Identify program components:

   • Functions and their signatures
   • Data structures (structs, classes, arrays)
   • Control flow patterns (loops, conditionals)
   • Memory management (allocation, pointers)
   • I/O operations
   • Dependencies and includes

2. Understand semantics:

   • What does the program compute?
   • What are the inputs and outputs?
   • Are there side effects?
   • What are the invariants and preconditions?

3. Note translation challenges:

   • Pointer arithmetic
   • Mutable state
   • Imperative loops
   • Manual memory management
   • Undefined behavior

Step 2: Design Lean4 Structure

Plan the Lean4 equivalent before writing code:

1. Choose appropriate types:

   • Int for signed integers
   • Nat for unsigned integers and array indices
   • Float for floating-point numbers
   • Array for dynamic arrays
   • List for linked lists
   • Custom structure types for structs/classes

2. Determine purity:

   • Pure functions: return values directly
   • Side effects: use IO monad
   • Mutable state: use IO.Ref or ST monad

3. Plan control flow translation:

   • Loops → Recursive functions
   • Mutable variables → Function parameters
   • Early returns → Conditional expressions

4. Handle memory:

   • Stack allocation → Direct values
   • Heap allocation → Automatic memory management
   • Pointers → Direct values or references

Step 3: Translate Code

Follow these translation principles:

Functions

Pattern: Pure function

// C/C++
int add(int a, int b) {
    return a + b;
}

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

Pattern: Function with side effects

// C/C++
void printSum(int a, int b) {
    printf("%d\n", a + b);
}

-- Lean4
def printSum (a b : Int) : IO Unit :=
  IO.println (a + b)

Control Flow

Pattern: If-else

// C/C++
int max(int a, int b) {
    if (a > b) return a;
    else return b;
}

-- Lean4
def max (a b : Int) : Int :=
  if a > b then a else b

Pattern: For loop → Tail recursion

// C/C++
int sum(int n) {
    int result = 0;
    for (int i = 0; i < n; i++) {
        result += i;
    }
    return result;
}

-- Lean4
def sum (n : Nat) : Nat :=
  let rec loop (i acc : Nat) : Nat :=
    if i >= n then acc
    else loop (i + 1) (acc + i)
  loop 0 0

Pattern: While loop → Recursion

// C/C++
int factorial(int n) {
    int result = 1;
    while (n > 1) {
        result *= n;
        n--;
    }
    return result;
}

-- Lean4
def factorial (n : Nat) : Nat :=
  let rec loop (n acc : Nat) : Nat :=
    if n <= 1 then acc
    else loop (n - 1) (acc * n)
  loop n 1

Data Structures

Pattern: Struct

// C/C++
struct Point {
    int x;
    int y;
};

-- Lean4
structure Point where
  x : Int
  y : Int
  deriving Repr

Pattern: Array

// C/C++
int arr[5] = {1, 2, 3, 4, 5};

-- Lean4
def arr : Array Int := #[1, 2, 3, 4, 5]

Pointers and References

Key principle: Lean4 doesn't have raw pointers. Translate based on usage:

• Read-only pointers: Pass by value
• Output parameters: Return values (use tuples for multiple returns)
• Mutable references: Use IO.Ref or return new values

// C/C++ - Output parameter
void swap(int* a, int* b) {
    int temp = *a;
    *a = *b;
    *b = temp;
}

-- Lean4 - Return tuple
def swap (a b : Int) : Int × Int :=
  (b, a)

Step 4: Ensure Type Correctness

Lean4's type system is strict. Address common type issues:

1. Integer types:

   • Use Nat for non-negative values (array indices, counts)
   • Use Int for potentially negative values
   • Convert explicitly: n.toNat, n.toInt

2. Array bounds:

   • Lean4 requires proof of valid indices
   • Use safe accessors: arr.get?, arr[i]?
   • Or use arr[i]! with runtime check

3. Division:

   • Natural number division: n / m (rounds down)
   • Integer division: use Int.div
   • Handle division by zero explicitly

4. Type annotations:

   • Add explicit types when inference fails
   • Use : Type for clarity

Step 5: Test and Verify

Ensure the translated code works correctly:

1. Compile check:

   lake build

2. Create test cases:

   #eval add 2 3        -- Should output 5
   #eval factorial 5    -- Should output 120

3. Compare outputs:

   • Run original C/C++ program
   • Run translated Lean4 program
   • Verify outputs match for same inputs

4. Handle edge cases:

   • Empty arrays
   • Zero values
   • Negative numbers
   • Boundary conditions

Step 6: Optimize and Refine

Improve the translated code:

1. Use Lean4 idioms:

   • Replace manual recursion with List.foldl, Array.foldl
   • Use pattern matching instead of nested if-else
   • Leverage standard library functions

2. Add documentation:

   /-- Calculate the sum of first n natural numbers -/
   def sum (n : Nat) : Nat :=
     n * (n + 1) / 2

3. Consider performance:

   • Use tail recursion for loops
   • Prefer Array over List for random access
   • Use @[inline] for small functions