def MeTTaIL.varsOf : AST → List String

Free base-variable names of a term, in left-to-right order.

Equations

• MeTTaIL.varsOf (MeTTaIL.AST.var (MeTTaIL.DottedPath.base x_1)) = [x_1]
• MeTTaIL.varsOf (MeTTaIL.AST.var path) = []
• MeTTaIL.varsOf (MeTTaIL.AST.sexp label args) = MeTTaIL.varsOfList args
• MeTTaIL.varsOf (b.subst r v) = MeTTaIL.varsOf b ++ MeTTaIL.varsOf r

def MeTTaIL.varsOfList : List AST → List String

Equations

• MeTTaIL.varsOfList [] = []
• MeTTaIL.varsOfList (a :: as) = MeTTaIL.varsOf a ++ MeTTaIL.varsOfList as

def MeTTaIL.LabelDeterminesRule (p : Presentation) : Prop

Grammar well-formedness: rules that share a label declare the same argument sorts. This is what lets a pattern and a matched subject, both headed by the same constructor, be aligned argument by argument.

Equations

• MeTTaIL.LabelDeterminesRule p = ∀ r₁ ∈ p.terms, ∀ r₂ ∈ p.terms, r₁.label = r₂.label → r₁.argSorts = r₂.argSorts

def MeTTaIL.bndLookup (bnds : List (String × AST)) (v : String) : Option AST

The matcher's name lookup, projected to the bound term.

Equations

• MeTTaIL.bndLookup bnds v = Option.map (fun (x : String × MeTTaIL.AST) => x.2) (List.find? (fun (b : String × MeTTaIL.AST) => b.1 == v) bnds)

def MeTTaIL.WSsub (p : Presentation) (Γ Δ : Ctx) (bnds : List (String × AST)) : Prop

bnds is a well-sorted substitution for Δ over Γ: each Δ-variable it binds is bound to a term that is well-sorted at that variable's sort.

Equations

• MeTTaIL.WSsub p Γ Δ bnds = ∀ (y : String) (ty : MeTTaIL.AST) (cy : MeTTaIL.Cat), MeTTaIL.bndLookup bnds y = some ty → List.lookup y Δ = some cy → MeTTaIL.WellSorted p Γ ty cy

theorem MeTTaIL.bndLookup_cons_self (x : String) (t : AST) (bnds0 : List (String × AST)) : bndLookup ((x, t) :: bnds0) x = some t

Looking up the freshly prepended variable returns its binding.

theorem MeTTaIL.bndLookup_cons_of_ne {x y : String} (h : x ≠ y) (t : AST) (bnds0 : List (String × AST)) : bndLookup ((x, t) :: bnds0) y = bndLookup bnds0 y

Looking up a different variable skips the prepended binding.

Inversions for the well-sortedness relation

theorem MeTTaIL.wellSorted_sexp_inv {p : Presentation} {Γ : Ctx} {l : Label} {ts : List AST} {c : Cat} (h : WellSorted p Γ (AST.sexp l ts) c) : ∃ r ∈ p.terms, r.label = l ∧ c = r.cat ∧ WellSortedList p Γ ts r.argSorts

A well-sorted application reveals the rule that types it.

theorem MeTTaIL.wellSortedList_nil_inv {p : Presentation} {Γ : Ctx} {ts : List AST} (h : WellSortedList p Γ ts []) : ts = []

A well-sorted argument list at the empty sort list is empty.

