Theory /Cortex /Graph /Safety

Cortex.Graph.Safety

proofs

On this page

Overview
Context
Theorem Split
Relation Reachability
Runtime-Style Edge Predicate
Endpoint Closure
Graph Expression Safety
Quotient Safety

Imports

import Cortex.Graph.Quotient

Overview

Safety-facing graph facts for the Cortex proof stack.

Context

Cortex.Graph.Relation gives Mokhov graph expressions their finite relation denotation. Track 2 and Track 3 need more than the algebraic laws: they need a shared path, acyclicity, and endpoint-closure vocabulary that can bridge the relation model into Pulse DAGs and Wire rewrite validity.

This module deliberately stays inside Cortex.Graph.*. It does not import Pulse or Wire; downstream tracks consume these declarations to avoid duplicating reachability and topology-validity definitions.

Theorem Split

The page defines relation-level paths and acyclicity, proves endpoint closure for Mokhov relation constructors and denoted graph expressions, and lifts the acyclicity predicate through raw graph equality and the quotient carrier.

namespace Cortex.Graph

Relation Reachability

namespace Relationvariable {α : Type}

Path relation source target is non-empty reachability through relation edges.

inductive Path (relation : Relation α) : α → α → Prop where
  | direct {source target : α} :
      (source, target) ∈ relation.edges → Path relation source target
  | trans {source middle target : α} :
      Path relation source middle →
        Path relation middle target →
          Path relation source target

Acyclic relation rules out non-empty paths from a node back to itself.

def Acyclic (relation : Relation α) : Prop :=
  ∀ node : α, ¬ Path relation node node

namespace Path

Path.source_mem keeps a reachable source inside an endpoint-closed relation.

theorem source_mem
    {relation : Relation α}
    (hEndpoints : EdgeEndpointsInVertices relation)
    {source target : α}
    (hPath : Path relation source target) :
    source ∈ relation.vertices := byα:Typerelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticessource:αtarget:αhPath:relation.Path source target⊢ source ∈ relation.vertices
  induction hPath with
  | direct hEdge =>directα:Typerelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticessource:αtarget:αsource✝:αtarget✝:αhEdge:(source✝, target✝) ∈ relation.edges⊢ source✝ ∈ relation.vertices
      exact (hEndpoints _ hEdge).1All goals completed! 🐙
  | trans _ _ ihLeft _ =>transα:Typerelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticessource:αtarget:αsource✝:αmiddle✝:αtarget✝:αa✝¹:relation.Path source✝ middle✝a✝:relation.Path middle✝ target✝ihLeft:source✝ ∈ relation.verticesa_ih✝:middle✝ ∈ relation.vertices⊢ source✝ ∈ relation.vertices
      exact ihLeftAll goals completed! 🐙

Path.target_mem keeps a reachable target inside an endpoint-closed relation.

theorem target_mem
    {relation : Relation α}
    (hEndpoints : EdgeEndpointsInVertices relation)
    {source target : α}
    (hPath : Path relation source target) :
    target ∈ relation.vertices := byα:Typerelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticessource:αtarget:αhPath:relation.Path source target⊢ target ∈ relation.vertices
  induction hPath with
  | direct hEdge =>directα:Typerelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticessource:αtarget:αsource✝:αtarget✝:αhEdge:(source✝, target✝) ∈ relation.edges⊢ target✝ ∈ relation.vertices
      exact (hEndpoints _ hEdge).2All goals completed! 🐙
  | trans _ _ _ ihRight =>transα:Typerelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticessource:αtarget:αsource✝:αmiddle✝:αtarget✝:αa✝¹:relation.Path source✝ middle✝a✝:relation.Path middle✝ target✝a_ih✝:middle✝ ∈ relation.verticesihRight:target✝ ∈ relation.vertices⊢ target✝ ∈ relation.vertices
      exact ihRightAll goals completed! 🐙

end Path

Runtime-Style Edge Predicate

section RuntimeEdgePredicatevariable [DecidableEq α]

