# Theoria

Theoria is an Elixir-native proof/spec kernel inspired by Lean's trusted-kernel
architecture.

The goal is not Lean compatibility. Theoria starts as a small, reliable core for
checking proof terms generated by Elixir DSLs, tactics, and domain-specific
specification tools. The first target domains are finite data structures, graph
algorithms, compiler passes, and static-analysis invariants.

Theoria is intentionally split into a small trusted kernel and future untrusted
convenience layers. DSLs and tactics may generate proof terms, but only the
kernel can admit checked declarations.

## Installation

```elixir
def deps do
  [
    {:theoria, "~> 0.1.0"}
  ]
end
```

## Design principles

- Keep the trusted kernel small.
- Treat DSLs, macros, tactics, and automation as untrusted proof generators.
- Admit a theorem only after the kernel checks its proof term.
- Use precise Elixir structs and result tuples so the codebase is friendly to
  Elixir's gradual set-theoretic type direction.
- Grow through tests and proof corpora before adding convenience layers.

See [`docs/design.md`](docs/design.md) for the current design notes.

## Current status

The initial kernel supports:

- universe terms (`Type n` as `Sort n`)
- de Bruijn bound variables
- constants
- lambda abstraction
- dependent function types (`forall`)
- application
- beta reduction
- definitional equality by normalization
- checked constants and definitions in an environment

## Example core term

```elixir
import Theoria.Term

identity_type =
  forall(:a, sort(0),
    forall(:x, bvar(0),
      bvar(1)
    )
  )

identity_proof =
  lam(:a, sort(0),
    lam(:x, bvar(0),
      bvar(0)
    )
  )

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

## Quality checks

The repository includes a Reach-style CI alias:

```bash
mix ci
```

It runs compilation with warnings as errors, formatting, Credo, ExDNA, Reach
architecture/smell checks, Dialyzer, and tests.

## Roadmap

1. Harden the kernel with more normalization, substitution, and negative tests.
2. Add equality and basic logical connectives.
3. Add primitive Bool/Nat/List theories.
4. Add a small Elixir DSL that elaborates to checked core terms.
5. Add finite graph/spec libraries for tools such as Reach.