def MeTTaIL.SubstFree : AST → Prop

A term of the rewriting fragment: no Subst node anywhere. Rule sides live here.

Equations

• MeTTaIL.SubstFree (MeTTaIL.AST.var path) = True
• MeTTaIL.SubstFree (MeTTaIL.AST.sexp label args) = MeTTaIL.SubstFreeList args
• MeTTaIL.SubstFree (body.subst repl v) = False

def MeTTaIL.SubstFreeList : List AST → Prop

Equations

• MeTTaIL.SubstFreeList [] = True
• MeTTaIL.SubstFreeList (a :: as) = (MeTTaIL.SubstFree a ∧ MeTTaIL.SubstFreeList as)

theorem MeTTaIL.wellSorted_substFree {p : Presentation} {Γ : Ctx} {t : AST} {c : Cat} : WellSorted p Γ t c → SubstFree t

Well-sorted terms are subst-free. The sort discipline (WellSorted has only var and sexp cases, no Subst rule) rejects every Subst node, so a Subst term is never well-sorted. Hence the subst-free fragment on which matcher correctness and the critical-pair confluence are stated coincides with the well-sorted-TERM fragment.

Scope, stated honestly: this does NOT by itself cover rules whose right-hand side is a Subst (for example the rho-calculus COMM rule in MeTTaILTests/Rholang.lean, whose RHS is .subst ...). Such a rule's RHS is not well-sorted as written, and its reduct becomes subst-free only after inst resolves the Subst. Subject reduction THROUGH that explicit-substitution resolution is a separate obligation (the binder fragment), not discharged by this lemma. So this closes the first-order rewriting fragment, not the binder fragment.

theorem MeTTaIL.wellSortedList_substFree {p : Presentation} {Γ : Ctx} {ts : List AST} {cs : List Cat} : WellSortedList p Γ ts cs → SubstFreeList ts

def MeTTaIL.AST.instStruct (bnds : List (String × AST)) : AST → AST

Structural instantiation: like AST.inst but it does NOT resolve a Subst node, rebuilding it structurally with its bound variable kept literally. This is exactly the reconstruction the matcher inverts: the matcher is purely structural and matches a Subst pattern's bound variable by syntactic equality, so matcher correctness is stated against instStruct for the FULL pattern language. On the subst-free fragment instStruct agrees with inst (instStruct_eq_inst_substFree), so the inst theorems are recovered as corollaries.

Equations

• One or more equations did not get rendered due to their size.
• MeTTaIL.AST.instStruct bnds (MeTTaIL.AST.var p) = MeTTaIL.AST.var p
• MeTTaIL.AST.instStruct bnds (MeTTaIL.AST.sexp l args) = MeTTaIL.AST.sexp l (MeTTaIL.AST.instStructList bnds args)
• MeTTaIL.AST.instStruct bnds (b.subst r w) = (MeTTaIL.AST.instStruct bnds b).subst (MeTTaIL.AST.instStruct bnds r) w

def MeTTaIL.AST.instStructList (bnds : List (String × AST)) : List AST → List AST

Structural instantiation through an argument list.

Equations

• MeTTaIL.AST.instStructList bnds [] = []
• MeTTaIL.AST.instStructList bnds (a :: as) = MeTTaIL.AST.instStruct bnds a :: MeTTaIL.AST.instStructList bnds as

theorem MeTTaIL.instStruct_eq_inst_substFree {bnds : List (String × AST)} {t : AST} : SubstFree t → AST.instStruct bnds t = AST.inst bnds t

On the subst-free fragment, structural instantiation and inst coincide (they differ only on Subst nodes, of which a subst-free term has none).

theorem MeTTaIL.instStructList_eq_instList_substFree {bnds : List (String × AST)} {ts : List AST} : SubstFreeList ts → AST.instStructList bnds ts = AST.instList bnds ts

def MeTTaIL.Ctx.extendPath (Γ : Ctx) (q : DottedPath) (c : Cat) : Ctx

Extend a typing context along a path: a base name y binds y : c; a qualified path binds nothing (no well-sorted variable can equal a qualified path), so the context is unchanged.

Equations

• Γ.extendPath (MeTTaIL.DottedPath.base y) c = (y, c) :: Γ
• Γ.extendPath q c = Γ

