feat: Introduce #check_simp command and usage. (#583)

Co-authored-by: François G. Dorais <fgdorais@gmail.com>

Std.lean

@@ -147,6 +147,7 @@ import Std.Tactic.Unreachable
 import Std.Tactic.Where
 import Std.Test.Internal.DummyLabelAttr
 import Std.Util.Cache
+import Std.Util.CheckTactic
 import Std.Util.ExtendedBinder
 import Std.Util.LibraryNote
 import Std.Util.Pickle

Std/Data/Array/Lemmas.lean

@@ -41,10 +41,26 @@ attribute [simp] isEmpty uget
 
 @[simp] theorem data_length {l : Array α} : l.data.length = l.size := rfl
 
+/-- # mem -/
+
 theorem mem_data {a : α} {l : Array α} : a ∈ l.data ↔ a ∈ l := (mem_def _ _).symm
 
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := fun.
 
+/-- # set -/
+
+@[simp] theorem set!_is_setD : @set! = @setD := rfl
+
+@[simp] theorem size_setD (a : Array α) (index : Nat) (val : α) :
+  (Array.setD a index val).size = a.size := by
+  if h : index < a.size  then
+    simp [setD, h]
+  else
+    simp [setD, h]
+
+
+/-- # get lemmas -/
+
 theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
   erw [Array.mem_def, getElem_eq_data_get]
   apply List.get_mem
@@ -131,6 +147,22 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :
     (a.set i v)[j]'(by simp [*]) = if i = j then v else a[j] := by
   if h : i.1 = j then subst j; simp [*] else simp [*]
 
+@[simp] theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
+  (setD a i v)[i]'h = v := by
+  simp at h
+  simp only [setD, h, dite_true, get_set, ite_true]
+
+/--
+This lemma simplifies a normal form from `get!`
+-/
+@[simp] theorem getD_get?_setD (a : Array α) (i : Nat) (v d : α) :
+  Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
+  if h : i < a.size then
+    simp [setD, h, getElem?, get_set]
+  else
+    have p : i ≥ a.size := Nat.le_of_not_gt h
+    simp [setD, h, get?_len_le, p]
+
 theorem set_set (a : Array α) (i : Fin a.size) (v v' : α) :
     (a.set i v).set ⟨i, by simp [i.2]⟩ v' = a.set i v' := by simp [set, List.set_set]
 

Std/Util/CheckTactic.lean

@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+import Lean.Elab.Tactic.ElabTerm
+
+/-
+This file is the home for commands to tactics behave as expected.
+
+It currently includes two tactixs:
+
+#check_tactic t ~> res
+
+
+only a #check_simp command that applies simp
+IT
+-/
+
+namespace Std.Tactic
+
+open Lean
+open Elab.Tactic
+open Meta
+
+/--
+Type used to lift an arbitrary value into a type parameter so it can
+appear in a proof goal.
+
+It is used by the #check_tactic command.
+-/
+private inductive CheckGoalType {α : Sort u} : (val : α) → Prop where
+| intro : (val : α) → CheckGoalType val
+
+/--
+`check_tactic_goal t` verifies that the goal has is equal to
+`CheckGoalType t` with reducible transparency.  It closes the goal if so
+and otherwise reports an error.
+
+It is used by #check_tactic.
+-/
+local syntax (name := check_tactic_goal) "check_tactic_goal " term : tactic
+
+
+/--
+Implementation of `check_tactic_goal`
+-/
+@[tactic check_tactic_goal] private def evalCheckTacticGoal : Tactic := fun stx =>
+  match stx with
+  | `(tactic| check_tactic_goal $exp) =>
+    closeMainGoalUsing (checkUnassigned := false) fun goalType => do
+      let u ← mkFreshLevelMVar
+      let type ← mkFreshExprMVar (.some (.sort u))
+      let val  ← mkFreshExprMVar (.some type)
+      let extType := mkAppN (.const ``CheckGoalType [u]) #[type, val]
+      if !(← isDefEq goalType extType) then
+        throwErrorAt stx "Goal{indentExpr goalType}\nis expected to match {indentExpr extType}"
+      let expTerm ← elabTermEnsuringType exp type
+      if !(← Meta.withReducible <| isDefEq val expTerm) then
+        throwErrorAt stx
+          m!"Term reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
+      return mkAppN (.const ``CheckGoalType.intro [u]) #[type, val]
+  | _ => throwErrorAt stx "check_goal syntax error"
+
+/--
+`#check_tactic t ~> r by commands` runs the tactic sequence `commands`
+on a goal with t in the type and sees if the resulting expression has
+reduced it to `r`.
+-/
+macro "#check_tactic " t:term "~>" result:term "by" tac:tactic : command =>
+  `(command|example : CheckGoalType $t := by $tac; check_tactic_goal $result)
+
+/--
+`#check_simp t ~> r` checks `try simp` reduces `t` to `r`.
+-/
+macro "#check_simp " t:term "~>" exp:term : command =>
+  `(command|#check_tactic $t ~> $exp by try simp)

test/array.lean

@@ -0,0 +1,21 @@
+import Std.Util.CheckTactic
+import Std.Data.Array
+
+section
+variable {α : Type _}
+variable [Inhabited α]
+variable (a : Array α)
+variable (i : Nat)
+variable (v d : α)
+variable (g : i < (a.set! i v).size)
+
+#check_simp (a.set! i v).get ⟨i, g⟩ ~> v
+#check_simp (a.set! i v).get! i ~> if i < a.size then v else default
+#check_simp (a.set! i v).getD i d ~> if i < a.size then v else d
+#check_simp (a.set! i v)[i] ~> v
+
+-- This doesn't work currently.
+-- It will be address in the comprehensive overhaul of array lemmas.
+-- #check_simp (a.set! i v)[i]? ~> .some v
+
+end