subgraphs

Stream: graph theory

[Jalex Stark]

After chatting a bit with @Kyle Miller , we think that a main bottleneck is in getting a good definition of subgraph. Kyle has a good understanding of how submonoids work, (after the recent refactor led by uh kevin and scott?) and we'd like to get the behavior of subgraphs to be as similar as we can.

[Jalex Stark]

@Michael Hahn has some sorrys where the right hting to do is apply subgraph induction and then do some simple manipulations with subgraphs.

[Jalex Stark]

My attempt to specify the right lemmas for the induction principle is here https://github.com/apurvnakade/mc2020-projects/blob/master/src/michael/graph_induction.lean
and the rest of michael's graphs code is in the same folder in that repo.

[Jalex Stark]

A particularly frustrating thing is this sorry,

card_edges_erase (e : G.E) : (G.erase e).card_edges + 1 = G.card_edges := sorry

which I referenced earlier as being a thing that's annoying with card_edges.