def Relation (A : Type u) : Type u

Equations

• Relation A = (A → A → Prop)

def IsReflexive {A : Type u_1} (r : Relation A) : Prop

Equations

• IsReflexive r = ∀ (x : A), r x x

@[reducible, inline]

abbrev IsTransitive {A : Type u_1} (r : Relation A) : Prop

Equations

• IsTransitive r = ∀ (x y z : A), r x y → r y z → r x z

def RComp {A : Type u} (R₁ R₂ : Relation A) : Relation A

Composition of two relations: RComp R₁ R₂ a c holds when some intermediate b has R₁ a b and R₂ b c. Read left-to-right: "first R₁, then R₂".

The scoped notation R₁ ∘ R₂ is available via open scoped Relations.

Equations

• RComp R₁ R₂ a c = ∃ (b : A), R₁ a b ∧ R₂ b c

def Relations.«term_∘_» : Lean.TrailingParserDescr

Equations

• Relations.«term_∘_» = Lean.ParserDescr.trailingNode `Relations.«term_∘_» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ ") (Lean.ParserDescr.cat `term 90))

inductive ReflTrans {A : Type u} (r : Relation A) : Relation A

r is dense when every related pair has an interpolating midpoint: r a c splits into r a b and r b c. This is exactly r ⊆ RComp r r, the dual of RComp.collapse's RComp r r ⊆ r (transitivity): density lets a single relatedness fact be re-expressed as the two-step form that a composed relation consumes.

• refl {A : Type u} {r : Relation A} (x : A) : ReflTrans r x x
• step {A : Type u} {r : Relation A} (x y z : A) : r x y → ReflTrans r y z → ReflTrans r x z

Type-valued reflexive transitive closure

ReflTrans lives in Prop, so Lean's large-elimination restriction forbids pattern-matching on it to produce data (e.g. a Nat step count). ReflTransT is the identical definition but in Type, which allows:

• Structural recursion on derivations — useful when a proof needs well-founded recursion keyed on the length of a multi-step execution (e.g. loop-simulation arguments where each iteration strictly shrinks the remaining trace).
• Step counting via ReflTransT.len — enables termination_by / decreasing_by on the derivation length.

Convert between the two with reflTrans_nonempty_T (Prop → Nonempty Type) and reflTransT_to_prop (Type → Prop). The Prop-to-Type direction requires Classical.choice (reflTrans_to_T), so definitions that use it are noncomputable; this is harmless when the final result is again a Prop.

inductive ReflTransT {A : Type u} (r : A → A → Prop) : A → A → Type u

• refl {A : Type u} {r : A → A → Prop} (x : A) : ReflTransT r x x
• step {A : Type u} {r : A → A → Prop} (x y z : A) : r x y → ReflTransT r y z → ReflTransT r x z

theorem reflTrans_nonempty_T {A : Type u} {r : A → A → Prop} {a b : A} : ReflTrans r a b → Nonempty (ReflTransT r a b)

noncomputable def reflTrans_to_T {A : Type u} {r : A → A → Prop} {a b : A} : ReflTrans r a b → ReflTransT r a b

Equations

• reflTrans_to_T h = Classical.choice ⋯

def ReflTransT.len {A : Type u_1} {r : A → A → Prop} {a b : A} : ReflTransT r a b → Nat

Equations

• (ReflTransT.refl a).len = 0
• (ReflTransT.step a y b a_1 rest).len = 1 + rest.len

Trace-producing reflexive transitive closure

inductive ReflTransTrace {A : Type u} {E : Type v} (r : A → List E → A → Prop) : A → List E → A → Prop

IsReflexive-transitive closure of a relation whose steps emit a list of observations. The accumulated trace is chronological: a step's output precedes the trace emitted by the remaining execution.

• refl {A : Type u} {E : Type v} {r : A → List E → A → Prop} (x : A) : ReflTransTrace r x [] x

  IsReflexive execution emits the empty trace.

• step {A : Type u} {E : Type v} {r : A → List E → A → Prop} (x : A) (emitted : List E) (y : A) (rest : List E) (z : A) : r x emitted y → ReflTransTrace r y rest z → ReflTransTrace r x (emitted ++ rest) z

  Prepend one labeled step to a traced execution, concatenating its events before the remaining trace.

def ReflTransTraceN {A : Type u} {E : Type v} (r : A → List E → A → Prop) : Nat → A → List E → A → Prop

ReflTransTrace bounded by a number of steps: x reaches z in at most n steps of r, emitting t. A property quantified over every bound covers every finite execution, with no induction on the execution itself.

Equations

• ReflTransTraceN r 0 x✝² x✝¹ x✝ = (x✝² = x✝ ∧ x✝¹ = [])
• ReflTransTraceN r n.succ x✝² x✝¹ x✝ = (x✝² = x✝ ∧ x✝¹ = [] ∨ ∃ (emitted : List E), ∃ (y : A), ∃ (rest : List E), r x✝² emitted y ∧ ReflTransTraceN r n y rest x✝ ∧ x✝¹ = emitted ++ rest)

Type-valued trace-producing reflexive transitive closure

The Type-valued analogue of ReflTransTrace, standing to it as ReflTransT does to ReflTrans. Living in Type permits structural recursion on a traced derivation to produce data — in particular a step count via ReflTransTraceT.len — which is what lets a loop-simulation argument recurse on the strictly shrinking length of the remaining execution while still tracking the chronological trace it emits.

inductive ReflTransTraceT {A : Type u} {E : Type v} (r : A → List E → A → Prop) : A → List E → A → Type (max u v)

• refl {A : Type u} {E : Type v} {r : A → List E → A → Prop} (x : A) : ReflTransTraceT r x [] x
• step {A : Type u} {E : Type v} {r : A → List E → A → Prop} (x : A) (emitted : List E) (y : A) (rest : List E) (z : A) : r x emitted y → ReflTransTraceT r y rest z → ReflTransTraceT r x (emitted ++ rest) z

def ReflTransTraceT.len {A : Type u} {E : Type v} {r : A → List E → A → Prop} {a : A} {tr : List E} {b : A} : ReflTransTraceT r a tr b → Nat

Equations

• (ReflTransTraceT.refl x✝).len = 0
• (ReflTransTraceT.step x✝¹ emitted y rest x✝ a rest_1).len = 1 + rest_1.len