Another kind of simp regression

Stream: mathlib4

[Bhavik Mehta]

Here's another simp regression I found while porting the exponential ramsey project:

import Mathlib.Init.Set
import Std.Logic

structure MySimpleGraph (V : Type u) where
  Adj : V → V → Prop
  loopless : ∀ x, ¬ Adj x x

namespace MySimpleGraph

@[simp] theorem irrefl {G : MySimpleGraph V} {v : V} : ¬G.Adj v v := G.loopless v

def neighbourSet {V : Type _} (G : MySimpleGraph V) (v : V)  :
    Set V := setOf (G.Adj v)

@[simp] theorem mem_neighbourFinset {V : Type _} (G : MySimpleGraph V) (v : V) (w : V) :
    w ∈ G.neighbourSet v ↔ G.Adj v w := Iff.rfl

variable {V V' : Type _} {K : Type _}

structure Foo (V K : Type _) :=
(get : (x y : V) → x ≠ y → K)
(symm : ∀ x y : V, (h : x ≠ y) → get y x h.symm = get x y h)

def Foo.labelGraph (C : Foo V K) (k : K) : MySimpleGraph V where
  Adj x y := ∃ h : x ≠ y, C.get x y h = k
  loopless := by
    intro x hx
    have ⟨h, _⟩ := hx
    exact h rfl

theorem Foo.labelGraph_adj {C : Foo V K} {k : K} (x y : V) :
    (C.labelGraph k).Adj x y ↔ ∃ H : x ≠ y, C.get x y H = k :=
  Iff.rfl

theorem SimpleGraph.extracted_1 {K : Type _} [DecidableEq K] {M : Nat}
    (C : Foo (Fin (M + 1)) K) (k' : K) (y : Fin (M + 1)) :
  ∀ (hy : y ∈ neighbourSet (C.labelGraph k') 0),
    C.get 0 y (Ne.symm (ne_of_mem_of_not_mem hy (by simp))) = k' := by
  simp only [mem_neighbourFinset, Foo.labelGraph_adj, ne_eq, forall_exists_index]
  simp

The final simp succeeds and closes the goal in Lean 3. I haven't yet managed to isolate mathlib from it, although what's left is hopefully not too bad to remove... hopefully it's pretty clear that originally this had lots of mathlib in it!

[Eric Wieser]

I think I understand how to make the mwe here, will report back shortly

[Eric Wieser]

import Std.Logic

def getOne (x : Nat) (_hx : x = 1) : Nat := x

example {P : Prop} : P → P := by simp only [imp_self]
example {x} (hx : x = 1) : ∀ h : getOne x hx = 1, getOne x h = 1 := id
example {x} (hx : x = 1) : ∀ h : getOne x hx = 1, getOne x h = 1 := by simp -- fails

[Bhavik Mehta]

Hmm I'm not sure that captures the regression since it also fails in Lean 3

[Eric Wieser]

This works in Lean 3:

import logic.basic

example {P : Prop} : P → P := by simp

example {α : Prop} {P : α → Prop} {f : ∀ {a}, P a → α} {a : α} : ∀ (h : P a), P (f h) := by
  simp

[Eric Wieser]

This fails in lean4:

import Std.Logic

example {P : Prop} : P → P := by simp

example {α : Prop} {P : α → Prop} {f : ∀ {a}, P a → α} {a : α} : (h : P a) → P (f h) := by
  simp

[Eric Wieser]

Note that rw [imp_self] works in lean4, so this is another rw vs simp thing

[Eric Wieser]

simp (config := { contextual := true}) can do it

[Bhavik Mehta]

Yes, this captures it, thanks! Here's a version which doesn't depend on std:

@[simp] theorem imp_self {a : Prop} : (a → a) ↔ True := ⟨fun _ => trivial, fun _ => id⟩

example {P : Prop} : P → P := by simp only [imp_self]

example {α : Prop} {P : α → Prop} {f : ∀ {a}, P a → α} {a : α} : (h : P a) → P (f h) := by
  simp only [imp_self]

[Bhavik Mehta]

Reported as https://github.com/leanprover/lean4/issues/2835