Error message told me to report on Zulip

Stream: new members

[Ilmārs Cīrulis]

import Mathlib.Combinatorics.SimpleGraph.Finite
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)) := sorry

def remove_last_vertex {n} (G : SimpleGraph (Fin (n + 1))) [DecidableRel G.Adj] :
    SimpleGraph (Fin n) := sorry

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
  sorry

lemma remove_last_vertex_of_complete_graph n :
    remove_last_vertex (⊤ : SimpleGraph (Fin (n + 1))) = (⊤ : SimpleGraph (Fin n)) := by
  sorry

lemma edgeset_card_of_complete_graph n [DecidableRel (⊤ : SimpleGraph (Fin n)).Adj] :
    (⊤ : 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
    -- the next line causes the error
    rw! (castMode := .all) [← h]
    sorry

[Ilmārs Cīrulis]

Error message:

Tactic depRewrite failed: motive
fun x h => x.edgeFinset.card = (n + 1).choose 2
is not type correct:
Application type mismatch: The argument
inst✝
has type
DecidableRel (@Top.top (SimpleGraph (Fin n✝)) SimpleGraph.completeAtomicBooleanAlgebra.toBooleanAlgebra.toTop).Adj
but is expected to have type
DecidableRel
(@Top.top (SimpleGraph (Fin (n + 1))) SimpleGraph.completeAtomicBooleanAlgebra.toBooleanAlgebra.toTop).Adj
in the application
@Eq.rec (SimpleGraph (Fin (n + 1))) ⊤ (fun x' h' => DecidableRel x'.Adj) inst✝
unlike with rw/rewrite, this error should NOT happen in rw!/rewrite!: please report it on the Lean Zulip

[Ilmārs Cīrulis]

It seems that I missed an error before this error. Shouldn't post when sleepy, probably.

When I replace last sorried lemma with

lemma edgeset_card_of_complete_graph n [DecidableRel (⊤ : SimpleGraph (Fin n)).Adj]:
    (⊤ : SimpleGraph (Fin n)).edgeFinset.card = n.choose 2 := by
  induction n with
  | zero => simp [Sym2.diagSet]
  | succ n iH => sorry

there's still some weird error:

(kernel) application type mismatch
⊤.fintypeEdgeSet
argument has type
DecidableRel ⊤.Adj
but function has type
[DecidableRel ⊤.Adj] → Fintype ↑⊤.edgeSetLean 4

It's possible that the rw! error was caused by this one.

[Riccardo Brasca]

I am not very familiar with the rw! tactic, but erasing [DecidableRel (⊤ : SimpleGraph (Fin n)).Adj]makes the error go away.

[Ilmārs Cīrulis]

Yes, that's true. Before addition of [DecidableRel (⊤ : SimpleGraph (Fin n)).Adj] everything was okay.

[Snir Broshi]

cc @Aaron Liu

[Aaron Liu]

yes I will take a look thanks for reporting it

[Aaron Liu]

huh interesting

[Aaron Liu]

it looks like the actual problem is with induction producing a goal that doesn't typecheck

[Aaron Liu]

and then rw! is the first tactic that checked the goal and found a problem

[Aaron Liu]

import Mathlib.Combinatorics.SimpleGraph.Finite
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)) := sorry

def remove_last_vertex {n} (G : SimpleGraph (Fin (n + 1))) [DecidableRel G.Adj] :
    SimpleGraph (Fin n) := sorry

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
  sorry

lemma remove_last_vertex_of_complete_graph n :
    remove_last_vertex (⊤ : SimpleGraph (Fin (n + 1))) = (⊤ : SimpleGraph (Fin n)) := by
  sorry

lemma edgeset_card_of_complete_graph n [DecidableRel (⊤ : SimpleGraph (Fin n)).Adj] :
    (⊤ : SimpleGraph (Fin n)).edgeFinset.card = n.choose 2 := by
  induction n with
  | zero => simp [Sym2.diagSet]
  | succ n iH =>
    -- fails
    run_tac do
      Lean.Elab.Tactic.withMainContext do
        let goal ← Lean.Elab.Tactic.getMainTarget
        Lean.Meta.check goal
    have h := add_vertex_remove_last_vertex_eq_self (⊤ : SimpleGraph (Fin (n + 1)))
    rw [remove_last_vertex_of_complete_graph] at h
    -- the next line causes the error
    rw! (castMode := .all) [← h]
    sorry

[Aaron Liu]

that makes this an instance of lean4#6544

[Ilmārs Cīrulis]

Thank you!