Spatial paths

A path is a finite sequence of locations, the spatial counterpart of a temporal interval. Zwarts gives paths an algebra: concatenation, defined only when one path ends where the next starts, the subpath order, and Krifka's adjacency of paths that share an endpoint. Zwarts's own paths are continuous curves, mathlib's topological _root_.Path, but he allows sequences of places as compatible with the algebra, and they keep every operation computable.

Pantcheva classifies paths by where they are inside a region. On any path parametrized by a bounded linear order of positions, a sequence of places or a curve, the positions inside the region form a set, and its order-theoretic shape is the path's: an upper set for a cofinal path (to), a lower set for a coinitial one (from), an interval missing both ends for a transitive one (past), the last position alone for a terminative one (up to). Reparametrizing keeps the shape and reversing the order reverses it, so a source path is a reversed goal path. An event domain's spatial trace sends each event to the path it traverses, as its temporal trace sends it to its run time.

Main definitions

• Spatial.Path: a directed trajectory, a source with later steps, ending at Path.goal.
• Spatial.Path.IsConcat, Subpath, adjacent, reverse: the path algebra.
• Spatial.Path.Direction: Place, Goal, Source and Route, in containment order.
• Spatial.Path.Shape, Shape.direction, Shape.transition: the eight shapes.
• Spatial.Path.IsCofinal, IsCoinitial, IsTransitive, IsTerminative, IsEgressive, IsProlative, IsApproximative, IsRecessive, HasShape: the shapes of a parametrized path relative to a region.
• Spatial.Path.toFun: a path's places indexed by their positions.
• Spatial.Localization: interior, surface or exterior.
• Event.SpatialTrace: the spatial trace of an event domain.

Main results

• Spatial.Path.Direction.lt_iff_shells_ssubset: the containment order is strict inclusion of head stacks.
• Spatial.Path.Shape.exists_direction_transition_iff: a direction and a transition combine into a shape exactly when the direction is not Place and a route is not delimited.
• Spatial.Path.hasShape_comp, hasShape_comp_ofDual: reparametrizing keeps the shape, and traversing the other way reverses it.
• Spatial.Path.hasShape_reverse: reversing a path reverses its shape.
• Spatial.Path.IsCofinal.not_isCoinitial: no path is both cofinal and coinitial.

References

• [Zwa05]
• [Kri98]
• [Pan11]

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

A path is a directed trajectory through space, given by the finite sequence of locations it visits.

• source : Loc

  The location the path starts from.

• steps : List Loc

  The later locations, which are 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 ⋯

@[instance_reducible]

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

Equations

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

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.

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

The goal of a path is its last location.

Equations

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

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

The points of a path are its locations from source to goal.

Equations

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

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

The constant path at l visits only l.

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

IsConcat p q r says that r is the concatenation p + q, defined only when p ends where q starts.

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 when concatenating some paths 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 is a scoped instance, since paths are also studied under a rival total lattice sum (the SemilatticeSup (Path Loc) of Studies/GoldbergJackendoff2004.lean). Activate it 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 when the goal of one is the source of the other, Krifka's spatial adjacency.

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.

Reversal

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

The reverse of a path traverses it from its goal to its source.

Equations

• p.reverse = { source := p.goal, steps := p.points.reverse.tail }

@[simp]

theorem Spatial.Path.source_reverse {Loc : Type u_1} (p : Path Loc) : p.reverse.source = p.goal

@[simp]

theorem Spatial.Path.points_reverse {Loc : Type u_1} (p : Path Loc) : p.reverse.points = p.points.reverse

@[simp]

theorem Spatial.Path.goal_reverse {Loc : Type u_1} (p : Path Loc) : p.reverse.goal = p.source

@[simp]

theorem Spatial.Path.reverse_reverse {Loc : Type u_1} (p : Path Loc) : p.reverse.reverse = p

Directions

inductive Spatial.Path.Direction : Type

The direction heads of a path, in containment order, Goal built on Place, Source on Goal, and Route on Source.

• place : Direction

  Place is static location, the base of the others.

• goal : Direction

  Goal is motion to.

• source : Direction

  Source is motion from.

• route : Direction

  Route is motion via or past.

@[instance_reducible]

instance Spatial.Path.instDecidableEqDirection : DecidableEq Direction

Equations

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

@[instance_reducible]

instance Spatial.Path.instReprDirection : Repr Direction

Equations

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