theorem MeTTaIL.subst1_wellSorted_path {p : Presentation} {Γ : Ctx} {q : DottedPath} {c : Cat} {repl : AST} (hr : WellSorted p Γ repl c) {t : AST} {d : Cat} : WellSorted p (Γ.extendPath q c) t d → WellSorted p Γ (AST.subst1 q repl t) d

The substitution lemma along an arbitrary path (the general subst1 half), the binder-fragment counterpart of inst_wellSorted: substituting a term well-sorted at c for the path q in a term well-sorted at d in the path-extended context yields a term well-sorted at d. For q = .base y this is the binder substitution lemma; for a qualified path it holds vacuously (no well-sorted variable matches a qualified path, so the term is unchanged and the extended context is Γ). This is the key lemma for subject reduction of rules whose right-hand side is a Subst (explicit substitution), such as the rho-calculus COMM rule (MeTTaILTests/Rholang.lean), whose reduct is inst-resolved through subst1, INCLUDING the captured-bound-variable (alpha) case where the match remaps the bound variable to another runtime variable. Kept here rather than in Semantics because it needs LawfulBEq DottedPath from DecEq.

theorem MeTTaIL.subst1List_wellSorted_path {p : Presentation} {Γ : Ctx} {q : DottedPath} {c : Cat} {repl : AST} (hr : WellSorted p Γ repl c) {ts : List AST} {cs : List Cat} : WellSortedList p (Γ.extendPath q c) ts cs → WellSortedList p Γ (AST.subst1List q repl ts) cs

theorem MeTTaIL.subst1_wellSorted {p : Presentation} {Γ : Ctx} {y : String} {c : Cat} {repl : AST} (hr : WellSorted p Γ repl c) {t : AST} {d : Cat} (ht : WellSorted p ((y, c) :: Γ) t d) : WellSorted p Γ (AST.subst1 (DottedPath.base y) repl t) d

The binder substitution lemma for a base variable y: the q = .base y instance of subst1_wellSorted_path (the original first-order/binder substitution lemma).

def MeTTaIL.AST.instSubstTarget (bnds : List (String × AST)) : DottedPath → DottedPath

The substitution target that AST.inst computes for a Subst node's bound variable w: a base name bound by the match to a runtime variable .var p is remapped to p (the capture-avoiding rename); otherwise w itself. Mirrors the let w' := ... inside AST.inst's .subst case.

Equations

• One or more equations did not get rendered due to their size.
• MeTTaIL.AST.instSubstTarget bnds x✝ = x✝

theorem MeTTaIL.inst_subst_eq (bnds : List (String × AST)) (b r : AST) (w : DottedPath) : AST.inst bnds (b.subst r w) = AST.subst1 (AST.instSubstTarget bnds w) (AST.inst bnds r) (AST.inst bnds b)

AST.inst on a Subst node resolves it to a subst1 along the remapped target.

theorem MeTTaIL.reduces_subst_wellSorted {p : Presentation} {Γ : Ctx} {bnds : List (String × AST)} {b r : AST} {w : DottedPath} {d cw : Cat} (hb : WellSorted p (Γ.extendPath (AST.instSubstTarget bnds w) cw) (AST.inst bnds b) d) (hr : WellSorted p Γ (AST.inst bnds r) cw) : WellSorted p Γ (AST.inst bnds (b.subst r w)) d

Subject reduction for a Subst right-hand side (the binder fragment), in FULL generality including the captured-bound-variable (alpha) case: the inst-resolved reduct of a rule whose RHS is subst b r w is well-sorted. inst resolves the explicit substitution to a subst1 along the remapped target instSubstTarget bnds w (the bound variable w, or the runtime variable it was matched to), so the reduct is well-sorted when the instantiated body inst bnds b is well-sorted at d in the context extended by that target and the instantiated inst bnds r is well-sorted at the target's sort. This covers the rho-calculus COMM rule's reduction, INCLUDING when its bound variable is captured/remapped by the match (the alpha case the earlier freshness-restricted version excluded).

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

If a variable is unbound, instantiation leaves it alone.

Instantiation depends only on the pattern's variables

