Inductive graphs - how good or bad is such idea?

Stream: graph theory

[Ilmārs Cīrulis]

I mean this idea by Martin Erwig: https://web.engr.oregonstate.edu/~erwig/papers/InductiveGraphs_JFP01.pdf
I will try to realize it and develop a bit further for training and curiosity purposes, but, still, I'm interested about usefulness of this idea from your much more experienced view point.

I got this far with my try (and also defined full graph, path graph and cycle graph, but that will wait until I define adjacency function and test my definitions with it):

inductive pre_simple_graph: Nat → Type :=
  | Empty: pre_simple_graph 0
  | Cons: forall n, List Nat → pre_simple_graph n → pre_simple_graph (n + 1)

def correct_simple_graph {n} (g: pre_simple_graph n): Prop :=
  match g with
  | .Empty => True
  | .Cons _ h t => h.Nodup ∧ (∀ x, x ∈ h → x < n) ∧ correct_simple_graph t

Don't beat me too hard. :sweat_smile:

[Kim Morrison]

You could also consider Cons : Set (Fin n) → pre_simple_graph n → pre_simple_graph (n + 1).

[Ilmārs Cīrulis]

Current state is here. And, yes, the biggest difficulty right now is proving properties of adjacent (symmetry and antireflexivity).

Variant with Set (Fin (n + 1)) was too difficult for me, although it makes the definition much more beautiful, in my opinion.

[Kyle Miller]

Something to keep in mind with SimpleGraph is that it's more of an interface for simple graphs than an actual data structure. Something you could do is define a function from inductive graphs to SimpleGraph to show that it actually "is" a simple graph.

[Ilmārs Cīrulis]

Will try, when I prove these two properties of adjacent as the first sanity check.

[Ilmārs Cīrulis]

Function from simple_graph to Mathlib's SimpleGraph is done. Now thinking about doing the reverse direction...

[Kyle Miller]

There should be an algorithm for it when you have [DecidableRel G.Adj]

[Ilmārs Cīrulis]

My try is here

Will think more, if there's some other approach because I had problems proving that it's bijective correspondence.

[Kyle Miller]

It's not a bijective correspondence, since there are multiple representations of the same graph via inductive graphs (unless each List is in strictly increasing order, or some normalization like that, to remove duplicates and ignore reorderings).

Going from a SimpleGraph to inductive graphs and back should give you an = graph, but going from inductive graphs and back should give you isomorphic graphs (you could state the theorem as "they have the same adjacency relation" rather than using = on the graphs themselves).

[Kyle Miller]

The most important theorem here would be to prove that your SimpleGraph_to_simple_graph is adjacency-relation-preserving. (Same for SimpleGraph_to_pre_simple_graph).

[Ilmārs Cīrulis]

Going to ask question here about one part/sorry here (and without mwe, because not sure how to make wme).

here, in the proof of adj_proof_2 at the first sorry I get such hypothesis:

H0 : y ∈
  match n✝ + 1, ↑(SimpleGraph_to_simple_graph (remove_last G)) with
  | .(0), pre_simple_graph.Empty => []
  | .(m + 1), pre_simple_graph.Cons m L g' => if x ∈ L then (n✝ + 1) :: neighbors_aux g' x else neighbors_aux g' x

Is there some way to convince Lean that it has to go to second branch of match and simplify the H0 accordingly?

[Kyle Miller]

maybe split at H0?

[Ilmārs Cīrulis]

Wow, thank you! It worked.

[Yakov Pechersky]

There's also a nice axiomatization of graphs here with a series of blog posts https://github.com/snowleopard/alga-paper https://blogs.ncl.ac.uk/andreymokhov/an-algebra-of-graphs/

[Ilmārs Cīrulis]

Something is wrong with my definition of SimpleGraph_to_pre_simple_graph, probably, as I can't prove that it conserves adjacency.
Will check it with some examples and similarly, maybe it is the reason.

[Ilmārs Cīrulis]

Hmm, it works correctly, afaict.

[Ilmārs Cīrulis]

If someone wants to tinker with the last proof (the adj_proof_2), the file is here [edit:] Although I believe now it is not provable and there is a mistake earlier. :dissolve:

I'm taking a pause because I'm clearly not understanding something. :sweat_smile:

[Ilmārs Cīrulis]

I hope I fixed some bugs in definitions. :melt:

[Ilmārs Cīrulis]

Almost done, only this tiny theorem is sorryed.
theorem fin_list_nodup n: (Fin.list n).Nodup := by sorry

[Ilmārs Cīrulis]

Hoorah, what a relief. :partying_face:

[Ilmārs Cīrulis]

Next step will be a try to prove degree-sum-formula (degree sum equals two cardinalities of edge set) which we already have in Mathlib. By induction on size or smth like that.

[Kyle Miller]

Given the map to simple graphs, maybe you could pull back the mathlib result?

[Ilmārs Cīrulis]

What exactly does "pull back" mean in this context? :sweat_smile:
My goal is to (re)prove Mathlib's result using inductive graphs.

[Ilmārs Cīrulis]

theorem sum_of_degrees_twice_of_edges {n} (g: simple_graph n):   ∑ (i ∈ Finset.range n), degree g i = 2 * (edges g).length

Done here for inductive graphs, now to transfer this result to usual SimpleGraphs.
(Big thanks to helpers with sums in some other chat.)

[Ilmārs Cīrulis]

Hmm, getting to Mathlib's version from the theorem for simple_graph is impressively hard. At least for me.
Although interesting and allows me to learn things.

[Ilmārs Cīrulis]

Exhausted, but it's done. :partying_face:
With help of the zulip chat, of course. :heart:

[Ilmārs Cīrulis]

For now the code is a bit messy, will reorganize later, probably.

[Ilmārs Cīrulis]

Ah, my variation is _almost_ as Mathlib's version:

theorem sum_degrees_eq_twice_card_edges_Fin_variant {n} (G: SimpleGraph (Fin n)) [DecidableRel G.Adj]:
  ∑ v, G.degree v = 2 * G.edgeFinset.card

But it should be relatively easy to get from this to exact Mathlib theorem, I believe. Will do it, of course.

[Ilmārs Cīrulis]

Ok, I stuck with such problem - two things seem to have equal types (at least visually), but assumption or exact doesn't work. :sad:

V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Fintype (Sym2 V)
equiv : V ≃ Fin (Fintype.card V)
G' : SimpleGraph (Fin (Fintype.card V)) := { Adj := fun v1 v2 ↦ G.Adj (equiv.invFun v1) (equiv.invFun v2), symm := ⋯, loopless := ⋯ }
H1 : ∀ (v : V), v ∈ Finset.univ ↔ equiv v ∈ Finset.univ
inst : (v : V) → Fintype ↑(G'.neighborSet (equiv v))
H2 : ∀ (x : V), G.degree x = G'.degree (equiv x)
⊢ ∀ (x : V), G.degree x = G'.degree (equiv x)

[Ilmārs Cīrulis]

Will try to make mwe.

[Ilmārs Cīrulis]

import Mathlib

theorem sum_degrees_eq_twice_card_edges_Fin_variant {n} (G: SimpleGraph (Fin n)) [DecidableRel G.Adj]:
  ∑ v, G.degree v = 2 * G.edgeFinset.card := by sorry

theorem sum_degrees_eq_twice_card_edges_Mathlib_version {V} (G: SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [Fintype (Sym2 V)]:
  ∑ v : V, G.degree v = 2 * G.edgeFinset.card := by
  have equiv := Fintype.equivFin V
  let G': SimpleGraph (Fin (Fintype.card V)) := by
    refine (SimpleGraph.mk (fun v1 v2 => G.Adj (equiv.invFun v1) (equiv.invFun v2)) ?_ ?_)
    . unfold Symmetric
      intros x y
      apply G.symm
    . unfold Irreflexive
      intros x
      apply G.loopless
  have H1: ∀ (v: V), v ∈ Finset.univ ↔ equiv v ∈ Finset.univ := by sorry
  have inst: ∀ v, Fintype ↑(G'.neighborSet (equiv v)) := by sorry
  have H2: ∀ (x: V), G.degree x = G'.degree (equiv x) := by sorry
  have H3: ∑ v, G.degree v = ∑ v, G'.degree v := by
    apply (Fintype.sum_equiv equiv (fun x => G.degree x) (fun x => G'.degree x))
    #check H2
    -- exact H2 fails
    exact H2
    sorry
  sorry

[Yakov Pechersky]

What does convert H2 give you?

[Ilmārs Cīrulis]

convert H2 does work.

[Ilmārs Cīrulis]

theorem sum_degrees_eq_twice_card_edges_Mathlib_version {V} (G: SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [Fintype (Sym2 V)]:
  ∑ v : V, G.degree v = 2 * G.edgeFinset.card

Done

[Ilmārs Cīrulis]

Great, importing all Mathlib for easier development was bad idea. :sweat:
I see (now, when reorganizing and making the code less ugly) that I have accidentally smuggled in and used the lemma https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/DegreeSum.html#SimpleGraph.two_mul_card_edgeFinset

Why did I do that? I don't know.

[Ilmārs Cīrulis]

Well, it doesn't depend on SimpleGraph.sum_degrees_eq_twice_card_edg (what I was trying to prove), as far as I can see.

[Ilmārs Cīrulis]

I will let it stay, probably :|

[Ilmārs Cīrulis]

Reorganized the repository (and rewrote code too a bit), now the structure is much better.

The SimpleGraph result is here now. As it can be seen, I made it depend on this theorem:

-- https://leanprover-community.github.io/mathlib4_docs/Mathlib/Combinatorics/SimpleGraph/DegreeSum.html#SimpleGraph.two_mul_card_edgeFinset
theorem two_mul_card_edgeFinset {V} (G : SimpleGraph V) [Fintype V] [DecidableRel G.Adj] [Fintype (Sym2 V)]:
  2 * G.edgeFinset.card = (Finset.filter (fun (x: V × V) => G.Adj x.1 x.2) Finset.univ).card := by sorry

Can that be proven in some easier way than in Mathlib? It seems that it's kinda byproduct of all technology used for main DegreeSum file result. Not sure, but it seems that way.

[Daniel Weber]

Are you planning to eventually contribute this to Mathlib? I wanted to prove that every graph is maxDegree + 1 colorable, and I realized that this should make it really easy

[Kyle Miller]

For what it's worth @Daniel Weber, I just hacked together greedy colorings for graphs with vertex type Fin n. Then you'd need to show that the image can be restricted to Fin (G.maxDegree + 1), and also reformulate this for a graph over an arbitrary fintype (you should be able to pull the result over G.map e, where e : V ≃ Fin (Fintype.card V))

-- At the bottom of Mathlib.Combinatorics.SimpleGraph.ConcreteColorings
-- after adding `import Mathlib.Combinatorics.SimpleGraph.Finite`

def greedyColoringFn : {n : ℕ} → (G : SimpleGraph (Fin n)) → [DecidableRel G.Adj] → Fin n → ℕ
  | 0, _, _ => nofun
  | n' + 1, G, _ =>
    let G' : SimpleGraph (Fin n') := G.comap (Fin.castLEEmb (by omega))
    let c := greedyColoringFn G'
    fun v =>
      if hv : v.1 < n' then
        c ⟨v, hv⟩
      else
        let used := (G.neighborFinset v).image fun w =>
          if hw : w.1 < n' then c ⟨w.1, hw⟩
          else 0 -- doesn't occur
        Nat.find (p := fun k => k ∉ used) (Infinite.exists_not_mem_finset used)

def greedyColoring {n} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] : Coloring G ℕ :=
  Coloring.mk (greedyColoringFn G) <| by
    induction n with
    | zero => rintro ⟨_, ⟨⟩⟩
    | succ n ih =>
      intro ⟨v, hv⟩ ⟨w, hw⟩
      wlog hvw : v < w
      · obtain rfl | hvw := eq_or_lt_of_not_lt hvw
        · intro h; exact (G.irrefl h).elim
        · intro h; exact (this _ ih _ _ _ _ _ hvw h.symm).symm
      rw [Nat.lt_succ_iff_lt_or_eq] at hv hw
      obtain hv | rfl := hv <;> obtain hw | rfl := hw
      · intro ha
        have := @ih (G.comap (Fin.castLEEmb (by omega))) _ ⟨v, hv⟩ ⟨w, hw⟩
        simpa [greedyColoringFn, hv, hw, ha] using this
      · intro ha
        simp [greedyColoringFn, hv]
        generalize_proofs _ _ hpf
        have := Nat.find_spec hpf
        specialize this ⟨v, _⟩ ha.symm
        simpa [hv] using this
      · exfalso; omega
      · simp

[Kyle Miller]

It shouldn't take too much more work from here:

lemma comap_neighborFinset_subset_neighborSet {V W} (G : SimpleGraph W) [LocallyFinite G]
    (f : V ↪ W) [LocallyFinite (G.comap f)] (v : V) :
    Finset.map f ((G.comap f).neighborFinset v) ⊆ G.neighborFinset (f v) := by
  intro w
  simp
  intros
  subst_vars
  assumption

lemma comap_degree_le_degree {V W} (G : SimpleGraph W) [LocallyFinite G]
    (f : V ↪ W) [LocallyFinite (G.comap f)] (v : V) :
    (G.comap f).degree v ≤ G.degree (f v) := by
  rw [← card_neighborFinset_eq_degree, ← card_neighborFinset_eq_degree]
  rw [← Finset.card_map f]
  convert Finset.card_le_card (comap_neighborFinset_subset_neighborSet G f v)

theorem greedyColoring_prop {n d} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
    (h : ∀ v, G.degree v ≤ d) :
    ∀ v, G.greedyColoring v ≤ d + 1 := by
  induction n with
  | zero => rintro ⟨_, ⟨⟩⟩
  | succ n ih =>
    specialize ih (G.comap (Fin.castLEEmb (by omega)))
    intro ⟨v, hv⟩
    change G.greedyColoringFn _ ≤ _
    simp only [greedyColoringFn]
    obtain hv | rfl := Nat.lt_succ_iff_lt_or_eq.mp hv
    · simp [hv]
      apply ih
      intro w
      specialize h ⟨w, by omega⟩
      refine le_trans ?_ h
      apply comap_degree_le_degree
    · simp only [lt_self_iff_false, ↓reduceDIte]
      specialize ih ?_
      · intro w
        refine le_trans ?_ (h ⟨w.1, by omega⟩)
        apply comap_degree_le_degree
      simp only [Nat.find_le_iff]
      /-
      d v : ℕ
      G : SimpleGraph (Fin (v + 1))
      inst✝ : DecidableRel G.Adj
      h : ∀ (v_1 : Fin (v + 1)), G.degree v_1 ≤ d
      hv : v < v + 1
      ih : ∀ (v_1 : Fin v), (SimpleGraph.comap (⇑(Fin.castLEEmb ⋯)) G).greedyColoring v_1 ≤ d + 1
      ⊢ ∃ m ≤ d + 1,
        m ∉
          Finset.image
            (fun w ↦
              if hw : ↑w < v then
                (SimpleGraph.comap (⇑(Fin.castLEEmb ⋯)) G).greedyColoringFn ⟨↑w, hw⟩
              else 0)
            (G.neighborFinset ⟨v, hv⟩)
      -/
      -- Need to show this `Finset.image` is in `[0,…,d+1]` and has cardinality `≤ d`.
      -- Then `m` can be an element not in the image but in this interval.
      sorry

[Kyle Miller]

Github just seems to have gone down in the middle of creating a draft PR, but in the branch kmill_greedy_coloring I have a very rough draft of this, and once Github comes back I'll also push a concrete greedy coloring:

noncomputable def greedyColoring'' {V} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] :
    Coloring G (Fin (G.maxDegree + 1))

[Kyle Miller]

Github's back, here's the draft PR: #15822

It can definitely use cleaning up. (I have been working on this running VS Code SSH'd over airplane wifi a fast computer on the ground, but the lag has been a bit difficult to deal with!)

[Mauricio Collares]

Daniel Weber said:

Are you planning to eventually contribute this to Mathlib? I wanted to prove that every graph is maxDegree + 1 colorable, and I realized that this should make it really easy

Ooh, this reminds me that proving Hajnal-Szemerédi (perhaps following https://kostochk.web.illinois.edu/docs/2008/cpc08k.pdf) would be a great project

[Ilmārs Cīrulis]

Oh, sorry for disappearing. New academic year starting (even if I study nothing now academically), lots of stuff happening, basically got distracted away from this chat and Lean and math.

Daniel Weber said:

Are you planning to eventually contribute this to Mathlib?

Probably not.

[Ilmārs Cīrulis]

Just in case, I'm pausing this for some unknown time period. Other stuff calls for me (for now).

[Alena Gusakov]

Mauricio Collares said:

Daniel Weber said:

Are you planning to eventually contribute this to Mathlib? I wanted to prove that every graph is maxDegree + 1 colorable, and I realized that this should make it really easy

Ooh, this reminds me that proving Hajnal-Szemerédi (perhaps following https://kostochk.web.illinois.edu/docs/2008/cpc08k.pdf) would be a great project

Does anyone mind if I take a crack at starting this?

[Kyle Miller]

@Alena Gusakov I already proved this a few messages up

[Kyle Miller]

I wonder if it's generalizable to infinite but locally finite graphs?

[Alena Gusakov]

Kyle Miller said:

Alena Gusakov I already proved this a few messages up

I meant the Hajnal-Szemeredi result, unless I'm misunderstanding

[Kyle Miller]

Oh, no, I just misread the message, sorry!

[Ilmārs Cīrulis]

Prfft, I see that I have deleted it (the repository etc.). Don't ask me "why", as I don't remember. :sweat_smile:

Oh well, let's start it from scratch again. This time with this definition by Kim Morrison here

import Mathlib

inductive simple_graph: Nat → Type where
  | Empty: simple_graph 0
  | Cons: ∀ {n}, Set (Fin n) → simple_graph n → simple_graph (n + 1)

def adjacent {n} (G: simple_graph n): Fin n → Fin n → Prop :=
  fun x y => match G with
             | simple_graph.Empty => False
             | @simple_graph.Cons m s g => if hx:(x.val = m)
                                           then ∃ y', y' ∈ s ∧ y.val = y'.val
                                           else if hy:(y.val = m)
                                                then ∃ x', x' ∈ s ∧ x.val = x'.val
                                                else adjacent g ⟨x.val, by omega⟩ ⟨y.val, by omega⟩

def adjacent_irrefl {n} (G: simple_graph n) (x: Fin n): adjacent G x x → False := by
  induction G with
  | Empty => cases x with | mk val isLt => omega
  | Cons s g iH =>
    unfold adjacent; split
    . cases x with | mk val isLt =>
      simp at *
      intros x' Hx' H
      cases x' with | mk val' isLt' =>
      simp at *
      omega
    . apply iH

def adjacent_symm {n} (G: simple_graph n) (x y: Fin n): adjacent G x y -> adjacent G y x := by
  intro H
  induction G with
  | Empty => itauto
  | Cons s g iH => unfold adjacent; unfold adjacent at H; aesop

[Ilmārs Cīrulis]

Does this make sense?
And what about use of aesop at the end, is it okay? (as it finishes the proof)

[Ilmārs Cīrulis]

Defined transformation (with this new and, imho, better definition of simple_graph) of simple_graph to standard SimpleGraph and back, also proved that it is bijection (?): SimpleGraph_to_simple_graph (simple_graph_to_SimpleGraph g) = g and simple_graph_to_SimpleGraph (SimpleGraph_to_simple_graph G) = G.

Here is a gist.

[Shreyas Srinivas]

The definition seems overkill

[Shreyas Srinivas]

In the adjacency relation, why can’t you just say “(either x = m and y is in s) or (y=m and x is in s) or (x and y are adjacent in the inductive argument)

[Shreyas Srinivas]

If I had to guess, a lot of your proofs will become simpler

[Ilmārs Cīrulis]

Hmm, I tried to rework the adjacency relation, but it's seems that it doesn't work out.

I need to use information that x.val <> m and y.val <> m to make recursive call adjacent g ⟨x.val, by omega⟩ ⟨y.val, by omega⟩ with argument n smaller by 1.

[Ilmārs Cīrulis]

At least, it seems not to work out if I keep the newest definition of simple_graph...

[Shreyas Srinivas]

Also with Fin, some strange things are possible:

import Mathlib

def x1 : Fin 3 := 3

def x2 : Fin 4 := 3

#eval x1 == x2
#eval x1
#eval x2

[Shreyas Srinivas]

I see that you are only comparing vals, but I'd like to check this carefully to be sure.

[Shreyas Srinivas]

So I was simplifying your defs and came across some strange behaviour:

import Mathlib

inductive IndGraph: Nat → Type where
  | Empty: IndGraph 0
  | Cons: ∀ {n}, Set (Fin n) → IndGraph n → IndGraph (n + 1)

def IndGraph.adjacent {n} (G: IndGraph n): Fin n → Fin n → Prop :=
  fun x y => match G with
             | IndGraph.Empty => False
             | @IndGraph.Cons m S Gₘ =>
                  if heq : x = y then False
                  else if hx:(x.val = m)
                  then (⟨y, by omega⟩: Fin m) ∈ S
                  else
                    if hy:(y.val = m)
                    then (⟨x, by omega⟩ : Fin m) ∈ S
                    else adjacent Gₘ ⟨x.val, by omega⟩ ⟨y.val, by omega⟩


def adjacent_irrefl {n} (G: IndGraph n): Irreflexive G.adjacent := by
  simp only [Irreflexive]
  intro x
  induction G with (simp [IndGraph.adjacent])


def adjacent_symm {n} (G: IndGraph n): Symmetric G.adjacent := by
  simp [Symmetric]
  intro x y H
  induction G with (simp[IndGraph.adjacent] <;> aesop)
  | Cons x S Gₙ =>
      simp_all [IndGraph.adjacent]
      --sorry -- If you add this sorry, you are told that there is no goal left. If you remove the sorry then there is an unsolved goal.

@Kyle Miller : Is this some strange bug? (tagging you because you are already in this conversation according to Zulip, I hope that's fine).

[Shreyas Srinivas]

fwiw, I think I can finish the proof differently. It's this strange behaviour of "add sorry and then you are told there are no goals, but remove sorry and there are goals" that is confusing

[Shreyas Srinivas]

The above code but fixed and simpler

import Mathlib

inductive IndGraph: Nat → Type where
  | Empty: IndGraph 0
  | Cons: ∀ {n}, Set (Fin n) → IndGraph n → IndGraph (n + 1)

def IndGraph.adjacent {n} (G: IndGraph n): Fin n → Fin n → Prop :=
  fun x y => match G with
             | IndGraph.Empty => False
             | @IndGraph.Cons m S Gₘ =>
                  if heq : x = y then False
                  else if hx:(x.val = m)
                  then (⟨y, by omega⟩: Fin m) ∈ S
                  else
                    if hy:(y.val = m)
                    then (⟨x, by omega⟩ : Fin m) ∈ S
                    else adjacent Gₘ ⟨x.val, by omega⟩ ⟨y.val, by omega⟩


theorem adjacent_irrefl {n} (G: IndGraph n): Irreflexive G.adjacent := by
  simp only [Irreflexive]
  intro x
  induction G with (simp [IndGraph.adjacent])


theorem adjacent_symm {n} (G: IndGraph n): Symmetric G.adjacent := by
  simp [Symmetric]
  intro x y H
  induction G with (simp_all [IndGraph.adjacent] <;> aesop)

[Ilmārs Cīrulis]

Yes, it looks much better without that existence quantifiers. Thank you very much!

[Shreyas Srinivas]

I am guessing all the proofs further below can also be simplified like this.

[Kevin Buzzard]

With the weird sorry issue -- is it due to aesop not solving the goal when the induction is set up?

[Shreyas Srinivas]

No clue. I managed to solve it more shortly as shown in the spoilers.

[Shreyas Srinivas]

Fwiw, this is not the first time I am seeing this. It also happens when I put other tactics that touch hypotheses inside the brackets after induction .. with.

[Shreyas Srinivas]

@Ilmārs Cīrulis : There is a further simplification possible if you assume that in each inductive step, you only connect vertex number (n + 1) to some set of vertices. Then you can simply omit the vertex parameter in the inductive definition

[Shreyas Srinivas]

I take that back. you already use an implicit parameter

[Ilmārs Cīrulis]

Updated the gist

[Shreyas Srinivas]

The subsequent proofs can also be shortened

[Shreyas Srinivas]

For example in IndGraph_equiv theorem, the first case should be doable with cases g2 <;> cases g1<;> rfl