unexpected error on `[norm_cast]`

Stream: new members

[Asei Inoue]

import Mathlib.Tactic

def IntBase := Nat × Nat

def IntBase.equiv : IntBase → IntBase → Prop :=
  fun (a₁, b₁) (a₂, b₂) => a₁ + b₂ = b₁ + a₂

instance : Setoid IntBase where
  r := IntBase.equiv
  iseqv := by
    constructor
    case refl =>
      intro ⟨x, y⟩
      dsimp [IntBase.equiv]
      ac_rfl
    case symm =>
      intro ⟨x, y⟩ ⟨x', y'⟩ h
      dsimp [IntBase.equiv] at *
      omega
    case trans =>
      intro ⟨x, y⟩ ⟨x', y'⟩ ⟨x'', y''⟩ hxy hyz
      dsimp [IntBase.equiv] at *
      omega

/-- my original Int impl -/
def myInt := Quot IntBase.equiv

instance : Coe Nat myInt where
  coe n := ⟦(n, 0)⟧

theorem myInt_eq {x y : Nat} : (x : myInt) = (y : myInt) ↔ x = y := by
  constructor <;> intro h
  · simp [(· ≈ ·), Setoid.r, IntBase.equiv] at h
    exact h
  · rw [h]

-- why this error occurs??
/-
error: norm_cast: badly shaped lemma, lhs must contain at least one coe
  ⟦(x, 0)⟧ = ⟦(y, 0)⟧
-/
attribute [norm_cast] myInt_eq

[Kyle Miller]

You need there to be a function tagged with @[coe].

import Mathlib.Tactic

def IntBase := Nat × Nat

def IntBase.mk (a b : Nat) : IntBase := (a, b)

def IntBase.equiv : IntBase → IntBase → Prop :=
  fun (a₁, b₁) (a₂, b₂) => a₁ + b₂ = b₁ + a₂

instance IntBase.setoid : Setoid IntBase where
  r := IntBase.equiv
  iseqv := by
    constructor
    case refl =>
      intro ⟨x, y⟩
      dsimp [IntBase.equiv]
      ac_rfl
    case symm =>
      intro ⟨x, y⟩ ⟨x', y'⟩ h
      dsimp [IntBase.equiv] at *
      omega
    case trans =>
      intro ⟨x, y⟩ ⟨x', y'⟩ ⟨x'', y''⟩ hxy hyz
      dsimp [IntBase.equiv] at *
      omega

/-- my original Int impl -/
abbrev myInt := Quotient IntBase.setoid

@[coe]
def myInt.ofNat (n : Nat) : myInt := ⟦(n, 0)⟧

instance : Coe Nat myInt where
  coe := myInt.ofNat

theorem myInt_eq {x y : Nat} : (x : myInt) = (y : myInt) ↔ x = y := by
  constructor <;> intro h
  · simp [myInt.ofNat, (· ≈ ·), Setoid.r, IntBase.equiv] at h
    exact h
  · rw [h]

attribute [norm_cast] myInt_eq