validation.md

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:

Check	Source	Native checker
Theorem modules	Theoria.Library.*.Theorems via Theoria.Validation.TheoremModuleCheck	Theoria.Validation.Checkable / Theoria.Theorem.check_all/2
Definitional equality	%Theoria.Validation.DefeqCheck{}	Theoria.Validation.Checkable / Theoria.Normalize.defeq?/3
Inductive specs	%Theoria.Validation.InductiveCheck{}	Theoria.Validation.Checkable / Theoria.Inductive.check_spec/2 and Theoria.Inductive.verify_env/2
Explicit indexed matcher spec	Internal Vec matcher validation	Theoria.Validation.IndexedMatchers / Theoria.Equation.Matcher.Indexed.Package

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:

Need	Put it in
Reusable proposition proof	Theoria.Library.*.Theorems
Reduction/iota/defeq behavior	Theoria.Library.*.Validation as %Theoria.Validation.DefeqCheck{}
Inductive declaration invariant	Theoria.Library.*.Validation as %Theoria.Validation.InductiveCheck{}
Shared validation term helper	Theoria.Validation.Terms
External oracle mapping issue	Theoria.Lean.Encode.*

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

Kernel differential reports

Use mix theoria.kernel.check for production/reference kernel assurance. It covers curated infer/check/normalize/defeq cases, rejection cases, theorem modules, generated artifacts, indexed artifacts, reference replay of the Prelude environment, replay of theorem-module-installed environments, and replay of environments extended with generated and indexed artifacts.

Coverage, explanation, and JSON modes are intended for CI and tooling:

mix theoria.kernel.check --coverage
mix theoria.kernel.check --explain
mix theoria.kernel.check --json --coverage

The JSON output is encoded through Jason encoders and includes structured artifact replay counts and skip entries. A skipped artifact means it was not replayed as an installed declaration in that environment; it is not silently treated as checked. Rewrite/simp remain untrusted search even when these reports pass—the trusted boundary is still the final kernel-checked artifact or theorem declaration.

After adding checks, run:

mix theoria.validate
mix theoria.lean.check