chore: fix test

GE.ge and GT.gt are reducible

src/Init/Grind/Util.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Classical
-
 public section
-
 namespace Lean.Grind
 
 /-- A helper gadget for annotating nested proofs in goals. -/

src/Init/Sym/Lemmas.lean

@@ -14,6 +14,8 @@ public section
 namespace Lean.Sym
 
 theorem ne_self (a : α) : (a ≠ a) = False := by simp
+theorem not_true_eq : (¬ True) = False := by simp
+theorem not_false_eq : (¬ False) = True := by simp
 
 theorem ite_cond_congr {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α)
     (c' : Prop) {inst' : Decidable c'} (h : c = c') : @ite α c inst a b = @ite α c' inst' a b := by
@@ -46,6 +48,8 @@ theorem UInt32.lt_eq_true (a b : UInt32) (h : decide (a < b) = true) : (a < b) =
 theorem UInt64.lt_eq_true (a b : UInt64) (h : decide (a < b) = true) : (a < b) = True := by simp_all
 theorem Fin.lt_eq_true (a b : Fin n) (h : decide (a < b) = true) : (a < b) = True := by simp_all
 theorem BitVec.lt_eq_true (a b : BitVec n) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem String.lt_eq_true (a b : String) (h : decide (a < b) = true) : (a < b) = True := by simp_all
+theorem Char.lt_eq_true (a b : Char) (h : decide (a < b) = true) : (a < b) = True := by simp_all
 
 theorem Nat.lt_eq_false (a b : Nat) (h : decide (a < b) = false) : (a < b) = False := by simp_all
 theorem Int.lt_eq_false (a b : Int) (h : decide (a < b) = false) : (a < b) = False := by simp_all
@@ -60,6 +64,8 @@ theorem UInt32.lt_eq_false (a b : UInt32) (h : decide (a < b) = false) : (a < b)
 theorem UInt64.lt_eq_false (a b : UInt64) (h : decide (a < b) = false) : (a < b) = False := by simp_all
 theorem Fin.lt_eq_false (a b : Fin n) (h : decide (a < b) = false) : (a < b) = False := by simp_all
 theorem BitVec.lt_eq_false (a b : BitVec n) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem String.lt_eq_false (a b : String) (h : decide (a < b) = false) : (a < b) = False := by simp_all
+theorem Char.lt_eq_false (a b : Char) (h : decide (a < b) = false) : (a < b) = False := by simp_all
 
 theorem Nat.le_eq_true (a b : Nat) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
 theorem Int.le_eq_true (a b : Int) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
