Theoria's rewrite and simp engines are untrusted search/construction helpers. A proof-producing step is accepted only when the generated core proof checks with the native kernel.
Capability reports describe which structural paths currently have proof construction support. The matrix is path-oriented, while actual rewrite-step diagnostics are parent-term aware.
Supported paths
| Path | Capability | Notes |
|---|---|---|
[] | :top_level | Uses the rule proof directly. |
[:arg], [:fun] | :application_congruence | Application congruence. Nested application paths are supported when every segment is :arg or :fun. |
[:left], [:right] | :equality_side | Equality-side transport. |
[:base] | :eq_rec_base_congruence | EqRec base congruence. |
[:proof] | :eq_rec_proof_congruence | EqRec proof congruence; this does not assume proof irrelevance. |
[:base, ...], [:proof, ...] | outer EqRec capability with inner | Supported when the nested path is itself supported. |
[:value] | :value_congruence | Step-aware support for implemented constructor-value transports, currently let values. |
Nested capability JSON may contain an inner capability:
{
"supported": true,
"reason": "eq_rec_base_congruence",
"description": "EqRec base congruence",
"inner": {
"supported": true,
"reason": "application_congruence",
"description": "application congruence",
"inner": null
}
}Current boundaries
| Path | Boundary |
|---|---|
[:domain], [:body] | Binder paths need context-sensitive transport. |
[:type] under equality/let/EqRec | Type-changing transport is not generalized yet. |
[:motive] under EqRec | Motive transport is not supported. |
non-definitional Refl.value | Reported as :refl_value_boundary; homogeneous equality alone is not enough to rewrite proof types safely without stronger typed transport. |
Unsupported paths are deliberate boundaries, not trusted failures. The caller can still inspect the rewritten term, but no proof is trusted unless Theoria.Kernel.check/3 accepts it.
CLI
mix theoria.simp --capabilities
mix theoria.simp --capabilities --json
Theoria.Simp.Result.proof_status_counts/1 summarizes checked/missing/unsupported step proofs for a simplification trace.