Cortex.Graph.Relation

On this page
  1. Overview
  2. Context
  3. Theorem Split
  4. Relation Model
  5. Mokhov Laws in the Relation Denotation
  6. AST Denotation
  7. Relation Realization
Imports
import Cortex.Graph.Core import Mathlib.Data.Finset.Basic import Mathlib.Data.Finset.Prod

Overview

Extensional denotation for Mokhov graphs.

Context

Cortex.Graph.Core defines the free syntax tree generated by empty, vertex, overlay, and connect. The algebraic laws do not hold by definitional equality on that tree. They do hold for the standard relation denotation: a finite vertex set plus a finite edge set, with connect adding every cross edge from the left vertex set to the right vertex set.

This module is phase 1 of the quotient story. It proves the laws on the denotation. A later Cortex.Graph.Quotient module can use this as the semantic model for lifting the laws back to graph equivalence.

Theorem Split

The page first defines finite relation operations, then proves Mokhov's laws extensionally, and finally connects the AST syntax to the relation model through denote.

namespace Cortex.Graph

Relation Model

Relation α is the concrete finite graph model: vertices plus directed edges.

structure Relation (α : Type) where vertices : Finset α edges : Finset (α × α) deriving DecidableEqnamespace Relationvariable {α : Type}@[ext] theorem ext {r s : Relation α} (h_vertices : r.vertices = s.vertices) (h_edges : r.edges = s.edges) : r = s := α:Typer:Relation αs:Relation αh_vertices:r.vertices = s.verticesh_edges:r.edges = s.edges⊢ r = s cases r with α:Types:Relation αrVertices:Finset αrEdges:Finset (α × α)h_vertices:{ vertices := rVertices, edges := rEdges }.vertices = s.verticesh_edges:{ vertices := rVertices, edges := rEdges }.edges = s.edges⊢ { vertices := rVertices, edges := rEdges } = s cases s with α:TyperVertices:Finset αrEdges:Finset (α × α)sVertices:Finset αsEdges:Finset (α × α)h_vertices:{ vertices := rVertices, edges := rEdges }.vertices = { vertices := sVertices, edges := sEdges }.verticesh_edges:{ vertices := rVertices, edges := rEdges }.edges = { vertices := sVertices, edges := sEdges }.edges⊢ { vertices := rVertices, edges := rEdges } = { vertices := sVertices, edges := sEdges } α:TyperVertices:Finset αrEdges:Finset (α × α)sEdges:Finset (α × α)h_edges:{ vertices := rVertices, edges := rEdges }.edges = { vertices := rVertices, edges := sEdges }.edges⊢ { vertices := rVertices, edges := rEdges } = { vertices := rVertices, edges := sEdges } α:TyperVertices:Finset αrEdges:Finset (α × α)⊢ { vertices := rVertices, edges := rEdges } = { vertices := rVertices, edges := rEdges } All goals completed! 🐙variable [DecidableEq α]

empty is the relation with no vertices and no edges.

def empty : Relation α := { vertices := ∅, edges := ∅ }

vertex v is the relation with one vertex and no edges.

def vertex (v : α) : Relation α := { vertices := {v}, edges := ∅ }

overlay r s unions the vertex sets and edge sets.

def overlay (r s : Relation α) : Relation α := { vertices := r.vertices ∪ s.vertices , edges := r.edges ∪ s.edges }

cross left right is every directed edge from a left vertex to a right vertex.

def cross (left right : Finset α) : Finset (α × α) := left ×ˢ right

connect r s overlays two relations and adds every cross edge from r to s.

def connect (r s : Relation α) : Relation α := { vertices := r.vertices ∪ s.vertices , edges := r.edges ∪ s.edges ∪ cross r.vertices s.vertices }

Mokhov Laws in the Relation Denotation