@@ -74,6 +80,8 @@ theorem UInt32.le_eq_true (a b : UInt32) (h : decide (a ≤ b) = true) : (a ≤
 theorem UInt64.le_eq_true (a b : UInt64) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
 theorem Fin.le_eq_true (a b : Fin n) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
 theorem BitVec.le_eq_true (a b : BitVec n) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem String.le_eq_true (a b : String) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
+theorem Char.le_eq_true (a b : Char) (h : decide (a ≤ b) = true) : (a ≤ b) = True := by simp_all
 
 theorem Nat.le_eq_false (a b : Nat) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
 theorem Int.le_eq_false (a b : Int) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
@@ -88,62 +96,8 @@ theorem UInt32.le_eq_false (a b : UInt32) (h : decide (a ≤ b) = false) : (a
 theorem UInt64.le_eq_false (a b : UInt64) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
 theorem Fin.le_eq_false (a b : Fin n) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
 theorem BitVec.le_eq_false (a b : BitVec n) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
-
-theorem Nat.gt_eq_true (a b : Nat) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Int.gt_eq_true (a b : Int) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Rat.gt_eq_true (a b : Rat) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Int8.gt_eq_true (a b : Int8) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Int16.gt_eq_true (a b : Int16) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Int32.gt_eq_true (a b : Int32) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Int64.gt_eq_true (a b : Int64) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem UInt8.gt_eq_true (a b : UInt8) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem UInt16.gt_eq_true (a b : UInt16) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem UInt32.gt_eq_true (a b : UInt32) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem UInt64.gt_eq_true (a b : UInt64) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem Fin.gt_eq_true (a b : Fin n) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-theorem BitVec.gt_eq_true (a b : BitVec n) (h : decide (a > b) = true) : (a > b) = True := by simp_all
-
-theorem Nat.gt_eq_false (a b : Nat) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Int.gt_eq_false (a b : Int) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Rat.gt_eq_false (a b : Rat) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Int8.gt_eq_false (a b : Int8) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Int16.gt_eq_false (a b : Int16) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Int32.gt_eq_false (a b : Int32) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Int64.gt_eq_false (a b : Int64) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem UInt8.gt_eq_false (a b : UInt8) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem UInt16.gt_eq_false (a b : UInt16) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem UInt32.gt_eq_false (a b : UInt32) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem UInt64.gt_eq_false (a b : UInt64) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem Fin.gt_eq_false (a b : Fin n) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-theorem BitVec.gt_eq_false (a b : BitVec n) (h : decide (a > b) = false) : (a > b) = False := by simp_all
-
-theorem Nat.ge_eq_true (a b : Nat) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Int.ge_eq_true (a b : Int) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Rat.ge_eq_true (a b : Rat) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Int8.ge_eq_true (a b : Int8) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Int16.ge_eq_true (a b : Int16) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Int32.ge_eq_true (a b : Int32) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Int64.ge_eq_true (a b : Int64) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem UInt8.ge_eq_true (a b : UInt8) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem UInt16.ge_eq_true (a b : UInt16) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem UInt32.ge_eq_true (a b : UInt32) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem UInt64.ge_eq_true (a b : UInt64) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem Fin.ge_eq_true (a b : Fin n) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-theorem BitVec.ge_eq_true (a b : BitVec n) (h : decide (a ≥ b) = true) : (a ≥ b) = True := by simp_all
-
-theorem Nat.ge_eq_false (a b : Nat) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Int.ge_eq_false (a b : Int) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Rat.ge_eq_false (a b : Rat) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Int8.ge_eq_false (a b : Int8) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Int16.ge_eq_false (a b : Int16) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Int32.ge_eq_false (a b : Int32) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Int64.ge_eq_false (a b : Int64) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem UInt8.ge_eq_false (a b : UInt8) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem UInt16.ge_eq_false (a b : UInt16) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem UInt32.ge_eq_false (a b : UInt32) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem UInt64.ge_eq_false (a b : UInt64) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem Fin.ge_eq_false (a b : Fin n) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
-theorem BitVec.ge_eq_false (a b : BitVec n) (h : decide (a ≥ b) = false) : (a ≥ b) = False := by simp_all
+theorem String.le_eq_false (a b : String) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
+theorem Char.le_eq_false (a b : Char) (h : decide (a ≤ b) = false) : (a ≤ b) = False := by simp_all
 
 theorem Nat.eq_eq_true (a b : Nat) (h : decide (a = b) = true) : (a = b) = True := by simp_all
 theorem Int.eq_eq_true (a b : Int) (h : decide (a = b) = true) : (a = b) = True := by simp_all
@@ -158,6 +112,8 @@ theorem UInt32.eq_eq_true (a b : UInt32) (h : decide (a = b) = true) : (a = b) =
 theorem UInt64.eq_eq_true (a b : UInt64) (h : decide (a = b) = true) : (a = b) = True := by simp_all
 theorem Fin.eq_eq_true (a b : Fin n) (h : decide (a = b) = true) : (a = b) = True := by simp_all
 theorem BitVec.eq_eq_true (a b : BitVec n) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem String.eq_eq_true (a b : String) (h : decide (a = b) = true) : (a = b) = True := by simp_all
+theorem Char.eq_eq_true (a b : Char) (h : decide (a = b) = true) : (a = b) = True := by simp_all
 
 theorem Nat.eq_eq_false (a b : Nat) (h : decide (a = b) = false) : (a = b) = False := by simp_all
 theorem Int.eq_eq_false (a b : Int) (h : decide (a = b) = false) : (a = b) = False := by simp_all
@@ -172,34 +128,8 @@ theorem UInt32.eq_eq_false (a b : UInt32) (h : decide (a = b) = false) : (a = b)
 theorem UInt64.eq_eq_false (a b : UInt64) (h : decide (a = b) = false) : (a = b) = False := by simp_all
 theorem Fin.eq_eq_false (a b : Fin n) (h : decide (a = b) = false) : (a = b) = False := by simp_all
 theorem BitVec.eq_eq_false (a b : BitVec n) (h : decide (a = b) = false) : (a = b) = False := by simp_all
-
-theorem Nat.ne_eq_true (a b : Nat) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Int.ne_eq_true (a b : Int) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Rat.ne_eq_true (a b : Rat) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Int8.ne_eq_true (a b : Int8) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Int16.ne_eq_true (a b : Int16) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Int32.ne_eq_true (a b : Int32) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Int64.ne_eq_true (a b : Int64) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem UInt8.ne_eq_true (a b : UInt8) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem UInt16.ne_eq_true (a b : UInt16) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem UInt32.ne_eq_true (a b : UInt32) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem UInt64.ne_eq_true (a b : UInt64) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem Fin.ne_eq_true (a b : Fin n) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-theorem BitVec.ne_eq_true (a b : BitVec n) (h : decide (a ≠ b) = true) : (a ≠ b) = True := by simp_all
-
-theorem Nat.ne_eq_false (a b : Nat) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Int.ne_eq_false (a b : Int) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Rat.ne_eq_false (a b : Rat) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Int8.ne_eq_false (a b : Int8) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Int16.ne_eq_false (a b : Int16) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Int32.ne_eq_false (a b : Int32) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Int64.ne_eq_false (a b : Int64) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem UInt8.ne_eq_false (a b : UInt8) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem UInt16.ne_eq_false (a b : UInt16) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem UInt32.ne_eq_false (a b : UInt32) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem UInt64.ne_eq_false (a b : UInt64) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem Fin.ne_eq_false (a b : Fin n) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
-theorem BitVec.ne_eq_false (a b : BitVec n) (h : decide (a ≠ b) = false) : (a ≠ b) = False := by simp_all
+theorem String.eq_eq_false (a b : String) (h : decide (a = b) = false) : (a = b) = False := by simp_all
+theorem Char.eq_eq_false (a b : Char) (h : decide (a = b) = false) : (a = b) = False := by simp_all
 
 theorem Nat.dvd_eq_true (a b : Nat) (h : decide (a ∣ b) = true) : (a ∣ b) = True := by simp_all
 theorem Int.dvd_eq_true (a b : Int) (h : decide (a ∣ b) = true) : (a ∣ b) = True := by simp_all

src/Lean/Meta/Sym/LitValues.lean

@@ -73,4 +73,14 @@ def getFinValue? (e : Expr) : OptionT Id FinValue := do
   let : NeZero n := ⟨h⟩
   return { n, val := Fin.ofNat n v }
 
+def getCharValue? (e : Expr) : OptionT Id Char := do
+  let_expr Char.ofNat n := e | failure
+  let .lit (.natVal n) := n | failure
+  return Char.ofNat n
+
+def getStringValue? (e : Expr) : Option String :=
+  match e with
+  | .lit (.strVal s) => some s
+  | _ => none
+
 end Lean.Meta.Sym

src/Lean/Meta/Sym/ProofInstInfo.lean

@@ -7,14 +7,15 @@ module
 prelude
 public import Lean.Meta.Sym.SymM
 import Lean.Meta.Sym.IsClass
-import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Sym.Util
+import Lean.Meta.Transform
 namespace Lean.Meta.Sym
 
 /--
 Preprocesses types that used for pattern matching and unification.
 -/
 public def preprocessType (type : Expr) : MetaM Expr := do
-  let type ← Grind.unfoldReducible type
+  let type ← Sym.unfoldReducible type
   let type ← Core.betaReduce type
   zetaReduce type
 

src/Lean/Meta/Sym/Simp/EvalGround.lean

@@ -9,6 +9,7 @@ public import Lean.Meta.Sym.Simp.SimpM
 import Init.Sym.Lemmas
 import Init.Data.Int.Gcd
 import Lean.Meta.Sym.LitValues
+import Lean.Meta.Sym.AlphaShareBuilder
 namespace Lean.Meta.Sym.Simp
 
 /-!
@@ -392,6 +393,8 @@ def evalLT (α : Expr) (a b : Expr) : SimpM Result :=
   | UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.lt_eq_true) (mkConst ``UInt64.lt_eq_false) (. < .) a b
   | Fin n => evalFinPred n (mkConst ``Fin.lt_eq_true) (mkConst ``Fin.lt_eq_false) (. < .) a b
   | BitVec n => evalBitVecPred n (mkConst ``BitVec.lt_eq_true) (mkConst ``BitVec.lt_eq_false) (. < .) a b
+  | String => evalBinPred getStringValue? (mkConst ``String.lt_eq_true) (mkConst ``String.lt_eq_false) (. < .) a b
+  | Char => evalBinPred getCharValue? (mkConst ``Char.lt_eq_true) (mkConst ``Char.lt_eq_false) (. < .) a b
   | _ => return .rfl
 
 def evalLE (α : Expr) (a b : Expr) : SimpM Result :=
@@ -409,40 +412,8 @@ def evalLE (α : Expr) (a b : Expr) : SimpM Result :=
   | UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.le_eq_true) (mkConst ``UInt64.le_eq_false) (. ≤ .) a b
   | Fin n => evalFinPred n (mkConst ``Fin.le_eq_true) (mkConst ``Fin.le_eq_false) (. ≤ .) a b
   | BitVec n => evalBitVecPred n (mkConst ``BitVec.le_eq_true) (mkConst ``BitVec.le_eq_false) (. ≤ .) a b