edgeBool relation source target is the boolean edge predicate for a finite relation.

def edgeBool (relation : Relation α) (source target : α) : Bool :=
  decide ((source, target) ∈ relation.edges)

edgeBool_true_iff relates the boolean edge predicate to relation membership.

theorem edgeBool_true_iff
    (relation : Relation α)
    (source target : α) :
    edgeBool relation source target = true ↔ (source, target) ∈ relation.edges := byα:Typeinst✝:DecidableEq αrelation:Relation αsource:αtarget:α⊢ relation.edgeBool source target = true ↔ (source, target) ∈ relation.edges
  simp [edgeBool]All goals completed! 🐙

edgeBool_true_of_mem turns relation membership into a true runtime-style edge.

theorem edgeBool_true_of_mem
    {relation : Relation α}
    {source target : α}
    (hEdge : (source, target) ∈ relation.edges) :
    edgeBool relation source target = true :=
  (edgeBool_true_iff relation source target).2 hEdge

Path.of_edgeBool_true turns a true runtime-style edge into relation reachability.

theorem Path.of_edgeBool_true
    {relation : Relation α}
    {source target : α}
    (hEdge : edgeBool relation source target = true) :
    Path relation source target :=
  Path.direct ((edgeBool_true_iff relation source target).1 hEdge)

edgeBool_source_mem keeps runtime-style edge sources inside endpoint-closed relations.

theorem edgeBool_source_mem
    {relation : Relation α}
    (hEndpoints : EdgeEndpointsInVertices relation)
    {source target : α}
    (hEdge : edgeBool relation source target = true) :
    source ∈ relation.vertices := byα:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticessource:αtarget:αhEdge:relation.edgeBool source target = true⊢ source ∈ relation.vertices
  have hMember : (source, target) ∈ relation.edges :=
    (edgeBool_true_iff relation source target).1 hEdgeα:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticessource:αtarget:αhEdge:relation.edgeBool source target = truehMember:(source, target) ∈ relation.edges⊢ source ∈ relation.vertices
  exact (hEndpoints _ hMember).1All goals completed! 🐙

edgeBool_target_mem keeps runtime-style edge targets inside endpoint-closed relations.

theorem edgeBool_target_mem
    {relation : Relation α}
    (hEndpoints : EdgeEndpointsInVertices relation)
    {source target : α}
    (hEdge : edgeBool relation source target = true) :
    target ∈ relation.vertices := byα:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticessource:αtarget:αhEdge:relation.edgeBool source target = true⊢ target ∈ relation.vertices
  have hMember : (source, target) ∈ relation.edges :=
    (edgeBool_true_iff relation source target).1 hEdgeα:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticessource:αtarget:αhEdge:relation.edgeBool source target = truehMember:(source, target) ∈ relation.edges⊢ target ∈ relation.vertices
  exact (hEndpoints _ hMember).2All goals completed! 🐙

end RuntimeEdgePredicate

Endpoint Closure

empty_edgeEndpointsInVertices says the empty relation is endpoint-closed.

theorem empty_edgeEndpointsInVertices :
    EdgeEndpointsInVertices (empty : Relation α) := byα:Type⊢ empty.EdgeEndpointsInVertices
  intro edge hEdgeα:Typeedge:α × αhEdge:edge ∈ empty.edges⊢ edge.1 ∈ empty.vertices ∧ edge.2 ∈ empty.vertices
  simp [empty] at hEdgeAll goals completed! 🐙

vertex_edgeEndpointsInVertices says a singleton vertex relation is endpoint-closed.

theorem vertex_edgeEndpointsInVertices (vertexValue : α) :
    EdgeEndpointsInVertices (vertex vertexValue) := byα:TypevertexValue:α⊢ (vertex vertexValue).EdgeEndpointsInVertices
  intro edge hEdgeα:TypevertexValue:αedge:α × αhEdge:edge ∈ (vertex vertexValue).edges⊢ edge.1 ∈ (vertex vertexValue).vertices ∧ edge.2 ∈ (vertex vertexValue).vertices
  simp [vertex] at hEdgeAll goals completed! 🐙

