Examples Gallery
The ImandraX examples repository contains 23 verified examples covering algorithms, mathematical theorems, hardware verification, and more. All examples are written in IML and can be run in the VS Code extension.
Sorting algorithms
| Example | Description | Key techniques |
|---|---|---|
| Insertion Sort | Proves sortedness and element preservation | Rewrite rules, automatic induction |
| Merge Sort | Full correctness with both automatic and manual proofs | Custom measures, forward chaining, manual tactics |
| Quick Sort | Correctness via partition into "smalls" and "bigs" | Forward-chaining length lemmas |
Mathematical theorems
| Example | Description | Key techniques |
|---|---|---|
| Pigeon Hole Principle | For arbitrary-length lists — contrast with SAT/resolution! | Generalization, lemma instantiation |
| Cantor's Pairing | Bijection from ℕ × ℕ to ℕ | Arithmetic reasoning |
| Coins (3s and 5s) | Any integer ≥ 8 is a sum of 3s and 5s | Constructive proofs |
| Summation Identities | Closed forms for ∑(4k-1), ∑k, ∑k³ | Arithmetic induction |
| Farkas' Lemma | Proof checker for polynomial constraints | Nonlinear arithmetic |
| Bags (Multisets) | Library of multiset operations and theorems | Rich library development |
| Permutations | Permutation via mutual subbag inclusion | Imports, compositional reasoning |
| Fulcrum Theorems | Bounds on the balance-point problem | Arithmetic bounds |
Algorithms
| Example | Description | Key techniques |
|---|---|---|
| Boyer-Moore Majority Vote | MJRTY algorithm correctness and uniqueness | Strategic lemma usage |
| Ackermann's Function | Relationship between Ackermann and Peter's versions | Lexicographic termination |
| Towers of Hanoi | Solver correctness | Recursive algorithm verification |
| Gilbreath's Card Trick | Mathematical card trick — lineage: de Bruijn → Huet → Moore → Boyer → Passmore | Historical proof chain |
| Tautology Checker | SAT solver via if-normalization (Boyer-Moore '79) | Decision procedure verification |
| Mutilated Chessboard | Classic impossibility theorem | Combinatorial reasoning |
Compilers & machines
| Example | Description | Key techniques |
|---|---|---|
| Expression Compiler | Compiler from expressions to a stack machine | Custom induction schemes |
| Stack Machine | Machine with registers and a loop program computing 1+2+...+n | Machine verification |
Hardware verification
| Example | Description | Key techniques |
|---|---|---|
| Ripple-Carry Adder | Full adder correctness for arbitrary bit widths | Automatic induction, bit-level reasoning |
Control systems
| Example | Description | Key techniques |
|---|---|---|
| Vehicle Controller | Boyer-Green-Moore feedback controller under bounded disturbance | Control system verification |
Data structures
| Example | Description | Key techniques |
|---|---|---|
| Tree Flattening | Tail-recursive flatten equals naive flatten | Classic induction benchmark |
Learning ImandraX
| Example | Description | Key techniques |
|---|---|---|
| Simplification Examples | Demonstrates [%simp], [%simp_only], [%norm] | Tactic language tutorial |