feat: use RArray in simp_arith meta code (#6068 part 1)

This PR prepares #6068 by using the `RArray` data structure in
`simp_arith` the simp-arith meta code.

After the subsequent stage0 we can change the simp-arith theorems in
`Init`.

src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean

@@ -8,6 +8,7 @@ import Lean.Meta.Check
 import Lean.Meta.Offset
 import Lean.Meta.AppBuilder
 import Lean.Meta.KExprMap
+import Lean.Data.RArray
 
 namespace Lean.Meta.Linear.Nat
 
@@ -141,8 +142,11 @@ end ToLinear
 
 export ToLinear (toLinearCnstr? toLinearExpr)
 
-def toContextExpr (ctx : Array Expr) : MetaM Expr := do
-  mkListLit (mkConst ``Nat) ctx.toList
+def toContextExpr (ctx : Array Expr) : Expr :=
+  if h : 0 < ctx.size then
+    RArray.toExpr (mkConst ``Nat) id (RArray.ofArray ctx h)
+  else
+    RArray.toExpr (mkConst ``Nat) id (RArray.leaf (mkNatLit 0))
 
 def reflTrue : Expr :=
   mkApp2 (mkConst ``Eq.refl [levelOne]) (mkConst ``Bool) (mkConst ``Bool.true)

src/Lean/Meta/Tactic/LinearArith/Nat/Simp.lean

@@ -31,17 +31,17 @@ def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
     let c₂ := c₁.norm
     if c₂.isUnsat then
       let r := mkConst ``False
-      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (← toContextExpr ctx) (toExpr c) reflTrue
+      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (toContextExpr ctx) (toExpr c) reflTrue
       return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
     else if c₂.isValid then
       let r := mkConst ``True
-      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr ctx) (toExpr c) reflTrue
+      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (toContextExpr ctx) (toExpr c) reflTrue
       return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
     else
       let c₂ : LinearCnstr := c₂.toExpr
       let r ← c₂.toArith ctx
       if r != lhs then
-        let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
+        let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (toContextExpr ctx) (toExpr c) (toExpr c₂) reflTrue
         return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
       else
         return none
@@ -81,7 +81,7 @@ def simpExpr? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   if p'.length < p.length then
     -- We only return some if monomials were fused
     let e' : LinearExpr := p'.toExpr
-    let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr e) (toExpr e') reflTrue
+    let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (toContextExpr ctx) (toExpr e) (toExpr e') reflTrue
     let r ← e'.toArith ctx
     return some (r, p)
   else