Imperative Code to Coq Model Extraction Patterns

Imperative Code to Coq Model Extraction Patterns

This reference provides detailed patterns for extracting mathematical models from imperative code for reasoning in Coq.

Table of Contents

1. Basic Data Types
2. State and Variables
3. Functions and Procedures
4. Control Flow
5. Data Structures
6. Memory and Pointers
7. Specifications

Basic Data Types

Integers

Imperative Code:

int x = 42;
unsigned int y = 10;

Coq Model:

(* Use Z for arbitrary precision integers *)
Definition x : Z := 42.

(* Use nat for natural numbers *)
Definition y : nat := 10.

Booleans

Imperative Code:

bool flag = true;

Coq Model:

Definition flag : bool := true.

Enumerations

Imperative Code:

enum Color { RED, GREEN, BLUE };

Coq Model:

Inductive Color : Type :=
  | RED : Color
  | GREEN : Color
  | BLUE : Color.

State and Variables

Program State

Imperative Code:

int x = 0;
int y = 0;

void update() {
    x = x + 1;
    y = y * 2;
}

Coq Model:

(* Model state as a record *)
Record State : Type := mkState {
  x : Z;
  y : Z
}.

(* Initial state *)
Definition init_state : State := {|
  x := 0;
  y := 0
|}.

(* State update function *)
Definition update (s : State) : State := {|
  x := s.(x) + 1;
  y := s.(y) * 2
|}.

Mutable Variables

Imperative Code:

counter = 0

def increment():
    global counter
    counter += 1

Coq Model:

(* Model as state transformation *)
Definition counter_state : Type := Z.

Definition init_counter : counter_state := 0.

Definition increment (c : counter_state) : counter_state :=
  c + 1.

Functions and Procedures

Pure Functions

Imperative Code:

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

Coq Model:

Definition add (a b : Z) : Z := a + b.

Functions with Side Effects

Imperative Code:

int global_sum = 0;

void add_to_sum(int x) {
    global_sum += x;
}

Coq Model:

(* Model state explicitly *)
Definition add_to_sum (x : Z) (sum : Z) : Z :=
  sum + x.

(* Or use a state monad *)
Definition add_to_sum_stateful (x : Z) : State -> State :=
  fun s => {| sum := s.(sum) + x |}.

Procedures with Multiple Effects

Imperative Code:

void swap(int *a, int *b) {
    int temp = *a;
    *a = *b;
    *b = temp;
}

Coq Model:

(* Model as tuple transformation *)
Definition swap (ab : Z * Z) : Z * Z :=
  let (a, b) := ab in (b, a).

(* Or with explicit state *)
Record SwapState : Type := mkSwapState {
  a : Z;
  b : Z
}.

Definition swap_state (s : SwapState) : SwapState := {|
  a := s.(b);
  b := s.(a)
|}.

Control Flow

Conditionals

Imperative Code:

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

Coq Model:

Definition max (a b : Z) : Z :=
  if a >? b then a else b.

Loops as Recursion

Imperative Code:

int factorial(int n) {
    int result = 1;
    for (int i = 1; i <= n; i++) {
        result *= i;
    }
    return result;
}

Coq Model:

Fixpoint factorial (n : nat) : nat :=
  match n with
  | 0 => 1
  | S n' => n * factorial n'
  end.

(* Or model the loop state explicitly *)
Record FactState : Type := mkFactState {
  i : nat;
  result : nat
}.

Fixpoint factorial_loop (n : nat) (s : FactState) : nat :=
  match n with
  | 0 => s.(result)
  | S n' =>
      if s.(i) <=? n then
        factorial_loop n' {| i := S s.(i); result := s.(result) * s.(i) |}
      else
        s.(result)
  end.

While Loops

Imperative Code:

int sum_to_n(int n) {
    int sum = 0;
    int i = 0;
    while (i < n) {
        sum += i;
        i++;
    }
    return sum;
}

Coq Model:

(* Model as tail-recursive function *)
Fixpoint sum_to_n_aux (n i sum : nat) : nat :=
  match n with
  | 0 => sum
  | S n' =>
      if i <? n then
        sum_to_n_aux n (S i) (sum + i)
      else
        sum
  end.

