rw failing to rewrite coercions...but only sometimes

Stream: mathlib4

[Thomas Murrills]

I have the expression ↑1 in a couple places in my tactic state, and it looks the same in each place on mouseover: @Nat.cast α NonAssocRing.toNatCast 1 : α.

They're the same under pp.all true, too:

@Nat.cast.{u_1} α (@NonAssocRing.toNatCast.{u_1} α (@Ring.toNonAssocRing.{u_1} α inst✝))
    (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))

The problem: in one case, rw [Nat.cast_one] successfully rewrites it—in another, it doesn't. Here's a MWE (up to Invertible).

import Mathlib.Algebra.Invertible

structure Foo [Ring α] (a : α) (x : ℕ) where
  inv : Invertible (x : α)
  eq : a = ⅟(x : α)

theorem bar {α} [Ring α] {a : α} : Foo a 1 → Unit
  | ⟨inv, eq⟩ => by rw [Nat.cast_one] at inv -- rewrite works (and leaves unsolved goals)

theorem bar' {α} [Ring α] {a : α} : Foo a 1 → Unit
  | ⟨inv, eq⟩ => by rw [Nat.cast_one] at eq -- rewrite fails

It only seems to happen under ⅟—remove that from the type of eq and the problem disappears.

Does it have something to do with finding the right instances, maybe?

[Eric Wieser]

Does simp_rw succeed?

[Thomas Murrills]

No, unfortunately.

[Thomas Murrills]

I should give some extra info: the actual error is

tactic 'rewrite' failed, motive is not type correct
a: α
eq: a = ⅟↑1
⊢ Unit

and I don't know what that implies in this context...

[Eric Wieser]

Does inv really not appear in the context?

[Thomas Murrills]

inv does appear in the original context, but it fails nonetheless

[Thomas Murrills]

Here's the initial tactic state:

α: Type u_1
inst✝: Ring α
a: α
inv: Invertible ↑1
eq: a = ⅟↑1
⊢ Unit

[Eric Wieser]

The problem is that eq refers to inv

[Eric Wieser]

And you need to rewrite both at once

[Thomas Murrills]

Oh, good catch. Hmmm...how do you actually make that happen?

[Thomas Murrills]

Ideally I'd like to rewrite invto something new and then be able to rewrite it the same way wherever it appears in some other specified hypothesis

[Eric Wieser]

I would guess you want to use docs#Invertible.copy to create a inv'

[Eric Wieser]

It looks like we're missing simps on that definition, as you'd then use the lemma it generates

[Thomas Murrills]

Hmm, inv is the one the rewrite works for—I have no trouble producing Invertible 1 via Nat.cast_one. But how do I use that to rewrite the inv inside eq?

[Thomas Murrills]

What do you mean by the lemma it generates?

[Eric Wieser]

simps not simp. It genertes the lemma Invertible.invOf_copy, if I'm not mistaken

[Kyle Miller]

This can be solved with a congruence lemma

@[congr]
theorem Invertible.cong [Ring α] (x y : α) [Invertible x] (h : x = y) :
  ⅟x = @Invertible.invOf _ _ _ y (by subst h; assumption) :=
by subst h; rfl

theorem bar' {α} [Ring α] {a : α} : Foo a 1 → Unit
  | ⟨inv, eq⟩ => by simp_rw [Nat.cast_one] at eq -- rewrite succeeds

[Kyle Miller]

I'm not sure I wrote this one right

[Eric Wieser]

If by subst h; assumption is of type Invertible _, then you should use Invertible.copy there

[Kyle Miller]

Sure, that would be better. In any case, what this is doing is helping simp by telling it "to do a rewrite for an Inv expression, you can just rewrite its main argument. I'll handle the typeclass instances."

[Eric Wieser]

This didn't work in Lean 3, right?

[Kyle Miller]

Very likely not. It used a more conservative heuristic for what could be a congr lemma

[Kyle Miller]

IIRC, it required all term arguments (even instances) to have corresponding eq arguments, but here you've got Mul and One

[Kyle Miller]

Any idea why keyword arguments don't work here?

@[congr]
theorem Invertible.cong [Ring α] (x y : α) [Invertible x] (h : x = y) :
  ⅟x = Invertible.invOf (self := Invertible.copy ‹_› _ h.symm) y :=
by subst h; rfl

The error is

function expected at
  ⅟y
term has type
  α

[Thomas Murrills]

This is great! Feel free to PR, but I can also just slip this in just under Invertible.copy in the norm_num PR I'm working on if that's more convenient and sounds good to everyone.

[Kyle Miller]

This works:

def f [inst : Ring α] (x : α) := x + x
def f' (x : α) [inst : Ring α] := x + x

#eval f (inst := Int.instRingInt) 3
#eval f' (inst := Int.instRingInt) 3

It seems to have to do with class fields. This is unexpected to me:

class Baz (α : Type) (x : α) where
  y : α

instance bazinst (n : Int) : Baz Int n where
  y := n + 37

#check Baz.y (self := bazinst 5)
-- Baz.y 5 : Int

[Kyle Miller]

It's unexpected since in Baz.y the argument x is explicit