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:
2. Functions and their signatures
3. Data structures (structs, classes, arrays)
4. Control flow patterns (loops, conditionals)
5. Memory management (allocation, pointers)
6. I/O operations
7. Dependencies and includes

1. Understand semantics:
2. What does the program compute?
3. What are the inputs and outputs?
4. Are there side effects?
5. What are the invariants and preconditions?

1. Note translation challenges:
2. Pointer arithmetic
3. Mutable state
4. Imperative loops
5. Manual memory management
6. Undefined behavior

Step 2: Design Lean4 Structure

Plan the Lean4 equivalent before writing code:

1. Choose appropriate types:
2. Int for signed integers
3. Nat for unsigned integers and array indices
4. Float for floating-point numbers
5. Array for dynamic arrays
6. List for linked lists
7. Custom structure types for structs/classes

1. Determine purity:
2. Pure functions: return values directly
3. Side effects: use IO monad
4. Mutable state: use IO.Ref or ST monad

1. Plan control flow translation:
2. Loops → Recursive functions
3. Mutable variables → Function parameters
4. Early returns → Conditional expressions

1. Handle memory:
2. Stack allocation → Direct values
3. Heap allocation → Automatic memory management
4. 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:
2. Use Nat for non-negative values (array indices, counts)
3. Use Int for potentially negative values
4. Convert explicitly: n.toNat, n.toInt

1. Array bounds:
2. Lean4 requires proof of valid indices
3. Use safe accessors: arr.get?, arr[i]?
4. Or use arr[i]! with runtime check

1. Division:
2. Natural number division: n / m (rounds down)
3. Integer division: use Int.div
4. Handle division by zero explicitly

1. Type annotations:
2. Add explicit types when inference fails
3. Use : Type for clarity

Step 5: Test and Verify

Ensure the translated code works correctly:

1. Compile check:

``bash lake build ``

1. Create test cases:

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

1. Compare outputs:
2. Run original C/C++ program
3. Run translated Lean4 program
4. Verify outputs match for same inputs

1. Handle edge cases:
2. Empty arrays
3. Zero values
4. Negative numbers
5. Boundary conditions

Step 6: Optimize and Refine

Improve the translated code:

1. Use Lean4 idioms:
2. Replace manual recursion with List.foldl, Array.foldl
3. Use pattern matching instead of nested if-else
4. Leverage standard library functions

1. Add documentation:

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

1. Consider performance:
2. Use tail recursion for loops
3. Prefer Array over List for random access
4. Use @[inline] for small functions

Common Translation Patterns

For detailed patterns, see [translation_patterns.md](references/translation_patterns.md).

Quick Reference

| C/C++ | Lean4 | |-------|-------| | int x | def x : Int | | unsigned int x | def x : Nat | | float x | def x : Float | | bool x | def x : Bool | | char* str | def str : String | | int arr[] | def arr : Array Int | | struct S | structure S where | | for (...) | let rec loop ... | | while (...) | let rec loop ... | | if (...) {...} | if ... then ... else ... | | switch (...) | match ... with | | return x | x (last expression) | | void f() | def f : IO Unit | | printf(...) | IO.println ... |

Examples

Example 1: Simple Algorithm

C/C++ Input:

int gcd(int a, int b) {
    while (b != 0) {
        int temp = b;
        b = a % b;
        a = temp;
    }
    return a;
}

Lean4 Output:

def gcd (a b : Nat) : Nat :=
  if b = 0 then a
  else gcd b (a % b)

Example 2: Array Processing

C/C++ Input:

int findMax(int arr[], int size) {
    int max = arr[0];
    for (int i = 1; i < size; i++) {
        if (arr[i] > max) {
            max = arr[i];
        }
    }
    return max;
}

Lean4 Output:

def findMax (arr : Array Int) : Option Int :=
  if arr.isEmpty then
    none
  else
    some (arr.foldl max arr[0]!)

Example 3: Struct with Methods

C/C++ Input:

struct Rectangle {
    int width;
    int height;

    int area() {
        return width * height;
    }

    int perimeter() {
        return 2 * (width + height);
    }
};

Lean4 Output:

structure Rectangle where
  width : Nat
  height : Nat
  deriving Repr

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

def Rectangle.perimeter (r : Rectangle) : Nat :=
  2 * (r.width + r.height)

Example 4: I/O Program

C/C++ Input:

#include <stdio.h>

int main() {
    int n;
    printf("Enter a number: ");
    scanf("%d", &n);
    printf("Factorial: %d\n", factorial(n));
    return 0;
}

Lean4 Output:

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

def main : IO Unit := do
  IO.print "Enter a number: "
  let input ← IO.getStdIn >>= (·.getLine)
  match input.trim.toNat? with
  | some n =>
    IO.println s!"Factorial: {factorial n}"
  | none =>
    IO.print