inductive MeTTaIL.RewStep (p : Presentation) : AST → AST → Prop

One-step rewriting closed under context, the standard reduction relation of the presentation's rewrite system. The top rule embeds the existing top-level Reduces; the other rules let a step happen inside a sexp argument or a Subst component.

• top {p : Presentation} {t t' : AST} : Reduces p t t' → RewStep p t t'
• arg {p : Presentation} {l : Label} {pre post : List AST} {a a' : AST} : RewStep p a a' → RewStep p (AST.sexp l (pre ++ a :: post)) (AST.sexp l (pre ++ a' :: post))
• substB {p : Presentation} {b b' r : AST} {v : DottedPath} : RewStep p b b' → RewStep p (b.subst r v) (b'.subst r v)
• substR {p : Presentation} {b r r' : AST} {v : DottedPath} : RewStep p r r' → RewStep p (b.subst r v) (b.subst r' v)

theorem MeTTaIL.reduces_of_mem_baseReducts {p : Presentation} {t t' : AST} (h : t' ∈ baseReducts p t) : Reduces p t t'

Every member of baseReducts is a genuine top-level reduction.

def MeTTaIL.oneStep (p : Presentation) : AST → Option AST

One leftmost-outermost rewrite step, or none if the term is in normal form. Try a base rewrite at the root; if none applies, descend left to right into the arguments, then into the Subst components.

Equations

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

def MeTTaIL.oneStepList (p : Presentation) : List AST → Option (List AST)

One step inside the first reducible element of a list, or none if all are in normal form.

Equations

• MeTTaIL.oneStepList p [] = none
• MeTTaIL.oneStepList p (a :: as) = match MeTTaIL.oneStep p a with | some a' => some (a' :: as) | none => Option.map (fun (as' : List MeTTaIL.AST) => a :: as') (MeTTaIL.oneStepList p as)

theorem MeTTaIL.oneStep_sound (p : Presentation) (t : AST) {t' : AST} : oneStep p t = some t' → RewStep p t t'

Soundness: every executable one-step reduct is a genuine context rewrite.

theorem MeTTaIL.oneStepList_sound (p : Presentation) (args : List AST) {args' : List AST} : oneStepList p args = some args' → ∃ (pre : List AST), ∃ (a : AST), ∃ (a' : AST), ∃ (post : List AST), args = pre ++ a :: post ∧ args' = pre ++ a' :: post ∧ RewStep p a a'

Soundness for the list reducer: the result reduces exactly one element in place.