Spatial paths

Directed trajectories between locations, as finite location sequences — the spatial analog of temporal intervals, carrying [Zwa05]'s Appendix A path algebra in discrete form: partial concatenation (defined only head-to-tail), the subpath order, and endpoint-sharing adjacency ([Kri98]). Zwarts's own paths are continuous constant-speed curves [0,1] → ℝ³ — mathlib's topological _root_.Path, whose trans reparametrizes, so the algebra would need the arc-length quotient there; the paper endorses the constructive sequence-of-places route as equally compatible with the algebra, and it keeps every operation computable.

Main declarations

• Path: a directed trajectory — source plus later steps, with endpoint Path.goal; Path.const is the constant path, the identity of concatenation and least in the subpath order.
• Path.IsConcat: concatenation as in [Zwa05]'s (67) — r is p + q, defined only when p ends where q starts; associative, neither commutative nor idempotent.
• Path.Subpath: the subpath order of (68) — p ≤ q iff r + p + r′ = q for some r, r′; equivalently infix-hood of point sequences (Path.subpath_iff_infix), whence a scoped PartialOrder (open scoped Spatial.Path).
• Path.adjacent: endpoint-sharing spatial adjacency ([Kri98]), the spatial half of the movement relations in Studies/Krifka1998.lean.
• Path.Directionality: the source/goal/route trichotomy of directional prepositions ([Zwa05]); paired with Features.Telicity at use sites — the paper's two independent classificatory axes.

structure Spatial.Path (Loc : Type u_1) : Type u_1

A directed trajectory through space, as the finite sequence of visited locations. The spatial analog of a temporal NonemptyInterval.

• source : Loc

  The starting location p(0).

• steps : List Loc

  The later locations, ending at p(1); empty for a constant path.

@[instance_reducible]

instance Spatial.instDecidableEqPath {Loc✝ : Type u_1} [DecidableEq Loc✝] : DecidableEq (Path Loc✝)

Equations

• Spatial.instDecidableEqPath = Spatial.instDecidableEqPath.decEq

def Spatial.instDecidableEqPath.decEq {Loc✝ : Type u_1} [DecidableEq Loc✝] (x✝ x✝¹ : Path Loc✝) : Decidable (x✝ = x✝¹)

Equations