def Spatial.Path.instReprDirection.repr : Direction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Spatial.Path.instFintypeDirection : Fintype Direction

Equations

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

def Spatial.Path.Direction.rank : Direction → Fin 4

The number of heads below a direction.

Equations

• Spatial.Path.Direction.place.rank = 0
• Spatial.Path.Direction.goal.rank = 1
• Spatial.Path.Direction.source.rank = 2
• Spatial.Path.Direction.route.rank = 3

def Spatial.Path.Direction.shells (d : Direction) : Finset (Fin 4)

The heads a direction contains, a downward-closed stack.

Equations

• d.shells = Finset.Iic d.rank

theorem Spatial.Path.Direction.lt_iff_shells_ssubset (d₁ d₂ : Direction) : d₁.rank < d₂.rank ↔ d₁.shells ⊂ d₂.shells

Strict rank is strict inclusion of head stacks.

def Spatial.Path.Direction.reverse : Direction → Direction

The direction of a path traversed the other way swaps Goal and Source and keeps Place and Route.

Equations

• Spatial.Path.Direction.goal.reverse = Spatial.Path.Direction.source
• Spatial.Path.Direction.source.reverse = Spatial.Path.Direction.goal
• x✝.reverse = x✝

@[simp]

theorem Spatial.Path.Direction.reverse_reverse (d : Direction) : d.reverse.reverse = d

Shapes

inductive Spatial.Path.Transition : Type

How a path relates its run inside the region to its run outside.

• transitional : Transition

  The path changes its relation to the region, as to does.

• delimited : Transition

  The path changes it at one point, which bounds the motion, as up to does.

• nonTransitional : Transition

  The path does not change it, as towards does.

@[instance_reducible]

instance Spatial.Path.instDecidableEqTransition : DecidableEq Transition

Equations

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

def Spatial.Path.instReprTransition.repr : Transition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Spatial.Path.instReprTransition : Repr Transition

Equations

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

@[instance_reducible]

instance Spatial.Path.instFintypeTransition : Fintype Transition

Equations

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

inductive Spatial.Path.Shape : Type

The eight shapes of a path relative to a region.

• cofinal : Shape

  A cofinal path runs outside, then inside, as to does.

• coinitial : Shape

  A coinitial path runs inside, then outside, as from does.

• transitive : Shape

  A transitive path runs outside, inside and outside, as past does.

• terminative : Shape

  A terminative path runs outside up to its goal, which is inside, as up to does.

• egressive : Shape

  An egressive path starts inside and runs outside, as starting from does.

• approximative : Shape

  An approximative path runs outside, nearer at each point, as towards does.

• recessive : Shape

  A recessive path runs outside, farther at each point, as away from does.

• prolative : Shape

  A prolative path runs inside throughout, as along does.

@[instance_reducible]

instance Spatial.Path.instDecidableEqShape : DecidableEq Shape

Equations

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

@[instance_reducible]

instance Spatial.Path.instReprShape : Repr Shape

Equations

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

def Spatial.Path.instReprShape.repr : Shape → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Spatial.Path.instReprShape.repr Spatial.Path.Shape.cofinal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Spatial.Path.Shape.cofinal")).group prec✝

@[instance_reducible]

instance Spatial.Path.instFintypeShape : Fintype Shape

Equations

• Spatial.Path.instFintypeShape = { elems := { val := ↑Spatial.Path.Shape.enumList, nodup := Spatial.Path.Shape.enumList_nodup }, complete := Spatial.Path.instFintypeShape._proof_1 }

def Spatial.Path.Shape.direction : Shape → Direction

The direction of a shape.

Equations

• Spatial.Path.Shape.cofinal.direction = Spatial.Path.Direction.goal
• Spatial.Path.Shape.terminative.direction = Spatial.Path.Direction.goal
• Spatial.Path.Shape.approximative.direction = Spatial.Path.Direction.goal
• Spatial.Path.Shape.coinitial.direction = Spatial.Path.Direction.source
• Spatial.Path.Shape.egressive.direction = Spatial.Path.Direction.source
• Spatial.Path.Shape.recessive.direction = Spatial.Path.Direction.source
• Spatial.Path.Shape.transitive.direction = Spatial.Path.Direction.route
• Spatial.Path.Shape.prolative.direction = Spatial.Path.Direction.route

def Spatial.Path.Shape.transition : Shape → Transition

The transition of a shape.

Equations

