Some problem with rewriting

Stream: new members

[Ilmārs Cīrulis]

See the line before the last sorry that I have commented out. The attempt to rewrite keeps going with no end, until heartbeats are exhausted.

I tried to use set_option trace.Meta.isDefEq true in, but it didn't help.
set_option pp.all true just made my eyes hurt with no gain (but I will try again).

import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Data.Fin.VecNotation
import Mathlib.Tactic.DepRewrite

set_option linter.flexible false
set_option linter.unusedDecidableInType false


def add_vertex {n} (G : SimpleGraph (Fin n)) (vertices : Finset (Fin n)) :
    SimpleGraph (Fin (n + 1)) :=
  ⟨fun (x y : Fin (n + 1)) =>
    if h₁ : x = Fin.last n
    then if h₂ : y = Fin.last n
         then False
         else (⟨y.val, by grind⟩ : Fin n) ∈ vertices
    else if h₂ : y = Fin.last n
         then (⟨x.val, by grind⟩ : Fin n) ∈ vertices
         else G.Adj ⟨x.val, by grind⟩ ⟨y.val, by grind⟩,
    by intros x y h; split_ifs at * <;> try grind
       exact G.symm h,
    by intros x h; simp at h; grind⟩

def remove_last_vertex {n} (G : SimpleGraph (Fin (n + 1))) [DecidableRel G.Adj] :
    SimpleGraph (Fin n) :=
  ⟨fun x y => G.Adj x.castSucc y.castSucc,
   fun _ _ h => G.symm h,
   fun _ h => G.irrefl h⟩

lemma add_vertex_remove_last_vertex_eq_self {n} (G : SimpleGraph (Fin (n + 1)))
    [DecidableRel G.Adj] :
    add_vertex (remove_last_vertex G) {x : Fin n | G.Adj (Fin.last n) x.castSucc} = G := by
    ext x y; simp [add_vertex, remove_last_vertex]; split_ifs
    · rename_i h; subst h; simp; intros h h₀; subst h₀; exact G.irrefl h
    · rename_i h₁ h₂; subst h₂; constructor <;> exact fun h => G.symm h
    · rfl

instance add_vertex_decidable_adj :
    ∀ {n} (G : SimpleGraph (Fin n)) (vs : Finset (Fin n)) [DecidableRel G.Adj]
    [∀ x, Decidable (x ∈ vs)], DecidableRel (add_vertex G vs).Adj := by
  intros n G vs h₁ h₂
  intros x y; simp [add_vertex]
  split_ifs <;> rename_i h₃
  · by_cases h₄ : y = Fin.last n <;> simp [h₄]
    · exact instDecidableFalse
    · apply h₂
  · apply h₂
  · apply h₁

lemma add_vertex_edgeFinset_card {n} (G : SimpleGraph (Fin n)) (vs : Finset (Fin n))
    [DecidableRel G.Adj] [∀ x, Decidable (x ∈ vs)] :
    (add_vertex G vs).edgeFinset.card = G.edgeFinset.card + vs.card := by sorry


lemma remove_last_vertex_of_complete_graph n :
    remove_last_vertex (⊤ : SimpleGraph (Fin (n + 1))) = (⊤ : SimpleGraph (Fin n)) := by
  ext x y; simp [remove_last_vertex]

lemma edgeset_card_of_complete_graph n :
    (⊤ : SimpleGraph (Fin n)).edgeFinset.card = n.choose 2 := by
  induction n with
  | zero => simp [Sym2.diagSet]
  | succ n iH =>
    have h := add_vertex_remove_last_vertex_eq_self (⊤ : SimpleGraph (Fin (n + 1)))
    rw [remove_last_vertex_of_complete_graph] at h
    rw! (castMode := .all) [← h] -- bad sign, probably
    -- rw [add_vertex_edgeFinset_card] -- keeps going until heartbeats end
    sorry

[Ilmārs Cīrulis]

