structure MeTTaIL.AC.ACMatch : Type

Internal result of AC matching: bindings plus the AC representative matched syntactically.

• bnds : List (String × AST)
• witness : AST

structure MeTTaIL.AC.ACMatchList : Type

Internal list result of AC matching.

• bnds : List (String × AST)
• witnesses : List AST

def MeTTaIL.AC.acRestPattern (l : Label) (fixed : AST) (restVar : String) : AST

Pattern for one fixed AC leaf and one rest variable.

Equations

• MeTTaIL.AC.acRestPattern l fixed restVar = MeTTaIL.AST.sexp l [fixed, MeTTaIL.AST.var (MeTTaIL.DottedPath.base restVar)]

def MeTTaIL.AC.bindBase (v : String) (t : AST) (bnds : List (String × AST)) : Option (List (String × AST))

Bind a base variable consistently with the ordinary matcher.

Equations

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

theorem MeTTaIL.AC.bindBase_eq_matchPat (v : String) (t : AST) (bnds : List (String × AST)) : bindBase v t bnds = (AST.var (DottedPath.base v)).matchPat t bnds

bindBase is the ordinary matcher on a base variable.

def MeTTaIL.AC.matchACRestLoop (l : Label) (fixed : AST) (restVar : String) (bnds : List (String × AST)) (preRev : List AST) : List AST → Option ACMatch

Search loop for one AC collection. preRev stores leaves already skipped, in reverse order.

Equations

• One or more equations did not get rendered due to their size.
• MeTTaIL.AC.matchACRestLoop l fixed restVar bnds preRev [] = none

def MeTTaIL.AC.matchACRest (l : Label) (fixed : AST) (restVar : String) (subject : AST) (bnds : List (String × AST)) : Option ACMatch

Search one AC collection for a fixed leaf and bind the rest variable to the rebuilt remainder.

Equations

• One or more equations did not get rendered due to their size.
• MeTTaIL.AC.matchACRest l fixed restVar subject bnds = none

theorem MeTTaIL.AC.matchACRestLoop_witness (l : Label) (fixed : AST) (restVar : String) (bnds : List (String × AST)) {preRev leaves : List AST} {r : ACMatch} : matchACRestLoop l fixed restVar bnds preRev leaves = some r → (acRestPattern l fixed restVar).matchPat r.witness bnds = some r.bnds

A successful AC-rest search returns a syntactic representative that the ordinary matcher accepts.

theorem MeTTaIL.AC.matchACRest_witness {l : Label} {fixed : AST} {restVar : String} {subject : AST} {bnds : List (String × AST)} {r : ACMatch} (hm : matchACRest l fixed restVar subject bnds = some r) : (acRestPattern l fixed restVar).matchPat r.witness bnds = some r.bnds

A successful AC-rest match returns a syntactic representative accepted by the ordinary matcher.

theorem MeTTaIL.AC.matchACRestLoop_complete_of_split (l : Label) (fixed : AST) (restVar : String) (bnds : List (String × AST)) {preRev leaves : List AST} : (∃ (pre : List AST) (leaf : AST) (tail : List AST) (bnds₁ : List (String × AST)) (bnds₂ : List (String × AST)), leaves = pre ++ leaf :: tail ∧ fixed.matchPat leaf bnds = some bnds₁ ∧ bindBase restVar (rebuild l (preRev.reverse ++ pre ++ tail)) bnds₁ = some bnds₂) → ∃ (r : ACMatch), matchACRestLoop l fixed restVar bnds preRev leaves = some r

If a chosen split of the flattened leaves has a matching fixed leaf and a bindable rebuilt rest, the AC-rest search succeeds. This is completeness for the linear search shape, not uniqueness of the returned bindings.

def MeTTaIL.AC.ACRestFlatSplit (l : Label) (fixed a b : AST) (restVar : String) (bnds : List (String × AST)) : Prop

A flattened binary AC subject has a split that the linear AC-rest matcher can use.

Equations

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

theorem MeTTaIL.AC.matchACRest_complete_of_flat_split {l : Label} {fixed a b : AST} {restVar : String} {bnds : List (String × AST)} (h : ACRestFlatSplit l fixed a b restVar bnds) : ∃ (r : ACMatch), matchACRest l fixed restVar (AST.sexp l [a, b]) bnds = some r

Completeness for one binary AC subject, stated over a split of its flattened leaves.