• Spatial.Path.Shape.cofinal.transition = Spatial.Path.Transition.transitional
• Spatial.Path.Shape.coinitial.transition = Spatial.Path.Transition.transitional
• Spatial.Path.Shape.transitive.transition = Spatial.Path.Transition.transitional
• Spatial.Path.Shape.terminative.transition = Spatial.Path.Transition.delimited
• Spatial.Path.Shape.egressive.transition = Spatial.Path.Transition.delimited
• Spatial.Path.Shape.approximative.transition = Spatial.Path.Transition.nonTransitional
• Spatial.Path.Shape.recessive.transition = Spatial.Path.Transition.nonTransitional
• Spatial.Path.Shape.prolative.transition = Spatial.Path.Transition.nonTransitional

theorem Spatial.Path.Shape.direction_transition_injective : Function.Injective fun (s : Shape) => (s.direction, s.transition)

A shape is its direction and its transition.

theorem Spatial.Path.Shape.exists_direction_transition_iff (d : Direction) (t : Transition) : (∃ (s : Shape), s.direction = d ∧ s.transition = t) ↔ d ≠ Direction.place ∧ (d = Direction.route → t ≠ Transition.delimited)

A direction and a transition make a shape exactly when the direction is not Place and a Route is not delimited.

def Spatial.Path.Shape.reverse : Shape → Shape

The shape of a path traversed the other way.

Equations

• Spatial.Path.Shape.cofinal.reverse = Spatial.Path.Shape.coinitial
• Spatial.Path.Shape.coinitial.reverse = Spatial.Path.Shape.cofinal
• Spatial.Path.Shape.terminative.reverse = Spatial.Path.Shape.egressive
• Spatial.Path.Shape.egressive.reverse = Spatial.Path.Shape.terminative
• Spatial.Path.Shape.approximative.reverse = Spatial.Path.Shape.recessive
• Spatial.Path.Shape.recessive.reverse = Spatial.Path.Shape.approximative
• x✝.reverse = x✝

@[simp]

theorem Spatial.Path.Shape.reverse_reverse (s : Shape) : s.reverse.reverse = s

@[simp]

theorem Spatial.Path.Shape.direction_reverse (s : Shape) : s.reverse.direction = s.direction.reverse

@[simp]

theorem Spatial.Path.Shape.transition_reverse (s : Shape) : s.reverse.transition = s.transition

def Spatial.Path.Shape.IsBounded (s : Shape) : Prop

A shape is bounded when it has a transition, which makes the motion telic.

Equations

• s.IsBounded = (s.transition ≠ Spatial.Path.Transition.nonTransitional)

@[instance_reducible]

instance Spatial.Path.Shape.instDecidablePredIsBounded : DecidablePred IsBounded

Equations

• s.instDecidablePredIsBounded = { decide := !decide (s.transition = Spatial.Path.Transition.nonTransitional), reflects_decide := ⋯ }

Shapes relative to a region

A path parametrized by a bounded linear order of positions, a sequence of places or a curve, has the shape its positions inside a region give it: a cofinal path's form an upper set, a coinitial path's a lower set, a transitive path's an interval inside the path.

def Spatial.Path.IsCofinal {ι : Type u_2} {α : Type u_4} [LinearOrder ι] [BoundedOrder ι] (R : Set α) (γ : ι → α) : Prop

A cofinal path starts outside R, ends inside it, and stays inside once in, as a path to R does.

Equations

