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

One-step reduction induced by a presentation's rewrites.

• step {p : Presentation} {t t' : AST} (rd : RewriteDecl) (bnds bnds' : List (String × AST)) : rd ∈ p.rewrites → rd.rw.conclusion.fst.matchPat t [] = some bnds → PremisesHold p rd.rw.premises bnds bnds' → t' = AST.inst bnds' rd.rw.conclusion.snd → Reduces p t t'

inductive MeTTaIL.PremisesHold (p : Presentation) : List Hyp → List (String × AST) → List (String × AST) → Prop

The premises of a rewrite hold under the current bindings, extending them with each premise's target binding (the reduct of its source).

• nil {p : Presentation} {bnds : List (String × AST)} : PremisesHold p [] bnds bnds
• cons {p : Presentation} {h : Hyp} {hs : List Hyp} {bnds rest : List (String × AST)} {B : AST} : Reduces p (AST.inst bnds (AST.var h.src)) B → PremisesHold p hs ((h.tgt.baseName, B) :: bnds) rest → PremisesHold p (h :: hs) bnds rest

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

Many-step reduction: the reflexive-transitive closure of Reduces.

• refl {p : Presentation} {t : AST} : ReducesMany p t t
• tail {p : Presentation} {t u v : AST} : ReducesMany p t u → Reduces p u v → ReducesMany p t v

theorem MeTTaIL.ReducesMany.single {p : Presentation} {t t' : AST} (h : Reduces p t t') : ReducesMany p t t'

A single reduction is a one-step reduction sequence.

theorem MeTTaIL.ReducesMany.trans {p : Presentation} {t u v : AST} (h₁ : ReducesMany p t u) (h₂ : ReducesMany p u v) : ReducesMany p t v

Many-step reduction is transitive.

theorem MeTTaIL.reduces_base (p : Presentation) (rd : RewriteDecl) (lhs rhs t : AST) (bnds : List (String × AST)) (hmem : rd ∈ p.rewrites) (hrw : rd.rw = Rewrite.base lhs rhs) (hmatch : lhs.matchPat t [] = some bnds) : Reduces p t (AST.inst bnds rhs)

A base rewrite (no premises) whose left-hand side matches t reduces t to the instantiated right-hand side.

theorem MeTTaIL.reduces_of_applyBaseRewrite (p : Presentation) (rd : RewriteDecl) (t t' : AST) (hmem : rd ∈ p.rewrites) (h : applyBaseRewrite rd t = some t') : Reduces p t t'

The executable matcher is sound for the reduction relation: every reduct that applyBaseRewrite produces from a rewrite of p is a genuine one-step reduction.