feat: some string simprocs (#4233)

For the SSFT24 summer school.

src/Init/Data/String/Basic.lean

@@ -24,6 +24,14 @@ instance : LT String :=
 instance decLt (s₁ s₂ : @& String) : Decidable (s₁ < s₂) :=
   List.hasDecidableLt s₁.data s₂.data
 
+@[reducible] protected def le (a b : String) : Prop := ¬ b < a
+
+instance : LE String :=
+  ⟨String.le⟩
+
+instance decLE (s₁ s₂ : String) : Decidable (s₁ ≤ s₂) :=
+  inferInstanceAs (Decidable (Not _))
+
 /--
 Returns the length of a string in Unicode code points.
 

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

@@ -45,6 +45,11 @@ builtin_dsimproc [simp, seval] reduceVal (Char.val _) := fun e => do
   let_expr Char.val arg ← e | return .continue
   let some c ← fromExpr? arg | return .continue
   return .done <| toExpr c.val
+
+builtin_simproc [simp, seval] reduceLT  (( _ : Char) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc [simp, seval] reduceLE  (( _ : Char) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc [simp, seval] reduceGT  (( _ : Char) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc [simp, seval] reduceGE  (( _ : Char) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
 builtin_simproc [simp, seval] reduceEq  (( _ : Char) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : Char) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
 builtin_dsimproc [simp, seval] reduceBEq  (( _ : Char) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)

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

@@ -32,4 +32,25 @@ builtin_dsimproc [simp, seval] reduceMk (String.mk _) := fun e => do
   unless e.isAppOfArity ``String.mk 1 do return .continue
   reduceListChar e.appArg! ""
 
+@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : String → String → 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 : String → String → Bool) (e : Expr) : SimpM DStep := 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 <| toExpr (op n m)
+
+builtin_simproc [simp, seval] reduceLT  (( _ : String) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc [simp, seval] reduceLE  (( _ : String) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc [simp, seval] reduceGT  (( _ : String) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc [simp, seval] reduceGE  (( _ : String) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+builtin_simproc [simp, seval] reduceEq  (( _ : String) = _)  := reduceBinPred ``Eq 3 (. = .)
+builtin_simproc [simp, seval] reduceNe  (( _ : String) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
+builtin_dsimproc [simp, seval] reduceBEq  (( _ : String) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
+builtin_dsimproc [simp, seval] reduceBNe  (( _ : String) != _)  := reduceBoolPred ``bne 4 (. != .)
+
 end String

tests/lean/run/simp6.lean

@@ -31,9 +31,10 @@ of_eq_true (eq_true_of_decide (Eq.refl true))
 #print ex6
 
 theorem ex7 : (if "hello" = "world" then 1 else 2) = 2 := by
-  simp (config := { decide := false })
-  -- Goal is now `⊢ "hello" = "world" → False`
-  simp (config := { decide := true })
+  simp (config := { decide := false }) [-String.reduceEq]
+  guard_target =ₛ ¬ "hello" = "world"
+  fail_if_success simp [-String.reduceEq]
+  simp (config := { decide := true }) [-String.reduceEq]
 
 theorem ex8 : (10 + 2000 = 20) = False :=
   by simp

tests/lean/run/string_simprocs.lean

@@ -0,0 +1,60 @@
+abbrev Value := BitVec 32
+
+def Env := String → Value
+
+namespace Env
+
+def set (x : String) (v : Value) (ρ : Env) : Env :=
+  fun y => if x = y then v else ρ y
+
+def get (x : String) (ρ : Env) : Value :=
+  ρ x
+
+def init (i : Value) : Env := fun _ => i
+
+end Env
+
+@[simp] theorem Env.get_init : (Env.init v).get x = v := by rfl
+
+@[simp] theorem Env.get_set_same {ρ : Env} : (ρ.set x v).get x = v := by
+  simp [get, set]
+
+@[simp] theorem Env.get_set_different {ρ : Env} : x ≠ y → (ρ.set x v).get y = ρ.get y := by
+  intro; simp [get, set, *]
+
+example : (((Env.init 0).set "x" 1).set "y" 2).get "y" = 2 := by
+  simp
+
+example : (((Env.init 0).set "x" 1).set "y" 2).get "x" = 1 := by
+  simp
+
+example : (((Env.init 0).set "x" 1).set "y" 2).get "z" = 0 := by
+  simp
+
+example : "hello" ≠ "foo" := by
+  simp
+
+example : "hello" != "foo" := by
+  simp
+
+example : "hello" == "hello" := by
+  simp
+
+example : "hello" == "foo" → False := by
+  simp
+
+example : "hello" = "foo" → False := by
+  simp [-String.reduceEq]
+  guard_target =ₛ ¬ "hello" = "foo"
+  simp
+
+example : "hello" ≤ "hellz" := by simp
+example : "hello" < "hellz" := by simp
+example : "hellz" > "hello" := by simp
+example : "hellz" ≥ "hello" := by simp
+example : "abcd" > "abc" := by simp
+
+example : 'b' > 'a' := by simp
+example : 'a' ≥ 'a' := by simp
+example : 'a' < 'b' := by simp
+example : 'a' ≤ 'a' := by simp