grind cannot see past CoeFun

Stream: lean4

[Jakub Nowak]

import Mathlib

namespace Sym2'

inductive Rel (α : Type u) : α × α → α × α → Prop
  | refl (x y : α) : Rel _ (x, y) (x, y)
  | swap (x y : α) : Rel _ (x, y) (y, x)

def Rel.setoid (α : Type u) : Setoid (α × α) :=
  ⟨Rel α, sorry⟩

abbrev Sym2 (α : Type u) := Quotient (Rel.setoid α)

abbrev Sym2.mk {α : Type u} (p : α × α) : Sym2 α := Quotient.mk (Rel.setoid α) p

example {x y z w : α} : Sym2.mk (x, y) = Sym2.mk (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z := by
  -- This works.
  simp only [Quotient.eq, Rel.setoid]
  grind only [Rel]

example {x y z w : α} : Sym2.mk (x, y) = Sym2.mk (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z := by
  -- This works.
  simp only [Quotient.eq]
  show Rel α (x, y) (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
  grind only [Rel]

example {x y z w : α} : Sym2.mk (x, y) = Sym2.mk (z, w) ↔ x = z ∧ y = w ∨ x = w ∧ y = z := by
  -- This doesn't work.
  grind [Quotient.eq, Rel.setoid, Rel]
  -- True propositions contain
  -- [prop] (Rel.setoid α) (x, y) (x, y)
  -- [prop] (Rel.setoid α) (x, y) (z, w)
  -- [prop] (Rel.setoid α) (z, w) (x, y)
  -- [prop] (Rel.setoid α) (z, w) (z, w)
  -- but no
  -- [prop] Rel α (x, y) (x, y)
  -- [prop] Rel α (x, y) (z, w)
  -- [prop] Rel α (z, w) (x, y)
  -- [prop] Rel α (z, w) (z, w)

end Sym2'

Although, it works in this smaller case I've tried to make:

structure Foo where
  f : Nat → Nat

instance : CoeFun Foo (fun _ ↦ Nat → Nat) where
  coe := Foo.f

variable (foo : Foo)

example : foo 2 = foo.f 2 := by
  simp only

example : foo 2 = foo.f 2 := by
  grind only

Not sure why that happens then.

[Jakub Nowak]

So, I think what's happening is that (Rel.setoid α) (x, y) (x, y) and Rel α (x, y) (x, y) are just defeq, but grind won't convert first to the second, because there are not grind_patterns that would lead it to this conversion.

Although I'm still not sure why adding Rel.setoid to simp patterns made it successfully convert (Rel.setoid α) (x, y) (x, y) to Rel α (x, y) (x, y), but grind wasn't able to do that conversion, even though there's Rel.setoid.eq_1: [Rel.setoid #0] pattern.

[Jakub Nowak]

I've tried adding

theorem t₁ {α : Type u} {s : Setoid α} {a b : α} : s a b ↔ s.r a b := Iff.rfl
grind_pattern t₁ => s a b

but the E-matching pattern from this t₁: [@Setoid.r #3 #2 #1 #0], which is kinda weird, why is it t₁: [@Setoid.r #3 #2 #1 #0], and not t₁: [@Setoid #3 #2 #1 #0]? I think this might be the main cause of the problem.

[Jakub Nowak]

Adding this works though.

@[grind?]
theorem t₂ {α : Type u} {a b : α × α} : Rel.setoid α a b ↔ Rel α a b := Iff.rfl

[Jakub Nowak]

I think I finally understand the issue. grind displays (Rel.setoid α) (x, y) (x, y) and doesn't display (Rel.setoid α).r (x, y) (x, y) because they are exactly the same. The first is delaborated version of the second.

Now, adding

@[grind?]
theorem t₃ {α : Type u} {a b : α × α} : (Rel.setoid α).r a b ↔ Rel α a b := Iff.rfl

makes grind [Quotient.eq, Rel] work.

So it seems like the real issue is that grind cannot unfold projection.

[Jakub Nowak]

I made another topic: #lean4 > `grind` should unfold projections.