Breaking change in `rw` in Lean 3.11.0

[cipher1024]

Prerequisites

• [ ] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

rw does not find occurrence of LHS of equation unless all the arguments are specified.

Steps to Reproduce

The following code worked in 3.8, 3.9 and 3.10

inductive fin' : ℕ → Type
| raise {n : ℕ} : fin' n → fin' n.succ
| last {n : ℕ} : fin' n.succ

def fin'.elim0 {α} : fin' 0 → α .

universes u

def typevec (n : ℕ) := fin' n → Type*

def arrow {n} (α β : typevec n) := Π i : fin' n, α i → β i

infixl ` ⟹ `:40 := arrow
open nat

def append1 {n} (α : typevec n) (β : Type*) : typevec (n+1)
| (fin'.raise i) := α i
| fin'.last      := β

def repeat : Π (n : ℕ) (t : Sort*), typevec n
| 0 t := fin'.elim0
| (nat.succ i) t := append1 (repeat i t) t

def of_repeat : Π {n i} (x : repeat n Prop i), Prop
| (nat.succ n) (fin'.raise i) x := @of_repeat n i x
| (nat.succ n) fin'.last x := x

namespace typevec

def id {n} {α : typevec n} : α ⟹ α := λ i x, x

def drop {n} (α : typevec (n+1)) : typevec n := λ i, α i.raise

def last {n} (α : typevec (n+1)) : Type* := α fin'.last

end typevec

open typevec

def drop_fun {n} {α β : typevec (n+1)} (f : α ⟹ β) : drop α ⟹ drop β :=
λ i, f i.raise

infixl ` ::: `:67 := append1

def subtype_ : Π {n} {α : typevec.{u} n} (p : α ⟹ repeat n Prop), typevec n
| 0 α p := fin'.elim0
| (succ n) α p := @subtype_ n (drop α) (drop_fun p) ::: _root_.subtype (λ x, p fin'.last x)

def to_subtype : Π {n} {α : typevec.{u} n} (p : α ⟹ repeat n Prop), (λ (i : fin' n), { x // of_repeat $ p i x }) ⟹ subtype_ p
| (succ n) α p (fin'.raise i) x := to_subtype (drop_fun p) i x
| (succ n) α p fin'.last x := x

def of_subtype : Π {n} {α : typevec.{u} n} (p : α ⟹ repeat n Prop),
  subtype_ p ⟹ (λ (i : fin' n), { x // of_repeat $ p i x })
| (succ n) α p (fin'.raise i) x := of_subtype _ i x
| (succ n) α p fin'.last x := x

example {i_n : ℕ}
  (i_a : fin' i_n)
  {α : typevec i_n.succ}
  (p : α ⟹ repeat i_n.succ Prop)
  (x : subtype_ p i_a.raise) :
  to_subtype p i_a.raise (of_subtype p i_a.raise x) = id i_a.raise x :=
begin
  rw [of_subtype,to_subtype],
  admit
end

Expected behavior: [What you expect to happen]

The rewrite should succeed and the proof should be admitted.

Actual behavior: [What actually happens]

The second equation in rw fails.

Reproduces how often: [What percentage of the time does it reproduce?] 100%

Versions

The code fails in the 3.11 release and succeeds in the 3.10 release on Mac OS X 10.15.5

Lean (version 3.10.0, commit 2c578165cc85, Release) Lean (version 3.11.0, commit fb3f3e88be8a, Release)

You can get this information from copy and pasting the output of lean --version, please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[bryangingechen]

Zulip thread

[cipher1024]

Specifically, @digama0 pointed out that redefining of_repeat fixes the problem:

def of_repeat {n i} : repeat n Prop i → Prop :=
begin
  induction i with n i IH,
  { exact IH },
  { exact id }
end