def MeTTaIL.SortPreserving (p : Presentation) : Prop

A presentation's reductions are head-sort-preserving when every base reduction keeps the head category, the sort of the term's outermost constructor. This is the semantic content of the category check in checkRewrite (which requires a rule's two sides to have compatible categories): firing a rule does not change the head sort. An assumed side-condition here (see sortPreserving_of_no_rewrites for satisfiability and headCat_inst_sexp for half of the discharge).

Equations

• MeTTaIL.SortPreserving p = ∀ (t t' : MeTTaIL.AST), MeTTaIL.Reduces p t t' → MeTTaIL.AST.headCat p.terms t = MeTTaIL.AST.headCat p.terms t'

theorem MeTTaIL.rewStep_preserves_headCat {p : Presentation} (h : SortPreserving p) {t t' : AST} (hstep : RewStep p t t') : AST.headCat p.terms t = AST.headCat p.terms t'

Head-sort preservation under the full context-closed relation: if base reductions keep the head category, so does RewStep. The congruence cases hold structurally: a step inside a sexp argument keeps the operator, hence its category; a step inside a Subst keeps the body that determines the category.

theorem MeTTaIL.rewStepMany_preserves_headCat {p : Presentation} (h : SortPreserving p) {t t' : AST} (hm : RewStepMany p t t') : AST.headCat p.terms t = AST.headCat p.terms t'

Many-step reduction preserves the head category.

theorem MeTTaIL.eval_preserves_headCat {p : Presentation} (h : SortPreserving p) (fuel : Nat) (t : AST) : AST.headCat p.terms (eval p fuel t) = AST.headCat p.terms t

The normalizer preserves the head category: eval keeps a term at its head sort, via eval_sound.

theorem MeTTaIL.sortPreserving_of_no_rewrites {p : Presentation} (hp : p.rewrites = []) : SortPreserving p

SortPreserving is satisfiable: a presentation with no rewrite rules preserves the head sort vacuously, since nothing reduces. So the conditional preservation theorems are not empty.

theorem MeTTaIL.headCat_inst_sexp (defs : List Rule) (bnds : List (String × AST)) (l : Label) (args : List AST) : AST.headCat defs (AST.inst bnds (AST.sexp l args)) = AST.headCat defs (AST.sexp l args)

Instantiation preserves a constructor head category: substituting into a sexp-headed term keeps the head label, hence its category. This is the right-hand-side half of the substitution lemma that would discharge SortPreserving from a per-rule head-category check; the left-hand-side half (matching against a constructor-headed pattern forces the same head) awaits LawfulBEq Label.