@[simp] theorem overlay_empty_left (r : Relation α) : overlay empty r = r := α:Typeinst✝:DecidableEq αr:Relation α⊢ empty.overlay r = r α:Typeinst✝:DecidableEq αr:Relation αx:α⊢ x ∈ (empty.overlay r).vertices ↔ x ∈ r.verticesα:Typeinst✝:DecidableEq αr:Relation αx:α × α⊢ x ∈ (empty.overlay r).edges ↔ x ∈ r.edges α:Typeinst✝:DecidableEq αr:Relation αx:α⊢ x ∈ (empty.overlay r).vertices ↔ x ∈ r.verticesα:Typeinst✝:DecidableEq αr:Relation αx:α × α⊢ x ∈ (empty.overlay r).edges ↔ x ∈ r.edges All goals completed! 🐙@[simp] theorem overlay_empty_right (r : Relation α) : overlay r empty = r := α:Typeinst✝:DecidableEq αr:Relation α⊢ r.overlay empty = r α:Typeinst✝:DecidableEq αr:Relation αx:α⊢ x ∈ (r.overlay empty).vertices ↔ x ∈ r.verticesα:Typeinst✝:DecidableEq αr:Relation αx:α × α⊢ x ∈ (r.overlay empty).edges ↔ x ∈ r.edges α:Typeinst✝:DecidableEq αr:Relation αx:α⊢ x ∈ (r.overlay empty).vertices ↔ x ∈ r.verticesα:Typeinst✝:DecidableEq αr:Relation αx:α × α⊢ x ∈ (r.overlay empty).edges ↔ x ∈ r.edges All goals completed! 🐙theorem overlay_comm (r s : Relation α) : overlay r s = overlay s r := α:Typeinst✝:DecidableEq αr:Relation αs:Relation α⊢ r.overlay s = s.overlay r α:Typeinst✝:DecidableEq αr:Relation αs:Relation αx:α⊢ x ∈ (r.overlay s).vertices ↔ x ∈ (s.overlay r).verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αx:α × α⊢ x ∈ (r.overlay s).edges ↔ x ∈ (s.overlay r).edges α:Typeinst✝:DecidableEq αr:Relation αs:Relation αx:α⊢ x ∈ (r.overlay s).vertices ↔ x ∈ (s.overlay r).verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αx:α × α⊢ x ∈ (r.overlay s).edges ↔ x ∈ (s.overlay r).edges All goals completed! 🐙theorem overlay_assoc (r s t : Relation α) : overlay (overlay r s) t = overlay r (overlay s t) := α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation α⊢ (r.overlay s).overlay t = r.overlay (s.overlay t) α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α⊢ x ∈ ((r.overlay s).overlay t).vertices ↔ x ∈ (r.overlay (s.overlay t)).verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ ((r.overlay s).overlay t).edges ↔ x ∈ (r.overlay (s.overlay t)).edges α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α⊢ x ∈ ((r.overlay s).overlay t).vertices ↔ x ∈ (r.overlay (s.overlay t)).verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ ((r.overlay s).overlay t).edges ↔ x ∈ (r.overlay (s.overlay t)).edges All goals completed! 🐙@[simp] theorem connect_empty_left (r : Relation α) : connect empty r = r := α:Typeinst✝:DecidableEq αr:Relation α⊢ empty.connect r = r α:Typeinst✝:DecidableEq αr:Relation αx:α⊢ x ∈ (empty.connect r).vertices ↔ x ∈ r.verticesα:Typeinst✝:DecidableEq αr:Relation αx:α × α⊢ x ∈ (empty.connect r).edges ↔ x ∈ r.edges α:Typeinst✝:DecidableEq αr:Relation αx:α⊢ x ∈ (empty.connect r).vertices ↔ x ∈ r.verticesα:Typeinst✝:DecidableEq αr:Relation αx:α × α⊢ x ∈ (empty.connect r).edges ↔ x ∈ r.edges All goals completed! 🐙@[simp] theorem connect_empty_right (r : Relation α) : connect r empty = r := α:Typeinst✝:DecidableEq αr:Relation α⊢ r.connect empty = r α:Typeinst✝:DecidableEq αr:Relation αx:α⊢ x ∈ (r.connect empty).vertices ↔ x ∈ r.verticesα:Typeinst✝:DecidableEq αr:Relation αx:α × α⊢ x ∈ (r.connect empty).edges ↔ x ∈ r.edges α:Typeinst✝:DecidableEq αr:Relation αx:α⊢ x ∈ (r.connect empty).vertices ↔ x ∈ r.verticesα:Typeinst✝:DecidableEq αr:Relation αx:α × α⊢ x ∈ (r.connect empty).edges ↔ x ∈ r.edges All goals completed! 🐙theorem connect_assoc (r s t : Relation α) : connect (connect r s) t = connect r (connect s t) := α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation α⊢ (r.connect s).connect t = r.connect (s.connect t) α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α⊢ x ∈ ((r.connect s).connect t).vertices ↔ x ∈ (r.connect (s.connect t)).verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ ((r.connect s).connect t).edges ↔ x ∈ (r.connect (s.connect t)).edges α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α⊢ x ∈ ((r.connect s).connect t).vertices ↔ x ∈ (r.connect (s.connect t)).vertices All goals completed! 🐙 α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ ((r.connect s).connect t).edges ↔ x ∈ (r.connect (s.connect t)).edges α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ r.edges ∨ x ∈ s.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ s.vertices ∨ x ∈ t.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices ∨ x.1 ∈ s.vertices ∧ x.2 ∈ t.vertices ↔ x ∈ r.edges ∨ x ∈ s.edges ∨ x ∈ t.edges ∨ x.1 ∈ s.vertices ∧ x.2 ∈ t.vertices ∨ x.1 ∈ r.vertices ∧ x.2 ∈ s.vertices ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices All goals completed! 🐙theorem connect_distrib_overlay_left (r s t : Relation α) : connect r (overlay s t) = overlay (connect r s) (connect r t) := α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation α⊢ r.connect (s.overlay t) = (r.connect s).overlay (r.connect t) α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α⊢ x ∈ (r.connect (s.overlay t)).vertices ↔ x ∈ ((r.connect s).overlay (r.connect t)).verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ (r.connect (s.overlay t)).edges ↔ x ∈ ((r.connect s).overlay (r.connect t)).edges α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α⊢ x ∈ (r.connect (s.overlay t)).vertices ↔ x ∈ ((r.connect s).overlay (r.connect t)).verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ (r.connect (s.overlay t)).edges ↔ x ∈ ((r.connect s).overlay (r.connect t)).edges α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ r.edges ∨ x ∈ s.edges ∨ x ∈ t.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ s.vertices ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices ↔ x ∈ r.edges ∨ x ∈ s.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ s.vertices ∨ x ∈ r.edges ∨ x ∈ t.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α⊢ x ∈ r.vertices ∨ x ∈ s.vertices ∨ x ∈ t.vertices ↔ x ∈ r.vertices ∨ x ∈ s.vertices ∨ x ∈ r.vertices ∨ x ∈ t.verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ r.edges ∨ x ∈ s.edges ∨ x ∈ t.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ s.vertices ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices ↔ x ∈ r.edges ∨ x ∈ s.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ s.vertices ∨ x ∈ r.edges ∨ x ∈ t.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices All goals completed! 🐙theorem connect_distrib_overlay_right (r s t : Relation α) : connect (overlay r s) t = overlay (connect r t) (connect s t) := α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation α⊢ (r.overlay s).connect t = (r.connect t).overlay (s.connect t) α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α⊢ x ∈ ((r.overlay s).connect t).vertices ↔ x ∈ ((r.connect t).overlay (s.connect t)).verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ ((r.overlay s).connect t).edges ↔ x ∈ ((r.connect t).overlay (s.connect t)).edges α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α⊢ x ∈ ((r.overlay s).connect t).vertices ↔ x ∈ ((r.connect t).overlay (s.connect t)).verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ ((r.overlay s).connect t).edges ↔ x ∈ ((r.connect t).overlay (s.connect t)).edges α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ r.edges ∨ x ∈ s.edges ∨ x ∈ t.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices ∨ x.1 ∈ s.vertices ∧ x.2 ∈ t.vertices ↔ x ∈ r.edges ∨ x ∈ t.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices ∨ x ∈ s.edges ∨ x ∈ t.edges ∨ x.1 ∈ s.vertices ∧ x.2 ∈ t.vertices α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α⊢ x ∈ r.vertices ∨ x ∈ s.vertices ∨ x ∈ t.vertices ↔ x ∈ r.vertices ∨ x ∈ t.vertices ∨ x ∈ s.vertices ∨ x ∈ t.verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ r.edges ∨ x ∈ s.edges ∨ x ∈ t.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices ∨ x.1 ∈ s.vertices ∧ x.2 ∈ t.vertices ↔ x ∈ r.edges ∨ x ∈ t.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices ∨ x ∈ s.edges ∨ x ∈ t.edges ∨ x.1 ∈ s.vertices ∧ x.2 ∈ t.vertices All goals completed! 🐙

