Flex

A Lean 4 library for a constraint-solving framework for Constrained Horn Clauses (CHCs).

---

Using as a Dependency

Prerequisites

• Lean 4 installed via elan

Step 1 — Add to your lakefile.toml

[[require]]
name = "Flex"
git = "https://github.com/jam-khan/Flex"
rev = "main"

Step 2 — Fetch the dependency

lake update

This clones the repo into .lake/packages/Flex/ using your local Git credentials.

Step 3 — Build

lake build

Note: Flex is mathlib-free — the only dependency is aesop (built from source on the first build).

---

Importing

A single import gives you everything:

import Flex

This includes all core types, tactics, elaboration, and the solver.

Example

import Flex

def ex1 : Prop :=
  ∃ κ : Int → Prop,
    ∀ x : Int,
      0 ≤ x →
      (∀ ν : Int, ν = x - 1 → κ ν)
    ∧ (∀ y : Int, κ y →
        ∀ ν : Int, ν = y + 1 → 0 ≤ ν)

See the Demo/ folder for more worked examples.