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

1. Understand semantics:

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

1. 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

1. Determine purity:

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

1. Plan control flow translation:

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

1. 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 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  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 

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 >= (·.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 [translationpatterns.md](references/translationpatterns.md) for comprehensive pattern catalog
• Lean4 documentation: https://lean-lang.org/documentation/
• Lean4 standard library: https://github.com/leanprover/lean4/tree/master/src/Init

Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

• Author: ArabelaTso
• Source: ArabelaTso/Skills-4-SE
• License: Apache-2.0
• Homepage: https://ArabelaTso.github.io/Skills-4-SE/

Install and usage instructions live in the source repository linked above.