feat: add removeUnnecessaryCasts

see #988

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -142,9 +142,30 @@ def getSimpLetCase (n : Name) (t : Expr) (v : Expr) (b : Expr) : MetaM SimpLetCa
     else
       return SimpLetCase.dep
 
+#check Eq.ndrec
+
 /-- Given the application `e`, remove unnecessary casts of the form `Eq.rec a rfl` and `Eq.ndrec a rfl`. -/
-def removeUnnecessaryCasts (e : Expr) : MetaM Expr :=
-  return e -- TODO
+partial def removeUnnecessaryCasts (e : Expr) : MetaM Expr := do
+  let mut args := e.getAppArgs
+  let mut modified := false
+  for i in [:args.size] do
+    let arg := args[i]
+    if isDummyEqRec arg then
+      args := args.set! i (elimDummyEqRec arg)
+      modified := true
+  if modified then
+    return mkAppN e.getAppFn args
+  else
+    return e
+where
+  isDummyEqRec (e : Expr) : Bool :=
+    (e.isAppOfArity ``Eq.rec 6 || e.isAppOfArity ``Eq.ndrec 6) && e.appArg!.isAppOf ``Eq.refl
+
+  elimDummyEqRec (e : Expr) : Expr :=
+    if isDummyEqRec e then
+      elimDummyEqRec e.appFn!.appFn!.appArg!
+    else
+      e
 
 partial def simp (e : Expr) : M Result := withIncRecDepth do
   checkMaxHeartbeats "simp"

tests/lean/arrayGetU.lean

@@ -0,0 +1,17 @@
+def f (a : Array Nat) (i : Nat) (v : Nat) (h : i < a.size) : Array Nat :=
+  a.set ⟨i, h⟩ (a.get ⟨i, h⟩ + v)
+
+set_option pp.proofs true
+
+theorem ex1 (h₃ : i = j) : f a i (0 + v) h₁ = f a j v h₂ := by
+  simp
+  trace_state
+  simp [h₃]
+
+theorem ex2 (h₃ : i = j) : f a (0 + i) (0 + v) h₁ = f a j v h₂ := by
+  simp
+  trace_state
+  simp [h₃]
+
+theorem ex3 (h₃ : i = j) : f a (0 + i) (0 + v) h₁ = f a j v h₂ := by
+  simp [h₃]

tests/lean/arrayGetU.lean.expected.out

@@ -0,0 +1,14 @@
+i j : Nat
+a : Array Nat
+v : Nat
+h₁ : i < Array.size a
+h₂ : j < Array.size a
+h₃ : i = j
+⊢ f a i v h₁ = f a j v h₂
+i j : Nat
+a : Array Nat
+v : Nat
+h₁ : 0 + i < Array.size a
+h₂ : j < Array.size a
+h₃ : i = j
+⊢ f a i v (Nat.zero_add i ▸ h₁) = f a j v h₂