Skip to content

README.md

Latest commit

 

History

History
49 lines (30 loc) · 1.97 KB

README.md

File metadata and controls

49 lines (30 loc) · 1.97 KB

Insertion Sort Correctness Proofs in Lean: A Comparison of Different Specifications

This repository contains correctness proofs for Insertion Sort under different specifications in Lean.
The goal is to compare how different specifications affect the structure and difficulty of correctness proofs.
This work was inspired by Verified Functional Algorithms of Software Foundations. For more details, see the accompanying paper Insertion_Sort.pdf

A correctness proof for a sorting algorithm typically involves these two properties:

  1. Sortedness: The output list is sorted.
  2. Content Preservation: The output list contains the same elements as the original list.

We provide two different specifications for each property and prove correctness under each specification. Here is the overall structure:

1. Proof of Sortedness

  1. Inductive Definition
    File: InductiveProof.lean
    Inductive predicate describing sortedness

  2. Index-Based Definition
    File: IndexProof.lean
    A numeric formulation using ∀ i < j, l[i] ≤ l[j]

  3. Equivalence of the Two Definitions
    File: SortedEq.lean

2. Proof of Content Preservation

  1. Permutation-Based Proof
    File: PermProof.lean
    Uses Permutation relation

  2. Multiset-Based Proof
    File: MultisetProof.lean
    Uses the equality of multisets

  3. Equivalence of the Two Approaches
    File: PermEq.lean

References

Software Foundations, Volume 3: Verified Functional Algorithms
Andrew W. Appel et al.
https://softwarefoundations.cis.upenn.edu/vfa-current/toc.html