Definition sum_to_n (n : nat) : nat :=
  sum_to_n_aux n 0 0.

Data Structures

Arrays

Imperative Code:

int arr[5] = {1, 2, 3, 4, 5};
int sum = 0;
for (int i = 0; i < 5; i++) {
    sum += arr[i];
}

Coq Model:

Require Import List.
Import ListNotations.

Definition arr : list Z := [1; 2; 3; 4; 5].

Fixpoint sum_list (l : list Z) : Z :=
  match l with
  | [] => 0
  | x :: xs => x + sum_list xs
  end.

Definition sum : Z := sum_list arr.

Structs/Records

Imperative Code:

struct Point {
    int x;
    int y;
};

int distance_squared(struct Point p) {
    return p.x * p.x + p.y * p.y;
}

Coq Model:

Record Point : Type := mkPoint {
  x : Z;
  y : Z
}.

Definition distance_squared (p : Point) : Z :=
  p.(x) * p.(x) + p.(y) * p.(y).

Linked Lists

Imperative Code:

struct Node {
    int data;
    struct Node* next;
};

Coq Model:

(* Use Coq's built-in list type *)
Inductive list (A : Type) : Type :=
  | nil : list A
  | cons : A -> list A -> list A.

(* Or define custom inductive type *)
Inductive IntList : Type :=
  | Empty : IntList
  | Node : Z -> IntList -> IntList.

Memory and Pointers

Pointer Dereferencing

Imperative Code:

int get_value(int *ptr) {
    return *ptr;
}

Coq Model:

(* Model memory as a map *)
Require Import FMaps.

Definition Memory := FMap.t Z Z.

Definition get_value (addr : Z) (mem : Memory) : option Z :=
  FMap.find addr mem.

Memory Updates

Imperative Code:

void set_value(int *ptr, int value) {
    *ptr = value;
}

Coq Model:

Definition set_value (addr : Z) (value : Z) (mem : Memory) : Memory :=
  FMap.add addr value mem.

Heap Allocation

Imperative Code:

int* allocate() {
    int* ptr = malloc(sizeof(int));
    *ptr = 42;
    return ptr;
}

Coq Model:

(* Model heap as state with fresh address generation *)
Record HeapState : Type := mkHeapState {
  memory : Memory;
  next_addr : Z
}.

Definition allocate (value : Z) (h : HeapState) : Z * HeapState :=
  let addr := h.(next_addr) in
  let new_mem := FMap.add addr value h.(memory) in
  (addr, {| memory := new_mem; next_addr := addr + 1 |}).

Specifications

Preconditions and Postconditions

Imperative Code:

// Requires: n >= 0
// Ensures: result >= 0
int abs(int n) {
    if (n < 0) return -n;
    else return n;
}

Coq Model:

Definition abs (n : Z) : Z :=
  if n <? 0 then -n else n.

(* Specification *)
Lemma abs_nonneg : forall n : Z,
  abs n >= 0.
Proof.
  intros n.
  unfold abs.
  destruct (n <? 0) eqn:E.
  - (* n < 0 case *)
    apply Z.ltb_lt in E.
    lia.
  - (* n >= 0 case *)
    apply Z.ltb_ge in E.
    lia.
Qed.

Lemma abs_spec : forall n : Z,
  (n >= 0 -> abs n = n) /\ (n < 0 -> abs n = -n).
Proof.
  intros n.
  unfold abs.
  split; intros H.
  - (* n >= 0 *)
    destruct (n <? 0) eqn:E.
    + apply Z.ltb_lt in E. lia.
    + reflexivity.
  - (* n < 0 *)
    destruct (n <? 0) eqn:E.
    + reflexivity.
    + apply Z.ltb_ge in E. lia.
Qed.

Loop Invariants

Imperative Code:

// Invariant: sum = sum of arr[0..i-1]
int array_sum(int arr[], int n) {
    int sum = 0;
    for (int i = 0; i < n; i++) {
        sum += arr[i];
    }
    return sum;
}

Coq Model:

Require Import List.
Import ListNotations.

Fixpoint sum_first_n (l : list Z) (n : nat) : Z :=
  match n, l with
  | 0, _ => 0
  | S n', x :: xs => x + sum_first_n xs n'
  | S n', [] => 0
  end.

Fixpoint array_sum_aux (l : list Z) (i : nat) (sum : Z) : Z :=
  match l with
  | [] => sum
  | x :: xs =>
      if i <? length (x :: xs) then
        array_sum_aux xs (S i) (sum + x)
      else
        sum
  end.

(* Invariant: sum = sum_first_n original_list i *)
Lemma array_sum_invariant : forall l i sum,
  array_sum_aux l i sum = sum + sum_first_n l (length l - i).
Proof.
  (* Proof by induction *)
Admitted.

Functional Correctness

Imperative Code:

// Returns the maximum element in array
int find_max(int arr[], int n) {
    int max = arr[0];
    for (int i = 1; i < n; i++) {
        if (arr[i] > max) {
            max = arr[i];
        }
    }
    return max;
}

Coq Model:

Require Import List.
Import ListNotations.

Fixpoint find_max (l : list Z) (default : Z) : Z :=
  match l with
  | [] => default
  | [x] => x
  | x :: xs => Z.max x (find_max xs default)
  end.

(* Specification: result is in the list *)
Lemma find_max_in_list : forall l default,
  l <> [] ->
  In (find_max l default) l.
Proof.
  (* Proof by induction *)
Admitted.

(* Specification: result is >= all elements *)
Lemma find_max_is_max : forall l default x,
  In x l ->
  x <= find_max l default.
Proof.
  (* Proof by induction *)
Admitted.

Common Patterns

State Machine

Imperative Code:

enum State { IDLE, RUNNING, STOPPED };
enum State current_state = IDLE;

void start() {
    if (current_state == IDLE) {
        current_state = RUNNING;
    }
}

void stop() {
    if (current_state == RUNNING) {
        current_state = STOPPED;
    }
}

Coq Model:

Inductive MachineState : Type :=
  | IDLE : MachineState
  | RUNNING : MachineState
  | STOPPED : MachineState.

Definition start (s : MachineState) : MachineState :=
  match s with
  | IDLE => RUNNING
  | _ => s
  end.

Definition stop (s : MachineState) : MachineState :=
  match s with
  | RUNNING => STOPPED
  | _ => s
  end.

(* Specify valid transitions *)
Inductive valid_transition : MachineState -> MachineState -> Prop :=
  | trans_start : valid_transition IDLE RUNNING
  | trans_stop : valid_transition RUNNING STOPPED
  | trans_stay : forall s, valid_transition s s.

Binary Search

Imperative Code:

int binary_search(int arr[], int n, int target) {
    int left = 0;
    int right = n - 1;
    while (left <= right) {
        int mid = (left + right) / 2;
        if (arr[mid] == target) {
            return mid;
        } else if (arr[mid] < target) {
            left = mid + 1;
        } else {
            right = mid - 1;
        }
    }
    return -1;
}

Coq Model:

Require Import List.
Import ListNotations.

Fixpoint binary_search_aux (l : list Z) (target : Z) (left right : nat) : option nat :=
  match right - left with
  | 0 =>
      match nth_error l left with
      | Some v => if v =? target then Some left else None
      | None => None
      end
  | S _ =>
      if left <=? right then
        let mid := (left + right) / 2 in
        match nth_error l mid with
        | Some v =>
            if v =? target then Some mid
            else if v <? target then
              binary_search_aux l target (S mid) right
            else
              binary_search_aux l target left (mid - 1)
        | None => None
        end
      else None
  end.

Definition binary_search (l : list Z) (target : Z) : option nat :=
  binary_search_aux l target 0 (length l - 1).

(* Specification: if result is Some i, then l[i] = target *)
Lemma binary_search_correct : forall l target i,
  binary_search l target = Some i ->
  nth_error l i = Some target.
Proof.
  (* Proof *)
Admitted.