# 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

```elixir
def deps do
  [
    {:theoria, "~> 0.6.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:

```elixir
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:

```elixir
{: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:

```elixir
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:

```bash
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:

```text
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:

```elixir
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:

```elixir
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:

```elixir
{: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.

The 0.4 development line also starts proof-producing simplification:

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

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

Inspect them from Mix:

```bash
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:

```elixir
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:

```elixir
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`](docs/design.md) — kernel and environment design
- [`docs/theorem_modules.md`](docs/theorem_modules.md) — writing checked theorem modules
- [`docs/inductives.md`](docs/inductives.md) — inductive specs and recursors
- [`docs/trusted_boundary.md`](docs/trusted_boundary.md) — what is trusted versus automation
- [`docs/validation.md`](docs/validation.md) — native validation workflow
- [`docs/assurance.md`](docs/assurance.md) — kernel assurance reports and summaries

Additional maintainer and experimental notes live in the `docs/` directory. See [`CHANGELOG.md`](CHANGELOG.md) for release history.

## Validation

Theoria itself is validated with:

```bash
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:

```bash
mix theoria.validate
mix theoria.validate --only defeq
mix theoria.kernel.check
mix theoria.kernel.check --json
```

Contributors with Lean installed can also run:

```bash
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`](LICENSE).