theorem MeTTaIL.wellSortedList_cons_inv {p : Presentation} {Γ : Ctx} {t : AST} {ts : List AST} {cs : List Cat} (h : WellSortedList p Γ (t :: ts) cs) : ∃ (c : Cat) (cs' : List Cat), cs = c :: cs' ∧ WellSorted p Γ t c ∧ WellSortedList p Γ ts cs'

A well-sorted nonempty argument list splits head and tail.

theorem MeTTaIL.wellSortedList_cons_sort_inv {p : Presentation} {Γ : Ctx} {ts : List AST} {c : Cat} {cs' : List Cat} (h : WellSortedList p Γ ts (c :: cs')) : ∃ (t' : AST) (ts'' : List AST), ts = t' :: ts'' ∧ WellSorted p Γ t' c ∧ WellSortedList p Γ ts'' cs'

A well-sorted argument list at a nonempty sort list splits, aligning head and head-sort.

theorem MeTTaIL.wellSortedList_arg_subst {p : Presentation} {Γ : Ctx} {a a' : AST} (ha : ∀ (ca : Cat), WellSorted p Γ a ca → WellSorted p Γ a' ca) {pre post : List AST} {cs : List Cat} : WellSortedList p Γ (pre ++ a :: post) cs → WellSortedList p Γ (pre ++ a' :: post) cs

Replacing one argument of a well-sorted list by a same-sorted term keeps the list well-sorted. The replacement need only preserve sorts at whatever sort the original argument had.

theorem MeTTaIL.inst_var_of_bndLookup {bnds : List (String × AST)} {v : String} {ty : AST} (h : bndLookup bnds v = some ty) : AST.inst bnds (AST.var (DottedPath.base v)) = ty

If a variable is bound, instantiation returns the bound term.

theorem MeTTaIL.matchPat_var_spec {x : String} {t : AST} {bnds0 bnds : List (String × AST)} (hm : (AST.var (DottedPath.base x)).matchPat t bnds0 = some bnds) : (bnds = bnds0 ∧ ∃ (ty : AST), bndLookup bnds0 x = some ty) ∨ List.find? (fun (b : String × AST) => b.1 == x) bnds0 = none ∧ bnds = (x, t) :: bnds0

Variable matching either leaves the bindings unchanged (a consistent re-match, so the variable was already bound) or prepends a new binding (so the variable was previously unbound).

Shared matcher inversions

Three small inversions factor out the structural unfolding the three families below (monotonicity, coverage, the substitution invariant) all repeat: a constructor-headed pattern forces the subject's head and reduces to a list match, and a cons list match splits into a head match and a tail match.

theorem MeTTaIL.matchPat_sexp_inv {l : Label} {ps : List AST} {t : AST} {bnds0 bnds : List (String × AST)} (hm : (AST.sexp l ps).matchPat t bnds0 = some bnds) : ∃ (ts : List AST), t = AST.sexp l ts ∧ AST.matchPatList ps ts bnds0 = some bnds

A successful constructor-headed match reduces to a successful list match against the same head.

theorem MeTTaIL.matchPatList_cons_eq {p : AST} {ps : List AST} {t' : AST} {ts'' : List AST} {bnds0 bnds : List (String × AST)} (hm : AST.matchPatList (p :: ps) (t' :: ts'') bnds0 = some bnds) : ∃ (bnds1 : List (String × AST)), p.matchPat t' bnds0 = some bnds1 ∧ AST.matchPatList ps ts'' bnds1 = some bnds

A cons list match against a known cons subject splits into a head match and a tail match.

theorem MeTTaIL.matchPatList_cons_inv {p : AST} {ps ts : List AST} {bnds0 bnds : List (String × AST)} (hm : AST.matchPatList (p :: ps) ts bnds0 = some bnds) : ∃ (t' : AST) (ts'' : List AST) (bnds1 : List (String × AST)), ts = t' :: ts'' ∧ p.matchPat t' bnds0 = some bnds1 ∧ AST.matchPatList ps ts'' bnds1 = some bnds

A successful cons list match forces a cons subject and splits into a head and a tail match.

Monotonicity: matching only extends the binding set

The matcher either leaves the bindings untouched (an already-bound variable that matches consistently) or prepends a new one. Either way a binding once present is found unchanged afterwards.

theorem MeTTaIL.matchPat_find_mono {p : Presentation} {Δ : Ctx} {lhs : AST} {c : Cat} : WellSorted p Δ lhs c → ∀ {t : AST} {bnds0 bnds : List (String × AST)}, lhs.matchPat t bnds0 = some bnds → ∀ {y : String} {v : String × AST}, List.find? (fun (b : String × AST) => b.1 == y) bnds0 = some v → List.find? (fun (b : String × AST) => b.1 == y) bnds = some v

Matching a well-sorted pattern preserves every existing binding.

theorem MeTTaIL.matchPatList_find_mono {p : Presentation} {Δ : Ctx} {ps : List AST} {cs : List Cat} : WellSortedList p Δ ps cs → ∀ {ts : List AST} {bnds0 bnds : List (String × AST)}, AST.matchPatList ps ts bnds0 = some bnds → ∀ {y : String} {v : String × AST}, List.find? (fun (b : String × AST) => b.1 == y) bnds0 = some v → List.find? (fun (b : String × AST) => b.1 == y) bnds = some v

Matching a well-sorted argument list preserves every existing binding.

theorem MeTTaIL.bndLookup_mono {p : Presentation} {Δ : Ctx} {ps : List AST} {cs : List Cat} (hargs : WellSortedList p Δ ps cs) {ts : List AST} {bnds0 bnds : List (String × AST)} (hm : AST.matchPatList ps ts bnds0 = some bnds) {x : String} {ty : AST} (h : bndLookup bnds0 x = some ty) : bndLookup bnds x = some ty

bndLookup version of monotonicity through a list match.

theorem MeTTaIL.matchPat_var_bound {x : String} {t : AST} {bnds0 bnds : List (String × AST)} (hm : (AST.var (DottedPath.base x)).matchPat t bnds0 = some bnds) : ∃ (ty : AST), bndLookup bnds x = some ty

Matching a variable pattern binds that variable.

Coverage: matching binds every pattern variable

theorem MeTTaIL.matchPat_cover {p : Presentation} {Δ : Ctx} {lhs : AST} {c : Cat} : WellSorted p Δ lhs c → ∀ {t : AST} {bnds0 bnds : List (String × AST)}, lhs.matchPat t bnds0 = some bnds → ∀ {x : String}, x ∈ varsOf lhs → ∃ (ty : AST), bndLookup bnds x = some ty

Every variable of a well-sorted pattern is bound after a successful match.

theorem MeTTaIL.matchPatList_cover {p : Presentation} {Δ : Ctx} {ps : List AST} {cs : List Cat} : WellSortedList p Δ ps cs → ∀ {ts : List AST} {bnds0 bnds : List (String × AST)}, AST.matchPatList ps ts bnds0 = some bnds → ∀ {x : String}, x ∈ varsOfList ps → ∃ (ty : AST), bndLookup bnds x = some ty

Every variable of a well-sorted argument list is bound after a successful list match.

The well-sorted-substitution invariant

Matching a well-sorted subject against a well-sorted pattern keeps the bindings a well-sorted substitution: each variable is bound to a term well-sorted at that variable's declared sort.

theorem MeTTaIL.matchPat_wssub {p : Presentation} {Γ Δ : Ctx} (hwf : LabelDeterminesRule p) {lhs : AST} {c : Cat} : WellSorted p Δ lhs c → ∀ {t : AST} {bnds0 bnds : List (String × AST)}, WellSorted p Γ t c → lhs.matchPat t bnds0 = some bnds → WSsub p Γ Δ bnds0 → WSsub p Γ Δ bnds

Matching against a well-sorted pattern preserves the well-sorted-substitution invariant.

theorem MeTTaIL.matchPatList_wssub {p : Presentation} {Γ Δ : Ctx} (hwf : LabelDeterminesRule p) {ps : List AST} {cs : List Cat} : WellSortedList p Δ ps cs → ∀ {ts : List AST} {bnds0 bnds : List (String × AST)}, WellSortedList p Γ ts cs → AST.matchPatList ps ts bnds0 = some bnds → WSsub p Γ Δ bnds0 → WSsub p Γ Δ bnds

Matching an argument list against a well-sorted pattern list preserves the invariant.

Subject reduction for a base rewrite

The two halves combine: matching gives a well-sorted substitution (matchPat_wssub) that covers every pattern variable (matchPat_cover), and instantiation preserves well-sortedness (inst_wellSorted). So a base rewrite whose two sides are well-sorted under a shared context, applied to a well-sorted subject, yields a well-sorted result at the same sort.

theorem MeTTaIL.subjectReduction_base {p : Presentation} {Γ Δ : Ctx} (hwf : LabelDeterminesRule p) {lhs rhs t : AST} {c : Cat} {bnds : List (String × AST)} (hlhs : WellSorted p Δ lhs c) (hrhs : WellSorted p Δ rhs c) (hcov : ∀ (x : String) (cx : Cat), List.lookup x Δ = some cx → x ∈ varsOf lhs) (hsub : WellSorted p Γ t c) (hmatch : lhs.matchPat t [] = some bnds) : WellSorted p Γ (AST.inst bnds rhs) c

Lifting through the reduction relation

Subject reduction lifts from base contractions to the runtime's full one-step RewStep and many-step RewStepMany. The congruence case (a step inside an argument) holds because the argument keeps its sort, and the Subst cases are vacuous: a well-sorted term has no Subst node. The top-level hypothesis is exactly base-contraction preservation, supplied by subjectReduction_base for well-sorted rules.

theorem MeTTaIL.rewStep_preserves_wellSorted {p : Presentation} {Γ : Ctx} (htop : ∀ (t t' : AST) (c : Cat), Reduces p t t' → WellSorted p Γ t c → WellSorted p Γ t' c) {t t' : AST} (hstep : RewStep p t t') {c : Cat} : WellSorted p Γ t c → WellSorted p Γ t' c

One-step subject reduction: if base reductions preserve sorts, so does the context-closed RewStep.

theorem MeTTaIL.rewStepMany_preserves_wellSorted {p : Presentation} {Γ : Ctx} (htop : ∀ (t t' : AST) (c : Cat), Reduces p t t' → WellSorted p Γ t c → WellSorted p Γ t' c) {t t' : AST} (hsteps : RewStepMany p t t') {c : Cat} : WellSorted p Γ t c → WellSorted p Γ t' c

Many-step subject reduction: sorts are preserved along any reduction sequence.

A worked instance: recursive subject reduction with a variable rule

srPres declares a sort T, a constant a, and two unary symbols f, g, with the rewrite (f x) ~> (g x) carrying a real pattern variable x : T. Reducing the ground term (f a) binds x to a and produces (g a); subjectReduction_sr is the machine-checked statement that the result is well-sorted at T, obtained from subjectReduction_base (so every subterm keeps its declared sort across the variable-instantiating step).

def MeTTaIL.srPres : Presentation

A presentation with a constant, two unary symbols, and a variable-carrying rewrite.

Equations

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

theorem MeTTaIL.srPres_wf : LabelDeterminesRule srPres

theorem MeTTaIL.srLhs_ws : WellSorted srPres [("x", MeTTaIL.srT✝)] (AST.sexp (Label.id "f") [AST.var (DottedPath.base "x")]) MeTTaIL.srT✝

The pattern (f x) is well-sorted at T in the context x : T.

theorem MeTTaIL.srRhs_ws : WellSorted srPres [("x", MeTTaIL.srT✝)] (AST.sexp (Label.id "g") [AST.var (DottedPath.base "x")]) MeTTaIL.srT✝

The contractum (g x) is well-sorted at T in the same context.

theorem MeTTaIL.srSubj_ws : WellSorted srPres [] (AST.sexp (Label.id "f") [AST.sexp (Label.id "a") []]) MeTTaIL.srT✝

The subject (f a) is well-sorted at T in the empty context (it is ground).

theorem MeTTaIL.srCov (x : String) (cx : Cat) : List.lookup x [("x", MeTTaIL.srT✝)] = some cx → x ∈ varsOf (AST.sexp (Label.id "f") [AST.var (DottedPath.base "x")])

The rule's context is covered by the variables of its left-hand side.

theorem MeTTaIL.srMatch : (AST.sexp (Label.id "f") [AST.var (DottedPath.base "x")]).matchPat (AST.sexp (Label.id "f") [AST.sexp (Label.id "a") []]) [] = some [("x", AST.sexp (Label.id "a") [])]

Matching the subject against the pattern binds x to a.

theorem MeTTaIL.subjectReduction_sr : WellSorted srPres [] (AST.inst [("x", AST.sexp (Label.id "a") [])] (AST.sexp (Label.id "g") [AST.var (DottedPath.base "x")])) MeTTaIL.srT✝

Subject reduction on the concrete step (f a) ~> (g a): the result is well-sorted at T.

theorem MeTTaIL.srResult : AST.inst [("x", AST.sexp (Label.id "a") [])] (AST.sexp (Label.id "g") [AST.var (DottedPath.base "x")]) = AST.sexp (Label.id "g") [AST.sexp (Label.id "a") []]

And the instantiated contractum is concretely (g a).