Theoria

Elixir-native proof and specification kernel inspired by Lean's trusted-kernel architecture.

Theoria checks small proof terms generated by Elixir DSLs and domain tools. The goal is not Lean compatibility: the kernel stays native to Elixir, while borrowing the proven shape of theorem-prover architecture — a tiny trusted core, explicit environments, de Bruijn terms internally, and untrusted ergonomics on top.

Elixir 1.19+. The package is experimental: the kernel and validation flow are the focus, while higher-level equation syntax and tactic ergonomics are still being designed.

Installation

def deps do
  [
    {:theoria, "~> 0.2.0"}
  ]
end

Why Theoria

Elixir projects can already express many runtime contracts with tests, types, and static analysis. Theoria adds a small object-language kernel for facts that need proof terms: algebraic laws, recursion equations, indexed-data invariants, and proof-carrying specifications for tools such as analyzers or compilers.

The trusted boundary is deliberately narrow:

• Theoria.Term is the core language.
• Theoria.Kernel checks terms and admits declarations.
• Theoria.Env stores checked constants, definitions, theorems, axioms, inductives, constructors, recursors, and matcher declarations.
• Theoria.Syntax, Theoria.DSL, theorem macros, equation/rewrite/simp helpers, validation builders, and Lean encoding are conveniences only; they generate terms or metadata that the kernel still checks.

Quickstart

Use the quoted term DSL for readable terms and proofs:

import Theoria.DSL

identity_type =
  term do
    forall :a, type(0) do
      a ~> a
    end
  end

identity_proof =
  term do
    lam :a, type(0) do
      lam :x, a do
        x
      end
    end
  end

:ok = Theoria.Kernel.check(Theoria.new_env(), elab!(identity_proof), elab!(identity_type))

Start from the standard prelude when using the built-in libraries:

{:ok, env} = Theoria.Prelude.env()

term =
  term do
    eq(nat(), nat_add(succ(zero), zero), succ(zero))
  end
  |> elab!()

{:ok, _sort} = Theoria.Kernel.infer(env, term)

Theorem modules

The theorem macro defines checked theorem functions while keeping admission explicit:

defmodule MyProofs do
  use Theoria.DSL

  theorem :identity do
    type do
      forall :a, type(0) do
        forall :x, var(:a) do
          var(:a)
        end
      end
    end

    proof do
      lam :a, type(0) do
        lam :x, var(:a) do
          var(:x)
        end
      end
    end
  end
end

{:ok, theorem} = MyProofs.identity_theorem()
MyProofs.__theoria_theorems__()
#=> [:identity]

Validate Theoria's native corpus from Mix:

mix theoria.check
mix theoria.validate --only defeq
mix theoria.validate --axioms
mix theoria.theorems MyApp.Proofs

mix theoria.check is the full native validation entrypoint. It checks theorem modules, definitional-equality checks, and inductive specs against Theoria.Prelude.env/0.

Built-in libraries

The standard prelude loads libraries in dependency order:

Logic → Bool → Nat → List → Vec

Current declarations include:

The built-in theorem corpus currently covers logic, equality, Bool, Nat, List, and Vec facts, including equality symmetry/transitivity/substitution/congruence and recursor computation by reflexivity.

Inductives and recursors

Inductive families are described with structs and admitted through the kernel:

alias Theoria.Inductive
alias Theoria.Inductive.Spec

import Theoria.DSL

spec =
  :Switch
  |> Spec.new(term(do: sort(1)) |> elab!())
  |> Spec.constructor(:on, term(do: const(:Switch)) |> elab!())
  |> Spec.constructor(:off, term(do: const(:Switch)) |> elab!())

{:ok, spec} = Inductive.complete(spec)
{:ok, env} = Theoria.Kernel.add_inductive(Theoria.new_env(), spec)

Admission records Lean-style metadata for type formers, constructors, recursors, and iota rules. Normalization reduces recursors from this metadata rather than by hardcoded names. Indexed recursors such as vec_ind carry index-pattern metadata and reduce when the explicit index arguments match the selected constructor.

Equality transport

Eq.rec is primitive for now and reduces on reflexivity. The untrusted Theoria.Equality helpers build transport terms:

alias Theoria.Equality
alias Theoria.Term

transport =
  Equality.subst(
    Term.const(:Nat),
    Term.lam(:n, Term.const(:Nat), Term.eq(Term.const(:Nat), Term.bvar(0), Term.bvar(0))),
    Term.refl(Term.const(:zero)),
    Term.refl(Term.const(:zero))
  )

The resulting term is not trusted until checked by Theoria.Kernel.

Equation and matcher metadata

Theoria already compiles a small internal Bool/Nat/List equation fragment into auditable metadata:

{:ok, env} = Theoria.Prelude.env()
Theoria.Equation.Info.fetch(env, :nat_add)
alias Theoria.Equation.Identity

Theoria.Equation.Eqns.get(env, :nat_add)
Theoria.Equation.Eqns.realize(env, Identity.equation(:nat_add, :succ))

Generated ordinary equations, matcher equations, unfold equations, and checked matcher declarations are validated natively. Equation artifacts are identified by Theoria.Equation.Identity structs and can be checked or installed directly under those structured keys. This is internal groundwork rather than stable public equation-definition syntax.

Inspect them from Mix:

mix theoria.equations
mix theoria.equations bool_and
mix theoria.simp --examples

Rewrite and simp helpers are untrusted consumers of generated equation lemmas; they do not produce trusted proofs yet.

Inspect and errors

Core terms, levels, theorems, trust reports, and inductive reports implement Elixir's Inspect protocol:

inspect(elab!(identity_type))
#=> "#Theoria<∀ a : Type 1, a → a>"

Errors also render terms through the same pretty-printer, so failed checks show readable actual and expected types.

Library API

Useful entry points:

Theoria.new_env()
Theoria.prelude_env()

Theoria.Kernel.infer(env, term)
Theoria.Kernel.check(env, proof, type)
Theoria.Kernel.add_definition(env, name, type, value)
Theoria.Kernel.add_theorem(env, name, type, proof)
Theoria.Kernel.trust_report(env, name)

Theoria.Normalize.normalize(env, term)
Theoria.Normalize.defeq?(env, left, right)

Theoria.Theorem.check_all(MyProofs, env)
Theoria.Theorem.add_all_to_env(MyProofs, env)

Documentation

Guides included with the package:

• docs/release_0_2.md — 0.2 release boundary and API stability notes
• docs/design.md — kernel and environment design notes
• docs/inductives.md — inductive specifications and recursor generation
• docs/theorem_modules.md — theorem module workflow
• docs/validation.md — native validation corpus
• docs/lean_validation.md — contributor-only Lean oracle validation
• docs/equations.md — internal equation, matcher, rewrite, and simp groundwork
• CHANGELOG.md — release history

Validation

Theoria itself is validated with:

mix ci
mix docs
mix hex.build

mix ci runs compilation with warnings as errors, formatting, Credo, ExDNA duplication checks, Reach architecture/smell checks, Dialyzer, native validation, and the test suite. Run validation directly with:

mix theoria.validate
mix theoria.validate --only defeq

Contributors with Lean installed can also run:

mix theoria.lean.check
mix theoria.lean.check --only equality,bool,nat,list,vec

This translates Theoria's native validation data to a Lean oracle file and asks Lean to check it. Lean is not required for normal use.

License

MIT. See LICENSE.