• Spatial.instDecidableEqPath.decEq { source := a, steps := a_1 } { source := b, steps := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Spatial.instReprPath.repr {Loc✝ : Type u_1} [Repr Loc✝] : Path Loc✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Spatial.instReprPath {Loc✝ : Type u_1} [Repr Loc✝] : Repr (Path Loc✝)

Equations

• Spatial.instReprPath = { reprPrec := Spatial.instReprPath.repr }

def Spatial.Path.goal {Loc : Type u_1} (p : Path Loc) : Loc

The endpoint p(1).

Equations

• p.goal = p.steps.getLastD p.source

def Spatial.Path.points {Loc : Type u_1} (p : Path Loc) : List Loc

The full point sequence p(0) … p(1).

Equations

• p.points = p.source :: p.steps

def Spatial.Path.const {Loc : Type u_1} (l : Loc) : Path Loc

The constant path at a location.

Equations

• Spatial.Path.const l = { source := l, steps := [] }

@[simp]

theorem Spatial.Path.goal_const {Loc : Type u_1} (l : Loc) : (const l).goal = l

theorem Spatial.Path.points_ne_nil {Loc : Type u_1} (p : Path Loc) : p.points ≠ []

theorem Spatial.Path.points_injective {Loc : Type u_1} : Function.Injective points

Concatenation and subpaths

def Spatial.Path.IsConcat {Loc : Type u_1} (p q r : Path Loc) : Prop

r is the concatenation p + q, defined only when p ends where q starts. Associative, neither commutative nor idempotent.

Equations

• p.IsConcat q r = (p.goal = q.source ∧ r = { source := p.source, steps := p.steps ++ q.steps })

theorem Spatial.Path.IsConcat.source_eq {Loc : Type u_1} {p q r : Path Loc} (h : p.IsConcat q r) : r.source = p.source

theorem Spatial.Path.IsConcat.goal_eq {Loc : Type u_1} {p q r : Path Loc} (h : p.IsConcat q r) : r.goal = q.goal

theorem Spatial.Path.IsConcat.points_eq {Loc : Type u_1} {p q r : Path Loc} (h : p.IsConcat q r) : r.points = p.points ++ q.steps

theorem Spatial.Path.isConcat_const {Loc : Type u_1} (l : Loc) : (const l).IsConcat (const l) (const l)

A constant path concatenates with itself to itself.

def Spatial.Path.Subpath {Loc : Type u_1} (p q : Path Loc) : Prop

p is a subpath of q if concatenating some r, r′ around p yields q.

Equations

• p.Subpath q = ∃ (r : Spatial.Path Loc), ∃ (r' : Spatial.Path Loc), ∃ (m : Spatial.Path Loc), r.IsConcat p m ∧ m.IsConcat r' q

theorem Spatial.Path.subpath_iff_infix {Loc : Type u_1} {p q : Path Loc} : p.Subpath q ↔ p.points <:+: q.points

Subpath-hood is infix-hood of point sequences.

@[instance_reducible]

def Spatial.Path.instSubpathOrder {Loc : Type u_1} : PartialOrder (Path Loc)

The subpath order, as a scoped instance: path sets are also studied under a rival total lattice sum ([Kri98]'s part structures, hypothesized as SemilatticeSup (Path Loc) in Events/SpatialTrace.lean). Activate with open scoped Spatial.Path.

Equations

• Spatial.Path.instSubpathOrder = { le := Spatial.Path.Subpath, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem Spatial.Path.const_source_le {Loc : Type u_1} (p : Path Loc) : const p.source ≤ p

Constant paths are least in the subpath order.

Adjacency

def Spatial.Path.adjacent {Loc : Type u_1} (p1 p2 : Path Loc) : Prop

Two paths are adjacent if one's goal is the other's source — [Kri98]'s spatial adjacency ∞_H, the spatial half of the movement relations in Studies/Krifka1998.lean.

Equations

• p1.adjacent p2 = (p1.goal = p2.source ∨ p2.goal = p1.source)

theorem Spatial.Path.adjacent_comm {Loc : Type u_1} {p1 p2 : Path Loc} : p1.adjacent p2 ↔ p2.adjacent p1

Path adjacency is symmetric.

@[simp]

theorem Spatial.Path.adjacent_self {Loc : Type u_1} {p : Path Loc} : p.adjacent p ↔ p.goal = p.source

A path is adjacent to itself iff it is a loop.

theorem Spatial.Path.IsConcat.adjacent {Loc : Type u_1} {p q r : Path Loc} (h : p.IsConcat q r) : p.adjacent q

Concatenable paths are adjacent.

Directionality

inductive Spatial.Path.Directionality : Type

The source/goal/route trichotomy of directional prepositions ([Zwa05]): source prepositions (from, out of) locate the starting point p(0), goal prepositions (to, into) the endpoint p(1), route prepositions (over, through, via) an interior point. Independent of prepositional aspect — to is goal-directed telic, towards goal-directed atelic — so consumers pair it with Features.Telicity; the aspect axis is grounded in Studies/Zwarts2005.lean.

• source : Directionality
• goal : Directionality
• route : Directionality

@[instance_reducible]

instance Spatial.Path.instDecidableEqDirectionality : DecidableEq Directionality

Equations

• Spatial.Path.instDecidableEqDirectionality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Spatial.Path.instReprDirectionality.repr : Directionality → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Spatial.Path.instReprDirectionality : Repr Directionality

Equations

• Spatial.Path.instReprDirectionality = { reprPrec := Spatial.Path.instReprDirectionality.repr }