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/C++
int add(int a, int b) {
    return a + b;
}
```

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

**Pattern: Function with side effects**
```c
// C/C++
void printSum(int a, int b) {
    printf("%d\n", a + b);
}
```

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

#### Control Flow

**Pattern: If-else**
```c
// C/C++
int max(int a, int b) {
    if (a > b) return a;
    else return b;
}
```

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

**Pattern: For loop → Tail recursion**
```c
// C/C++
int sum(int n) {
    int result = 0;
    for (int i = 0; i < n; i++) {
        result += i;
    }
    return result;
}
```

```lean
-- 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/C++
int factorial(int n) {
    int result = 1;
    while (n > 1) {
        result *= n;
        n--;
    }
    return result;
}
```

```lean
-- 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/C++
struct Point {
    int x;
    int y;
};
```

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

**Pattern: Array**
```c
// C/C++
int arr[5] = {1, 2, 3, 4, 5};
```

```lean
-- 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/C++ - Output parameter
void swap(int* a, int* b) {
    int temp = *a;
    *a = *b;
    *b = temp;
}
```

```lean
-- 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:**
   ```bash
   lake build
   ```

2. **Create test cases:**
   ```lean
   #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:**
   ```lean
   /-- 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

## 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` |