LeanDatabase

Formalising Relational Databases in Lean 4

Summer School : LeanLang for Programming • July 2026 • IISc Bangalore • Organised by Emergence India Labs

CONTRIBUTORS Project Team

Siddhartha Gadgil
Anirudh Gupta
Ajay Kumar Nair
Dattabhasvant Gadiyaram

GitHub Logo

Github Repository: siddhartha-gadgil/LeanDatabase

WHAT? Relational Databases and SQL

A lot of information in the world is stored in relational databases — think of your bank account, your social media feed, or the data behind a web app.

The way we interact with relational databases is through SQL queries, which are used to retrieve, manipulate, and analyze data.

SQL is the lingua franca of data science, data engineering, and analytics.

It is the most widely used language for interacting with structured data. In short, it is the language in which we talk to the databases that power our digital world.

SELECT customer_id, SUM(amount) AS total_spent
FROM orders
WHERE status = 'paid'
GROUP BY customer_id;

WHY? SQL Querying

Almost always there is more than one way to write a query that returns the same result.

You might want to rewrite a query to make it more performance-efficient, or to make it easier to read.

One might use an LLM to rewrite a query, but how do you know the rewritten query is equivalent to the original?

HOW? Proving SQL Equivalence in Lean

Here are some examples of SQL queries that are equivalent, but not obviously so. We will show how our Lean formalisation can prove their equivalence.

1

table

Column	Type
`age`	`INT`
`isActive`	`BOOL`
`height`	`FLOAT`

SELECT * FROM table
WHERE NOT (age > 30 OR isActive)

≡

SELECT * FROM table
WHERE NOT (age > 30)
  AND NOT isActive

Proof

example :
    sql%([table_schema]) "SELECT * FROM table
                          WHERE NOT (age > 30 OR isActive)"
      = sql%([table_schema]) "SELECT * FROM table
                              WHERE NOT (age > 30) AND NOT isActive" := by⊢ (fun table =>
    LeanDatabase.restriction
      (fun coords =>
        let table.age := coords 0;
        let table.isActive := coords 1;
        !(decide (table.age > 30) || table.isActive))
      table) =
  fun table =>
  LeanDatabase.restriction
    (fun coords =>
      let table.age := coords 0;
      let table.isActive := coords 1;
      !decide (table.age > 30) && !table.isActive)
    table
  sql_equivAll goals completed! 🐙

2

r1

Column	Type
`is_high_value`	`BOOL`
`val`	`INT`

r2

Column	Type
`is_high_value`	`BOOL`
`val`	`INT`

SELECT * FROM
  (SELECT * FROM r1
   UNION
   SELECT * FROM r2)
WHERE is_high_value

≡

SELECT * FROM r1
  WHERE is_high_value
UNION
SELECT * FROM r2
  WHERE is_high_value

Proof

example :
    sql%([r1_schema, r2_schema])
        "SELECT * FROM (SELECT * FROM r1 UNION SELECT * FROM r2) AS u
         WHERE is_high_value"
      = sql%([r1_schema, r2_schema])
        "SELECT * FROM r1 WHERE r1.is_high_value
         UNION
         SELECT * FROM r2 WHERE r2.is_high_value" := by⊢ (fun r1 r2 =>
    LeanDatabase.restriction
      (fun coords =>
        let r1.is_high_value := coords 0;
        r1.is_high_value)
      (LeanDatabase.union r1 r2)) =
  fun r1 r2 =>
  LeanDatabase.union
    (LeanDatabase.restriction
      (fun coords =>
        let r1.is_high_value := coords 0;
        r1.is_high_value)
      r1)
    (LeanDatabase.restriction
      (fun coords =>
        let r2.is_high_value := coords 0;
        r2.is_high_value)
      r2)
  sql_equivAll goals completed! 🐙

3

customers

Column	Type
`customer_id`	`INT`
`name`	`STRING`

orders

Column	Type
`customer_id`	`INT`
`total`	`INT`

SELECT * FROM customers c
WHERE EXISTS (
  SELECT 1 FROM orders o
  WHERE orders.customer_id
      = customers.customer_id)

≡

SELECT * FROM customers c
WHERE customers.customer_id IN (
  SELECT customer_id
  FROM orders)

Proof

