recall command

Stream: lean4

[Johan Commelin]

For expository purposes, I think it's very nice if you can sometimes "recall" a definition. How hard would it be to have a recall command that behaves as follows

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

and the only thing it will do is roughly a #check. So it checks that HasFDerivAtFilter exists, and that the type that is written down after recall is defeq to the existing type in the library.

[Johan Commelin]

Sorry, it should be a bit more than a #check. Because for defs it shouldn't just check that the types are defeq, but also the terms.
When recalling a theorem/lemma statement, it is of course enough that the types are defeq.

[Johan Commelin]

When recalling a theorem statement, recalling the proof should be optional.

[Damiano Testa]

Should the order of hypotheses matter?

[Damiano Testa]

In your example, for instance, if I recalled x before f, I would imagine that you would still want the check to pass, right?

[Johan Commelin]

No, it doesn't have to be sophisticated like that.

[Johan Commelin]

It should really be a way to recall a definition or theorem that will be used in some file that gives an expository account of some maths in Lean.

[Damiano Testa]

A possible approach to the question of exact recalling is to interpret recall as theorem, catch the existing declaration error, check defeq of the current and the found declaration and report the correct error/message.

[Johan Commelin]

In fact, I think recall may be quite pedantic about how well the statement matches the "original"

[Johan Commelin]

What I find important is that I can use the exact same name as the original.

[Johan Commelin]

So recall shouldn't attempt to add any new decl to the environment

[Damiano Testa]

So you would really like something like: if you printedtyped the output of #check up to defeq, it should pass, otherwise fail?

[Johan Commelin]

yes, but with defs I don't just want to check the types but also the terms

[Johan Commelin]

recall Complex.exp : \C \to \C := id

should give an error.

[Johan Commelin]

Or recall Real.pi : \R := 0

[Damiano Testa]

Ok, these would be all things that you can enforce after you have extracted the actual declaration from the environment. I do not have much experience in doing this, but I am up for trying to implement it!

[Siddhartha Gadgil]

I can also try this. What would be nice is to also have a code action after a #check that can turn it into a recall.

[Damiano Testa]

One more thing: in your initial recall example, there were no Type or instances: I was assuming that they were present thanks to a previous variable command. Is this the case or you really just want a sublist of the arguments?

[Damiano Testa]

Siddhartha, I had the same idea!

[Johan Commelin]

@Damiano Testa That's right, they were present thanks to an implicit variable command.

[Kyle Miller]

@Johan Commelin

syntax "recall " ident ppIndent(optDeclSig) declVal : command

