Theoria validation

Theoria owns its validation corpus. External tools such as Lean consume this corpus, but they do not decide which examples, theorem modules, or reduction checks matter.

Run native validation with:

mix theoria.validate

Check a downstream theorem module with:

mix theoria.theorems MyApp.Proofs

To narrow the corpus while developing:

mix theoria.validate --only bool
mix theoria.validate --only nat,list
mix theoria.validate --only defeq
mix theoria.validate --only inductives
mix theoria.validate --axioms

What is validated

Theoria.Validation.Corpus currently contains three kinds of checks:

The default corpus covers Logic, Equality, Bool, Nat, List, and Vec theorem modules, built-in reduction checks, deterministic small normalized Bool/Nat/List/Vec terms, the built-in inductive specs, equation metadata, generated equation theorem realization, matcher equation realization, one explicit indexed Vec matcher spec, indexed matcher equation metadata, checked statement types, metadata-only lemmas, and validation-only theorem realization. The indexed matcher validation constructs and admits the matcher inside validation only; it is not installed by Prelude.env/0. Indexed matcher equations can be exercised through Theoria.Library.Vec.env_with_indexed_matcher/1; passing install_equations: true also installs the realized indexed equation theorems into that opt-in environment. Prelude still does not install them, and rewrite/simp still exclude indexed matcher equations until simplification policy is finalized.

Defeq checks

Defeq checks are first-class Theoria values:

%Theoria.Validation.DefeqCheck{
  category: :nat,
  name: "nat_add_one_zero",
  left: left,
  right: right
}

They are checked by Theoria before any external oracle sees them:

Theoria.Validation.DefeqCheck.check(env, check)

Use these for kernel reduction behavior such as beta, zeta, recursor iota, indexed iota, and small deterministic normalized examples.

Lean oracle boundary

Lean validation is optional contributor hardening:

mix theoria.lean.check

It translates the Theoria validation corpus into Lean source and asks Lean to check the same proof and defeq claims. It also emits Lean #check type checks for the indexed Vec matcher equation statement shapes. Lean is not Theoria's source of truth and is not required for normal use.

Adding new checks

Prefer adding validation data close to the Theoria feature it exercises. Library validation metadata lives under modules such as Theoria.Library.Bool.Validation, Theoria.Library.Nat.Validation, Theoria.Library.List.Validation, and Theoria.Library.Vec.Validation.

Guidelines:

1. Add a theorem to the appropriate Theoria.Library.*.Theorems module when it is a reusable library fact.
2. Add a %Theoria.Validation.DefeqCheck{} in the owning library validation module when the point is definitional equality or reduction behavior.
3. Add an inductive check in the owning library validation module when a built-in spec/declaration shape needs to stay validated.

Downstream theorem example

defmodule MyApp.Proofs do
  use Theoria.DSL

  theorem :identity do
    type do
      term do
        forall :p, prop() do
          p ~> p
        end
      end
    end

    proof do
      term do
        lam :p, prop() do
          lam :hp, p do
            hp
          end
        end
      end
    end
  end
end

{:ok, env} = Theoria.Prelude.env()
Theoria.Theorem.check_all(MyApp.Proofs, env)

From Mix:

mix theoria.theorems MyApp.Proofs

After adding checks, run:

mix theoria.validate
mix theoria.lean.check