example :
    sql%([customers_schema, orders_schema])
        "SELECT * FROM customers
         WHERE EXISTS (SELECT * FROM orders WHERE orders.customer_id = customers.customer_id)"
      = sql%([customers_schema, orders_schema])
        "SELECT * FROM customers
         WHERE customers.customer_id IN (SELECT orders.customer_id FROM orders)" := by⊢ (fun customers orders =>
    LeanDatabase.semijoin customers orders fun coords =>
      let customers.customer_id := coords 0;
      fun orders.coords =>
      let orders.customer_id := orders.coords 0;
      decide (orders.customer_id = customers.customer_id)) =
  fun customers orders =>
  LeanDatabase.semijoin customers orders fun coords =>
    let customers.customer_id := coords 0;
    fun orders.coords =>
    let orders.customer_id := orders.coords 0;
    decide (customers.customer_id = orders.customer_id)
  sql_equivAll goals completed! 🐙

4

employees

Column	Type
`emp_id`	`INT`
`dept_id`	`INT`
`salary`	`INT`

departments

Column	Type
`dept_id`	`INT`
`name`	`STRING`
`budget`	`INT`

SELECT * FROM
  (SELECT * FROM employees
   WHERE salary > 50000) AS e
JOIN departments
  ON e.dept_id
   = departments.dept_id
WHERE departments.budget
    > 100000

≡

SELECT * FROM employees
JOIN departments
  ON employees.dept_id
   = departments.dept_id
WHERE employees.salary
    > 50000
  AND departments.budget
    > 100000

Proof

example :
    sql%([employees_schema, departments_schema])
        "SELECT * FROM (SELECT * FROM employees WHERE salary > 50000) AS e
         JOIN departments ON dept_id = departments.dept_id
         WHERE departments.budget > 100000"
      = sql%([employees_schema, departments_schema])
        "SELECT * FROM employees
         JOIN departments ON employees.dept_id = departments.dept_id
         WHERE employees.salary > 50000 AND departments.budget > 100000" := by⊢ (fun employees departments =>
    LeanDatabase.restriction
      (fun coords =>
        let employees.dept_id := coords 1;
        let departments.dept_id := coords 3;
        let departments.budget := coords 5;
        decide (departments.budget > 100000) && decide (employees.dept_id = departments.dept_id))
      (LeanDatabase.TypedRelationOfList.append
        (LeanDatabase.restriction
          (fun coords =>
            let employees.salary := coords 2;
            decide (employees.salary > 50000))
          employees)
        departments)) =
  fun employees departments =>
  LeanDatabase.restriction
    (fun coords =>
      let employees.dept_id := coords 1;
      let employees.salary := coords 2;
      let departments.dept_id := coords 3;
      let departments.budget := coords 5;
      decide (employees.salary > 50000) && decide (departments.budget > 100000) &&
        decide (employees.dept_id = departments.dept_id))
    (employees.append departments)
  sql_equivAll goals completed! 🐙

5

orders

Column	Type
`order_id`	`INT`
`region`	`STRING`
`amount`	`INT`
`status`	`STRING`

(SELECT * FROM
  (SELECT * FROM orders WHERE region = "US") AS a
 WHERE NOT (NOT (amount > 100)) AND status = "completed")
UNION
(SELECT * FROM
  (SELECT * FROM orders WHERE region = "EU") AS b
 WHERE amount > 100 AND status = "completed")

≡

SELECT * FROM orders
WHERE (region = "US" OR region = "EU")
  AND amount > 100 AND status = "completed"

Proof

