feat: add recall command (#5278)

Mathlib.lean

@@ -2759,6 +2759,7 @@ import Mathlib.Tactic.PushNeg
 import Mathlib.Tactic.Qify
 import Mathlib.Tactic.Qify.Attr
 import Mathlib.Tactic.RSuffices
+import Mathlib.Tactic.Recall
 import Mathlib.Tactic.Recover
 import Mathlib.Tactic.Relation.Rfl
 import Mathlib.Tactic.Relation.Symm

Mathlib/Tactic.lean

@@ -104,6 +104,7 @@ import Mathlib.Tactic.PushNeg
 import Mathlib.Tactic.Qify
 import Mathlib.Tactic.Qify.Attr
 import Mathlib.Tactic.RSuffices
+import Mathlib.Tactic.Recall
 import Mathlib.Tactic.Recover
 import Mathlib.Tactic.Relation.Rfl
 import Mathlib.Tactic.Relation.Symm

Mathlib/Tactic/Recall.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2023 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone, Kyle Miller
+-/
+import Lean.Elab.MutualDef
+import Std.Tactic.OpenPrivate
+
+/-!
+# `recall` command
+-/
+
+namespace Mathlib.Tactic.Recall
+
+/--
+The `recall` command redeclares a previous definition for illustrative purposes.
+This can be useful for files that give an expository account of some theory in Lean.
+
+The syntax of the command mirrors `def`, so all the usual bells and whistles work.
+```
+recall List.cons_append (a : α) (as bs : List α) : (a :: as) ++ bs = a :: (as ++ bs) := rfl
+```
+Also, one can leave out the body.
+```
+recall Nat.add_comm (n m : Nat) : n + m = m + n
+```
+
+The command verifies that the new definition type-checks and that the type and value
+provided are definitionally equal to the original declaration. However, this does not
+capture some details (like binders), so the following works without error.
+```
+recall Nat.add_comm {n m : Nat} : n + m = m + n
+```
+-/
+syntax (name := recall) "recall " ident ppIndent(optDeclSig) (declVal)? : command
+
+open Lean Meta Elab Command Term
+open private elabHeaders from Lean.Elab.MutualDef
+
+elab_rules : command
+  | `(recall $id $sig:optDeclSig $[$val?]?) => withoutModifyingEnv do
+    let some info := (← getEnv).find? id.getId
+      | throwError "unknown constant '{id}'"
+    runTermElabM fun _ => discard <| addTermInfo id (mkConst id.getId)
+    let id' := mkIdentFrom id (← mkAuxName id.getId 1)
+    if let some val := val? then
+      let some infoVal := info.value?
+        | throwErrorAt val "constant '{id}' has no defined value"
+      elabCommand <| ← `(noncomputable def $id':declId $sig:optDeclSig $val)
+      let some newInfo := (← getEnv).find? id'.getId | return -- def already threw
+      runTermElabM fun _ => do
+        let mvs ← newInfo.levelParams.mapM fun _ => mkFreshLevelMVar
+        let newType := newInfo.type.instantiateLevelParams newInfo.levelParams mvs
+        unless (← isDefEq info.type newType) do
+          throwTypeMismatchError none info.type newInfo.type (mkConst id.getId)
+        let newVal := newInfo.value?.get!.instantiateLevelParams newInfo.levelParams mvs
+        unless (← isDefEq infoVal newVal) do
+          let err :=
+            m!"value mismatch{indentD id.getId}\nhas value{indentExpr newVal}\n" ++
+            m!"but is expected to have value{indentExpr infoVal}"
+          throwErrorAt val err
+    else
+      let (binders, type?) := expandOptDeclSig sig
+      let views := #[{
+        declId := id', binders, type?, value := .missing,
+        ref := ← getRef, kind := default, modifiers := {}
+      : DefView}]
+      runTermElabM fun _ => do
+        let elabView := (← elabHeaders views)[0]!
+        unless (← isDefEq info.type elabView.type) do
+          throwTypeMismatchError none info.type elabView.type (mkConst id.getId)

test/Recall.lean

@@ -0,0 +1,89 @@
+import Std.Tactic.GuardMsgs
+import Mathlib.Tactic.Recall
+import Mathlib.Analysis.Calculus.Deriv.Basic
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
+import Mathlib.Data.Complex.Exponential
+
+-- Remark: When the test is run by make/CI, this option is not set, so we set it here.
+set_option pp.unicode.fun true
+
+/-
+Motivating examples from the initial Zulip thread:
+https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/recall.20command
+-/
+
+section
+variable {𝕜 : Type _} [NontriviallyNormedField 𝕜]
+variable {E : Type _} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+variable {F : Type _} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+recall HasFDerivAtFilter (f : E → F) (f' : E →L[𝕜] F) (x : E) (L : Filter E) :=
+  (fun x' => f x' - f x - f' (x' - x)) =o[L] fun x' => x' - x
+end
+
+/--
+error: value mismatch
+  Complex.exp
+has value
+  id
+but is expected to have value
+  fun z ↦ CauSeq.lim (Complex.exp' z)
+-/
+#guard_msgs in recall Complex.exp : ℂ → ℂ := id
+
+/--
+error: value mismatch
+  Real.pi
+has value
+  0
+but is expected to have value
+  2 * Classical.choose Real.exists_cos_eq_zero
+-/
+#guard_msgs in recall Real.pi : ℝ := 0
+
+/-
+Other example tests
+-/
+
+recall id (x : α) : α := x
+
+/--
+error: type mismatch
+  id
+has type
+  {α : Sort u_1} → α → α → ℕ : Type u_1
+but is expected to have type
+  {α : Sort u} → α → α : Sort (imax (u + 1) u)
+-/
+#guard_msgs in recall id (_x _y : α) : ℕ := 0
+
+recall id (_x : α) : α
+
+def foo := 22
+
+recall foo := 22
+
+recall foo : Nat
+
+/--
+error: value mismatch
+  foo
+has value
+  23
+but is expected to have value
+  22
+-/
+#guard_msgs in recall foo := 23
+
+recall Nat.add_comm (n m : Nat) : n + m = m + n
+
+-- Caveat: the binder kinds are not checked
+recall Nat.add_comm {n m : Nat} : n + m = m + n
+
+/-- error: unknown constant 'nonexistent' -/
+#guard_msgs in recall nonexistent
+
+axiom bar : Nat
+/-- error: constant 'bar' has no defined value -/
+#guard_msgs in recall bar := bar
+
+recall List.cons_append (a : α) (as bs : List α) : (a :: as) ++ bs = a :: (as ++ bs) := rfl