section EndpointConstructorsvariable [DecidableEq α]

overlay_edgeEndpointsInVertices preserves endpoint closure under overlay.

theorem overlay_edgeEndpointsInVertices
    {left right : Relation α}
    (hLeft : EdgeEndpointsInVertices left)
    (hRight : EdgeEndpointsInVertices right) :
    EdgeEndpointsInVertices (overlay left right) := byα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVertices⊢ (left.overlay right).EdgeEndpointsInVertices
  intro edge hEdgeα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.overlay right).edges⊢ edge.1 ∈ (left.overlay right).vertices ∧ edge.2 ∈ (left.overlay right).vertices
  have hCases : edge ∈ left.edges ∨ edge ∈ right.edges := byα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVertices⊢ (left.overlay right).EdgeEndpointsInVertices
    simpa [overlay] using hEdgeAll goals completed! 🐙
  rcases hCases with hLeftEdge | hRightEdgeinlα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.overlay right).edgeshLeftEdge:edge ∈ left.edges⊢ edge.1 ∈ (left.overlay right).vertices ∧ edge.2 ∈ (left.overlay right).verticesinrα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.overlay right).edgeshRightEdge:edge ∈ right.edges⊢ edge.1 ∈ (left.overlay right).vertices ∧ edge.2 ∈ (left.overlay right).vertices
  ·inlα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.overlay right).edgeshLeftEdge:edge ∈ left.edges⊢ edge.1 ∈ (left.overlay right).vertices ∧ edge.2 ∈ (left.overlay right).vertices rcases hLeft edge hLeftEdge with ⟨hSource, hTarget⟩inlα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.overlay right).edgeshLeftEdge:edge ∈ left.edgeshSource:edge.1 ∈ left.verticeshTarget:edge.2 ∈ left.vertices⊢ edge.1 ∈ (left.overlay right).vertices ∧ edge.2 ∈ (left.overlay right).vertices
    exact
      ⟨ Finset.mem_union_left right.vertices hSource
      , Finset.mem_union_left right.vertices hTarget
      ⟩All goals completed! 🐙
  ·inrα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.overlay right).edgeshRightEdge:edge ∈ right.edges⊢ edge.1 ∈ (left.overlay right).vertices ∧ edge.2 ∈ (left.overlay right).vertices rcases hRight edge hRightEdge with ⟨hSource, hTarget⟩inrα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.overlay right).edgeshRightEdge:edge ∈ right.edgeshSource:edge.1 ∈ right.verticeshTarget:edge.2 ∈ right.vertices⊢ edge.1 ∈ (left.overlay right).vertices ∧ edge.2 ∈ (left.overlay right).vertices
    exact
      ⟨ Finset.mem_union_right left.vertices hSource
      , Finset.mem_union_right left.vertices hTarget
      ⟩All goals completed! 🐙

connect_edgeEndpointsInVertices preserves endpoint closure under connect.

