How to turn abbrev into def

Stream: new members

[Moritz R]

If in the following i replace abbrev by def the rule Sym2.eq doesn't apply any more
(leaving constructors s( , )), although it looks to me, as if the types exactly check out? rw works

import Mathlib.Data.Sym.Sym2

abbrev Atom := Sym2 (Nat)

def Atom.subst: Atom → Atom :=
  Quot.lift (fun ts ↦ s(ts.fst, ts.snd)) (by
    simp only [Sym2.rel_iff', Sym2.eq, Prod.mk.injEq, Prod.swap_prod_mk, Prod.forall] --generated by simp_all
    grind
  )

[Robin Arnez]

simp only looks through abbrevs and not defs so when it finds an (a : Atom) = b (@Eq Atom a b) it doesn't match (_ : Sym2 _) = _ (@Eq (Sym2 _) _ _) and doesn't try to apply the Sym2.eq theorem (which matches on the type to be Sym2 _).

[Moritz R]

Yes, but the hover info in the infoview on the s( , ) shows me that it's seen as a Sym2.mk, so it should apply?

[Moritz R]

image.png

[Robin Arnez]

Well, if you hover over the equality though you'll see:

@Eq Atom s(a, b) s(a_1, b_1) : Prop

so the type Atom doesn't match Sym2 _ which simp expects.

[Moritz R]

uffff

[Moritz R]

thank you!

[Moritz R]

But i still don't get, how do i need to formulate my replacement lemma?
This doesn't work.

@[simp]
lemma bb : ((Sym2.mk p) : Atom) = ((Sym2.mk p') : Atom) ↔ Sym2.Rel _ p p' := by
  simp

[Robin Arnez]

In general, don't use operations through a def, that's called defeq abuse and it will give you a ton of trouble. There are two options to solve this though:

1. one-field structure: instead of using def, wrap the type in a structure with one field:

import Mathlib.Data.Sym.Sym2

structure Atom where
  toSym2 : Sym2 Nat

def Atom.subst (a : Atom) : Atom :=
  Quot.lift (fun ts ↦ ⟨s(ts.fst, ts.snd)⟩) (by simp) a.toSym2

2. add API: write two functions to convert between both types:

import Mathlib.Data.Sym.Sym2

def Atom := Sym2 Nat
def Atom.ofSym2 : Sym2 Nat ≃ Atom := Equiv.refl _
abbrev Atom.toSym2 : Atom ≃ Sym2 Nat := Atom.ofSym2.symm

def Atom.subst (a : Atom) : Atom :=
  Quot.lift (fun ts ↦ .ofSym2 s(ts.fst, ts.snd)) (by simp) a.toSym2