Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Temporal Graphs

Lax623795.TemporalGraphs · concepts/Lax623795/TemporalGraphs.lean · lax-623795

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A temporal graph has a positive finite lifetime and an undirected, loop-free graph at each consecutive positive time step. Its footprint contains every edge that appears during its lifetime, and it is always connected when every snapshot is connected. A temporal walk may be empty, with no visited vertices, or nonempty, with a start time, an end time, and snapshot edges traversed at strictly increasing times. A nonempty walk may remain at one vertex throughout its time interval. The reachable vertex set of XX in a time interval consists of the vertices reachable within that interval from at least one vertex of XX.

    Concept map
    1 concept; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
    2import Mathlib.Data.List.Chain
    3import Mathlib.Data.PNat.Notation
    4
    5/-!
    6---
    7title: Temporal Graphs
    8type: definition
    9---
    10
    11A temporal graph has a positive finite lifetime and an undirected, loop-free graph
    12at each consecutive positive time step. Its footprint contains every edge that
    13appears during its lifetime, and it is always connected when every snapshot is
    14connected. A temporal walk may be empty, with no visited vertices, or nonempty,
    15with a start time, an end time, and snapshot edges traversed at strictly increasing
    16times. A nonempty walk may remain at one vertex throughout its time interval. The
    17reachable vertex set of `X` in a time interval consists of the vertices reachable
    18within that interval from at least one vertex of `X`.
    19-/
    20
    21universe u
    22
    23namespace Lax623795.TemporalGraphs
    24
    25/--
    26A finite-lifetime temporal graph on the vertex type `V`.
    27
    28The positive natural number `lifetime` is the final time step. The snapshots are
    29indexed consecutively by the positive times `1, ..., lifetime`.
    30Each snapshot is the undirected, loop-free simple graph whose edges are
    31active at that time. The vertex type `V` is not required to be finite.
    32-/
    33structure TemporalGraph (V : Type u) where
    34 lifetime : ℕ+
    35 snapshot : { t : ℕ+ // t.val ≤ lifetime.val } → SimpleGraph V
    36
    37namespace TemporalGraph
    38
    39/-- A valid positive time step during the lifetime of `G`. -/
    40abbrev Timestep {V : Type u} (G : TemporalGraph V) :=
    41 { t : ℕ+ // t.val ≤ G.lifetime.val }
    42
    43/-- Two vertices are adjacent in `G` at time `t`. -/
    44def AdjAt {V : Type u} (G : TemporalGraph V)
    45 (t : G.Timestep) (x y : V) : Prop :=
    46 (G.snapshot t).Adj x y
    47
    48/-- The set of vertices adjacent to `v` in `G` at time `t`. -/
    49def neighborSetAt {V : Type u} (G : TemporalGraph V)
    50 (t : G.Timestep) (v : V) : Set V :=
    51 (G.snapshot t).neighborSet v
    52
    53/-- The static graph containing every edge that appears in any snapshot of `G`. -/
    54def footprint {V : Type u} (G : TemporalGraph V) : SimpleGraph V :=
    55 ⨆ t, G.snapshot t
    56
    57/-- A temporal graph is always connected when each of its snapshots is connected. -/
    58def AlwaysConnected {V : Type u} (G : TemporalGraph V) : Prop :=
    59 ∀ t, (G.snapshot t).Connected
    60
    61/-- A visit records the vertex occupied by a walk at a particular time step. -/
    62structure Visit {V : Type u} (G : TemporalGraph V) where
    63 vertex : V
    64 timestep : G.Timestep
    65
    66/-- `next` may follow `current` when time increases and the walk waits or traverses an edge. -/
    67def IsValidSuccessor {V : Type u} (G : TemporalGraph V)
    68 (current next : G.Visit) : Prop :=
    69 current.timestep.val.val < next.timestep.val.val ∧
    70 (current.vertex = next.vertex ∨
    71 G.AdjAt next.timestep current.vertex next.vertex)
    72
    73/--
    74A temporal walk is a chain of timed vertex visits.
    75
    76Times strictly increase. Between consecutive visits the walk either remains at the
    77same vertex or traverses an edge active at the later time. The empty list is the
    78temporal walk with no visited vertices.
    79-/
    80structure TemporalWalk {V : Type u} (G : TemporalGraph V) where
    81 visits : List G.Visit
    82 chain : visits.IsChain (G.IsValidSuccessor)
    83
    84namespace TemporalWalk
    85
    86/-- The temporal walk with no visited vertices. -/
    87def empty {V : Type u} (G : TemporalGraph V) : G.TemporalWalk where
    88 visits := []
    89 chain := .nil
    90
    91/-- The instantaneous temporal walk consisting of one visit. -/
    92def singleton {V : Type u} (G : TemporalGraph V)
    93 (v : V) (t : G.Timestep) : G.TemporalWalk where
    94 visits := [⟨v, t⟩]
    95 chain := .singleton _
    96
    97/-- A temporal walk that stays at `v` from `startTime` until the later `endTime`. -/
    98def stay {V : Type u} (G : TemporalGraph V) (v : V)
    99 (startTime endTime : G.Timestep)
    100 (h : startTime.val.val < endTime.val.val) : G.TemporalWalk where
    101 visits := [⟨v, startTime⟩, ⟨v, endTime⟩]
    102 chain := by
    103 simp [IsValidSuccessor, h]
    104
    105/-- The first visit of `W`, or `none` when `W` is empty. -/
    106def startVisit? {V : Type u} {G : TemporalGraph V} (W : G.TemporalWalk) : Option G.Visit :=
    107 W.visits.head?
    108
    109/-- The final visit of `W`, or `none` when `W` is empty. -/
    110def endVisit? {V : Type u} {G : TemporalGraph V} (W : G.TemporalWalk) : Option G.Visit :=
    111 W.visits.getLast?
    112
    113/-- The starting vertex of `W`, or `none` when `W` is empty. -/
    114def startVertex? {V : Type u} {G : TemporalGraph V} (W : G.TemporalWalk) : Option V :=
    115 W.startVisit?.map Visit.vertex
    116
    117/-- The final vertex of `W`, or `none` when `W` is empty. -/
    118def endVertex? {V : Type u} {G : TemporalGraph V} (W : G.TemporalWalk) : Option V :=
    119 W.endVisit?.map Visit.vertex
    120
    121/-- The starting time of `W`, or `none` when `W` is empty. -/
    122def startTime? {V : Type u} {G : TemporalGraph V} (W : G.TemporalWalk) : Option G.Timestep :=
    123 W.startVisit?.map Visit.timestep
    124
    125/-- The final time of `W`, or `none` when `W` is empty. -/
    126def endTime? {V : Type u} {G : TemporalGraph V} (W : G.TemporalWalk) : Option G.Timestep :=
    127 W.endVisit?.map Visit.timestep
    128
    129/-- Every visit of `W` occurs in the inclusive interval from `startTime` to `endTime`. -/
    130def IsWithin {V : Type u} {G : TemporalGraph V} (W : G.TemporalWalk)
    131 (startTime endTime : G.Timestep) : Prop :=
    132 ∀ visit ∈ W.visits,
    133 startTime.val.val ≤ visit.timestep.val.val ∧
    134 visit.timestep.val.val ≤ endTime.val.val
    135
    136/--
    137Two temporal walks can be concatenated when either one is empty, or when the first
    138ends at exactly the timed vertex where the second begins.
    139-/
    140def CanConcat {V : Type u} {G : TemporalGraph V}
    141 (W W' : G.TemporalWalk) : Prop :=
    142 match W.visits, W'.visits with
    143 | [], _ => True
    144 | _, [] => True
    145 | left, first :: _ => left.getLast? = some first
    146
    147/--
    148Concatenate compatible temporal walks, counting their common timed vertex only once.
    149The empty temporal walk is a left and right identity.
    150-/
    151def concat {V : Type u} {G : TemporalGraph V}
    152 (W W' : G.TemporalWalk) (h : W.CanConcat W') : G.TemporalWalk := by
    153 rcases W with ⟨visits, chain⟩
    154 rcases W' with ⟨visits', chain'⟩
    155 cases visits with
    156 | nil => exact ⟨visits', chain'⟩
    157 | cons first rest =>
    158 cases visits' with
    159 | nil => exact ⟨first :: rest, chain⟩
    160 | cons first' rest' =>
    161 refine ⟨(first :: rest) ++ rest', ?_⟩
    162 cases rest' with
    163 | nil => simpa using chain
    164 | cons second' tail' =>
    165 apply chain.append chain'.tail
    166 intro last hlast next hnext
    167 have hjoin : (first :: rest).getLast? = some first' := h
    168 have hlast_eq : last = first' := by
    169 rw [hjoin] at hlast
    170 have hlast_eq' : first' = last := by simpa using hlast
    171 exact hlast_eq'.symm
    172 have hnext_eq : next = second' := by
    173 have hnext_eq' : second' = next := by simpa using hnext
    174 exact hnext_eq'.symm
    175 simpa [hlast_eq, hnext_eq] using chain'.rel
    176
    177end TemporalWalk
    178
    179/-- Vertex `finish` is temporally reachable from `start` if a temporal walk joins them. -/
    180def Reachable {V : Type u} (G : TemporalGraph V) (start finish : V) : Prop :=
    181 ∃ W : G.TemporalWalk,
    182 W.startVertex? = some start ∧ W.endVertex? = some finish
    183
    184/--
    185The vertices reachable within `[startTime, endTime]` from at least one vertex in `X`.
    186-/
    187def reachableVertexSet {V : Type u} (G : TemporalGraph V) (X : Set V)
    188 (startTime endTime : G.Timestep) : Set V :=
    189 { finish | ∃ start ∈ X, ∃ W : G.TemporalWalk,
    190 W.startVertex? = some start ∧
    191 W.endVertex? = some finish ∧
    192 W.IsWithin startTime endTime }
    193
    194end TemporalGraph
    195
    196end Lax623795.TemporalGraphs
    197
    Builds on

    none

    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…