connect_decomposition proves Mokhov's decomposition law in the relation denotation.

theorem connect_decomposition (r s t : Relation α) : connect (connect r s) t = overlay (overlay (connect r s) (connect r t)) (connect s t) := α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation α⊢ (r.connect s).connect t = ((r.connect s).overlay (r.connect t)).overlay (s.connect t) α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α⊢ x ∈ ((r.connect s).connect t).vertices ↔ x ∈ (((r.connect s).overlay (r.connect t)).overlay (s.connect t)).verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ ((r.connect s).connect t).edges ↔ x ∈ (((r.connect s).overlay (r.connect t)).overlay (s.connect t)).edges α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α⊢ x ∈ ((r.connect s).connect t).vertices ↔ x ∈ (((r.connect s).overlay (r.connect t)).overlay (s.connect t)).verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ ((r.connect s).connect t).edges ↔ x ∈ (((r.connect s).overlay (r.connect t)).overlay (s.connect t)).edges α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ r.edges ∨ x ∈ s.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ s.vertices ∨ x ∈ t.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices ∨ x.1 ∈ s.vertices ∧ x.2 ∈ t.vertices ↔ x ∈ r.edges ∨ x ∈ s.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ s.vertices ∨ x ∈ r.edges ∨ x ∈ t.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices ∨ x ∈ s.edges ∨ x ∈ t.edges ∨ x.1 ∈ s.vertices ∧ x.2 ∈ t.vertices α:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α⊢ x ∈ r.vertices ∨ x ∈ s.vertices ∨ x ∈ t.vertices ↔ x ∈ r.vertices ∨ x ∈ s.vertices ∨ x ∈ r.vertices ∨ x ∈ t.vertices ∨ x ∈ s.vertices ∨ x ∈ t.verticesα:Typeinst✝:DecidableEq αr:Relation αs:Relation αt:Relation αx:α × α⊢ x ∈ r.edges ∨ x ∈ s.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ s.vertices ∨ x ∈ t.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices ∨ x.1 ∈ s.vertices ∧ x.2 ∈ t.vertices ↔ x ∈ r.edges ∨ x ∈ s.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ s.vertices ∨ x ∈ r.edges ∨ x ∈ t.edges ∨ x.1 ∈ r.vertices ∧ x.2 ∈ t.vertices ∨ x ∈ s.edges ∨ x ∈ t.edges ∨ x.1 ∈ s.vertices ∧ x.2 ∈ t.vertices All goals completed! 🐙end Relation