theorem MeTTaIL.inst_agree {bnds1 bnds2 : List (String × AST)} {lhs : AST} : SubstFree lhs → (∀ v ∈ varsOf lhs, bndLookup bnds1 v = bndLookup bnds2 v) → AST.inst bnds1 lhs = AST.inst bnds2 lhs

Two substitutions agreeing on a (subst-free) term's variables instantiate it the same way.

theorem MeTTaIL.instList_agree {bnds1 bnds2 : List (String × AST)} {args : List AST} : SubstFreeList args → (∀ v ∈ varsOfList args, bndLookup bnds1 v = bndLookup bnds2 v) → AST.instList bnds1 args = AST.instList bnds2 args

The argument-list version.

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

instStruct on a bound base variable returns its binding (defeq to the inst version).

theorem MeTTaIL.instStruct_var_none {bnds : List (String × AST)} {v : String} (h : bndLookup bnds v = none) : AST.instStruct bnds (AST.var (DottedPath.base v)) = AST.var (DottedPath.base v)

instStruct leaves an unbound base variable alone (defeq to the inst version).

theorem MeTTaIL.instStruct_var_eq_inst {bnds : List (String × AST)} {v : String} : AST.instStruct bnds (AST.var (DottedPath.base v)) = AST.inst bnds (AST.var (DottedPath.base v))

instStruct and inst coincide on a base variable (they have identical defining clauses there).

theorem MeTTaIL.instStruct_agree {bnds1 bnds2 : List (String × AST)} {t : AST} : (∀ v ∈ varsOf t, bndLookup bnds1 v = bndLookup bnds2 v) → AST.instStruct bnds1 t = AST.instStruct bnds2 t

Two substitutions agreeing on a term's variables instantiate it the same way, for the FULL language (the instStruct counterpart of inst_agree, with no subst-free restriction).

theorem MeTTaIL.instStructList_agree {bnds1 bnds2 : List (String × AST)} {args : List AST} : (∀ v ∈ varsOfList args, bndLookup bnds1 v = bndLookup bnds2 v) → AST.instStructList bnds1 args = AST.instStructList bnds2 args

The argument-list version.

theorem MeTTaIL.matchPat_subst_inv {pb pr : AST} {pv : DottedPath} {t : AST} {bnds0 bnds : List (String × AST)} (hm : (pb.subst pr pv).matchPat t bnds0 = some bnds) : ∃ (tb : AST) (tr : AST), t = tb.subst tr pv ∧ ∃ (bnds1 : List (String × AST)), pb.matchPat tb bnds0 = some bnds1 ∧ pr.matchPat tr bnds1 = some bnds

A successful Subst-headed match forces a Subst subject with the same (syntactic) bound variable, and splits into a match of the body and a match of the replacement.

Matching a variable reconstructs the matched term

theorem MeTTaIL.matchPat_qual {i : String} {r : DottedPath} {t : AST} {bnds0 bnds : List (String × AST)} (hm : (AST.var (DottedPath.qualified i r)).matchPat t bnds0 = some bnds) : bnds = bnds0 ∧ t = AST.var (DottedPath.qualified i r)

A successful match of a qualified-path variable forces the term to be that variable and leaves the bindings unchanged (it is a structural-equality match).

theorem MeTTaIL.matchPat_var_inst {x : String} {t : AST} {bnds0 bnds : List (String × AST)} (hm : (AST.var (DottedPath.base x)).matchPat t bnds0 = some bnds) : AST.inst bnds (AST.var (DottedPath.base x)) = t

Matching a base variable binds it to the matched term: instantiation gives the term back. The repeated-variable case uses the matcher's consistency test t' == t, the equality re-check that MORK's VarRefRecheck/BindingEnv Verus proofs validate.

Matching only extends the bindings, and binds every pattern variable

BindingEnv in MORK's Verus proofs: a re-match is a no-op and a fresh bind only adds.

theorem MeTTaIL.matchPat_mono_all {lhs t : AST} {bnds0 bnds : List (String × AST)} : lhs.matchPat t bnds0 = some bnds → ∀ {v : String} {ty : AST}, bndLookup bnds0 v = some ty → bndLookup bnds v = some ty

