This table tracks Theoria's proof/equation abstractions against the Lean 4 source architecture. Lean is a contributor-only oracle for Theoria, not a runtime dependency or source of truth.
| Lean abstraction | Lean role | Theoria abstraction | Status | Missing on Theoria side |
|---|---|---|---|---|
PreDefinition | Not-yet-finalized definition package | Equation.Definition.Spec, Equation.Signature | 🟡 | No mutual predefinition groups, equation-affecting options, termination data, or elaborator-owned predefinition pipeline. |
Structural.EqnInfo | Stores recursive equation metadata: declaration, levels, type/value, rec arg, fixed params | Equation.Info | 🟢 | Fixed params are parameter positions, not full permutations. No recursion kind or mutual group metadata. |
FixedParamPerms | Computes fixed/varying params across recursive groups | Equation.FixedParams | 🟡 | Signature-level fixed parameter derivation exists, but no permutations, dependency analysis, or mutual recursion support. |
Matcher.Info / AltParamInfo | Matcher arity, params, discriminants, alternatives, universe elimination, overlaps | Equation.Matcher.Info, Equation.Matcher.Descriptor, Equation.Matcher.Type, Equation.Matcher.Spec, Env.Matcher | 🟡 | Checked matcher declarations exist and Bool/Nat/List, including binary Bool, have real matcher type/body; descriptors are now informed by checked recursor metadata, Recursor.Descriptor records indexed rule patterns, and matcher descriptors can represent indexed Vec-like shapes with normalized fields, but matcher type/body generation still has no dependent/indexed support, discriminant dependency analysis, or universe-elim sophistication. |
mkEqnTypes / mkEqns | Computes equation theorem statements and realizes proofs | Schema.Builder, Equation.Lemma, Eqns | 🟡 | Current generated equations are template-driven for supported fragments, not derived by splitting normalized match goals. |
getEqnsFor? / registerGetEqnsFn | Lazy central lookup for equation theorem names | Equation.Eqns, Equation.Extension | 🟡 | Lazy realization APIs exist, but there is no persistent lazy theorem registry; source lookup is derived from in-memory registry snapshots built from typed metadata. |
mkUnfoldEq / getUnfoldFor? | Unfold equation theorem generation | Eqns.unfold/2, Lemma.unfold_for/1 | 🟡 | Early direct unfold lemmas only; no separate lazy unfold theorem registry. |
MatchEqsExt | Matcher-specific equation theorem extension | Matcher.Equation, Matcher.Eqns, Env.Matcher | 🟡 | Matcher equations are schema-derived and theorem-checkable, but there is no persistent matcher equation extension or broadly independently compiled matcher body yet. |
brecOn / below machinery | Structural recursion beyond simple primitive recursors | None | 🔴 | No below dictionaries or general structural recursion checker. |
| Simp theorem DB | Attribute/prioritized proof-producing simplification | Simp.Rule, Simp.Database, Simp.Step | 🟠 | No attributes, indexing, conditional rules, congruence, or proof-producing simplification. |
Current equation flow:
Signature + Case.Template + Clause/Pattern
→ Schema.Builder
→ Compiler
→ Compiled
→ Definition.Spec
→ Info
→ Eqns
→ Rewrite/SimpThe main remaining Lean-alignment target is to turn descriptor-derived matcher type shapes into dependent/indexed matcher type/body generation, replace template-driven equation generation with equation type generation from matcher/definition structure, then add richer fixed-parameter permutations and a persistent lazy theorem registry.