AST Denotation

variable {α : Type} [DecidableEq α]

denote g interprets a Mokhov graph expression as a finite relation.

def denote : Graph α → Relation α | Graph.empty => Relation.empty | Graph.vertex v => Relation.vertex v | Graph.overlay g h => Relation.overlay (denote g) (denote h) | Graph.connect g h => Relation.connect (denote g) (denote h)@[simp] theorem denote_empty : denote (α := α) Graph.empty = Relation.empty := rfl@[simp] theorem denote_vertex (v : α) : denote (Graph.vertex v) = Relation.vertex v := rfl@[simp] theorem denote_overlay (g h : Graph α) : denote (Graph.overlay g h) = Relation.overlay (denote g) (denote h) := rfl@[simp] theorem denote_connect (g h : Graph α) : denote (Graph.connect g h) = Relation.connect (denote g) (denote h) := rfltheorem denote_overlay_comm (g h : Graph α) : denote (Graph.overlay g h) = denote (Graph.overlay h g) := Relation.overlay_comm (denote g) (denote h)theorem denote_connect_decomposition (g h k : Graph α) : denote (Graph.connect (Graph.connect g h) k) = denote (Graph.overlay (Graph.overlay (Graph.connect g h) (Graph.connect g k)) (Graph.connect h k)) := Relation.connect_decomposition (denote g) (denote h) (denote k)

Relation Realization

Relation.EdgeEndpointsInVertices r says each edge endpoint appears in the vertex set.

def Relation.EdgeEndpointsInVertices (relation : Relation α) : Prop := ∀ edge, edge ∈ relation.edges → edge.1 ∈ relation.vertices ∧ edge.2 ∈ relation.vertices