• Spatial.Path.IsCofinal R γ = (IsUpperSet (γ ⁻¹' R) ∧ γ ⊥ ∉ R ∧ γ ⊤ ∈ R)

def Spatial.Path.IsCoinitial {ι : Type u_2} {α : Type u_4} [LinearOrder ι] [BoundedOrder ι] (R : Set α) (γ : ι → α) : Prop

A coinitial path starts inside R, ends outside it, and stays outside once out, as a path from R does.

Equations

• Spatial.Path.IsCoinitial R γ = (IsLowerSet (γ ⁻¹' R) ∧ γ ⊥ ∈ R ∧ γ ⊤ ∉ R)

def Spatial.Path.IsTransitive {ι : Type u_2} {α : Type u_4} [LinearOrder ι] [BoundedOrder ι] (R : Set α) (γ : ι → α) : Prop

A transitive path starts and ends outside R and is inside it over one stretch, as a path past R is.

Equations

• Spatial.Path.IsTransitive R γ = ((γ ⁻¹' R).OrdConnected ∧ (γ ⁻¹' R).Nonempty ∧ γ ⊥ ∉ R ∧ γ ⊤ ∉ R)

def Spatial.Path.IsTerminative {ι : Type u_2} {α : Type u_4} [LinearOrder ι] [BoundedOrder ι] (R : Set α) (γ : ι → α) : Prop

A terminative path is inside R at its end only, as a path up to R is.

Equations

• Spatial.Path.IsTerminative R γ = (γ ⁻¹' R = {⊤} ∧ ⊥ ≠ ⊤)

def Spatial.Path.IsEgressive {ι : Type u_2} {α : Type u_4} [LinearOrder ι] [BoundedOrder ι] (R : Set α) (γ : ι → α) : Prop

An egressive path is inside R at its start only, as a path starting from R is.

Equations

• Spatial.Path.IsEgressive R γ = (γ ⁻¹' R = {⊥} ∧ ⊥ ≠ ⊤)

def Spatial.Path.IsProlative {ι : Type u_2} {α : Type u_4} (R : Set α) (γ : ι → α) : Prop

A prolative path is inside R throughout, as a path along R is.

Equations

• Spatial.Path.IsProlative R γ = ∀ (i : ι), γ i ∈ R

def Spatial.Path.IsApproximative {ι : Type u_2} {α : Type u_4} {β : Type u_5} [LinearOrder ι] (R : Set α) (γ : ι → α) [Preorder β] (d : α → β) : Prop

An approximative path is outside R throughout and nearer to it by d at each later position, as a path towards R is.

Equations

• Spatial.Path.IsApproximative R γ d = ((∀ (i : ι), γ i ∉ R) ∧ StrictAnti (d ∘ γ))

def Spatial.Path.IsRecessive {ι : Type u_2} {α : Type u_4} {β : Type u_5} [LinearOrder ι] (R : Set α) (γ : ι → α) [Preorder β] (d : α → β) : Prop

A recessive path is outside R throughout and farther from it by d at each later position, as a path away from R is.

Equations

• Spatial.Path.IsRecessive R γ d = ((∀ (i : ι), γ i ∉ R) ∧ StrictMono (d ∘ γ))

def Spatial.Path.HasShape {ι : Type u_2} {α : Type u_4} {β : Type u_5} [LinearOrder ι] [BoundedOrder ι] (R : Set α) (γ : ι → α) [Preorder β] (d : α → β) : Shape → Prop

HasShape d R γ s says that γ has shape s relative to R, d measuring nearness to it.

Equations

• Spatial.Path.HasShape R γ d Spatial.Path.Shape.cofinal = Spatial.Path.IsCofinal R γ
• Spatial.Path.HasShape R γ d Spatial.Path.Shape.coinitial = Spatial.Path.IsCoinitial R γ
• Spatial.Path.HasShape R γ d Spatial.Path.Shape.transitive = Spatial.Path.IsTransitive R γ
• Spatial.Path.HasShape R γ d Spatial.Path.Shape.terminative = Spatial.Path.IsTerminative R γ
• Spatial.Path.HasShape R γ d Spatial.Path.Shape.egressive = Spatial.Path.IsEgressive R γ
• Spatial.Path.HasShape R γ d Spatial.Path.Shape.approximative = Spatial.Path.IsApproximative R γ d
• Spatial.Path.HasShape R γ d Spatial.Path.Shape.recessive = Spatial.Path.IsRecessive R γ d
• Spatial.Path.HasShape R γ d Spatial.Path.Shape.prolative = Spatial.Path.IsProlative R γ

theorem Spatial.Path.IsTerminative.isCofinal {ι : Type u_2} {α : Type u_4} [LinearOrder ι] [BoundedOrder ι] {R : Set α} {γ : ι → α} (h : IsTerminative R γ) : IsCofinal R γ

A terminative path is cofinal.

theorem Spatial.Path.IsCofinal.not_isCoinitial {ι : Type u_2} {α : Type u_4} [LinearOrder ι] [BoundedOrder ι] {R : Set α} {γ : ι → α} (h : IsCofinal R γ) : ¬IsCoinitial R γ

No path is both cofinal and coinitial.

theorem Spatial.Path.HasShape.comp {ι : Type u_2} {κ : Type u_3} {α : Type u_4} {β : Type u_5} [LinearOrder ι] [BoundedOrder ι] [LinearOrder κ] [BoundedOrder κ] {R : Set α} {γ : ι → α} [Preorder β] {d : α → β} {s : Shape} (h : HasShape R γ d s) (e : κ ≃o ι) : HasShape R (γ ∘ ⇑e) d s

A path keeps its shape under reparametrization by an order isomorphism.

theorem Spatial.Path.hasShape_comp {ι : Type u_2} {κ : Type u_3} {α : Type u_4} {β : Type u_5} [LinearOrder ι] [BoundedOrder ι] [LinearOrder κ] [BoundedOrder κ] {R : Set α} {γ : ι → α} [Preorder β] {d : α → β} (e : κ ≃o ι) {s : Shape} : HasShape R (γ ∘ ⇑e) d s ↔ HasShape R γ d s

Reparametrizing a path by an order isomorphism keeps its shape.

theorem Spatial.Path.hasShape_comp_ofDual {ι : Type u_2} {α : Type u_4} {β : Type u_5} [LinearOrder ι] [BoundedOrder ι] {R : Set α} {γ : ι → α} [Preorder β] {d : α → β} {s : Shape} : HasShape R (γ ∘ ⇑OrderDual.ofDual) d s ↔ HasShape R γ d s.reverse

Traversing a path the other way, on the dual order of positions, reverses its shape.

Sequences of places as parametrized paths

def Spatial.Path.toFun {Loc : Type u_2} (p : Path Loc) : Fin (p.steps.length + 1) → Loc

A path's places, indexed by their positions.

Equations

• p.toFun i = p.points.get ⟨↑i, ⋯⟩

@[instance_reducible]

instance Spatial.Path.instCoeFunForallFinHAddNatLengthStepsOfNat {Loc : Type u_2} : CoeFun (Path Loc) fun (p : Path Loc) => Fin (p.steps.length + 1) → Loc

Equations

• Spatial.Path.instCoeFunForallFinHAddNatLengthStepsOfNat = { coe := Spatial.Path.toFun }

@[simp]

theorem Spatial.Path.coe_bot {Loc : Type u_2} (p : Path Loc) : p.toFun ⊥ = p.source

@[simp]

theorem Spatial.Path.coe_top {Loc : Type u_2} (p : Path Loc) : p.toFun ⊤ = p.goal

theorem Spatial.Path.length_steps_reverse {Loc : Type u_2} (p : Path Loc) : p.reverse.steps.length = p.steps.length

def Spatial.Path.revIso {Loc : Type u_2} (p : Path Loc) : Fin (p.reverse.steps.length + 1) ≃o (Fin (p.steps.length + 1))ᵒᵈ

The positions of a reversed path, as an order isomorphism onto the dual of the path's.

Equations

• p.revIso = (Fin.castOrderIso ⋯).trans Fin.revOrderIso.symm

theorem Spatial.Path.coe_reverse {Loc : Type u_2} (p : Path Loc) : p.reverse.toFun = (p.toFun ∘ ⇑OrderDual.ofDual) ∘ ⇑p.revIso

A reversed path is the path read on the dual order of positions.

theorem Spatial.Path.hasShape_reverse {Loc : Type u_2} (p : Path Loc) {β : Type u_3} [Preorder β] {d : Loc → β} {R : Set Loc} {s : Shape} : HasShape R p.reverse.toFun d s ↔ HasShape R p.toFun d s.reverse

Reversing a path reverses its shape.

Localization

inductive Spatial.Localization : Type

The part of the reference object a spatial expression localizes in, orthogonal to the direction.

• interior : Localization

  The interior, as of in, into and out of.

• surface : Localization

  The surface, as of on, onto and off.

• exterior : Localization

  The exterior, as of at, to and from.

@[instance_reducible]

instance Spatial.instDecidableEqLocalization : DecidableEq Localization

Equations

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

def Spatial.instReprLocalization.repr : Localization → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Spatial.instReprLocalization : Repr Localization

Equations

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

@[instance_reducible]

instance Spatial.instFintypeLocalization : Fintype Localization

Equations

• Spatial.instFintypeLocalization = { elems := { val := ↑Spatial.Localization.enumList, nodup := Spatial.Localization.enumList_nodup }, complete := Spatial.instFintypeLocalization._proof_1 }

class Event.SpatialTrace (E : Type u_1) (Loc : outParam (Type u_2)) : Type (max u_1 u_2)

The spatial trace of an event domain E, which sends each event to the path its theme traverses.

• σ : E → Spatial.Path Loc

  The path traversed in an event.