-  | _ => return .rfl
-
-def evalGT (α : Expr) (a b : Expr) : SimpM Result :=
-  match_expr α with
-  | Nat => evalBinPred getNatValue? (mkConst ``Nat.gt_eq_true) (mkConst ``Nat.gt_eq_false) (. > .) a b
-  | Int => evalBinPred getIntValue? (mkConst ``Int.gt_eq_true) (mkConst ``Int.gt_eq_false) (. > .) a b
-  | Rat => evalBinPred getRatValue? (mkConst ``Rat.gt_eq_true) (mkConst ``Rat.gt_eq_false) (. > .) a b
-  | Int8 => evalBinPred getInt8Value? (mkConst ``Int8.gt_eq_true) (mkConst ``Int8.gt_eq_false) (. > .) a b
-  | Int16 => evalBinPred getInt16Value? (mkConst ``Int16.gt_eq_true) (mkConst ``Int16.gt_eq_false) (. > .) a b
-  | Int32 => evalBinPred getInt32Value? (mkConst ``Int32.gt_eq_true) (mkConst ``Int32.gt_eq_false) (. > .) a b
-  | Int64 => evalBinPred getInt64Value? (mkConst ``Int64.gt_eq_true) (mkConst ``Int64.gt_eq_false) (. > .) a b
-  | UInt8 => evalBinPred getUInt8Value? (mkConst ``UInt8.gt_eq_true) (mkConst ``UInt8.gt_eq_false) (. > .) a b
-  | UInt16 => evalBinPred getUInt16Value? (mkConst ``UInt16.gt_eq_true) (mkConst ``UInt16.gt_eq_false) (. > .) a b
-  | UInt32 => evalBinPred getUInt32Value? (mkConst ``UInt32.gt_eq_true) (mkConst ``UInt32.gt_eq_false) (. > .) a b
-  | UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.gt_eq_true) (mkConst ``UInt64.gt_eq_false) (. > .) a b
-  | Fin n => evalFinPred n (mkConst ``Fin.gt_eq_true) (mkConst ``Fin.gt_eq_false) (. > .) a b
-  | BitVec n => evalBitVecPred n (mkConst ``BitVec.gt_eq_true) (mkConst ``BitVec.gt_eq_false) (. > .) a b
-  | _ => return .rfl
-
-def evalGE (α : Expr) (a b : Expr) : SimpM Result :=
-  match_expr α with
-  | Nat => evalBinPred getNatValue? (mkConst ``Nat.ge_eq_true) (mkConst ``Nat.ge_eq_false) (. ≥ .) a b
-  | Int => evalBinPred getIntValue? (mkConst ``Int.ge_eq_true) (mkConst ``Int.ge_eq_false) (. ≥ .) a b
-  | Rat => evalBinPred getRatValue? (mkConst ``Rat.ge_eq_true) (mkConst ``Rat.ge_eq_false) (. ≥ .) a b
-  | Int8 => evalBinPred getInt8Value? (mkConst ``Int8.ge_eq_true) (mkConst ``Int8.ge_eq_false) (. ≥ .) a b
-  | Int16 => evalBinPred getInt16Value? (mkConst ``Int16.ge_eq_true) (mkConst ``Int16.ge_eq_false) (. ≥ .) a b
-  | Int32 => evalBinPred getInt32Value? (mkConst ``Int32.ge_eq_true) (mkConst ``Int32.ge_eq_false) (. ≥ .) a b
-  | Int64 => evalBinPred getInt64Value? (mkConst ``Int64.ge_eq_true) (mkConst ``Int64.ge_eq_false) (. ≥ .) a b
-  | UInt8 => evalBinPred getUInt8Value? (mkConst ``UInt8.ge_eq_true) (mkConst ``UInt8.ge_eq_false) (. ≥ .) a b
-  | UInt16 => evalBinPred getUInt16Value? (mkConst ``UInt16.ge_eq_true) (mkConst ``UInt16.ge_eq_false) (. ≥ .) a b
-  | UInt32 => evalBinPred getUInt32Value? (mkConst ``UInt32.ge_eq_true) (mkConst ``UInt32.ge_eq_false) (. ≥ .) a b
-  | UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.ge_eq_true) (mkConst ``UInt64.ge_eq_false) (. ≥ .) a b
-  | Fin n => evalFinPred n (mkConst ``Fin.ge_eq_true) (mkConst ``Fin.ge_eq_false) (. ≥ .) a b
-  | BitVec n => evalBitVecPred n (mkConst ``BitVec.ge_eq_true) (mkConst ``BitVec.ge_eq_false) (. ≥ .) a b
+  | String => evalBinPred getStringValue? (mkConst ``String.le_eq_true) (mkConst ``String.le_eq_false) (. ≤ .) a b
+  | Char => evalBinPred getCharValue? (mkConst ``Char.le_eq_true) (mkConst ``Char.le_eq_false) (. ≤ .) a b
   | _ => return .rfl
 
 def evalEq (α : Expr) (a b : Expr) : SimpM Result :=