graphOfVertices vertices is the edge-free graph containing the listed vertices.

def graphOfVertices : List α → Graph α | [] => Graph.empty | vertex :: rest => Graph.overlay (Graph.vertex vertex) (graphOfVertices rest)

graphOfEdges edges is the overlay of singleton-edge graphs for the listed edges.

def graphOfEdges : List (α × α) → Graph α | [] => Graph.empty | edge :: rest => Graph.overlay (Graph.edge edge.1 edge.2) (graphOfEdges rest)

graphOfRelation relation chooses a non-extractable graph representative for a relation.

noncomputable def graphOfRelation (relation : Relation α) : Graph α := Graph.overlay (graphOfVertices relation.vertices.toList) (graphOfEdges relation.edges.toList)

Denotation of graphOfVertices is exactly the listed vertices and no edges.

theorem denote_graphOfVertices (vertices : List α) : denote (graphOfVertices vertices) = { vertices := vertices.toFinset, edges := ∅ } := α:Typeinst✝:DecidableEq αvertices:List α⊢ denote (graphOfVertices vertices) = { vertices := vertices.toFinset, edges := ∅ } induction vertices with α:Typeinst✝:DecidableEq α⊢ denote (graphOfVertices []) = { vertices := [].toFinset, edges := ∅ } α:Typeinst✝:DecidableEq αx:α⊢ x ∈ (denote (graphOfVertices [])).vertices ↔ x ∈ { vertices := [].toFinset, edges := ∅ }.verticesα:Typeinst✝:DecidableEq αx:α × α⊢ x ∈ (denote (graphOfVertices [])).edges ↔ x ∈ { vertices := [].toFinset, edges := ∅ }.edges α:Typeinst✝:DecidableEq αx:α⊢ x ∈ (denote (graphOfVertices [])).vertices ↔ x ∈ { vertices := [].toFinset, edges := ∅ }.verticesα:Typeinst✝:DecidableEq αx:α × α⊢ x ∈ (denote (graphOfVertices [])).edges ↔ x ∈ { vertices := [].toFinset, edges := ∅ }.edges All goals completed! 🐙 α:Typeinst✝:DecidableEq αvertex:αrest:List αih:denote (graphOfVertices rest) = { vertices := rest.toFinset, edges := ∅ }⊢ denote (graphOfVertices (vertex :: rest)) = { vertices := (vertex :: rest).toFinset, edges := ∅ } α:Typeinst✝:DecidableEq αvertex:αrest:List αih:denote (graphOfVertices rest) = { vertices := rest.toFinset, edges := ∅ }⊢ (denote (Graph.vertex vertex)).overlay { vertices := rest.toFinset, edges := ∅ } = { vertices := (vertex :: rest).toFinset, edges := ∅ } α:Typeinst✝:DecidableEq αvertex:αrest:List αih:denote (graphOfVertices rest) = { vertices := rest.toFinset, edges := ∅ }x:α⊢ x ∈ ((denote (Graph.vertex vertex)).overlay { vertices := rest.toFinset, edges := ∅ }).vertices ↔ x ∈ { vertices := (vertex :: rest).toFinset, edges := ∅ }.verticesα:Typeinst✝:DecidableEq αvertex:αrest:List αih:denote (graphOfVertices rest) = { vertices := rest.toFinset, edges := ∅ }x:α × α⊢ x ∈ ((denote (Graph.vertex vertex)).overlay { vertices := rest.toFinset, edges := ∅ }).edges ↔ x ∈ { vertices := (vertex :: rest).toFinset, edges := ∅ }.edges α:Typeinst✝:DecidableEq αvertex:αrest:List αih:denote (graphOfVertices rest) = { vertices := rest.toFinset, edges := ∅ }x:α⊢ x ∈ ((denote (Graph.vertex vertex)).overlay { vertices := rest.toFinset, edges := ∅ }).vertices ↔ x ∈ { vertices := (vertex :: rest).toFinset, edges := ∅ }.verticesα:Typeinst✝:DecidableEq αvertex:αrest:List αih:denote (graphOfVertices rest) = { vertices := rest.toFinset, edges := ∅ }x:α × α⊢ x ∈ ((denote (Graph.vertex vertex)).overlay { vertices := rest.toFinset, edges := ∅ }).edges ↔ x ∈ { vertices := (vertex :: rest).toFinset, edges := ∅ }.edges All goals completed! 🐙

