theorem MeTTaIL.matchPat_sexp_head {l : Label} {ps : List AST} {t : AST} {bnds bnds' : List (String × AST)} (h : (AST.sexp l ps).matchPat t bnds = some bnds') : ∃ (ts : List AST), t = AST.sexp l ts

Matcher head-inversion: a successful match against a constructor-headed pattern (l ps) forces the matched term to have the same head l. Uses LawfulBEq Label to turn the matcher's l == m into l = m.

theorem MeTTaIL.headCat_of_matchPat {defs : List Rule} {l : Label} {ps : List AST} {t : AST} {bnds bnds' : List (String × AST)} (h : (AST.sexp l ps).matchPat t bnds = some bnds') : AST.headCat defs t = AST.headCat defs (AST.sexp l ps)

A matched term has the same head category as the (constructor-headed) pattern it matched.

def MeTTaIL.RulesHeadCatOk (p : Presentation) : Prop

The per-rule head-category check: every rewrite's conclusion has constructor-headed sides whose head categories agree. This is the semantic content of checkRewrite's catCompatible test restricted to determined (non-variable) heads, and it is exactly what is needed to discharge SortPreserving.

Equations

• One or more equations did not get rendered due to their size.

theorem MeTTaIL.sortPreserving_of_rulesHeadCatOk {p : Presentation} (h : RulesHeadCatOk p) : SortPreserving p

Discharging SortPreserving from the checkable per-rule condition: if every rule keeps the head category between its conclusion's two constructor-headed sides, every base reduction does, so the whole reduction relation preserves the head sort. The matched redex has the left head category (headCat_of_matchPat), the contractum has the right head category (headCat_inst_sexp), and the rule condition equates them.

A worked instance: head-sort preservation on a concrete presentation

demoPres declares a sort T, the constants a, b, and a unary f, with the single rewrite (f a) ~> b. Its terms give every operator the category T, so the rule keeps the head category, and SortPreserving demoPres follows from the criterion.

def MeTTaIL.demoPres : Presentation

A small presentation with populated grammar and one head-sort-preserving rule.

Equations

• One or more equations did not get rendered due to their size.

theorem MeTTaIL.rulesHeadCatOk_demoPres : RulesHeadCatOk demoPres

theorem MeTTaIL.sortPreserving_demoPres : SortPreserving demoPres

The concrete presentation preserves the head sort under reduction.