Reduction System

A reduction system is an operational semantics expressed as a relation between terms.

structure ReductionSystem (Term : Type u) : Type u

A reduction system is a relation between Terms.

• Red : Term → Term → Prop

  The reduction relation.

Multi-step reductions

@[reducible, inline]

abbrev ReductionSystem.MRed {Term : Type u_1} (rs : ReductionSystem Term) (a : Term) : Term → Prop

Multi-step reduction relation.

Equations

• rs.MRed = Relation.ReflTransGen rs.Red

theorem ReductionSystem.MRed.refl {Term : Type u_1} (rs : ReductionSystem Term) (t : Term) : rs.MRed t t

All multi-step reduction relations are reflexive.

theorem ReductionSystem.MRed.single {Term : Type u_1} {a b : Term} (rs : ReductionSystem Term) (h : rs.Red a b) : rs.MRed a b

Any reduction is a multi-step

instance instTransRedMRed {Term : Type u_1} (rs : ReductionSystem Term) : Trans rs.Red rs.MRed rs.MRed

Equations

• instTransRedMRed rs = inferInstance

instance instTransMRedRed {Term : Type u_1} (rs : ReductionSystem Term) : Trans rs.MRed rs.Red rs.MRed

Equations

• instTransMRedRed rs = inferInstance

def commandCreate_reduction_sys__ : Lean.ParserDescr

A command to create a ReductionSystem from a relation, robust to use of variable

Equations

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

def commandReduction_notation__ : Lean.ParserDescr

This command adds notations for a ReductionSystem.Red and ReductionSystem.MRed. This should not usually be called directly, but from the reduction_sys attribute.

As an example reduction_notation foo "β" will add the notations "⭢β" and "↠β".

Note that the string used will afterwards be registered as a notation. This means that if you have also used this as a constructor name, you will need quotes to access corresponding cases, e.g. «β» in the above example.

Equations

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

def reduction_sys : Lean.ParserDescr

This attribute calls the reduction_notation command for the annotated declaration, such as in:

@[reduction rs "ₙ", simp]
def PredReduction (a b : ℕ) : Prop := a = b + 1

Equations

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