Denotation of graphOfEdges contains each listed edge and its endpoints.

theorem denote_graphOfEdges (edges : List (α × α)) : denote (graphOfEdges edges) = { vertices := (edges.map Prod.fst).toFinset ∪ (edges.map Prod.snd).toFinset edges := edges.toFinset } := α:Typeinst✝:DecidableEq αedges:List (α × α)⊢ denote (graphOfEdges edges) = { vertices := (List.map Prod.fst edges).toFinset ∪ (List.map Prod.snd edges).toFinset, edges := edges.toFinset } induction edges with α:Typeinst✝:DecidableEq α⊢ denote (graphOfEdges []) = { vertices := (List.map Prod.fst []).toFinset ∪ (List.map Prod.snd []).toFinset, edges := [].toFinset } α:Typeinst✝:DecidableEq αx:α⊢ x ∈ (denote (graphOfEdges [])).vertices ↔ x ∈ { vertices := (List.map Prod.fst []).toFinset ∪ (List.map Prod.snd []).toFinset, edges := [].toFinset }.verticesα:Typeinst✝:DecidableEq αx:α × α⊢ x ∈ (denote (graphOfEdges [])).edges ↔ x ∈ { vertices := (List.map Prod.fst []).toFinset ∪ (List.map Prod.snd []).toFinset, edges := [].toFinset }.edges α:Typeinst✝:DecidableEq αx:α⊢ x ∈ (denote (graphOfEdges [])).vertices ↔ x ∈ { vertices := (List.map Prod.fst []).toFinset ∪ (List.map Prod.snd []).toFinset, edges := [].toFinset }.verticesα:Typeinst✝:DecidableEq αx:α × α⊢ x ∈ (denote (graphOfEdges [])).edges ↔ x ∈ { vertices := (List.map Prod.fst []).toFinset ∪ (List.map Prod.snd []).toFinset, edges := [].toFinset }.edges All goals completed! 🐙 α:Typeinst✝:DecidableEq αedge:α × αrest:List (α × α)ih:denote (graphOfEdges rest) = { vertices := (List.map Prod.fst rest).toFinset ∪ (List.map Prod.snd rest).toFinset, edges := rest.toFinset }⊢ denote (graphOfEdges (edge :: rest)) = { vertices := (List.map Prod.fst (edge :: rest)).toFinset ∪ (List.map Prod.snd (edge :: rest)).toFinset, edges := (edge :: rest).toFinset } α:Typeinst✝:DecidableEq αedge:α × αrest:List (α × α)ih:denote (graphOfEdges rest) = { vertices := (List.map Prod.fst rest).toFinset ∪ (List.map Prod.snd rest).toFinset, edges := rest.toFinset }⊢ (denote (Graph.edge edge.1 edge.2)).overlay { vertices := (List.map Prod.fst rest).toFinset ∪ (List.map Prod.snd rest).toFinset, edges := rest.toFinset } = { vertices := (List.map Prod.fst (edge :: rest)).toFinset ∪ (List.map Prod.snd (edge :: rest)).toFinset, edges := (edge :: rest).toFinset } α:Typeinst✝:DecidableEq αedge:α × αrest:List (α × α)ih:denote (graphOfEdges rest) = { vertices := (List.map Prod.fst rest).toFinset ∪ (List.map Prod.snd rest).toFinset, edges := rest.toFinset }x:α⊢ x ∈ ((denote (Graph.edge edge.1 edge.2)).overlay { vertices := (List.map Prod.fst rest).toFinset ∪ (List.map Prod.snd rest).toFinset, edges := rest.toFinset }).vertices ↔ x ∈ { vertices := (List.map Prod.fst (edge :: rest)).toFinset ∪ (List.map Prod.snd (edge :: rest)).toFinset, edges := (edge :: rest).toFinset }.verticesα:Typeinst✝:DecidableEq αedge:α × αrest:List (α × α)ih:denote (graphOfEdges rest) = { vertices := (List.map Prod.fst rest).toFinset ∪ (List.map Prod.snd rest).toFinset, edges := rest.toFinset }x:α × α⊢ x ∈ ((denote (Graph.edge edge.1 edge.2)).overlay { vertices := (List.map Prod.fst rest).toFinset ∪ (List.map Prod.snd rest).toFinset, edges := rest.toFinset }).edges ↔ x ∈ { vertices := (List.map Prod.fst (edge :: rest)).toFinset ∪ (List.map Prod.snd (edge :: rest)).toFinset, edges := (edge :: rest).toFinset }.edges α:Typeinst✝:DecidableEq αedge:α × αrest:List (α × α)ih:denote (graphOfEdges rest) = { vertices := (List.map Prod.fst rest).toFinset ∪ (List.map Prod.snd rest).toFinset, edges := rest.toFinset }x:α⊢ x ∈ ((denote (Graph.edge edge.1 edge.2)).overlay { vertices := (List.map Prod.fst rest).toFinset ∪ (List.map Prod.snd rest).toFinset, edges := rest.toFinset }).vertices ↔ x ∈ { vertices := (List.map Prod.fst (edge :: rest)).toFinset ∪ (List.map Prod.snd (edge :: rest)).toFinset, edges := (edge :: rest).toFinset }.vertices All goals completed! 🐙 α:Typeinst✝:DecidableEq αedge:α × αrest:List (α × α)ih:denote (graphOfEdges rest) = { vertices := (List.map Prod.fst rest).toFinset ∪ (List.map Prod.snd rest).toFinset, edges := rest.toFinset }x:α × α⊢ x ∈ ((denote (Graph.edge edge.1 edge.2)).overlay { vertices := (List.map Prod.fst rest).toFinset ∪ (List.map Prod.snd rest).toFinset, edges := rest.toFinset }).edges ↔ x ∈ { vertices := (List.map Prod.fst (edge :: rest)).toFinset ∪ (List.map Prod.snd (edge :: rest)).toFinset, edges := (edge :: rest).toFinset }.edges All goals completed! 🐙

