Refinement Step Generator

Generate systematic refinement steps that transform high-level specifications into concrete, executable implementations while preserving correctness through formal proofs.

Overview

Refinement is the process of transforming abstract specifications into concrete implementations through a series of correctness-preserving steps. Each refinement step:

Makes the specification more concrete (closer to executable code)
Preserves correctness through formal proof obligations
Maintains a clear abstraction relation between levels
Can be verified independently

This skill provides guidance for generating refinement steps in Isabelle/HOL and Coq.

Refinement Workflow

Abstract Specification
    ↓ [Data Refinement]
Refined Data Structures
    ↓ [Algorithmic Refinement]
Concrete Algorithm
    ↓ [Implementation Refinement]
Executable Code

Each arrow represents a refinement step with proof obligations.

Core Refinement Types

1. Data Refinement

Transform abstract data types into concrete data structures.

Example: Set → List

Abstract (Isabelle):

definition insert_set :: "'a ⇒ 'a set ⇒ 'a set" where
  "insert_set x S = S ∪ {x}"

definition member_set :: "'a ⇒ 'a set ⇒ bool" where
  "member_set x S = (x ∈ S)"

Concrete (Isabelle):

definition insert_list :: "'a ⇒ 'a list ⇒ 'a list" where
  "insert_list x xs = (if x ∈ set xs then xs else x # xs)"

definition member_list :: "'a ⇒ 'a list ⇒ bool" where
  "member_list x xs = (x ∈ set xs)"

Abstraction Relation:

definition abs_list :: "'a list ⇒ 'a set" where
  "abs_list xs = set xs"

Proof Obligations:

lemma insert_refines:
  "abs_list (insert_list x xs) = insert_set x (abs_list xs)"
  by (simp add: insert_list_def insert_set_def abs_list_def)

lemma member_refines:
  "member_list x xs = member_set x (abs_list xs)"
  by (simp add: member_list_def member_set_def abs_list_def)

2. Algorithmic Refinement

Transform specifications into algorithms.

Example: Sorting Specification → Insertion Sort

Abstract (Coq):

Definition is_sorted (l : list nat) : Prop :=
  forall i j, i < j < length l → nth i l 0 ≤ nth j l 0.

Definition sort_spec (input output : list nat) : Prop :=
  is_sorted output ∧ Permutation input output.

Concrete (Coq):

Fixpoint insert (x : nat) (l : list nat) : list nat :=
  match l with
  | [] => [x]
  | h :: t => if x <=? h then x :: l else h :: insert x t
  end.

Fixpoint insertion_sort (l : list nat) : list nat :=
  match l with
  | [] => []
  | h :: t => insert h (insertion_sort t)
  end.

Proof Obligations:

Theorem insertion_sort_correct : forall l,
  sort_spec l (insertion_sort l).
Proof.
  (* Prove is_sorted and Permutation properties *)
Qed.

3. Implementation Refinement

Transform algorithms into efficient implementations.

Example: Naive → Optimized

Abstract:

definition naive_reverse :: "'a list ⇒ 'a list" where
  "naive_reverse xs = rev xs"

Concrete (tail-recursive):

fun reverse_acc :: "'a list ⇒ 'a list ⇒ 'a list" where
  "reverse_acc [] acc = acc" |
  "reverse_acc (x # xs) acc = reverse_acc xs (x # acc)"

definition efficient_reverse :: "'a list ⇒ 'a list" where
  "efficient_reverse xs = reverse_acc xs []"

Proof Obligation:

lemma efficient_reverse_correct:
  "efficient_reverse xs = naive_reverse xs"
  by (simp add: efficient_reverse_def naive_reverse_def reverse_acc_correct)

Refinement Process

Step 1: Identify Abstraction Gap

Analyze the specification and identify what needs refinement:

Data structures: Abstract types (sets, maps) → Concrete structures (lists, trees)
Operations: Non-deterministic specs → Deterministic algorithms
Complexity: Inefficient → Efficient implementations

Step 2: Choose Refinement Strategy

Select appropriate refinement approach:

Data Refinement:

Define concrete data type
Define abstraction function
Prove operations preserve abstraction

Algorithmic Refinement:

Provide concrete algorithm
Prove algorithm satisfies specification
Maintain invariants

Compositional Refinement:

Refine components independently
Compose refinements
Prove composition preserves correctness

Step 3: Define Abstraction Relation

Establish connection between abstract and concrete levels:

Isabelle:

definition abs_rel :: "'concrete ⇒ 'abstract ⇒ bool" where
  "abs_rel c a = (abs_fun c = a)"

Coq:

Definition abs_rel (c : concrete) (a : abstract) : Prop :=
  abs_fun c = a.

Step 4: Generate Proof Obligations

For each operation, prove refinement correctness:

Forward Simulation:

If: abs_rel c a
    op_concrete c = c'
Then: ∃a'. op_abstract a = a' ∧ abs_rel c' a'

Backward Simulation:

If: abs_rel c a
    op_abstract a = a'
Then: ∃c'. op_concrete c = c' ∧ abs_rel c' a'

Step 5: Prove Obligations

Use proof tactics to discharge obligations:

Isabelle:

auto, simp, blast for automation
induction for recursive structures
case_tac for case analysis

Coq:

auto, simpl, reflexivity for automation
induction for recursive proofs
destruct for case analysis

Framework-Specific Guidance

Isabelle/HOL Refinement

For Isabelle-specific patterns and the Autoref framework, see references/isabelle_refinement.md.

Key features:

Refinement framework with ⊑ relation
Autoref for automatic refinement
Sepref for imperative refinement
Code generation support

Coq Refinement

For Coq-specific patterns and refinement tactics, see references/coq_refinement.md.

Key features:

Program for refinement with obligations
Equations for well-founded recursion
Refinement types
Extraction to OCaml/Haskell

Common Refinement Patterns

For detailed refinement patterns (data structures, algorithms, optimizations), see references/refinement_patterns.md.

Common patterns include:

Set → List/Tree refinement
Map → Association list/Hash table
Non-deterministic choice → Deterministic selection
Specification → Divide-and-conquer algorithm
Naive → Tail-recursive implementation

Example: Complete Refinement

Abstract Specification (Isabelle):

definition find_spec :: "'a list ⇒ ('a ⇒ bool) ⇒ 'a option" where
  "find_spec xs P = (if ∃x ∈ set xs. P x
                     then Some (SOME x. x ∈ set xs ∧ P x)
                     else None)"

Refinement Step 1: Deterministic Algorithm

fun find_impl :: "'a list ⇒ ('a ⇒ bool) ⇒ 'a option" where
  "find_impl [] P = None" |
  "find_impl (x # xs) P = (if P x then Some x else find_impl xs P)"