GraphTheoryStarter

Simple graph proofs through the public subject import

Open in Workbench View on GitHub

1-- Simple graph proofs through the public subject import.2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module GraphTheoryStarter7import Grace.Cumulus.GraphTheory89theorem neighbors_are_mutual (V E x y : Set)10  requires graph : SimpleGraph(V, E)11  requires hx : x ∈ V12  requires neighbor : y ∈ neighbors(V, E, x)13  shows x ∈ neighbors(V, E, y)14proof15  exact neighbors.symmetric with graph, hx, neighbor1617theorem induced_graph_is_subgraph (V E W : Set)18  requires graph : SimpleGraph(V, E)19  requires vertices : W ⊆ V20  shows Subgraph(V, E, W, inducedEdges(E, W))21proof22  exact inducedEdges.subgraph with graph, vertices2324theorem triangle_has_three_distinct_vertices (V E x y z : Set)25  requires graph : SimpleGraph(V, E)26  requires triangle : Triangle(E, x, y, z)27  shows x ≠ y ∧ y ≠ z ∧ z ≠ x28proof29  exact Triangle.distinct with graph, triangle3031theorem complement_twice (V E : Set)32  requires graph : SimpleGraph(V, E)33  shows complementEdges(V, complementEdges(V, E)) = E34proof35  exact complementEdges.involution with graph3637theorem vertices_cannot_enumerate_all_independent_subsets (V f : Set)38  shows ¬SurjectiveBetween(f, V, independentSets(V, empty))39proof40  exact Independent.no_surjection_from_vertices4142theorem path_certificate (V E weights source labels target cost : Set)43  requires feasible : PathPotential(V, E, weights, source, labels)44  requires targetIn : target ∈ V45  requires costNat : Nat(cost)46  requires path : HasPathCost(V, E, weights, source, target, cost)47  requires label : labels(target) = cost48  shows ShortestPathCost(V, E, weights, source, target, cost)49proof50  exact PathPotential.certifies_shortest at V, E, weights, source, labels,51    target, cost with feasible, targetIn, costNat, path, label52