A relation with all edge endpoints in its vertex set has a graph representative.

theorem denote_graphOfRelation {relation : Relation α} (hEndpoints : Relation.EdgeEndpointsInVertices relation) : denote (graphOfRelation relation) = relation := α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVertices⊢ denote (graphOfRelation relation) = relation α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVertices⊢ denote ((graphOfVertices relation.vertices.toList).overlay (graphOfEdges relation.edges.toList)) = relation α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVertices⊢ { vertices := relation.vertices.toList.toFinset, edges := ∅ }.overlay { vertices := (List.map Prod.fst relation.edges.toList).toFinset ∪ (List.map Prod.snd relation.edges.toList).toFinset, edges := relation.edges.toList.toFinset } = relation α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVertices⊢ ({ vertices := relation.vertices.toList.toFinset, edges := ∅ }.overlay { vertices := (List.map Prod.fst relation.edges.toList).toFinset ∪ (List.map Prod.snd relation.edges.toList).toFinset, edges := relation.edges.toList.toFinset }).vertices = relation.verticesα:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVertices⊢ ({ vertices := relation.vertices.toList.toFinset, edges := ∅ }.overlay { vertices := (List.map Prod.fst relation.edges.toList).toFinset ∪ (List.map Prod.snd relation.edges.toList).toFinset, edges := relation.edges.toList.toFinset }).edges = relation.edges α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVertices⊢ ({ vertices := relation.vertices.toList.toFinset, edges := ∅ }.overlay { vertices := (List.map Prod.fst relation.edges.toList).toFinset ∪ (List.map Prod.snd relation.edges.toList).toFinset, edges := relation.edges.toList.toFinset }).vertices = relation.vertices α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVertices⊢ ∀ (a : α), a ∈ ({ vertices := relation.vertices.toList.toFinset, edges := ∅ }.overlay { vertices := (List.map Prod.fst relation.edges.toList).toFinset ∪ (List.map Prod.snd relation.edges.toList).toFinset, edges := relation.edges.toList.toFinset }).vertices ↔ a ∈ relation.vertices α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:α⊢ vertex ∈ ({ vertices := relation.vertices.toList.toFinset, edges := ∅ }.overlay { vertices := (List.map Prod.fst relation.edges.toList).toFinset ∪ (List.map Prod.snd relation.edges.toList).toFinset, edges := relation.edges.toList.toFinset }).vertices ↔ vertex ∈ relation.vertices α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:α⊢ (vertex ∈ relation.vertices ∨ (∃ a ∈ relation.edges, a.1 = vertex) ∨ ∃ a ∈ relation.edges, a.2 = vertex) ↔ vertex ∈ relation.vertices α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:α⊢ (vertex ∈ relation.vertices ∨ (∃ a ∈ relation.edges, a.1 = vertex) ∨ ∃ a ∈ relation.edges, a.2 = vertex) → vertex ∈ relation.verticesα:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:α⊢ vertex ∈ relation.vertices → vertex ∈ relation.vertices ∨ (∃ a ∈ relation.edges, a.1 = vertex) ∨ ∃ a ∈ relation.edges, a.2 = vertex α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:α⊢ (vertex ∈ relation.vertices ∨ (∃ a ∈ relation.edges, a.1 = vertex) ∨ ∃ a ∈ relation.edges, a.2 = vertex) → vertex ∈ relation.vertices α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:αhVertex:vertex ∈ relation.vertices ∨ (∃ a ∈ relation.edges, a.1 = vertex) ∨ ∃ a ∈ relation.edges, a.2 = vertex⊢ vertex ∈ relation.vertices α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:αhVertex:vertex ∈ relation.vertices⊢ vertex ∈ relation.verticesα:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:αhEndpoint:(∃ a ∈ relation.edges, a.1 = vertex) ∨ ∃ a ∈ relation.edges, a.2 = vertex⊢ vertex ∈ relation.vertices α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:αhVertex:vertex ∈ relation.vertices⊢ vertex ∈ relation.vertices All goals completed! 🐙 α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:αhEndpoint:(∃ a ∈ relation.edges, a.1 = vertex) ∨ ∃ a ∈ relation.edges, a.2 = vertex⊢ vertex ∈ relation.vertices α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:αhSource:∃ a ∈ relation.edges, a.1 = vertex⊢ vertex ∈ relation.verticesα:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:αhTarget:∃ a ∈ relation.edges, a.2 = vertex⊢ vertex ∈ relation.vertices α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:αhSource:∃ a ∈ relation.edges, a.1 = vertex⊢ vertex ∈ relation.vertices α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ relation.edges⊢ edge.1 ∈ relation.vertices All goals completed! 🐙 α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:αhTarget:∃ a ∈ relation.edges, a.2 = vertex⊢ vertex ∈ relation.vertices α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesedge:α × αhEdge:edge ∈ relation.edges⊢ edge.2 ∈ relation.vertices All goals completed! 🐙 α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:α⊢ vertex ∈ relation.vertices → vertex ∈ relation.vertices ∨ (∃ a ∈ relation.edges, a.1 = vertex) ∨ ∃ a ∈ relation.edges, a.2 = vertex α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesvertex:αhVertex:vertex ∈ relation.vertices⊢ vertex ∈ relation.vertices ∨ (∃ a ∈ relation.edges, a.1 = vertex) ∨ ∃ a ∈ relation.edges, a.2 = vertex All goals completed! 🐙 α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVertices⊢ ({ vertices := relation.vertices.toList.toFinset, edges := ∅ }.overlay { vertices := (List.map Prod.fst relation.edges.toList).toFinset ∪ (List.map Prod.snd relation.edges.toList).toFinset, edges := relation.edges.toList.toFinset }).edges = relation.edges α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVertices⊢ ∀ (a : α × α), a ∈ ({ vertices := relation.vertices.toList.toFinset, edges := ∅ }.overlay { vertices := (List.map Prod.fst relation.edges.toList).toFinset ∪ (List.map Prod.snd relation.edges.toList).toFinset, edges := relation.edges.toList.toFinset }).edges ↔ a ∈ relation.edges α:Typeinst✝:DecidableEq αrelation:Relation αhEndpoints:relation.EdgeEndpointsInVerticesedge:α × α⊢ edge ∈ ({ vertices := relation.vertices.toList.toFinset, edges := ∅ }.overlay { vertices := (List.map Prod.fst relation.edges.toList).toFinset ∪ (List.map Prod.snd relation.edges.toList).toFinset, edges := relation.edges.toList.toFinset }).edges ↔ edge ∈ relation.edges All goals completed! 🐙end Cortex.Graph