@@ -464,27 +435,8 @@ def evalEq (α : Expr) (a b : Expr) : SimpM Result :=
   | UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.eq_eq_true) (mkConst ``UInt64.eq_eq_false) (. = .) a b
   | Fin n => evalFinPred n (mkConst ``Fin.eq_eq_true) (mkConst ``Fin.eq_eq_false) (. = .) a b
   | BitVec n => evalBitVecPred n (mkConst ``BitVec.eq_eq_true) (mkConst ``BitVec.eq_eq_false) (. = .) a b
-  | _ => return .rfl
-
-def evalNe (α : Expr) (a b : Expr) : SimpM Result :=
-  if isSameExpr a b then do
-    let e ← share <| mkConst ``False
-    let u ← getLevel α
-    return .step e (mkApp2 (mkConst ``ne_self [u]) α a) (done := true)
-  else match_expr α with
-  | Nat => evalBinPred getNatValue? (mkConst ``Nat.ne_eq_true) (mkConst ``Nat.ne_eq_false) (. ≠ .) a b
-  | Int => evalBinPred getIntValue? (mkConst ``Int.ne_eq_true) (mkConst ``Int.ne_eq_false) (. ≠ .) a b
-  | Rat => evalBinPred getRatValue? (mkConst ``Rat.ne_eq_true) (mkConst ``Rat.ne_eq_false) (. ≠ .) a b
-  | Int8 => evalBinPred getInt8Value? (mkConst ``Int8.ne_eq_true) (mkConst ``Int8.ne_eq_false) (. ≠ .) a b
-  | Int16 => evalBinPred getInt16Value? (mkConst ``Int16.ne_eq_true) (mkConst ``Int16.ne_eq_false) (. ≠ .) a b
-  | Int32 => evalBinPred getInt32Value? (mkConst ``Int32.ne_eq_true) (mkConst ``Int32.ne_eq_false) (. ≠ .) a b
-  | Int64 => evalBinPred getInt64Value? (mkConst ``Int64.ne_eq_true) (mkConst ``Int64.ne_eq_false) (. ≠ .) a b
-  | UInt8 => evalBinPred getUInt8Value? (mkConst ``UInt8.ne_eq_true) (mkConst ``UInt8.ne_eq_false) (. ≠ .) a b
-  | UInt16 => evalBinPred getUInt16Value? (mkConst ``UInt16.ne_eq_true) (mkConst ``UInt16.ne_eq_false) (. ≠ .) a b
-  | UInt32 => evalBinPred getUInt32Value? (mkConst ``UInt32.ne_eq_true) (mkConst ``UInt32.ne_eq_false) (. ≠ .) a b
-  | UInt64 => evalBinPred getUInt64Value? (mkConst ``UInt64.ne_eq_true) (mkConst ``UInt64.ne_eq_false) (. ≠ .) a b
-  | Fin n => evalFinPred n (mkConst ``Fin.ne_eq_true) (mkConst ``Fin.ne_eq_false) (. ≠ .) a b
-  | BitVec n => evalBitVecPred n (mkConst ``BitVec.ne_eq_true) (mkConst ``BitVec.ne_eq_false) (. ≠ .) a b
+  | Char => evalBinPred getCharValue? (mkConst ``Char.eq_eq_true) (mkConst ``Char.eq_eq_false) (. = .) a b
+  | String => evalBinPred getStringValue? (mkConst ``String.eq_eq_true) (mkConst ``String.eq_eq_false) (. = .) a b
   | _ => return .rfl
 
 def evalDvd (α : Expr) (a b : Expr) : SimpM Result :=