theorem MeTTaIL.AC.rebuild_middle_ac (acOp : Label → Bool) {l : Label} (hac : acOp l = true) (leaf : AST) (pre tail : List AST) (hrest : pre ++ tail ≠ []) : ACEq acOp (rebuild l (pre ++ leaf :: tail)) (AST.sexp l [leaf, rebuild l (pre ++ tail)])

Moving the selected AC leaf to the head preserves the rebuilt collection modulo AC.

theorem MeTTaIL.AC.matchACRestLoop_acEq (acOp : Label → Bool) {l : Label} (hac : acOp l = true) (fixed : AST) (restVar : String) (bnds : List (String × AST)) {preRev leaves : List AST} {r : ACMatch} : 2 ≤ (preRev.reverse ++ leaves).length → matchACRestLoop l fixed restVar bnds preRev leaves = some r → ACEq acOp (rebuild l (preRev.reverse ++ leaves)) r.witness

The AC-rest search witness is AC-equivalent to the rebuilt leaves being searched, provided the collection still has at least two leaves. That invariant is true for binary AC subjects.

theorem MeTTaIL.AC.flat_binary_length_two (l : Label) (a b : AST) : 2 ≤ (flat l (AST.sexp l [a, b])).length

A binary AC subject has at least two flattened leaves.

theorem MeTTaIL.AC.matchACRest_acEq {acOp : Label → Bool} {l : Label} (hac : acOp l = true) {fixed : AST} {restVar : String} {subject : AST} {bnds : List (String × AST)} {r : ACMatch} (hm : matchACRest l fixed restVar subject bnds = some r) : ACEq acOp subject r.witness

A successful AC-rest match returns a representative AC-equivalent to the subject.

def MeTTaIL.AC.matchPatACRaw (acOp : Label → Bool) : AST → AST → List (String × AST) → Option ACMatch

AC-aware first-order matching. The AC-specific case is linear: one fixed subpattern and one rest variable under an AC binary collection.

Equations

• One or more equations did not get rendered due to their size.
• MeTTaIL.AC.matchPatACRaw acOp (MeTTaIL.AST.sexp l [fixed, MeTTaIL.AST.var (MeTTaIL.DottedPath.base restVar)]) x✝¹ x✝ = if acOp l = true then MeTTaIL.AC.matchACRest l fixed restVar x✝¹ x✝ else none
• MeTTaIL.AC.matchPatACRaw acOp x✝² x✝¹ x✝ = if (x✝² == x✝¹) = true then some { bnds := x✝, witness := x✝¹ } else none

def MeTTaIL.AC.matchPatACRawList (acOp : Label → Bool) : List AST → List AST → List (String × AST) → Option ACMatchList

Pointwise AC-aware matching for argument lists.

Equations

• One or more equations did not get rendered due to their size.
• MeTTaIL.AC.matchPatACRawList acOp [] [] x✝ = some { bnds := x✝, witnesses := [] }
• MeTTaIL.AC.matchPatACRawList acOp x✝² x✝¹ x✝ = none

def MeTTaIL.AC.matchPatAC (acOp : Label → Bool) (pat t : AST) (bnds : List (String × AST)) : Option (List (String × AST))

Public AC-aware matcher.

Equations

• MeTTaIL.AC.matchPatAC acOp pat t bnds = Option.map (fun (r : MeTTaIL.AC.ACMatch) => r.bnds) (MeTTaIL.AC.matchPatACRaw acOp pat t bnds)

theorem MeTTaIL.AC.matchPatACRaw_acRest_sound {acOp : Label → Bool} {l : Label} {fixed subject : AST} {restVar : String} {bnds : List (String × AST)} {r : ACMatch} (hac : acOp l = true) (hm : matchPatACRaw acOp (acRestPattern l fixed restVar) subject bnds = some r) : ACEq acOp subject r.witness ∧ (acRestPattern l fixed restVar).matchPat r.witness bnds = some r.bnds

A successful linear AC-rest match has an AC-equivalent syntactic representative accepted by the ordinary matcher.

theorem MeTTaIL.AC.matchPatACRaw_acRest_witness {acOp : Label → Bool} {l : Label} {fixed subject : AST} {restVar : String} {bnds : List (String × AST)} {r : ACMatch} (hac : acOp l = true) (hm : matchPatACRaw acOp (acRestPattern l fixed restVar) subject bnds = some r) : (acRestPattern l fixed restVar).matchPat r.witness bnds = some r.bnds

A successful linear AC-rest match has a syntactic representative accepted by the ordinary matcher.

