chore: add empty test out

src/Init/Data/Array/Lemmas.lean

@@ -185,3 +185,84 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
 
 theorem mem_def (a : α) (as : Array α) : a ∈ as ↔ a ∈ as.data :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
+
+/-- # get -/
+@[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
+
+theorem getElem?_lt
+    (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some (a[i]) := dif_pos h
+
+theorem getElem?_ge
+    (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
+
+@[simp] theorem get?_eq_getElem? (a : Array α) (i : Nat) : a.get? i = a[i]? := rfl
+
+theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = none := by
+  simp [getElem?_ge, h]
+
+theorem getD_get? (a : Array α) (i : Nat) (d : α) :
+  Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
+  if h : i < a.size then
+    simp [setD, h, getElem?]
+  else
+    have p : i ≥ a.size := Nat.le_of_not_gt h
+    simp [setD, getElem?_len_le _ p, h]
+
+@[simp] theorem getD_eq_get? (a : Array α) (n d) : a.getD n d = (a[n]?).getD d := by
+  simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_get?, *]
+
+theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
+
+@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default := by
+  by_cases p : i < a.size <;> simp [getD_get?, get!_eq_getD, p]
+
+/-- # set -/
+
+@[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
+      (eq : i.val = j) (p : j < (a.set i v).size) :
+    (a.set i v)[j]'p = v := by
+  simp [set, getElem_eq_data_get, ←eq]
+
+@[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size)
+    (h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by
+  simp only [set, getElem_eq_data_get, List.get_set_ne _ h]
+
+theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
+    (h : j < (a.set i v).size) :
+    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v ▸ h) := by
+  by_cases p : i.1 = j <;> simp [p]
+
+@[simp] theorem getElem?_set_eq (a : Array α) (i : Fin a.size) (v : α) :
+    (a.set i v)[i.1]? = v := by simp [getElem?_lt, i.2]
+
+@[simp] theorem getElem?_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α)
+    (ne : i.val ≠ j) : (a.set i v)[j]? = a[j]? := by
+  by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
+
+/- # setD -/
+
+@[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]
+
+@[simp] theorem getElem_setD_eq (a : Array α) {i : Nat} (v : α) (h : _) :
+  (setD a i v)[i]'h = v := by
+  simp at h
+  simp only [setD, h, dite_true, getElem_set, ite_true]
+
+@[simp]
+theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a.setD i v)[i]? = some v := by
+  simp [getElem?_lt, p]
+
+/-- 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
+  by_cases h : i < a.size <;>
+    simp [setD, Nat.not_lt_of_le, h,  getD_get?]
+
+end Array

src/Init/Data/List/Lemmas.lean

@@ -665,3 +665,47 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ ·
     exact congrArg some <| anti.1
       ((le_minimum?_iff le_min_iff (xs := x::xs) rfl _).1 (le_refl _) _ h₁)
       (h₂ _ (minimum?_mem min_eq_or (xs := x::xs) rfl))
+
+#print get
+#print set
+
+@[simp] theorem get_cons_succ {as : List α} {h : i + 1 < (a :: as).length} :
+  (a :: as).get ⟨i+1, h⟩ = as.get ⟨i, Nat.lt_of_succ_lt_succ h⟩ := rfl
+
+@[simp] theorem get_cons_succ' {as : List α} {i : Fin as.length} :
+  (a :: as).get i.succ = as.get i := rfl
+
+@[simp] theorem set_nil (n : Nat) (a : α) : [].set n a = [] := rfl
+
+@[simp] theorem set_zero (x : α) (xs : List α) (a : α) :
+  (x :: xs).set 0 a = a :: xs := rfl
+
+@[simp] theorem set_succ (x : α) (xs : List α) (n : Nat) (a : α) :
+  (x :: xs).set n.succ a = x :: xs.set n a := rfl
+
+@[simp] theorem get_set_eq (l : List α) (i : Nat) (a : α) (h : i < (l.set i a).length) :
+    (l.set i a).get ⟨i, h⟩ = a :=
+  match l, i with
+  | [], _ => by
+    simp at h
+    contradiction
+  | _ :: _, 0 => by
+    simp
+  | _ :: l, i + 1 => by
+    simp [get_set_eq l]
+
+@[simp] theorem get_set_ne (l : List α) {i j : Nat} (h : i ≠ j) (a : α)
+    (hj : j < (l.set i a).length) :
+    (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, by simp at hj; exact hj⟩ :=
+  match l, i, j with
+  | [], _, _ => by
+    simp
+  | _ :: _, 0, 0 => by
+    contradiction
+  | _ :: _, 0, _ + 1 => by
+    simp
+  | _ :: _, _ + 1, 0 => by
+    simp
+  | _ :: l, i + 1, j + 1 => by
+    have g : i ≠ j := h ∘ congrArg (· + 1)
+    simp [get_set_ne l g]

src/Init/Meta.lean

@@ -1362,6 +1362,19 @@ structure OmegaConfig where
 
 end Omega
 
+namespace CheckTactic
+
+/--
+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.
+-/
+inductive CheckGoalType {α : Sort u} : (val : α) → Prop where
+| intro : (val : α) → CheckGoalType val
+
+end CheckTactic
+
 end Meta
 
 namespace Parser

src/Init/Notation.lean

@@ -613,3 +613,30 @@ everything else.
 -/
 syntax (name := guardMsgsCmd)
   (docComment)? "#guard_msgs" (ppSpace guardMsgsSpec)? " in" ppLine command : command
+
+namespace Parser
+
+/--
+`#check_tactic t ~> r by commands` runs the tactic sequence `commands`
+on a goal with `t` and sees if the resulting expression has reduced it
+to `r`.
+-/
+syntax (name := checkTactic) "#check_tactic " term "~>" term "by" tactic : command
+
+/--
+`#check_tactic_failure t by tac` runs the tactic `tac`
+on a goal with `t` and verifies it fails.
+-/
+syntax  (name := checkTacticFailure) "#check_tactic_failure " term "by" tactic : command
+
+/--
+`#check_simp t ~> r` checks `simp` reduces `t` to `r`.
+-/
+syntax (name := checkSimp) "#check_simp " term "~>" term : command
+
+/--
+`#check_simp t !~>` checks `simp` fails on reducing `t`.
+-/
+syntax (name := checkSimpFailure) "#check_simp " term "!~>" : command
+
+end Parser

src/Lean/Elab.lean

@@ -48,3 +48,4 @@ import Lean.Elab.Calc
 import Lean.Elab.InheritDoc
 import Lean.Elab.ParseImportsFast
 import Lean.Elab.GuardMsgs
+import Lean.Elab.CheckTactic

src/Lean/Elab/CheckTactic.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+prelude
+import Lean.Elab.Tactic.ElabTerm
+import Lean.Elab.Command
+import Lean.Elab.Tactic.Meta
+
+/-!
+Commands to validate tactic results.
+-/
+
+namespace Lean.Elab.CheckTactic
+
+open Lean.Meta CheckTactic
+open Lean.Elab.Tactic
+open Lean.Elab.Command
+
+private def matchCheckGoalType (stx : Syntax) (goalType : Expr) : MetaM (Expr × Expr × Level) := 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}"
+  pure (val, type, u)
+
+@[builtin_command_elab Lean.Parser.checkTactic]
+def elabCheckTactic : CommandElab := fun stx => do
+  let `(#check_tactic $t ~> $result by $tac) := stx | throwUnsupportedSyntax
+  withoutModifyingEnv $ do
+    runTermElabM $ fun _vars => do
+      let u ← Lean.Elab.Term.elabTerm t none
+      let type ← inferType u
+      let lvl ← mkFreshLevelMVar
+      let checkGoalType : Expr := mkApp2 (mkConst ``CheckGoalType [lvl]) type u
+      let mvar ← mkFreshExprMVar (.some checkGoalType)
+      let (goals, _) ← Lean.Elab.runTactic mvar.mvarId! tac.raw
+      let expTerm ← Lean.Elab.Term.elabTerm result (.some type)
+      match goals with
+      | [] =>
+        throwErrorAt stx
+          m!"{tac} closed goal, but is expected to reduce to {indentExpr expTerm}."
+      | [next] => do
+        let (val, _, _) ← matchCheckGoalType stx (←next.getType)
+        if !(← Meta.withReducible <| isDefEq val expTerm) then
+          throwErrorAt stx
+            m!"Term reduces to{indentExpr val}\nbut is expected to reduce to {indentExpr expTerm}"
+      | _ => do
+        throwErrorAt stx
+          m!"{tac} produced multiple goals, but is expected to reduce to {indentExpr expTerm}."
+      pure ()
+
+@[builtin_command_elab Lean.Parser.checkTacticFailure]
+def elabCheckTacticFailure : CommandElab := fun stx => do
+  let `(#check_tactic_failure $t by $tactic) := stx | throwUnsupportedSyntax
+  withoutModifyingEnv $ do
+    runTermElabM $ fun _vars => do
+      let val ← Lean.Elab.Term.elabTerm t none
+      let type ← inferType val
+      let lvl ← mkFreshLevelMVar
+      let checkGoalType : Expr := mkApp2 (mkConst ``CheckGoalType [lvl]) type val
+      let mvar ← mkFreshExprMVar (.some checkGoalType)
+      let act := Lean.Elab.runTactic mvar.mvarId! tactic.raw
+      match ← try (Term.withoutErrToSorry (some <$> act)) catch _ => pure none with
+        | none =>
+          pure ()
+        | some (gls, _) =>
+          let ppGoal (g : MVarId) := do
+                let (val, _type, _u) ← matchCheckGoalType stx (← g.getType)
+                pure m!"{indentExpr val}"
+          let msg ←
+            match gls with
+              | [] => pure m!"{tactic} expected to fail on {val}, but closed goal."
+              | [g] =>
+                pure <| m!"{tactic} expected to fail on {val}, but returned: {←ppGoal g}"
+              | gls =>
+                let app m g := do pure <| m ++ (←ppGoal g)
+                let init := m!"{tactic} expected to fail on {val}, but returned goals:"
+                gls.foldlM (init := init) app
+          throwErrorAt stx msg
+
+@[builtin_macro Lean.Parser.checkSimp]
+def expandCheckSimp : Macro := fun stx => do
+  let `(#check_simp $t ~> $exp) := stx | Macro.throwUnsupported
+  `(command|#check_tactic $t ~> $exp by simp)
+
+@[builtin_macro Lean.Parser.checkSimpFailure]
+def expandCheckSimpFailure : Macro := fun stx => do
+  let `(#check_simp $t !~>) := stx | Macro.throwUnsupported
+  `(command|#check_tactic_failure $t by simp)
+
+end Lean.Elab.CheckTactic

tests/lean/simpArrayIdx.lean

@@ -0,0 +1,26 @@
+section
+variable {α : Type _}
+variable [Inhabited α]
+variable (a : Array α)
+variable (i j : Nat)
+variable (v d : α)
+variable (g : i < (a.set! i v).size)
+variable (j_lt : j < (a.set! i v).size)
+
+#check_simp (i + 0) ~> i
+
+#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
+
+-- Checks with different index values.
+#check_simp (a.set! i v)[j]'j_lt  ~> (a.setD i v)[j]'_
+#check_simp (a.setD i v)[j]'j_lt !~>
+
+section
+variable (p : i < a.size)
+#check_tactic (a.set! i v)[i]? ~> .some v by simp[p]
+end
+
+end