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.7.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:

Library	Highlights
Logic	False, True, not, and, intro/eliminators
Equality	primitive Eq, refl, Eq.rec, transport helpers, equality theorems
Bool	Bool, true, false, generated recursor/inductor, boolean operations
Nat	Nat, zero, succ, generated recursor/inductor, nat_add
List	universe-polymorphic List, constructors, recursor/inductor, list_length, list_append
Vec	length-indexed Vec, vec_nil, vec_cons, indexed vec_ind

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 Bool/Nat/List equation fragment into auditable metadata:

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

summary = Equation.summary(env)
Equation.Summary.theorems(summary)

{:ok, identities} = Equation.identities(env, :nat_add)
{:ok, artifact} = Equation.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. The equation facade is the preferred API; matcher/indexed internals remain experimental before 1.0.

Theoria also includes experimental proof-producing simplification:

result = Theoria.Simp.normalize(env, term, prove: true)
result.realized

Theoria.Simp.add_theorem(env, :my_simp_theorem, term)

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. When proof production is requested, generated artifacts are trusted only after native kernel checking.

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

Start with:

• docs/design.md — kernel and environment design
• docs/theorem_modules.md — writing checked theorem modules
• docs/inductives.md — inductive specs and recursors
• docs/equations.md — generated equation identities, reports, and CLI workflow
• docs/trusted_boundary.md — what is trusted versus automation
• docs/validation.md — native validation workflow
• docs/assurance.md — kernel assurance reports and summaries
• docs/obligations.md — tool-generated claims, obligations, and certificates
• docs/public_api.md — stable, experimental, and internal API surfaces
• docs/roadmap.md — post-0.8 Elixir/Vibe roadmap

Additional maintainer and experimental notes live in the docs/ directory. See CHANGELOG.md for 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
mix theoria.kernel.check
mix theoria.kernel.check --json
mix theoria.typespecs MyApp.Context --json
mix theoria.spec --json

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.