Imperative to Coq Model Extractor

Overview

Extract abstract mathematical models from imperative code that can be used for formal reasoning and verification in Coq. This skill transforms imperative programs into functional Coq definitions with explicit state modeling, enabling formal proofs about program behavior.

Extraction Workflow

Step 1: Analyze Imperative Code

Understand the program structure and semantics:

1. Identify components:

   • Functions and their signatures
   • Data structures and types
   • State and mutable variables
   • Control flow (loops, conditionals)
   • Side effects and I/O

2. Understand semantics:

   • What does the program compute?
   • What state does it maintain?
   • What are the invariants?
   • What are preconditions and postconditions?

3. Note modeling challenges:

   • Mutable state
   • Imperative loops
   • Pointers and memory
   • Side effects

Step 2: Design Coq Model Structure

Plan the Coq representation:

1. Choose appropriate types:

   • Z for arbitrary precision integers
   • nat for natural numbers
   • bool for booleans
   • list for sequences
   • Record for structured state
   • Inductive types for enumerations

2. Model state explicitly:

   • Pure functions: Direct translation
   • Mutable state: State transformation functions
   • Side effects: Explicit state passing

3. Plan control flow translation:

   • Conditionals → Pattern matching or if-then-else
   • Loops → Recursive functions (Fixpoint)
   • Early returns → Conditional expressions

Step 3: Extract Core Model

Translate imperative constructs to Coq:

Pattern: Pure function

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

(* Coq Model *)
Definition add (a b : Z) : Z := a + b.

Pattern: Function with state

// Imperative
int counter = 0;
void increment() {
    counter++;
}

(* Coq Model *)
Definition counter_state : Type := Z.
Definition increment (c : counter_state) : counter_state := c + 1.

Pattern: Loop → Recursion

// Imperative
int sum(int n) {
    int total = 0;
    for (int i = 0; i < n; i++) {
        total += i;
    }
    return total;
}

(* Coq Model *)
Fixpoint sum_aux (n i total : nat) : nat :=
  match n with
  | 0 => total
  | S n' =>
      if i <? n then
        sum_aux n (S i) (total + i)
      else
        total
  end.

Definition sum (n : nat) : nat := sum_aux n 0 0.

Step 4: Add Specifications

Enhance the model with formal specifications:

1. Function specifications:

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

2. Loop invariants:

   (* Invariant: sum = sum of first i elements *)
   Lemma sum_invariant : forall n i total,
     i <= n ->
     sum_aux n i total = total + (sum of 0..i-1).
   Proof.
     (* Proof by induction *)
   Admitted.
   

3. Correctness properties:

   Lemma sum_correct : forall n,
     sum n = n * (n - 1) / 2.
   Proof.
     (* Proof *)
   Admitted.
   

Step 5: Verify and Test

Ensure the model is correct:

1. Type check:

   coqc model.v
   

2. Test with examples:

   Compute add 2 3.        (* Should output 5 *)
   Compute sum 5.          (* Should output 10 *)
   

3. Compare semantics:

   • Run original imperative program
   • Evaluate Coq model
   • Verify outputs match

Step 6: Refine and Document

Improve the extracted model:

1. Simplify definitions:

   • Use standard library functions
   • Remove redundant constructs
   • Factor out common patterns

2. Add documentation:

   (* Computes the absolute value of an integer *)
   Definition abs (n : Z) : Z := ...
   

3. Organize proofs:

   • Group related lemmas
   • Add proof sketches
   • Document proof strategies

Common Extraction Patterns

For detailed patterns, see extraction_patterns.md.

Quick Reference

Examples

Example 1: Simple Algorithm

Imperative Input (C):

int factorial(int n) {
    int result = 1;
    while (n > 1) {
        result *= n;
        n--;
    }
    return result;
}

Coq Model:

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

Lemma factorial_positive : forall n,
  factorial n >= 1.
Proof.
  induction n.
  - simpl. lia.
  - simpl. lia.
Qed.

Example 2: Array Processing

Imperative Input (Python):

def find_max(arr):
    max_val = arr[0]
    for i in range(1, len(arr)):
        if arr[i] > max_val:
            max_val = arr[i]
    return max_val

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.

Lemma find_max_in_list : forall l default,
  l <> [] ->
  In (find_max l default) l.
Proof.
  (* Proof by induction *)
Admitted.

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

Example 3: Stateful Program

Imperative Input (Java):

class Counter {
    private int count = 0;

    public void increment() {
        count++;
    }

    public int getCount() {
        return count;
    }
}

Coq Model:

Record CounterState : Type := mkCounter {
  count : nat
}.

Definition init_counter : CounterState := {|
  count := 0
|}.

Definition increment (s : CounterState) : CounterState := {|
  count := S s.(count)
|}.

Definition getCount (s : CounterState) : nat :=
  s.(count).

(* Specification *)
Lemma increment_increases : forall s,
  getCount (increment s) = S (getCount s).
Proof.
  intros s. unfold increment, getCount. simpl. reflexivity.
Qed.

Example 4: Binary Search

Imperative Input (C++):

int binary_search(int arr[], int n, int target) {
    int left = 0, 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.