(It's just me reproving very basic result from graph theory, using Mathlib as little as reasonably possible. After I'm done, I will definitely take a look at Mathlib's proof.)

[Aaron Liu]

you probably have a mismatched implicit argument somewhere

[Ilmārs Cīrulis]

Okay, will take a look at them right now.

[Aaron Liu]

aha

[Aaron Liu]

it's the decidability instance which rw! (castMode := .all) has inserted a cast into

[Aaron Liu]

I discovered this by replacing your last few lines with

    rw! (castMode := .all) [← h] -- bad sign, probably
    have := add_vertex_edgeFinset_card ⊤ {x | (⊤ : SimpleGraph (Fin (n + 1))).Adj (Fin.last n) x.castSucc}
/-
Type mismatch
  Eq.mpr (congrArg (fun x => x = ?m.73 x) this) ?m.76
has type
  (@SimpleGraph.edgeFinset (Fin (n + 1)) (add_vertex ⊤ {x | ⊤.Adj (Fin.last n) x.castSucc})
        (@SimpleGraph.fintypeEdgeSet (Fin (n + 1)) (add_vertex ⊤ {x | ⊤.Adj (Fin.last n) x.castSucc}) Sym2.instFintype
          fun a b => add_vertex_decidable_adj ⊤ {x | ⊤.Adj (Fin.last n) x.castSucc} a b)).card =
    ?m.73 (add_vertex ⊤ {x | ⊤.Adj (Fin.last n) x.castSucc}).edgeFinset.card
but is expected to have type
  (@SimpleGraph.edgeFinset (Fin (n + 1)) (add_vertex ⊤ {x | ⊤.Adj (Fin.last n) x.castSucc})
        (@SimpleGraph.fintypeEdgeSet (Fin (n + 1)) (add_vertex ⊤ {x | ⊤.Adj (Fin.last n) x.castSucc}) Sym2.instFintype
          (⋯ ▸ fun a b => SimpleGraph.Top.adjDecidable (Fin (n + 1)) a b))).card =
    (n + 1).choose 2
-/
    refine (congrArg (· = _) this).mpr ?_
    -- rw [add_vertex_edgeFinset_card] -- keeps going until heartbeats end
    sorry

[Ilmārs Cīrulis]

Thanks, I just wanted to ask how did you find it out.

[Ilmārs Cīrulis]

Such problem is the sign of bad approach/design, right?

[Aaron Liu]

maybe there should be a tactic that re-synthesizes all these instances

[Aaron Liu]

well I wouldn't say it's bad design really

[Aaron Liu]

though perhaps this could've been avoided by using a classical decidability instance within the proof and changing to the arbitrary decidability instance afterwards

[Ilmārs Cīrulis]

Okay, I solved it this way (removed the definition of instance and added additional Instance parameter to theorem).

import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Data.Fin.VecNotation
import Mathlib.Tactic.DepRewrite

set_option linter.flexible false
set_option linter.unusedDecidableInType false



def add_vertex {n} (G : SimpleGraph (Fin n)) (vertices : Finset (Fin n)) :
    SimpleGraph (Fin (n + 1)) :=
  ⟨fun (x y : Fin (n + 1)) =>
    if h₁ : x = Fin.last n
    then if h₂ : y = Fin.last n
         then False
         else (⟨y.val, by grind⟩ : Fin n) ∈ vertices
    else if h₂ : y = Fin.last n
         then (⟨x.val, by grind⟩ : Fin n) ∈ vertices
         else G.Adj ⟨x.val, by grind⟩ ⟨y.val, by grind⟩,
    by intros x y h; split_ifs at * <;> try grind
       exact G.symm h,
    by intros x h; simp at h; grind⟩

def remove_last_vertex {n} (G : SimpleGraph (Fin (n + 1))) [DecidableRel G.Adj] :
    SimpleGraph (Fin n) :=
  ⟨fun x y => G.Adj x.castSucc y.castSucc,
   fun _ _ h => G.symm h,
   fun _ h => G.irrefl h⟩

lemma add_vertex_remove_last_vertex_eq_self {n} (G : SimpleGraph (Fin (n + 1)))
    [DecidableRel G.Adj] :
    add_vertex (remove_last_vertex G) {x : Fin n | G.Adj (Fin.last n) x.castSucc} = G := by
    ext x y; simp [add_vertex, remove_last_vertex]; split_ifs
    · rename_i h; subst h; simp; intros h h₀; subst h₀; exact G.irrefl h
    · rename_i h₁ h₂; subst h₂; constructor <;> exact fun h => G.symm h
    · rfl

-- removed the instance

-- added additional instance parameeter to this lemma
lemma add_vertex_edgeFinset_card {n} (G : SimpleGraph (Fin n)) (vs : Finset (Fin n))
    [DecidableRel G.Adj] [∀ x, Decidable (x ∈ vs)] [DecidableRel (add_vertex G vs).Adj] :
    (add_vertex G vs).edgeFinset.card = G.edgeFinset.card + vs.card := by sorry

lemma remove_last_vertex_of_complete_graph n :
    remove_last_vertex (⊤ : SimpleGraph (Fin (n + 1))) = (⊤ : SimpleGraph (Fin n)) := by
  ext x y; simp [remove_last_vertex]


lemma edgeset_card_of_complete_graph n :
    (⊤ : SimpleGraph (Fin n)).edgeFinset.card = n.choose 2 := by
  induction n with
  | zero => simp [Sym2.diagSet]
  | succ n iH =>
    have h := add_vertex_remove_last_vertex_eq_self (⊤ : SimpleGraph (Fin (n + 1)))
    rw [remove_last_vertex_of_complete_graph] at h
    rw! (castMode := .all) [← h] -- bad sign, probably
    rw [add_vertex_edgeFinset_card]
    rw [iH]; simp
    have h₀ : ({x : Fin n | ¬ Fin.last n = x.castSucc} : Finset _) = Finset.univ := by
      ext x; simp; grind
    rw [h₀]
    simp [Nat.choose_succ_left, add_comm]