Dynamics and Generated Relations

SE.Persistence.Relation.Generated

Dynamics, and the two closures built from a step relation:

• Reach r: the reflexive-transitive closure, directed;
• Generated r: the equivalence closure, symmetric.

This module is generic. It knows nothing of classifications; later modules apply the closures to the steps of preserving transformations.

A Dynamics says how transformations act on a carrier. This module does not say what the carrier is.

structure SE.Persistence.Dynamics (T C : Type) : Type

How each transformation relates states of a carrier C: step t x y means y is a result of applying t to x.

• step : T → C → C → Prop

  step t x y: y is a result of applying t to x.

def SE.Persistence.freeDynamics (T : Type) : Dynamics T (T × Bool)

The free dynamics: each transformation t relates one private pair of states, (t, false) to (t, true), and nothing else.

Equations

• SE.Persistence.freeDynamics T = { step := fun (t : T) (x y : T × Bool) => x = (t, false) ∧ y = (t, true) }

inductive SE.Persistence.Reach {C : Type} (r : C → C → Prop) (x : C) : C → Prop

The reflexive-transitive closure of r, from a fixed start x.

• refl {C : Type} {r : C → C → Prop} {x : C} : Reach r x x
• tail {C : Type} {r : C → C → Prop} {x y z : C} : Reach r x y → r y z → Reach r x z

theorem SE.Persistence.Reach.single {C : Type} {r : C → C → Prop} {x y : C} (h : r x y) : Reach r x y

One step is a reach.

theorem SE.Persistence.Reach.trans {C : Type} {r : C → C → Prop} {x y z : C} (h1 : Reach r x y) (h2 : Reach r y z) : Reach r x z

Reach is transitive.

theorem SE.Persistence.Reach.mono {C : Type} {r s : C → C → Prop} (h : ∀ (x y : C), r x y → s x y) {x y : C} (hr : Reach r x y) : Reach s x y

Reach is monotone in the step relation.

inductive SE.Persistence.Generated {C : Type} (r : C → C → Prop) : C → C → Prop

The equivalence relation generated by r.

• rel {C : Type} {r : C → C → Prop} {x y : C} : r x y → Generated r x y
• refl {C : Type} {r : C → C → Prop} (x : C) : Generated r x x
• symm {C : Type} {r : C → C → Prop} {x y : C} : Generated r x y → Generated r y x
• trans {C : Type} {r : C → C → Prop} {x y z : C} : Generated r x y → Generated r y z → Generated r x z

theorem SE.Persistence.Generated.equivalence {C : Type} (r : C → C → Prop) : Equivalence (Generated r)

Generated r is an equivalence relation.

theorem SE.Persistence.Generated.le_of_equivalence {C : Type} {r s : C → C → Prop} (hs : Equivalence s) (h : ∀ (x y : C), r x y → s x y) {x y : C} (hg : Generated r x y) : s x y

Generated r is the least equivalence relation containing r.

theorem SE.Persistence.Generated.mono {C : Type} {r s : C → C → Prop} (h : ∀ (x y : C), r x y → s x y) {x y : C} (hg : Generated r x y) : Generated s x y

Generation is monotone in the generating relation.

theorem SE.Persistence.Reach.toGenerated {C : Type} {r : C → C → Prop} {x y : C} (h : Reach r x y) : Generated r x y

Every reach is a generated identity.