open Lean Elab Command in
elab_rules : command
  | `(recall $id $sig:optDeclSig $val) => withoutModifyingEnv <| do
    let name ← mkAuxName id.getId 1
    let id' := mkIdentFrom id name
    elabCommand <| ← `(def $id':declId $sig:optDeclSig $val)
    elabCommand <| ← `(example : @$id = @$id' := rfl)

recall id (x : α) : α := x

recall id (x : α) : ℕ := 0
/-
type mismatch
  @id_1
has type
  {α : Sort ?u.8944} → α → ℕ : Type ?u.8944
but is expected to have type
  {α : Sort ?u.8943} → α → α : Sort (imax (?u.8943 + 1) ?u.8943)
-/

[Kyle Miller]

def foo := 22

recall foo := 22

recall foo := 23
/-
type mismatch
  rfl
has type
  foo = foo : Prop
but is expected to have type
  foo = foo_1 : Prop
-/

[Johan Commelin]

Nice! And can I recall theorem statements without giving a proof?

[Kyle Miller]

Ah, not yet

[Scott Morrison]

Presumably just recall foo should generate Try this: recall foo := 22.

[Damiano Testa]

Or even already #check foo should have the option.

[Johan Commelin]

Or otherwise a recall? command could do that.

[Kyle Miller]

New version:

syntax "recall " ident ppIndent(optDeclSig) (declVal)? : command

open Lean Elab Command in
elab_rules : command
  | `(recall $id $sig:optDeclSig $val) => withoutModifyingEnv <| do
    let id' := mkIdentFrom id (← mkAuxName id.getId 1)
    elabCommand <| ← `(noncomputable def $id':declId $sig:optDeclSig $val)
    elabCommand <| ← `(example : @$id = @$id' := rfl)
  | `(recall $id $sig:optDeclSig) => withoutModifyingEnv <| do
    let mySorry := mkIdentFrom id (← mkAuxName `mySorry 1)
    let id' := mkIdentFrom id (← mkAuxName id.getId 1)
    elabCommand <| ← `(axiom $mySorry {α : Sort _} : α)
    elabCommand <| ← `(noncomputable def $id':declId $sig:optDeclSig := $mySorry)
    elabCommand <| ← `(example : type_of% @$id' := @$id)

recall id (x : α) : α := x

recall id (x : α) : ℕ := 0
/-
type mismatch
  @id_1
has type
  {α : Sort ?u.8944} → α → ℕ : Type ?u.8944
but is expected to have type
  {α : Sort ?u.8943} → α → α : Sort (imax (?u.8943 + 1) ?u.8943)
-/

recall id (_x : α) : α

def foo := 22

recall foo := 22

recall foo : ℕ

recall foo := 23
/-
type mismatch
  rfl
has type
  foo = foo : Prop
but is expected to have type
  foo = foo_1 : Prop
-/

recall Nat.add_comm (n m : Nat) : n + m = m + n

[Kyle Miller]

The way the no-value case works is that it creates the temporary definition using a custom sorry axiom (otherwise def reports "uses sorry" as a warning), and then there's a check that the type of this temporary definition is correct.

[Kyle Miller]

Both cases are using the def command itself so that you get all the usual binder and value elaboration rules without any extra work.

[Kyle Miller]

One problem with this is that it doesn't give an error if your recollection of the binder types is wrong:

recall Nat.add_comm (n m : Nat) : n + m = m + n

recall Nat.add_comm {n m : Nat} : n + m = m + n

[Mac Malone]

Here is a funny error message:

axiom bar : Nat
recall bar := 5
/-
type mismatch
  rfl
has type
  bar = bar : Prop
but is expected to have type
  bar = bar_1 : Prop
-/

[Mac Malone]

(I was thinking that the proper answer was that bar has no definitional value, but maybe saying it is not equal is sufficient?)

[Mac Malone]

Anyway, I stumbled onto this topic today and having recently learned how Lean elaborates the headers of mutual definitions, I wanted to give a more nuts and bolts version of @Kyle Miller's solution a try. The end result does not use sorry and elides the implementation details from its error messages. So, here is what I came up with:

import Lean
import Std.Tactic.OpenPrivate

open private elabHeaders from Lean.Elab.MutualDef

syntax "recall " ident ppIndent(optDeclSig) (declVal)? : command

open Lean Meta Elab Command Term in
elab_rules : command
  | `(recall $id $sig:optDeclSig $[$val?]?) => withoutModifyingEnv do
    let some info := (← getEnv).find? id.getId
      | throwError "unknown constant '{id}'"
    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
          throwErrorAt val "value mismatch{indentD id.getId}\nhas value{indentExpr newVal}\nbut is expected to have value{indentExpr infoVal}"
    else
      let (binders, type?) := expandOptDeclSig sig
      let views := #[{
        declId := id', binders, type?, value := .missing,
        ref := ← getRef, kind := .theorem, 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)

recall id (x : α) : α := x

recall id (x : α) : Nat := 0
/-
type mismatch
  id
has type
  {α : Sort u_1} → α → Nat : Type u_1
but is expected to have type
  {α : Sort u} → α → α : Sort (imax (u + 1) u)
-/

recall id (_x : α) : α

def foo := 22

recall foo := 22

recall foo : Nat

recall foo := 23
/-
value mismatch
  foo
has value
  23
but is expected to have value
  22
-/

recall Nat.add_comm (n m : Nat) : n + m = m + n

recall Nat.add_comm {n m : Nat} : n + m = m + n

axiom bar : Nat
recall bar := bar
/- constant 'bar' has no defined value -/

[Scott Morrison]

LGTM! PR?

[Johan Commelin]

@Mac Nice! That looks cool.

[Johan Commelin]

The thing with binder types is a tidbit unfortunate, but absolutely not a deal breaker, I think

[Mac Malone]

Scott Morrison said:

LGTM! PR?

Were should something like this be PR'd to? Std or Mathlib?

[Scott Morrison]

I would say Mathlib. There is both higher reviewing bandwidth, and more inclination towards "are we sure we really want this? let's find out!". Usually we wait for a specific reason (or Mario just wanting to) to move things up to Std.

[Mac Malone]

@Scott Morrison Perhaps surprisingly, this would actually be my first PR to Mathlib. I believe I have learned through osmosis here on the Zulip channel that PR's to mathlib are bit weird in that they generally come from branches on the repository rather than forks. Do I have that right, and how exactly does that work?

[Scott Morrison]

@Mac, yes, that's right. Our CI works better from a branch of the main repo. I've just sent an invite giving your write access to the mathlib4 repo.

[Scott Morrison]

(And yes, this is lame, and ideas for fixing it are welcome! I think the main issue is that CI needs to upload oleans to the global cache. :-)

[Mac Malone]

PR is up: !4#5278 (@Scott Morrison, I tagged you in case I made any mistakes in the process.)

[Scott Morrison]

Looks great. Left a query.

[Scott Morrison]

Ah -- one more thing, @Mac: you should add the awaiting-review label, or otherwise it won't make it onto the #queue4 and might never get merged. :-)

[Scott Morrison]

The other useful label to for authors to frequently add is awaiting-CI, which will automatically be removed again once you get a green tick.

[Mac Malone]

@Scott Morrison Thanks and thanks again for all your help!

[Patrick Massot]

@Mac I tried to use the recall command today and the version where users give only an identifier very rarely succeeds. For instance in:

recall add_assoc {G : Type _} [AddSemigroup G] (a b c : G) : a + b + c = a + (b + c)
recall add_assoc

The first call succeeds but not the second one which says

Error updating: Error fetching goals: Rpc error: InternalError: incorrect number of universe levels add_assoc.

[Patrick Massot]

recall Nat.add_assoc works but this is pretty much the only kind of example where I've able to get an answer.

[Jannis Limperg]

The error message makes me suspect that recall turns the name add_assoc into an Expr.const, but without specifying appropriate universe levels (should probably be level metavariables). Nat.add_assoc doesn't have universe levels, so there it works.

[Patrick Massot]

Yes, this is exactly what it sounds like.

[Mac Malone]

@Patrick Massot @Jannis Limperg Is right, I forgot to instantiate the level params in the identifier-only branch. Working on a fix now.

[Patrick Massot]

Thanks!

[Mac Malone]

Hmm, having worked on this somewhat. I am not sure my original diagnosis was correct. Instantiating the level params does not seem to fix the issue, and further debugging reveals the error only appears in interactive mode. Thus, the server seems to assuming some invariant that I am violating that the normal lean frontend does not.

[Mac Malone]

Found the problem: it had nothing to do with main recall command logic, was actual the term info node that was added to the info tree for go-to-def that was causing the error. Apparently the server checks that it has the right number of level parameters and I had not been providing them.

[Mac Malone]

I am, however, confused why this error only occurred on the ident-only branch and not the normal one.

[Mac Malone]

PR: #6004

[Mac Malone]

As an aside, #guard_msgs seems broken in VSCode (i.e., it errors there with what appears to be the same message, but not on the CLI).

[Kyle Miller]

@Mac What are you reporting about #guard_msgs?

[Mac Malone]

@Kyle Miller #guard_msgs is broken in Windows VSCode. That is, it reports a mismatch when there is none. For instance, I opened up e.g. mathlib's test/Explode.lean in VSCode and all the #guard_msgs commands error. I think the problem may be due to the embedded expression interactivity metadata because simple string messages like the last two #guard_msgs test cases in test/Recall.lean work correctly.

[Kyle Miller]

It's fine in VS Code on Linux. I wonder what the difference between Linux and Windows might be?

[Kyle Miller]

Maybe line endings need to be normalized? The test/Recall.lean examples both have no newlines.

[Kyle Miller]

Are you saying that the tests pass in the CLI on Windows? Is this any sort of unix-like environment you're working in?

[Mac Malone]

@Kyle Miller Yeah, line endings could definitely be it. My CLI is MSYS2 (so Unix-like).

[Mac Malone]

Yep, went and checked -- it was the line endings. Likely an artifact of Git autocrlf.

[Mac Malone]

The fix PR seems to be idling (#6004). @Patrick Massot, is there anything I should do to get eyes on it, or is this just the normal waiting game?

[Johan Commelin]

Meta PRs usually sit in the queue for a bit longer... there are fewer people qualified to review them.

[Patrick Massot]

I merged the PR since having no error message is better. But actually it made me realize the version giving only a name does nothing useful at all. I wrote a crappy version of what I had in mind in this case:

import Mathlib.Analysis.Calculus.ContDiff

open Lean Std Tactic TryThis

/-- Dumb version of `addSuggestion` which suggest to write a String instead of
valid syntax. -/
def Std.Tactic.TryThis.addTextSuggestion (ref : Syntax) (msg : String := "") : MetaM Unit := do
  logInfoAt ref m!"Try this: {msg}"
  if let some range := ref.getRange? then
    let map ← getFileMap
    let start := findLineStart map.source range.start
    let body := map.source.findAux (· ≠ ' ') range.start start
    let text := Format.prettyExtra msg
      (indent := (body - start).1) (column := (range.start - start).1)
    let stxRange := ref.getRange?.getD range
    let stxRange :=
    { start := map.lineStart (map.toPosition stxRange.start).line
      stop := map.lineStart ((map.toPosition stxRange.stop).line + 1) }
    let range := map.utf8RangeToLspRange range
    let json := Json.mkObj [("suggestion", text), ("range", toJson range), ("info", "")]
    Widget.saveWidgetInfo ``tryThisWidget json (.ofRange stxRange)

/-- Successively perform all string replacements in order. Slow. -/
def String.replace_list (s : String) : List (String × String) → String
| [] => s
| h::tail => (s.replace h.1 h.2).replace_list tail

/-- Try to remove distracting bits of the output of `#check`. This is
really a workaround which should be replaced by something smarter.  -/
def String.fix_decl (s : String) : String :=
  s.replace_list [(".{u_1}",""), (".{u_1, u_2}",""), (".{u_1, u_2, u_3}",""),
    ("Type u_1", "Type _"), ("Type u_2", "Type _"), ("Type u_3", "Type _"),
    ("inst✝ : ", ""), ("inst✝¹ : ", ""), ("inst✝² : ", ""), ("inst✝³ : ", ""),
    ("inst✝⁴ : ", ""), ("inst✝⁵ : ", ""), ("inst✝⁶ : ", ""), ("inst✝⁷ : ", ""),
    ("inst✝⁸ : ", ""), ("inst✝⁹ : ", "")]


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%$tk $id $sig:optDeclSig $[$val?]?) => withoutModifyingEnv do
    let declName := id.getId
    let some info := (← getEnv).find? declName
      | throwError "unknown constant '{declName}'"
    let declConst : Expr := mkConst declName <| info.levelParams.map Level.param
    discard <| liftTermElabM <| addTermInfo id declConst
    let (binders, _type?) := expandOptDeclSig sig
    if binders[0].isMissing && val?.isNone then -- User didn't provide any info
      let foo ← liftTermElabM <| PrettyPrinter.ppSignature declName
      liftTermElabM <| addTextSuggestion tk s!"recall {(toString foo.fmt).fix_decl}"

    let newId := mkIdentFrom id (← mkAuxName declName 1)
    if let some val := val? then
      let some infoVal := info.value?
        | throwErrorAt val "constant '{declName}' has no defined value"
      elabCommand <| ← `(noncomputable def $newId $sig:optDeclSig $val)
      let some newInfo := (← getEnv).find? newId.getId | return -- def already threw
      liftTermElabM 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 declConst
        let newVal := newInfo.value?.get!.instantiateLevelParams newInfo.levelParams mvs
        unless (← isDefEq infoVal newVal) do
          let err :=
            m!"value mismatch{indentExpr declConst}\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 := newId, binders, type?, value := .missing,
        ref := ← getRef, kind := default, modifiers := {}
      : DefView}]
      liftTermElabM do
        let elabView := (← elabHeaders views)[0]!
        unless (← isDefEq info.type elabView.type) do
          throwTypeMismatchError none info.type elabView.type declConst


recall add_assoc

There are many crappy things here. First the "Try this" replacement doesn't really work because it does not remove the identifier. This is probably easy to fix. More importantly, the two String functions at top are really dumb.

[Patrick Massot]

Note the new code in the recall command itself is only

    if binders[0].isMissing && val?.isNone then -- User didn't provide any info
      let foo ← liftTermElabM <| PrettyPrinter.ppSignature declName
      liftTermElabM <| addTextSuggestion tk s!"recall {(toString foo.fmt).fix_decl}"