theorem connect_edgeEndpointsInVertices
    {left right : Relation α}
    (hLeft : EdgeEndpointsInVertices left)
    (hRight : EdgeEndpointsInVertices right) :
    EdgeEndpointsInVertices (connect left right) := byα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVertices⊢ (left.connect right).EdgeEndpointsInVertices
  intro edge hEdgeα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.connect right).edges⊢ edge.1 ∈ (left.connect right).vertices ∧ edge.2 ∈ (left.connect right).vertices
  have hCases :
      edge ∈ left.edges ∨
        edge ∈ right.edges ∨
          edge.1 ∈ left.vertices ∧ edge.2 ∈ right.vertices := byα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVertices⊢ (left.connect right).EdgeEndpointsInVertices
    simpa [connect, cross, Finset.mem_product, or_assoc] using hEdgeAll goals completed! 🐙
  rcases hCases with hLeftEdge | hRestinlα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.connect right).edgeshLeftEdge:edge ∈ left.edges⊢ edge.1 ∈ (left.connect right).vertices ∧ edge.2 ∈ (left.connect right).verticesinrα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.connect right).edgeshRest:edge ∈ right.edges ∨ edge.1 ∈ left.vertices ∧ edge.2 ∈ right.vertices⊢ edge.1 ∈ (left.connect right).vertices ∧ edge.2 ∈ (left.connect right).vertices
  ·inlα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.connect right).edgeshLeftEdge:edge ∈ left.edges⊢ edge.1 ∈ (left.connect right).vertices ∧ edge.2 ∈ (left.connect right).vertices rcases hLeft edge hLeftEdge with ⟨hSource, hTarget⟩inlα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.connect right).edgeshLeftEdge:edge ∈ left.edgeshSource:edge.1 ∈ left.verticeshTarget:edge.2 ∈ left.vertices⊢ edge.1 ∈ (left.connect right).vertices ∧ edge.2 ∈ (left.connect right).vertices
    exact
      ⟨ Finset.mem_union_left right.vertices hSource
      , Finset.mem_union_left right.vertices hTarget
      ⟩All goals completed! 🐙
  ·inrα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.connect right).edgeshRest:edge ∈ right.edges ∨ edge.1 ∈ left.vertices ∧ edge.2 ∈ right.vertices⊢ edge.1 ∈ (left.connect right).vertices ∧ edge.2 ∈ (left.connect right).vertices rcases hRest with hRightEdge | hCrossinr.inlα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.connect right).edgeshRightEdge:edge ∈ right.edges⊢ edge.1 ∈ (left.connect right).vertices ∧ edge.2 ∈ (left.connect right).verticesinr.inrα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.connect right).edgeshCross:edge.1 ∈ left.vertices ∧ edge.2 ∈ right.vertices⊢ edge.1 ∈ (left.connect right).vertices ∧ edge.2 ∈ (left.connect right).vertices
    ·inr.inlα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.connect right).edgeshRightEdge:edge ∈ right.edges⊢ edge.1 ∈ (left.connect right).vertices ∧ edge.2 ∈ (left.connect right).vertices rcases hRight edge hRightEdge with ⟨hSource, hTarget⟩inr.inlα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.connect right).edgeshRightEdge:edge ∈ right.edgeshSource:edge.1 ∈ right.verticeshTarget:edge.2 ∈ right.vertices⊢ edge.1 ∈ (left.connect right).vertices ∧ edge.2 ∈ (left.connect right).vertices
      exact
        ⟨ Finset.mem_union_right left.vertices hSource
        , Finset.mem_union_right left.vertices hTarget
        ⟩All goals completed! 🐙
    ·inr.inrα:Typeinst✝:DecidableEq αleft:Relation αright:Relation αhLeft:left.EdgeEndpointsInVerticeshRight:right.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ (left.connect right).edgeshCross:edge.1 ∈ left.vertices ∧ edge.2 ∈ right.vertices⊢ edge.1 ∈ (left.connect right).vertices ∧ edge.2 ∈ (left.connect right).vertices exact
        ⟨ Finset.mem_union_left right.vertices hCross.1
        , Finset.mem_union_right left.vertices hCross.2
        ⟩All goals completed! 🐙

end EndpointConstructors

acyclic_of_eq transports relation acyclicity across relation equality.

theorem acyclic_of_eq
    {left right : Relation α}
    (hEq : left = right)
    (hAcyclic : Acyclic left) :
    Acyclic right := byα:Typeleft:Relation αright:Relation αhEq:left = righthAcyclic:left.Acyclic⊢ right.Acyclic
  cases hEqreflα:Typeleft:Relation αhAcyclic:left.Acyclic⊢ left.Acyclic
  exact hAcyclicAll goals completed! 🐙

acyclic_iff_of_eq states relation acyclicity is invariant under equality.