theorem MeTTaIL.AC.matchPatAC_acRest_raw {acOp : Label → Bool} {l : Label} {fixed subject : AST} {restVar : String} {bnds bnds' : List (String × AST)} (hm : matchPatAC acOp (acRestPattern l fixed restVar) subject bnds = some bnds') : ∃ (r : ACMatch), matchPatACRaw acOp (acRestPattern l fixed restVar) subject bnds = some r ∧ r.bnds = bnds'

Lift a public AC-rest match back to the raw matcher result it erased.

theorem MeTTaIL.AC.matchPatAC_acRest_sound {acOp : Label → Bool} {l : Label} {fixed subject : AST} {restVar : String} {bnds bnds' : List (String × AST)} (hac : acOp l = true) (hm : matchPatAC acOp (acRestPattern l fixed restVar) subject bnds = some bnds') : ∃ (witness : AST), ACEq acOp subject witness ∧ (acRestPattern l fixed restVar).matchPat witness bnds = some bnds'

Public soundness bridge for the linear AC-rest fragment used by Cordial Miners.

theorem MeTTaIL.AC.matchPatAC_acRest_witness {acOp : Label → Bool} {l : Label} {fixed subject : AST} {restVar : String} {bnds bnds' : List (String × AST)} (hac : acOp l = true) (hm : matchPatAC acOp (acRestPattern l fixed restVar) subject bnds = some bnds') : ∃ (witness : AST), (acRestPattern l fixed restVar).matchPat witness bnds = some bnds'

Public witness theorem for the linear AC-rest fragment used by Cordial Miners.

