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.println "Invalid input"

Best Practices

1. Start simple: Translate basic functions first, then build up complexity
2. Preserve semantics: Ensure the Lean4 code computes the same results
3. Use types wisely: Leverage Lean4's type system for correctness
4. Embrace immutability: Prefer pure functions over mutable state
5. Test thoroughly: Verify outputs match for various inputs
6. Document assumptions: Note any semantic differences or limitations
7. Leverage standard library: Use built-in functions when available
8. Handle errors gracefully: Use Option or Except for error cases

Limitations and Considerations

1. Undefined behavior: C/C++ undefined behavior must be handled explicitly in Lean4
2. Performance: Functional code may have different performance characteristics
3. Concurrency: C/C++ threading requires different approaches in Lean4
4. Low-level operations: Bit manipulation and pointer arithmetic need careful translation
5. External libraries: C/C++ library calls may not have direct Lean4 equivalents
6. Macros: C preprocessor macros need manual translation
7. Templates: C++ templates translate to Lean4 generics differently

Resources

• Translation patterns: See [translation_patterns.md](references/translation_patterns.md) for comprehensive pattern catalog
• Lean4 documentation: https://lean-lang.org/documentation/
• Lean4 standard library: https://github.com/leanprover/lean4/tree/master/src/Init