theorem acyclic_iff_of_eq
    {left right : Relation α}
    (hEq : left = right) :
    Acyclic left ↔ Acyclic right :=
  ⟨acyclic_of_eq hEq, acyclic_of_eq hEq.symm⟩

end Relation

Graph Expression Safety

variable {α : Type} [DecidableEq α]

denote_edgeEndpointsInVertices says every denoted graph relation is endpoint-closed.

theorem denote_edgeEndpointsInVertices (graph : Graph α) :
    Relation.EdgeEndpointsInVertices (denote graph) := byα:Typeinst✝:DecidableEq αgraph:Graph α⊢ (denote graph).EdgeEndpointsInVertices
  induction graph with
  | empty =>emptyα:Typeinst✝:DecidableEq α⊢ (denote Graph.empty).EdgeEndpointsInVertices
      exact Relation.empty_edgeEndpointsInVerticesAll goals completed! 🐙
  | vertex vertexValue =>vertexα:Typeinst✝:DecidableEq αvertexValue:α⊢ (denote (Graph.vertex vertexValue)).EdgeEndpointsInVertices
      exact Relation.vertex_edgeEndpointsInVertices vertexValueAll goals completed! 🐙
  | overlay left right leftIH rightIH =>overlayα:Typeinst✝:DecidableEq αleft:Graph αright:Graph αleftIH:(denote left).EdgeEndpointsInVerticesrightIH:(denote right).EdgeEndpointsInVertices⊢ (denote (left.overlay right)).EdgeEndpointsInVertices
      exact Relation.overlay_edgeEndpointsInVertices leftIH rightIHAll goals completed! 🐙
  | connect left right leftIH rightIH =>connectα:Typeinst✝:DecidableEq αleft:Graph αright:Graph αleftIH:(denote left).EdgeEndpointsInVerticesrightIH:(denote right).EdgeEndpointsInVertices⊢ (denote (left.connect right)).EdgeEndpointsInVertices
      exact Relation.connect_edgeEndpointsInVertices leftIH rightIHAll goals completed! 🐙

GraphPath graph source target is reachability through the graph denotation.

def GraphPath (graph : Graph α) (source target : α) : Prop :=
  Relation.Path (denote graph) source target

GraphAcyclic graph rules out non-empty denotational cycles.

def GraphAcyclic (graph : Graph α) : Prop :=
  Relation.Acyclic (denote graph)

graphAcyclic_iff_no_graphPath unfolds graph acyclicity through graph paths.

theorem graphAcyclic_iff_no_graphPath (graph : Graph α) :
    GraphAcyclic graph ↔ ∀ node : α, ¬ GraphPath graph node node :=
  Iff.rfl

graphAcyclic_no_self rules out self-reachability in an acyclic graph.

theorem graphAcyclic_no_self
    {graph : Graph α}
    (hAcyclic : GraphAcyclic graph)
    (node : α) :
    ¬ GraphPath graph node node :=
  hAcyclic node

graphAcyclic_false_of_path eliminates a cyclic path witness.

theorem graphAcyclic_false_of_path
    {graph : Graph α}
    {node : α}
    (hAcyclic : GraphAcyclic graph)
    (hPath : GraphPath graph node node) :
    False :=
  hAcyclic node hPath

graphPath_source_mem keeps graph-path sources inside the denoted vertex set.

theorem graphPath_source_mem
    {graph : Graph α}
    {source target : α}
    (hPath : GraphPath graph source target) :
    source ∈ (denote graph).vertices :=
  Relation.Path.source_mem (denote_edgeEndpointsInVertices graph) hPath

graphPath_target_mem keeps graph-path targets inside the denoted vertex set.

theorem graphPath_target_mem
    {graph : Graph α}
    {source target : α}
    (hPath : GraphPath graph source target) :
    target ∈ (denote graph).vertices :=
  Relation.Path.target_mem (denote_edgeEndpointsInVertices graph) hPath

namespace GraphEq

GraphEq.acyclic transports graph acyclicity across denotational graph equality.