@@ -554,6 +506,16 @@ macro "declare_eval_bin_bool_pred" id:ident op:term : command =>
 declare_eval_bin_bool_pred evalBEq (· == ·)
 declare_eval_bin_bool_pred evalBNe (· != ·)
 
+open Internal in
+def evalNot (a : Expr) : SimpM Result :=
+  /-
+  **Note**: We added `evalNot` because some abbreviations expanded into `Not`s.
+  -/
+  match_expr a with
+  | True => return .step (← mkConstS ``False) (mkConst ``Sym.not_true_eq) (done := true)
+  | False => return .step (← mkConstS ``True) (mkConst ``Sym.not_false_eq) (done := true)
+  | _ => return .rfl
+
 public structure EvalStepConfig where
   maxExponent := 255
 
@@ -594,14 +556,12 @@ public def evalGround (config : EvalStepConfig := {}) : Simproc := fun e =>
   | Int.fmod a b => evalBinInt Int.fmod a b
   | Int.bmod a b => evalIntBMod a b
   | LE.le α _ a b => evalLE α a b
-  | GE.ge α _ a b => evalGE α a b
   | LT.lt α _ a b => evalLT α a b
-  | GT.gt α _ a b => evalGT α a b
   | Dvd.dvd α _ a b => evalDvd α a b
   | Eq α a b => evalEq α a b
