[Merged by Bors] - feat(combinatorics/simple_graph): boolean_algebra for simple_graphs.

[ericrbg]

---

There's a couple questions I left in the comments; also, am happy to do further work, just ran out of ideas (creative brain isn't on today)

[eric-wieser]

There's an easier way to build the partial order instance:

Suggested change

	instance : bounded_lattice (simple_graph V) :=
	{ le := is_subgraph,
	sup := union,
	inf := inter,
	top := complete_graph V,
	bot := empty_graph V,
	le_refl := λ _ _ _ h, h,
	le_trans := λ x y z hxy hyz _ _ h, hyz (hxy h),
	le_antisymm := λ x y hxy hyx, by { ext v w, exact ⟨λ h, hxy h, λ h, hyx h⟩ },
	le_top := λ x v w h, x.ne_of_adj h,
	bot_le := λ x v w h, h.elim,
	sup_le := λ x y z hxy hyz v w h, h.cases_on (λ h, hxy h) (λ h, hyz h),
	le_sup_left := λ x y v w h, or.inl h,
	le_sup_right := λ x y v w h, or.inr h,
	le_inf := λ x y z hxy hyz v w h, ⟨hxy h, hyz h⟩,
	inf_le_left := λ x y v w h, h.1,
	inf_le_right := λ x y v w h, h.2 }
	instance : bounded_lattice (simple_graph V) :=
	{ le := is_subgraph,
	sup := union,
	inf := inter,
	top := complete_graph V,
	bot := empty_graph V,
	le_top := λ x v w h, x.ne_of_adj h,
	bot_le := λ x v w h, h.elim,
	sup_le := λ x y z hxy hyz v w h, h.cases_on (λ h, hxy h) (λ h, hyz h),
	le_sup_left := λ x y v w h, or.inl h,
	le_sup_right := λ x y v w h, or.inr h,
	le_inf := λ x y z hxy hyz v w h, ⟨hxy h, hyz h⟩,
	inf_le_left := λ x y v w h, h.1,
	inf_le_right := λ x y v w h, h.2,
	.. partial_order.lift simple_graph.adj (λ (x y : simple_graph V) h, by { ext, rw h }) }

I think a bounded_lattice.lift might be useful here.

[eric-wieser]

Zulip

[ericrbg]

for sure, I find it very weird that with your example, removing le ruins it all, even though the bounded_lattice you create has the lt implied by partial_order.lift instead of the lt implied by is_subgraph

[ericrbg]

also, i'll change this on the subgraph one too if we find a good way as it's pretty much a copy-paste of that

[eric-wieser]

It breaks if you remove le because pi.le is defined with (v w : V) not ⦃v w : V⦄, so you need extra underscores. I think your custom binders are better though.

[ericrbg]

(I am leaving this unresolved in case we get bounded_lattice.lift or further ideas)

[ericrbg]

i'm not super happy with some of the stuff I did to get the top/bot instances working, but I don't really have better ideas either

[eric-wieser]

I would lean towards defining these directly as the instances:

Suggested change

	/-- The union of two `simple_graph`s. -/
	protected def union (x y : simple_graph V) : simple_graph V :=
	{ adj := x.adj ⊔ y.adj,
	sym := λ v w h, by rwa [sup_apply, sup_apply, x.adj_comm, y.adj_comm] }
	/-- The intersection of two `simple_graph`s. -/
	protected def inter (x y : simple_graph V) : simple_graph V :=
	{ adj := x.adj ⊓ y.adj,
	sym := λ v w h, by rwa [inf_apply, inf_apply, x.adj_comm, y.adj_comm] }
	/-- We define `compl G` to be the `simple_graph V` such that no two adjacent vertices in `G`
	are adjacent in the complement, and every nonadjacent pair of vertices is adjacent
	(still ensuring that vertices are not adjacent to themselves.) -/
	protected def compl (G : simple_graph V) : simple_graph V :=
	{ adj := λ v w, v ≠ w ∧ ¬G.adj v w,
	sym := λ v w ⟨hne, _⟩, ⟨hne.symm, by rwa adj_comm⟩,
	loopless := λ v ⟨hne, _⟩, false.elim (hne rfl) }
	instance (V : Type u) : inhabited (simple_graph V) :=
	⟨complete_graph V⟩
	/-- The difference of two `simple_graph`s, which is the simple graph whose edges
	are all of those from the first graph that aren't in the second graph. -/
	protected def sdiff (x y : simple_graph V) : simple_graph V :=
	{ adj := x.adj \ y.adj,
	sym := λ v w h, by change x.adj w v ∧ ¬ y.adj w v; rwa [x.adj_comm, y.adj_comm] }
	/-- We define `Gᶜ` to be the `simple_graph V` such that no two adjacent vertices in `G`
	are adjacent in the complement, and every nonadjacent pair of vertices is adjacent
	(still ensuring that vertices are not adjacent to themselves.) -/
	instance : has_compl (simple_graph V) :=
	⟨{ adj := λ v w, v ≠ w ∧ ¬G.adj v w,
	sym := λ v w ⟨hne, _⟩, ⟨hne.symm, by rwa adj_comm⟩,
	loopless := λ v ⟨hne, _⟩, false.elim (hne rfl) }⟩
	/-- The difference of two `simple_graph`s, which is the simple graph whose edges
	are all of those from the first graph that aren't in the second graph. -/
	instance : has_sdiff (simple_graph V) :=
	⟨{ adj := x.adj \ y.adj,
	sym := λ v w h, by change x.adj w v ∧ ¬ y.adj w v; rwa [x.adj_comm, y.adj_comm] }⟩

etc. The corresponding foo_adj lemmas can go immediately after each instance.

[ericrbg]

shame simps makes something like simple_graph.has_sup_sup_adj: > ∀ {V : Type u} (x y : simple_graph V) (ᾰ ᾰ_1 : V), (x ⊔ y).adj ᾰ ᾰ_1 = (x.adj ⊔ y.adj) ᾰ ᾰ_1 here, so I have to do it manually

[eric-wieser]

@[simps {simp_rhs := tt}] does a better job probably, but still uses a weird lemma name.

[ericrbg]

it makes (x.adj ᾰ ∪ y.adj ᾰ) ᾰ_1 actually, which doesn't seem like the right simp-normal form

[ericrbg]

I didn't know we also had pi.has_union

[eric-wieser]

That's a little alarming - it must be swapping between set X and X -> Prop somewhere...

Does this fail if you put it in that file?

example {α} [has_sup α] (x y : α → α → Prop) (m n : α) : (x ⊔ y) m n :=
begin
  simp?,
  guard_target_strict x m n ∨ y m n,
  sorry
end

[ericrbg]

yep, the simp? output is simp only [set.sup_eq_union, sup_apply]

[eric-wieser]

Ouch, that shouldn't happen :(

[eric-wieser]

bors d+

[bors]

✌️ ericrbg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ericrbg]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests