chore: update stage0

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

@@ -9,3 +9,4 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.String

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.ToExpr
-import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
 
 namespace Char
 open Lean Meta Simp
@@ -19,6 +19,18 @@ def fromExpr? (e : Expr) : SimpM (Option Char) := OptionT.run do
   let some c ← fromExpr? e.appArg! | return .continue
   return .done { expr := toExpr (op c) }
 
+@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Char → Char → Bool) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some n ← fromExpr? e.appFn!.appArg! | return .continue
+  let some m ← fromExpr? e.appArg! | return .continue
+  evalPropStep e (op n m)
+
+@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Char → Char → Bool) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some n ← fromExpr? e.appFn!.appArg! | return .continue
+  let some m ← fromExpr? e.appArg! | return .continue
+  return .done { expr := toExpr (op n m) }
+
 builtin_simproc [simp, seval] reduceToLower (Char.toLower _) := reduceUnary ``Char.toLower Char.toLower
 builtin_simproc [simp, seval] reduceToUpper (Char.toUpper _) := reduceUnary ``Char.toUpper Char.toUpper
 builtin_simproc [simp, seval] reduceToNat (Char.toNat _) := reduceUnary ``Char.toNat Char.toNat
@@ -29,6 +41,14 @@ builtin_simproc [simp, seval] reduceIsAlpha (Char.isAlpha _) := reduceUnary ``Ch
 builtin_simproc [simp, seval] reduceIsDigit (Char.isDigit _) := reduceUnary ``Char.isDigit Char.isDigit
 builtin_simproc [simp, seval] reduceIsAlphaNum (Char.isAlphanum _) := reduceUnary ``Char.isAlphanum Char.isAlphanum
 builtin_simproc [simp, seval] reduceToString (toString (_ : Char)) := reduceUnary ``toString toString 3
+builtin_simproc [simp, seval] reduceVal (Char.val _) := fun e => do
+  unless e.isAppOfArity ``Char.val 1 do return .continue
+  let some c ← fromExpr? e.appArg! | return .continue
+  return .done { expr := UInt32.toExprCore c.val }
+builtin_simproc [simp, seval] reduceEq  (( _ : Char) = _)  := reduceBinPred ``Eq 3 (. = .)
+builtin_simproc [simp, seval] reduceNe  (( _ : Char) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
+builtin_simproc [simp, seval] reduceBEq  (( _ : Char) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
+builtin_simproc [simp, seval] reduceBNe  (( _ : Char) != _)  := reduceBoolPred ``bne 4 (. != .)
 
 /--
 Return `.done` for Char values. We don't want to unfold in the symbolic evaluator.
@@ -39,4 +59,13 @@ builtin_simproc ↓ [simp, seval] isValue (Char.ofNat _ ) := fun e => do
   unless (← fromExpr? e).isSome do return .continue
   return .done { expr := e }
 
+builtin_simproc [simp, seval] reduceOfNatAux (Char.ofNatAux _ _) := fun e => do
+  unless e.isAppOfArity ``Char.ofNatAux 2 do return .continue
+  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  return .done { expr := toExpr (Char.ofNat n) }
+
+builtin_simproc [simp, seval] reduceDefault ((default : Char)) := fun e => do
+  unless e.isAppOfArity ``default 2 do return .continue
+  return .done { expr := toExpr (default : Char) }
+
 end Char

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean

@@ -42,6 +42,12 @@ def Value.toExpr (v : Value) : Expr :=
   let some v₂ ← fromExpr? e.appArg! | return .continue
   evalPropStep e (op v₁.value v₂.value)
 
+@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← fromExpr? e.appArg! | return .continue
+  return .done { expr := Lean.toExpr (op v₁.value v₂.value) }
+
 /-
 The following code assumes users did not override the `Fin n` instances for the arithmetic operators.
 If they do, they must disable the following `simprocs`.
@@ -57,6 +63,10 @@ builtin_simproc [simp, seval] reduceLT  (( _ : Fin _) < _)  := reduceBinPred ``L
 builtin_simproc [simp, seval] reduceLE  (( _ : Fin _) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
 builtin_simproc [simp, seval] reduceGT  (( _ : Fin _) > _)  := reduceBinPred ``GT.gt 4 (. > .)
 builtin_simproc [simp, seval] reduceGE  (( _ : Fin _) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+builtin_simproc [simp, seval] reduceEq  (( _ : Fin _) = _)  := reduceBinPred ``Eq 3 (. = .)
+builtin_simproc [simp, seval] reduceNe  (( _ : Fin _) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
+builtin_simproc [simp, seval] reduceBEq  (( _ : Fin _) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
+builtin_simproc [simp, seval] reduceBNe  (( _ : Fin _) != _)  := reduceBoolPred ``bne 4 (. != .)
 
 /-- Return `.done` for Fin values. We don't want to unfold in the symbolic evaluator. -/
 builtin_simproc [seval] isValue ((OfNat.ofNat _ : Fin _)) := fun e => do

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean

@@ -49,6 +49,12 @@ def toExpr (v : Int) : Expr :=
   let some v₂ ← fromExpr? e.appArg! | return .continue
   evalPropStep e (op v₁ v₂)
 
+@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Int → Int → Bool) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some n ← fromExpr? e.appFn!.appArg! | return .continue
+  let some m ← fromExpr? e.appArg! | return .continue
+  return .done { expr := Lean.toExpr (op n m) }
+
 /-
 The following code assumes users did not override the `Int` instances for the arithmetic operators.
 If they do, they must disable the following `simprocs`.
@@ -93,5 +99,9 @@ builtin_simproc [simp, seval] reduceLT  (( _ : Int) < _)  := reduceBinPred ``LT.
 builtin_simproc [simp, seval] reduceLE  (( _ : Int) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
 builtin_simproc [simp, seval] reduceGT  (( _ : Int) > _)  := reduceBinPred ``GT.gt 4 (. > .)
 builtin_simproc [simp, seval] reduceGE  (( _ : Int) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+builtin_simproc [simp, seval] reduceEq  (( _ : Int) = _)  := reduceBinPred ``Eq 3 (. = .)
+builtin_simproc [simp, seval] reduceNe  (( _ : Int) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
+builtin_simproc [simp, seval] reduceBEq  (( _ : Int) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
+builtin_simproc [simp, seval] reduceBNe  (( _ : Int) != _)  := reduceBoolPred ``bne 4 (. != .)
 
 end Int

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

@@ -31,6 +31,12 @@ def fromExpr? (e : Expr) : SimpM (Option Nat) := do
   let some m ← fromExpr? e.appArg! | return .continue
   evalPropStep e (op n m)
 
+@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some n ← fromExpr? e.appFn!.appArg! | return .continue
+  let some m ← fromExpr? e.appArg! | return .continue
+  return .done { expr := toExpr (op n m) }
+
 builtin_simproc [simp, seval] reduceSucc (Nat.succ _) := reduceUnary ``Nat.succ 1 (· + 1)
 
 /-
@@ -50,6 +56,10 @@ builtin_simproc [simp, seval] reduceLT  (( _ : Nat) < _)  := reduceBinPred ``LT.
 builtin_simproc [simp, seval] reduceLE  (( _ : Nat) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
 builtin_simproc [simp, seval] reduceGT  (( _ : Nat) > _)  := reduceBinPred ``GT.gt 4 (. > .)
 builtin_simproc [simp, seval] reduceGE  (( _ : Nat) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+builtin_simproc [simp, seval] reduceEq  (( _ : Nat) = _)  := reduceBinPred ``Eq 3 (. = .)
+builtin_simproc [simp, seval] reduceNe  (( _ : Nat) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
+builtin_simproc [simp, seval] reduceBEq  (( _ : Nat) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
+builtin_simproc [simp, seval] reduceBNe  (( _ : Nat) != _)  := reduceBoolPred ``bne 4 (. != .)
 
 /-- Return `.done` for Nat values. We don't want to unfold in the symbolic evaluator. -/
 builtin_simproc [seval] isValue ((OfNat.ofNat _ : Nat)) := fun e => do

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.ToExpr
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
+
+namespace String
+open Lean Meta Simp
+
+def fromExpr? (e : Expr) : SimpM (Option String) := OptionT.run do
+  let .lit (.strVal s) := e | failure
+  return s
+
+builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : String)) := fun e => do
+  unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue
+  let some a ← fromExpr? e.appFn!.appArg! | return .continue
+  let some b ← fromExpr? e.appArg! | return .continue
+  return .done { expr := toExpr (a ++ b) }
+
+private partial def reduceListChar (e : Expr) (s : String) : SimpM Step := do
+  trace[Meta.debug] "reduceListChar {e}, {s}"
+  if e.isAppOfArity ``List.nil 1 then
+    return .done { expr := toExpr s }
+  else if e.isAppOfArity ``List.cons 3 then
+    let some c ← Char.fromExpr? e.appFn!.appArg! | return .continue
+    reduceListChar e.appArg! (s.push c)
+  else
+    return .continue
+
+builtin_simproc [simp, seval] reduceMk (String.mk _) := fun e => do
+  unless e.isAppOfArity ``String.mk 1 do return .continue
+  reduceListChar e.appArg! ""
+
+end String

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean

@@ -9,7 +9,10 @@ open Lean Meta Simp
 
 macro "declare_uint_simprocs" typeName:ident : command =>
 let ofNat := typeName.getId ++ `ofNat
+let ofNatCore := mkIdent (typeName.getId ++ `ofNatCore)
+let toNat := mkIdent (typeName.getId ++ `toNat)
 let fromExpr := mkIdent `fromExpr
+let toExprCore := mkIdent `toExprCore
 let toExpr := mkIdent `toExpr
 `(
 namespace $typeName
@@ -26,6 +29,10 @@ def $fromExpr (e : Expr) : OptionT SimpM Value := do
   let value := $(mkIdent ofNat) value
   return { value, ofNatFn := e.appFn!.appFn! }
 
+def $toExprCore (v : $typeName) : Expr :=
+  let vExpr := mkRawNatLit v.val
+  mkApp3 (mkConst ``OfNat.ofNat [levelZero]) (mkConst $(quote typeName.getId)) vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
+
 def $toExpr (v : Value) : Expr :=
   let vExpr := mkRawNatLit v.value.val
   mkApp2 v.ofNatFn vExpr (mkApp (mkConst $(quote (typeName.getId ++ `instOfNat))) vExpr)
@@ -43,6 +50,12 @@ def $toExpr (v : Value) : Expr :=
   let some m ← ($fromExpr e.appArg!) | return .continue
   evalPropStep e (op n.value m.value)
 
+@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : $typeName → $typeName → Bool) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
+  let some m ← ($fromExpr e.appArg!) | return .continue
+  return .done { expr := Lean.toExpr (op n.value m.value) }
+
 builtin_simproc [simp, seval] $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·)
 builtin_simproc [simp, seval] $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)
 builtin_simproc [simp, seval] $(mkIdent `reduceSub):ident ((_ - _ : $typeName)) := reduceBin ``HSub.hSub 6 (· - ·)
@@ -53,6 +66,23 @@ builtin_simproc [simp, seval] $(mkIdent `reduceLT):ident  (( _ : $typeName) < _)
 builtin_simproc [simp, seval] $(mkIdent `reduceLE):ident  (( _ : $typeName) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
 builtin_simproc [simp, seval] $(mkIdent `reduceGT):ident  (( _ : $typeName) > _)  := reduceBinPred ``GT.gt 4 (. > .)
 builtin_simproc [simp, seval] $(mkIdent `reduceGE):ident  (( _ : $typeName) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+builtin_simproc [simp, seval] reduceEq  (( _ : $typeName) = _)  := reduceBinPred ``Eq 3 (. = .)
+builtin_simproc [simp, seval] reduceNe  (( _ : $typeName) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
+builtin_simproc [simp, seval] reduceBEq  (( _ : $typeName) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
+builtin_simproc [simp, seval] reduceBNe  (( _ : $typeName) != _)  := reduceBoolPred ``bne 4 (. != .)
+
+builtin_simproc [simp, seval] $(mkIdent `reduceOfNatCore):ident ($ofNatCore _ _) := fun e => do
+  unless e.isAppOfArity $(quote ofNatCore.getId) 2 do return .continue
+  let some value ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let value := $(mkIdent ofNat) value
+  let eNew := $toExprCore value
+  return .done { expr := eNew }
+
+builtin_simproc [simp, seval] $(mkIdent `reduceToNat):ident ($toNat _) := fun e => do
+  unless e.isAppOfArity $(quote toNat.getId) 1 do return .continue
+  let some v ← ($fromExpr e.appArg!) | return .continue
+  let n := $toNat v.value
+  return .done { expr := mkNatLit n }
 
 /-- Return `.done` for UInt values. We don't want to unfold in the symbolic evaluator. -/
 builtin_simproc [seval] isValue ((OfNat.ofNat _ : $typeName)) := fun e => do