-  | Ne α a b => evalNe α a b
   | BEq.beq α _ a b => evalBEq α a b
   | bne α _ a b => evalBNe α a b
+  | Not a => evalNot a
   | _  => return .rfl
 
 end Lean.Meta.Sym.Simp

src/Lean/Meta/Sym/Util.lean

@@ -6,13 +6,55 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Sym.SymM
+public import Lean.Meta.Transform
+import Init.Grind.Util
+import Lean.Meta.WHNF
 namespace Lean.Meta.Sym
-open Grind
+
+/--
+Returns `true` if `declName` is the name of a grind helper declaration that
+should not be unfolded by `unfoldReducible`.
+-/
+def isGrindGadget (declName : Name) : Bool :=
+  declName == ``Grind.EqMatch
+
+/--
+Auxiliary function for implementing `unfoldReducible` and `unfoldReducibleSimproc`.
+Performs a single step.
+-/
+public def unfoldReducibleStep (e : Expr) : MetaM TransformStep := do
+  let .const declName _ := e.getAppFn | return .continue
+  unless (← isReducible declName) do return .continue
+  if isGrindGadget declName then return .continue
+  -- See comment at isUnfoldReducibleTarget.
+  if (← getEnv).isProjectionFn declName then return .continue
+  let some v ← unfoldDefinition? e | return .continue
+  return .visit v
+
+def isUnfoldReducibleTarget (e : Expr) : CoreM Bool := do
+  let env ← getEnv
+  return Option.isSome <| e.find? fun e => Id.run do
+    let .const declName _ := e | return false
+    if getReducibilityStatusCore env declName matches .reducible then
+      -- Remark: it is wasteful to unfold projection functions since
+      -- kernel projections are folded again in the `foldProjs` preprocessing step.
+      return !isGrindGadget declName && !env.isProjectionFn declName
+    else
+      return false
+
+/--
+Unfolds all `reducible` declarations occurring in `e`.
+This is meant as a preprocessing step. It does **not** guarantee maximally shared terms
+-/
+public def unfoldReducible (e : Expr) : MetaM Expr := do
+  if !(← isUnfoldReducibleTarget e) then return e
+  Meta.transform e (pre := unfoldReducibleStep)
+
 /--
 Instantiates metavariables, unfold reducible, and applies `shareCommon`.
 -/
 def preprocessExpr (e : Expr) : SymM Expr := do
-  shareCommon (← instantiateMVars e)
+  shareCommon (← unfoldReducible (← instantiateMVars e))
 
 /--
 Helper function that removes gaps, instantiate metavariables, and applies `shareCommon`.

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -11,6 +11,7 @@ import Lean.Util.ForEachExpr
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Match.Basic
 import Lean.Meta.Tactic.TryThis
+import Lean.Meta.Sym.Util
 public section
 namespace Lean.Meta.Grind
 /-!
@@ -281,7 +282,7 @@ private theorem normConfig_zetaDelta : normConfig.zetaDelta = true := rfl
 
 def preprocessPattern (pat : Expr) (normalizePattern := true) : MetaM Expr := do
   let pat ← instantiateMVars pat
-  let pat ← unfoldReducible pat
+  let pat ← Sym.unfoldReducible pat
   let pat ← if normalizePattern then normalize pat normConfig else pure pat
   let pat ← detectOffsets pat
   let pat ← foldProjs pat

src/Lean/Meta/Tactic/Grind/MarkNestedSubsingletons.lean

@@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Grind.Types
 import Init.Grind.Util
 import Lean.Meta.Sym.ExprPtr
+import Lean.Meta.Sym.Util
 import Lean.Meta.Tactic.Grind.Util
 public section
 namespace Lean.Meta.Grind
@@ -103,7 +104,7 @@ where
     -/
     /- We must also apply beta-reduction to improve the effectiveness of the congruence closure procedure. -/
     let e ← Core.betaReduce e
-    let e ← unfoldReducible e
+    let e ← Sym.unfoldReducible e
     /- We must mask proofs occurring in `prop` too. -/
     let e ← visit e
     let e ← eraseIrrelevantMData e

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

@@ -11,6 +11,7 @@ public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Util
 import Lean.Meta.Tactic.Grind.MatchDiscrOnly
 import Lean.Meta.Tactic.Grind.MarkNestedSubsingletons
+import Lean.Meta.Sym.Util
 public section
 namespace Lean.Meta.Grind
 
@@ -57,7 +58,7 @@ def preprocessImpl (e : Expr) : GoalM Simp.Result := do
   let e' ← instantiateMVars r.expr
   -- Remark: `simpCore` unfolds reducible constants, but it does not consistently visit all possible subterms.
   -- So, we must use the following `unfoldReducible` step. It is non-op in most cases
-  let e' ← unfoldReducible e'
+  let e' ← Sym.unfoldReducible e'
   let e' ← abstractNestedProofs e'
   let e' ← markNestedSubsingletons e'
   let e' ← eraseIrrelevantMData e'
@@ -97,6 +98,6 @@ but ensures assumptions made by `grind` are satisfied.
 -/
 def preprocessLight (e : Expr) : GoalM Expr := do
   let e ← instantiateMVars e
-  shareCommon (← canon (← normalizeLevels (← foldProjs (← eraseIrrelevantMData (← markNestedSubsingletons (← unfoldReducible e))))))
+  shareCommon (← canon (← normalizeLevels (← foldProjs (← eraseIrrelevantMData (← markNestedSubsingletons (← Sym.unfoldReducible e))))))
 
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/SimpUtil.lean

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Grind.Arith.Simproc
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core
 import Lean.Meta.Tactic.Grind.Util
+import Lean.Meta.Sym.Util
 import Init.Grind.Norm
 public section
 namespace Lean.Meta.Grind