Matching ANY pattern preserves every existing binding (monotonicity, unconditional: the matcher only ever adds bindings, including through a Subst pattern's two sub-matches).

theorem MeTTaIL.matchPatList_mono_all {ps ts : List AST} {bnds0 bnds : List (String × AST)} : AST.matchPatList ps ts bnds0 = some bnds → ∀ {v : String} {ty : AST}, bndLookup bnds0 v = some ty → bndLookup bnds v = some ty

The argument-list version.

theorem MeTTaIL.matchPat_mono {lhs : AST} : SubstFree lhs → ∀ {t : AST} {bnds0 bnds : List (String × AST)}, lhs.matchPat t bnds0 = some bnds → ∀ {v : String} {ty : AST}, bndLookup bnds0 v = some ty → bndLookup bnds v = some ty

Subst-free corollary of matchPat_mono_all (the original matchPat_mono).

theorem MeTTaIL.matchPatList_mono {ps : List AST} : SubstFreeList ps → ∀ {ts : List AST} {bnds0 bnds : List (String × AST)}, AST.matchPatList ps ts bnds0 = some bnds → ∀ {v : String} {ty : AST}, bndLookup bnds0 v = some ty → bndLookup bnds v = some ty

Subst-free corollary of matchPatList_mono_all (the original matchPatList_mono).

theorem MeTTaIL.matchPat_cover_all {lhs t : AST} {bnds0 bnds : List (String × AST)} : lhs.matchPat t bnds0 = some bnds → ∀ {v : String}, v ∈ varsOf lhs → ∃ (ty : AST), bndLookup bnds v = some ty

Every variable of ANY pattern is bound after a successful match (coverage, unconditional, including a Subst pattern whose variables come from its body and replacement).

theorem MeTTaIL.matchPatList_cover_all {ps ts : List AST} {bnds0 bnds : List (String × AST)} : AST.matchPatList ps ts bnds0 = some bnds → ∀ {v : String}, v ∈ varsOfList ps → ∃ (ty : AST), bndLookup bnds v = some ty

The argument-list version.

theorem MeTTaIL.matchPat_cover_sf {lhs : AST} : SubstFree lhs → ∀ {t : AST} {bnds0 bnds : List (String × AST)}, lhs.matchPat t bnds0 = some bnds → ∀ {v : String}, v ∈ varsOf lhs → ∃ (ty : AST), bndLookup bnds v = some ty

Subst-free corollary of matchPat_cover_all (the original matchPat_cover_sf).

theorem MeTTaIL.matchPatList_cover_sf {ps : List AST} : SubstFreeList ps → ∀ {ts : List AST} {bnds0 bnds : List (String × AST)}, AST.matchPatList ps ts bnds0 = some bnds → ∀ {v : String}, v ∈ varsOfList ps → ∃ (ty : AST), bndLookup bnds v = some ty

Subst-free corollary of matchPatList_cover_all (the original matchPatList_cover_sf).

Matcher correctness: a successful match reconstructs the matched term

theorem MeTTaIL.matchPat_instStruct_eq {lhs t : AST} {bnds0 bnds : List (String × AST)} : lhs.matchPat t bnds0 = some bnds → AST.instStruct bnds lhs = t

A successful match produces a substitution that STRUCTURALLY instantiates the pattern back to the matched term, for the FULL pattern language including Subst (the matcher inverts instStruct).

theorem MeTTaIL.matchPatList_instStruct_eq {ps ts : List AST} {bnds0 bnds : List (String × AST)} : AST.matchPatList ps ts bnds0 = some bnds → AST.instStructList bnds ps = ts

The argument-list version.

theorem MeTTaIL.matchPat_inst_eq {lhs : AST} (hsf : SubstFree lhs) {t : AST} {bnds0 bnds : List (String × AST)} (hm : lhs.matchPat t bnds0 = some bnds) : AST.inst bnds lhs = t

Subst-free corollary: a successful match inst-reconstructs the term (the original matchPat_inst_eq). On the subst-free fragment inst = instStruct.

theorem MeTTaIL.matchPatList_inst_eq {ps : List AST} (hsf : SubstFreeList ps) {ts : List AST} {bnds0 bnds : List (String × AST)} (hm : AST.matchPatList ps ts bnds0 = some bnds) : AST.instList bnds ps = ts

The argument-list version (the original matchPatList_inst_eq).

The runtime step is a genuine rule application

The matcher correctness certifies the runtime: when applyBaseRewrite fires a (subst-free) base rule on a term, the result really is the rule's right side instantiated at a substitution whose action on the left side gives back the original term. So t ~> t' genuinely instances lhs ~> rhs.

theorem MeTTaIL.applyBaseRewrite_genuine {rd : RewriteDecl} {lhs rhs t t' : AST} (hsf : SubstFree lhs) (hrw : rd.rw = Rewrite.base lhs rhs) (h : applyBaseRewrite rd t = some t') : ∃ (bnds : List (String × AST)), AST.inst bnds lhs = t ∧ t' = AST.inst bnds rhs

A successful base rewrite is a genuine rule application: there is a substitution bnds with t = lhs·bnds and t' = rhs·bnds.

Matcher completeness: the matcher finds every instance

The dual of matchPat_inst_eq: the matcher never misses a match. This mirrors the completeness half of MORK's VarRefRecheck (the re-check is sound and, under the right groundness, complete). Here completeness is unconditional, because a substitution is a function, so a pattern's instance has equal subterms at a repeated variable's positions and the consistency test always passes.

def MeTTaIL.CompatS (σ bnds : List (String × AST)) : Prop

bnds agrees with a substitution σ: it binds each variable exactly as σ instantiates it.

Equations

• MeTTaIL.CompatS σ bnds = ∀ (v : String) (ty : MeTTaIL.AST), MeTTaIL.bndLookup bnds v = some ty → ty = MeTTaIL.AST.inst σ (MeTTaIL.AST.var (MeTTaIL.DottedPath.base v))

theorem MeTTaIL.matchPat_instStruct_complete {σ : List (String × AST)} {lhs : AST} {bnds0 : List (String × AST)} : CompatS σ bnds0 → ∃ (bnds : List (String × AST)), lhs.matchPat (AST.instStruct σ lhs) bnds0 = some bnds ∧ CompatS σ bnds

The matcher succeeds on any STRUCTURAL instance of ANY pattern (full language, including Subst), threading a σ-compatible accumulator.

theorem MeTTaIL.matchPatList_instStruct_complete {σ : List (String × AST)} {args : List AST} {bnds0 : List (String × AST)} : CompatS σ bnds0 → ∃ (bnds : List (String × AST)), AST.matchPatList args (AST.instStructList σ args) bnds0 = some bnds ∧ CompatS σ bnds

The argument-list version.

theorem MeTTaIL.matchPat_complete {σ : List (String × AST)} {lhs : AST} (hsf : SubstFree lhs) {bnds0 : List (String × AST)} (hc : CompatS σ bnds0) : ∃ (bnds : List (String × AST)), lhs.matchPat (AST.inst σ lhs) bnds0 = some bnds ∧ CompatS σ bnds

Subst-free corollary: the matcher succeeds on any inst-instance (the original matchPat_complete).

theorem MeTTaIL.matchPatList_complete {σ : List (String × AST)} {args : List AST} (hsf : SubstFreeList args) {bnds0 : List (String × AST)} (hc : CompatS σ bnds0) : ∃ (bnds : List (String × AST)), AST.matchPatList args (AST.instList σ args) bnds0 = some bnds ∧ CompatS σ bnds

The argument-list version (the original matchPatList_complete).

theorem MeTTaIL.matchPat_iff_instStruct {lhs t : AST} : (∃ (bnds : List (String × AST)), lhs.matchPat t [] = some bnds) ↔ ∃ (σ : List (String × AST)), AST.instStruct σ lhs = t

Matcher correctness, both directions, for the FULL pattern language (including Subst): a pattern matches a term exactly when the term is a STRUCTURAL instance of the pattern.

theorem MeTTaIL.matchPat_iff_instance {lhs t : AST} (hsf : SubstFree lhs) : (∃ (bnds : List (String × AST)), lhs.matchPat t [] = some bnds) ↔ ∃ (σ : List (String × AST)), AST.inst σ lhs = t

Matcher correctness, both directions: a (subst-free) pattern matches a term exactly when the term is an inst-instance of the pattern. The subst-free corollary of matchPat_iff_instStruct.