example :
    sql%([complex_orders_schema])
        "SELECT * FROM (SELECT * FROM orders WHERE region = \"US\") AS a
         WHERE NOT (NOT (amount > 100)) AND status = \"completed\"
         UNION
         SELECT * FROM (SELECT * FROM orders WHERE region = \"EU\") AS b
         WHERE amount > 100 AND status = \"completed\""
      = sql%([complex_orders_schema])
        "SELECT * FROM orders
         WHERE (region = \"US\" OR region = \"EU\")
           AND amount > 100 AND status = \"completed\"" := by⊢ (fun orders =>
    LeanDatabase.union
      (LeanDatabase.restriction
        (fun coords =>
          let orders.amount := coords 2;
          let orders.status := coords 3;
          !!decide (orders.amount > 100) && decide (orders.status = "completed"))
        (LeanDatabase.restriction
          (fun coords =>
            let orders.region := coords 1;
            decide (orders.region = "US"))
          orders))
      (LeanDatabase.restriction
        (fun coords =>
          let orders.amount := coords 2;
          let orders.status := coords 3;
          decide (orders.amount > 100) && decide (orders.status = "completed"))
        (LeanDatabase.restriction
          (fun coords =>
            let orders.region := coords 1;
            decide (orders.region = "EU"))
          orders))) =
  fun orders =>
  LeanDatabase.restriction
    (fun coords =>
      let orders.region := coords 1;
      let orders.amount := coords 2;
      let orders.status := coords 3;
      (decide (orders.region = "US") || decide (orders.region = "EU")) &&
        (decide (orders.amount > 100) && decide (orders.status = "completed")))
    orders
  sql_equivAll goals completed! 🐙

UNDER THE HOOD How Does This Actually Work?

The real HOW? Architecture

Layer	File(s)	Job
Data model	`TypedRelation.lean`	Tables as typed `Finset`s of rows
Operators	`Operators/*.lean`	`restriction`, `join`, `groupBy`, `select`, …
Parser	`Parser/*.lean`, `SQLSyntax.lean`	SQL text → real Lean terms
Automation	`SQLEquiv.lean`, `SQLToolbox.lean`	The `sql_equiv` tactic + lemma library

ABSTRACTIONS Modeling Tables

A column is encoded in the definition TypedTuple.

-- A row is a dependent function
abbrev TypedTuple (colType : Fin n → Type) :=
  (i : Fin n) → colType i

A table is encoded in the structure TypedRelation.

@[ext]
structure TypedRelation
    (colType : Fin n → Type)
    [∀ i, DecidableEq (colType i)] where
  labels : Fin n → String
  rows   : Finset (TypedTuple colType)

Here is how you can construct an empty Table.

-- The empty relation
def emptyRel {colType : Fin n → Type}
    [∀ i, DecidableEq (colType i)]
    (l : Fin n → String) : TypedRelation colType :=
  { labels := l, rows := ∅ }

OPERATORS Relational Algebra in Lean (1/3)

Union is a simple operator that takes two relations with the same schema and returns a new relation containing all rows from both relations. In Lean, we can define the union of two TypedRelations as follows:

-- Union
@[simp, grind]
def union (r1 r2 : TypedRelation colType) :
    TypedRelation colType :=
  { labels := r1.labels,
    rows   := r1.rows ∪ r2.rows }

OPERATORS Relational Algebra in Lean (2/3)

Restriction is an operator that filters rows from a relation based on a given predicate. In Lean, we can define the restriction of a TypedRelation as follows:

-- Restriction (uses Finset.filter)
@[simp, grind]
def restriction (predicate : TypedTuple colType → Bool)
    (rel : TypedRelation colType) :
    TypedRelation colType :=
  { labels := rel.labels,
    rows   := rel.rows.filter (fun t => predicate t) }

OPERATORS Relational Algebra in Lean (3/3)

Projection is an operator that selects specific columns from a relation based on given indices. In Lean, we can define the projection of a TypedRelation as follows:

-- Projection (uses Finset.image)
@[simp]
def projection {m : Nat} (indices : Fin m → Fin n)
    (rel : TypedRelation colType) :
    TypedRelation (fun j => colType (indices j)) :=

  let _ : ∀ j, DecidableEq (colType (indices j)) :=
    fun _ => inferInstance
  { labels := fun j => rel.labels (indices j),
    rows   := rel.rows.image (fun t j => t (indices j)) }

THEOREMS Proving Properties for Free (1/2)

The following theorem states that a row is in the union of two relations if and only if it is in either of the two relations. This property can be proven using Lean's simp tactic, which simplifies expressions based on the definitions of the operators involved.

@[grind =]
theorem union_row (r1 r2 : TypedRelation colType)
    (row : TypedTuple colType) :
    row ∈ (union r1 r2).rows ↔
    row ∈ r1.rows ∨ row ∈ r2.rows := by
  simp [union, Finset.mem_union]

THEOREMS Proving Properties for Free (2/2)

This theorem states that the union of the restriction of a relation with a predicate and the restriction of the same relation with the negation of that predicate is equal to the original relation. This property can be proven using Lean's simp tactic, which simplifies expressions based on the definitions of the operators involved.

@[grind =]
theorem restriction_partition (p : TypedTuple colType → Bool) (r : TypedRelation colType) :
    union (restriction p r) (restriction (fun t => !p t) r) = r := by
  apply TypedRelation.ext
  · rfl
  · simp only [union, restriction]
    ext t
    simp only [Finset.mem_union, Finset.mem_filter]
    grind

THEOREMS More Verified Properties

@[simp, grind]
def union (r1 r2 : TypedRelation colType) : TypedRelation colType

@[simp, grind]
def restriction (predicate : TypedTuple colType → Bool)
    (rel : TypedRelation colType) : TypedRelation colType

@[grind =]
theorem union_idempotence (r : TypedRelation colType) :
    union r r = r

@[grind =]
theorem union_row (r1 r2 : TypedRelation colType) :
    (union r1 r2).rows = r1.rows ∪ r2.rows

@[grind =]
theorem projection_union {m : Nat} (indices : Fin m → Fin n)
    (r s : TypedRelation colType) :
    projection indices (union r s) =
    union (projection indices r) (projection indices s)

SYNTAX Defining SQL Grammar

syntax
  "SELECT " (" DISTINCT ")? sql_cols
  " FROM " sql_from
  (" WHERE " term)?
  (" GROUP " " BY " ident,* (" HAVING " term)?)?
  (" ORDER " " BY " sql_col,*)?
  (" LIMIT " num)?
  (";")? : sql_query

PARSER From String to AST

def parseSqlQuery
    (tables : List (Name × List (Name × LeanDatabase.SQLTypeProxy)))
    (str : String) : TermElabM (Expr × List (Name × LeanDatabase.SQLTypeProxy)) := do
  let tables := tables.map (fun (tableName, columns) =>
    (tableName, LeanDatabase.schemaWithFullNames tableName columns))
  let .ok stx := runParserCategory (← getEnv) `sql_query str
    | throwError "Failed to parse SQL query: {str}"
  let labels := tables.foldl (fun acc (_, columns) =>
    acc ++ columns.map (fun (name, _) => name)) []
  let stx ← LeanDatabase.expandNames labels stx
  LeanDatabase.elabSqlQuery tables stx

AUTOMATION The `sql_equiv` Tactic

macro "sql_simp" : tactic =>
  `(tactic| simp_all [Finset.filter_filter, Finset.image_image])

macro "sql_equiv" : tactic => `(tactic|
  (repeat (first
     | (apply TypedRelation.ext <;> try rfl)
     | refine Finset.filter_congr (fun _ _ => ?_)
     | refine Finset.image_congr (fun _ _ => ?_)
     | sql_simp
     | (apply funext; intro _))
   all_goals (first
     | grind +locals
     | (apply Finset.ext; sql_simp; grind +locals))))

WHAT'S NEXT Three Directions

Use plausible (counterexample search) as an infrastructure for disproof of equivalences.

SQL Safety Verification: Utilize the formalization of relational databases to automatically verify and check the safety of SQL queries.

Expanded Automation: Prove more theorems and annotate them with simp and grind so that sql_equiv handles as many cases as possible natively, or improve the sql_equiv tactic itself with smart metaprogramming.

Thank You

Questions?

LeanDatabase

CONTRIBUTORS Project Team

WHAT? Relational Databases and SQL

WHY? SQL Querying

HOW? Proving SQL Equivalence in Lean

1

Proof

2

Proof

3

Proof

4

Proof

5

Proof

UNDER THE HOOD How Does This Actually Work?

The real HOW? Architecture

ABSTRACTIONS Modeling Tables

OPERATORS Relational Algebra in Lean (1/3)

OPERATORS Relational Algebra in Lean (2/3)

OPERATORS Relational Algebra in Lean (3/3)

THEOREMS Proving Properties for Free (1/2)

THEOREMS Proving Properties for Free (2/2)

THEOREMS More Verified Properties

SYNTAX Defining SQL Grammar

PARSER From String to AST

AUTOMATION The sql_equiv Tactic

WHAT'S NEXT Three Directions

Thank You

AUTOMATION The `sql_equiv` Tactic