@@ -136,7 +137,7 @@ builtin_simproc_decl reduceCtorEqCheap (_ = _) := fun e => do
     return .done { expr := mkConst ``False, proof? := (← withDefault <| mkEqFalse' (← mkLambdaFVars #[h] (← mkNoConfusion (mkConst ``False) h))) }
 
 builtin_dsimproc_decl unfoldReducibleSimproc (_) := fun e => do
-  unfoldReducibleStep e
+  Sym.unfoldReducibleStep e
 
 /-- Returns the array of simprocs used by `grind`. -/
 protected def getSimprocs : MetaM (Array Simprocs) := do

src/Lean/Meta/Tactic/Grind/Util.lean

@@ -11,6 +11,7 @@ import Lean.ProjFns
 import Lean.Meta.WHNF
 import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.Tactic.Clear
+import Lean.Meta.Sym.Util
 public section
 namespace Lean.Meta.Grind
 /--
@@ -55,49 +56,11 @@ def _root_.Lean.MVarId.transformTarget (mvarId : MVarId) (f : Expr → MetaM Exp
   mvarId.assign mvarNew
   return mvarNew.mvarId!
 
-/--
-Returns `true` if `declName` is the name of a grind helper declaration that
-should not be unfolded by `unfoldReducible`.
--/
-def isGrindGadget (declName : Name) : Bool :=
-  declName == ``Grind.EqMatch
-
-def isUnfoldReducibleTarget (e : Expr) : CoreM Bool := do
-  let env ← getEnv
-  return Option.isSome <| e.find? fun e => Id.run do
-    let .const declName _ := e | return false
-    if getReducibilityStatusCore env declName matches .reducible then
-      -- Remark: it is wasteful to unfold projection functions since
-      -- kernel projections are folded again in the `foldProjs` preprocessing step.
-      return !isGrindGadget declName && !env.isProjectionFn declName
-    else
-      return false
-
-/--
-Auxiliary function for implementing `unfoldReducible` and `unfoldReducibleSimproc`.
-Performs a single step.
--/
-def unfoldReducibleStep (e : Expr) : MetaM TransformStep := do
-  let .const declName _ := e.getAppFn | return .continue
-  unless (← isReducible declName) do return .continue
-  if isGrindGadget declName then return .continue
-  -- See comment at isUnfoldReducibleTarget.
-  if (← getEnv).isProjectionFn declName then return .continue
-  let some v ← unfoldDefinition? e | return .continue
-  return .visit v
-
-/--
-Unfolds all `reducible` declarations occurring in `e`.
--/
-def unfoldReducible (e : Expr) : MetaM Expr := do
-  if !(← isUnfoldReducibleTarget e) then return e
-  Meta.transform e (pre := unfoldReducibleStep)
-
 /--
 Unfolds all `reducible` declarations occurring in the goal's target.
 -/
 def _root_.Lean.MVarId.unfoldReducible (mvarId : MVarId) : MetaM MVarId :=
-  mvarId.transformTarget Grind.unfoldReducible
+  mvarId.transformTarget Sym.unfoldReducible
 
 /--
 Beta-reduces the goal's target.

tests/lean/run/sym_simp_1.lean

@@ -116,7 +116,7 @@ example (as : Array (Nat → Nat)) (i : Nat) (_ : i < as.size) (h : as[i] a = b)
 trace: c a : Nat
 g : Nat → Nat
 h : ite (c > 0) a = g
-⊢ ite (c > 0) a = g
+⊢ ite (0 < c) a = g
 -/
 #guard_msgs in
 example (h : ite (c > 0) a = g) : ite (c > 0) (0 + a) = g := by

tests/lean/run/sym_simp_2.lean

@@ -122,10 +122,25 @@ example : ((2 : Int) ≠ 3) = True := by sym_simp
 example : ((1 : Rat) / 2 < 2 / 3) = True := by sym_simp
 example : ((1 : Rat) / 2 = 2 / 4) = True := by sym_simp
 
+-- Predicates: String
+example : "hello" < "world" := by sym_simp
+example : "a" ≤ "a" := by sym_simp
+example : ¬ "a" > "b" := by sym_simp
+example : "a" = "a" := by sym_simp
+example : "a" ≠ "b" := by sym_simp
+
+-- Predicates: Char
+example : 'h' < 'w' := by sym_simp
+example : 'a' ≤ 'a' := by sym_simp
+example : ¬ 'a' > 'b' := by sym_simp
+example : 'a' = 'a' := by sym_simp
+example : 'a' ≠ 'b' := by sym_simp
+
 -- Predicates: Fixed-width
 example : ((100 : UInt8) < 200) = True := by sym_simp
 example : ((-50 : Int8) < 50) = True := by sym_simp
 example : ((1000 : UInt16) ≤ 1000) = True := by sym_simp
+example : ((-50 : Int8) > 50) = False := by sym_simp
 
 -- Predicates: BitVec
 example : ((5 : BitVec 8) < 10) = True := by sym_simp

tests/lean/run/sym_simp_3.lean

@@ -37,7 +37,7 @@ example (f g : Nat → Nat → Nat) : (if a + 0 ≠ a then f else g) a (b + 0) =
 trace: a b : Nat
 f g : Nat → Nat → Nat
 h : a = b
-⊢ (if a ≠ b then id f else id (id g)) a (b + 0) = g a b
+⊢ (if ¬a = b then id f else id (id g)) a (b + 0) = g a b
 -/
 #guard_msgs in
 example (f g : Nat → Nat → Nat) (h : a = b) : (if a + 0 ≠ b then id f else id (id g)) a (b + 0) = g a b := by
@@ -136,7 +136,7 @@ example (f g : Nat → Nat → Nat) : (if _ : a + 0 ≠ a then f else g) a (b +
 trace: a b : Nat
 f g : Nat → Nat → Nat
 h : a = b
-⊢ (if h : a ≠ b then id f else id (id g)) a (b + 0) = g a b
+⊢ (if h : ¬a = b then id f else id (id g)) a (b + 0) = g a b
 -/
 #guard_msgs in
 example (f g : Nat → Nat → Nat) (h : a = b) : (if _ : a + 0 ≠ b then id f else id (id g)) a (b + 0) = g a b := by