theorem acyclic
    {left right : Graph α}
    (hEq : GraphEq left right)
    (hAcyclic : GraphAcyclic left) :
    GraphAcyclic right :=
  Relation.acyclic_of_eq hEq hAcyclic

GraphEq.acyclic_iff says graph acyclicity is invariant under GraphEq.

theorem acyclic_iff
    {left right : Graph α}
    (hEq : GraphEq left right) :
    GraphAcyclic left ↔ GraphAcyclic right :=
  ⟨acyclic hEq, acyclic hEq.symm⟩

end GraphEq

Quotient Safety

namespace AlgGraph

AlgGraph.Path graph source target is reachability through a quotient graph denotation.

def Path (graph : AlgGraph α) (source target : α) : Prop :=
  Relation.Path (denote graph) source target

AlgGraph.Acyclic graph is acyclicity of a quotient graph's relation denotation.

def Acyclic (graph : AlgGraph α) : Prop :=
  Relation.Acyclic (denote graph)

path_ofGraph identifies quotient reachability with raw graph reachability.

theorem path_ofGraph
    (graph : Graph α)
    (source target : α) :
    Path (ofGraph graph) source target ↔ GraphPath graph source target :=
  Iff.rfl

acyclic_ofGraph identifies quotient acyclicity with raw graph acyclicity.

theorem acyclic_ofGraph (graph : Graph α) :
    Acyclic (ofGraph graph) ↔ GraphAcyclic graph :=
  Iff.rfl

denote_edgeEndpointsInVertices says quotient graph denotations are endpoint-closed.

theorem denote_edgeEndpointsInVertices (graph : AlgGraph α) :
    Relation.EdgeEndpointsInVertices (denote graph) := byα:Typeinst✝:DecidableEq αgraph:AlgGraph α⊢ graph.denote.EdgeEndpointsInVertices
  refine Quotient.inductionOn graph ?_α:Typeinst✝:DecidableEq αgraph:AlgGraph α⊢ ∀ (a : Graph α), (denote ⟦a⟧).EdgeEndpointsInVertices
  intro rawGraphα:Typeinst✝:DecidableEq αgraph:AlgGraph αrawGraph:Graph α⊢ (denote ⟦rawGraph⟧).EdgeEndpointsInVertices
  exact Cortex.Graph.denote_edgeEndpointsInVertices rawGraphAll goals completed! 🐙

path_source_mem keeps quotient-path sources inside the quotient denotation.

theorem path_source_mem
    {graph : AlgGraph α}
    {source target : α}
    (hPath : Path graph source target) :
    source ∈ (denote graph).vertices :=
  Relation.Path.source_mem (denote_edgeEndpointsInVertices graph) hPath

path_target_mem keeps quotient-path targets inside the quotient denotation.

theorem path_target_mem
    {graph : AlgGraph α}
    {source target : α}
    (hPath : Path graph source target) :
    target ∈ (denote graph).vertices :=
  Relation.Path.target_mem (denote_edgeEndpointsInVertices graph) hPath

acyclic_congr transports quotient acyclicity across raw GraphEq representatives.

theorem acyclic_congr
    {left right : Graph α}
    (hEq : GraphEq left right) :
    Acyclic (ofGraph left) ↔ Acyclic (ofGraph right) := byα:Typeinst✝:DecidableEq αleft:Graph αright:Graph αhEq:GraphEq left right⊢ (ofGraph left).Acyclic ↔ (ofGraph right).Acyclic
  rw [acyclic_ofGraph left, acyclic_ofGraph right]α:Typeinst✝:DecidableEq αleft:Graph αright:Graph αhEq:GraphEq left right⊢ GraphAcyclic left ↔ GraphAcyclic right
  exact GraphEq.acyclic_iff hEqAll goals completed! 🐙

end AlgGraphend Cortex.Graph

Proof State Hover a tactic

Hover or focus a tactic to inspect its goals.

← PreviousCortex.Graph.Relation Next →Cortex.Pulse.Classify