theorem MeTTaIL.AC.matchPatAC_acRest_complete_of_flat_split {acOp : Label → Bool} {l : Label} {fixed a b : AST} {restVar : String} {bnds : List (String × AST)} (hac : acOp l = true) (h : ACRestFlatSplit l fixed a b restVar bnds) : ∃ (bnds' : List (String × AST)), matchPatAC acOp (acRestPattern l fixed restVar) (AST.sexp l [a, b]) bnds = some bnds'

Public completeness theorem for the linear AC-rest fragment. If the flattened binary AC subject has a split whose selected leaf matches the fixed subpattern and whose remaining leaves bind to the rest variable, the AC-aware matcher returns some bindings.

theorem MeTTaIL.AC.matchPatAC_acRest_complete_of_fresh_split {acOp : Label → Bool} {l : Label} {fixed a b : AST} {restVar : String} {bnds : List (String × AST)} {pre tail : List AST} {leaf : AST} {bnds₁ : List (String × AST)} (hac : acOp l = true) (hflat : flat l (AST.sexp l [a, b]) = pre ++ leaf :: tail) (hfixed : fixed.matchPat leaf bnds = some bnds₁) (hfresh : List.find? (fun (b : String × AST) => b.1 == restVar) bnds₁ = none) : ∃ (bnds' : List (String × AST)), matchPatAC acOp (acRestPattern l fixed restVar) (AST.sexp l [a, b]) bnds = some bnds'

Public completeness theorem for the common linear AC-rest case. If a selected flattened leaf matches the fixed subpattern and the rest variable is fresh after that match, the AC-aware matcher succeeds. This is the Cordial Miners rule shape: one observed fact or event, and one variable for the rest of the collection.

theorem MeTTaIL.AC.matchPatACRaw_sound (acOp : Label → Bool) (pat t : AST) (bnds : List (String × AST)) (r : ACMatch) : matchPatACRaw acOp pat t bnds = some r → ACEq acOp t r.witness ∧ pat.matchPat r.witness bnds = some r.bnds

Raw AC-aware matcher soundness. A successful match returns an AC-equivalent witness accepted by the ordinary matcher.

theorem MeTTaIL.AC.matchPatAC_sound {acOp : Label → Bool} {pat subject : AST} {bnds bnds' : List (String × AST)} (hm : matchPatAC acOp pat subject bnds = some bnds') : ∃ (witness : AST), ACEq acOp subject witness ∧ pat.matchPat witness bnds = some bnds'

Public AC-aware matcher soundness.

def MeTTaIL.AC.applyBaseRewriteAC (acOp : Label → Bool) (rd : RewriteDecl) (t : AST) : Option AST

Apply one premise-free rewrite using AC-aware matching.

Equations

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

def MeTTaIL.AC.baseReductsAC (acOp : Label → Bool) (p : Presentation) (t : AST) : List AST

Every top-level AC-aware base reduct of a term.

Equations

• MeTTaIL.AC.baseReductsAC acOp p t = List.filterMap (fun (rd : MeTTaIL.RewriteDecl) => MeTTaIL.AC.applyBaseRewriteAC acOp rd t) p.rewrites

theorem MeTTaIL.AC.reduces_of_applyBaseRewriteAC {acOp : Label → Bool} {p : Presentation} {rd : RewriteDecl} {t t' : AST} (hmem : rd ∈ p.rewrites) (h : applyBaseRewriteAC acOp rd t = some t') : ∃ (witness : AST), ACEq acOp t witness ∧ Reduces p witness t'

Every AC-aware base rewrite has an AC-equivalent ordinary-rewrite witness.

theorem MeTTaIL.AC.reduces_of_mem_baseReductsAC {acOp : Label → Bool} {p : Presentation} {t t' : AST} (h : t' ∈ baseReductsAC acOp p t) : ∃ (witness : AST), ACEq acOp t witness ∧ Reduces p witness t'

Every member of baseReductsAC has an AC-equivalent ordinary-rewrite witness.

theorem MeTTaIL.AC.rewStepModAC_of_mem_baseReductsAC {acOp : Label → Bool} {p : Presentation} {t t' : AST} (h : t' ∈ baseReductsAC acOp p t) : RewStepModAC acOp p t t'

A top-level executable AC-aware reduct is a genuine rewrite modulo AC.

theorem MeTTaIL.AC.rewStepModAC_arg {acOp : Label → Bool} {p : Presentation} {l : Label} {pre post : List AST} {a a' : AST} (h : RewStepModAC acOp p a a') : RewStepModAC acOp p (AST.sexp l (pre ++ a :: post)) (AST.sexp l (pre ++ a' :: post))

Lift a rewrite modulo AC through one sexp argument context.

theorem MeTTaIL.AC.rewStepModAC_substB {acOp : Label → Bool} {p : Presentation} {b b' r : AST} {v : DottedPath} (h : RewStepModAC acOp p b b') : RewStepModAC acOp p (b.subst r v) (b'.subst r v)

Lift a rewrite modulo AC through the body of a subst node.

theorem MeTTaIL.AC.rewStepModAC_substR {acOp : Label → Bool} {p : Presentation} {b r r' : AST} {v : DottedPath} (h : RewStepModAC acOp p r r') : RewStepModAC acOp p (b.subst r v) (b.subst r' v)

Lift a rewrite modulo AC through the replacement of a subst node.

def MeTTaIL.AC.oneStepAC' (acOp : Label → Bool) (p : Presentation) : AST → Option AST

One leftmost-outermost step using AC-aware matching at every visited node.

Equations

• One or more equations did not get rendered due to their size.
• MeTTaIL.AC.oneStepAC' acOp p (MeTTaIL.AST.var x_1) = match MeTTaIL.AC.baseReductsAC acOp p (MeTTaIL.AST.var x_1) with | r :: tail => some r | [] => none

def MeTTaIL.AC.oneStepACList' (acOp : Label → Bool) (p : Presentation) : List AST → Option (List AST)

One AC-aware step inside the first reducible list element.

Equations

• One or more equations did not get rendered due to their size.
• MeTTaIL.AC.oneStepACList' acOp p [] = none

def MeTTaIL.AC.evalAC' (acOp : Label → Bool) (p : Presentation) : ℕ → AST → AST

Fuel-bounded evaluation using the AC-aware stepper.

Equations

• MeTTaIL.AC.evalAC' acOp p 0 x✝ = x✝
• MeTTaIL.AC.evalAC' acOp p n.succ x✝ = match MeTTaIL.AC.oneStepAC' acOp p x✝ with | some t' => MeTTaIL.AC.evalAC' acOp p n t' | none => x✝

theorem MeTTaIL.AC.oneStepAC'_sound (acOp : Label → Bool) (p : Presentation) (t : AST) {t' : AST} : oneStepAC' acOp p t = some t' → RewStepModAC acOp p t t'

Soundness: every executable AC-aware one-step reduct is a genuine rewrite modulo AC.

theorem MeTTaIL.AC.oneStepACList'_sound (acOp : Label → Bool) (p : Presentation) (args : List AST) {args' : List AST} : oneStepACList' acOp p args = some args' → ∃ (pre : List AST) (a : AST) (a' : AST) (post : List AST), args = pre ++ a :: post ∧ args' = pre ++ a' :: post ∧ RewStepModAC acOp p a a'

Soundness for the AC-aware list stepper.

theorem MeTTaIL.AC.evalAC'_sound (acOp : Label → Bool) (p : Presentation) (fuel : ℕ) (t : AST) : Relation.ReflTransGen (RewStepModAC acOp p) t (evalAC' acOp p fuel t)

Soundness of fuel-bounded AC-aware evaluation.