Tactic Mode : let rec doesn't create a variable in the env

Stream: lean4

[Luna]

I was working on MIL and one of the proofs used Nat.recOn. I'm used to working with match statements so I reformatted the definition to use let rec f := ... but then found out that f doesn't show up in the tactic state. And even more odd, the variable f is still useable (but not unfoldable). See below:

example : True := by
  let rec f (n : Nat) : Nat :=
    match n with
    | Nat.zero => 0
    | n + 1 => f n + 2

  -- f is not defined in the tactic state

  let four := f 2  -- but I can still use it
  unfold f at four  -- Tactic `unfold` failed: Local variable `f` has no definition
  sorry

[Aaron Liu]

this is expected

[Aaron Liu]

though I think the documentation could be better at explaining this

[Robin Arnez]

It elaborates into a mutual block, i.e.

mutual

def _example : True := by
  -- f is not defined in the tactic state

  let four := _example.f 2  -- but I can still use it
  unfold _example.f at four  -- Tactic `unfold` failed: Local variable `f` has no definition
  sorry

def _example.f (n : Nat) : Nat :=
  match n with
  | Nat.zero => 0
  | n + 1 => _example.f n + 2

end

and you can't refer to the definition of something else in the same mutual block

[Luna]

So if I want to be able to unfold the let definition, do I have to use Nat.recOn?

[Robin Arnez]

Yeah, or write an auxiliary definition:

def test.f (n : Nat) : Nat :=
  match n with
  | Nat.zero => 0
  | n + 1 => test.f n + 2

def test : True := by
  let four := test.f 2
  unfold test.f at four -- ""works"" (unfold doesn't rewrite let values)
  sorry

[Luna]

In my situation, test.f uses variables defined in test (but never recurses on test). So it will be much harder to pull out the definition. I'll most likely just continue with the Net.recOn option.

And I'm confused because unfold rewrites the following:

example : True := by
  let a := 1 + 1
  have : a = 2 := by unfold a; rfl
  sorry

[Eric Wieser]

let rec doesn't behave all that similarly to let, if anything it's closer to have

[Kyle Miller]

There's an informal proposal to make the let rec tactic add the auxiliary definition to the environment. It's at the cost of not being able to do mutual recursion between the let rec definition and the theorem, but (1) you can use the let rec term or a where clause if you want the current behavior and (2) people ask about let rec not being unfoldable inside theorems all the time (which is reasonable, since the common case for defining a recursive definition with a tactic proof is to want to use its definition).

One other justification for having the let rec tactic diverge from the behavior of the let rec term is that doing mutual recursion through the terms produced by tactics is somewhat brittle (it's always surprising to me when recursion from within an induction actually works), so given the benefit (being able to unfold definitions), it's not only an acceptable compromise, but arguably promoting writing more stable proofs.

[Eric Wieser]

I assume that a proposal to give a new have rec the current opaque semantics and give let rec the ones you explained (without variation between tactic and term mode) would not be well-received?

[Kyle Miller]

Tactic mode is special since there's a strict order for elaboration, which makes it clear how the proposed let rec tactic could work.

Your suggestion is worth considering, and a complete RFC ought to evaluate the idea. (With that idea, where clauses would be sugar for have rec instead.) It's a rather large breaking change, and my feeling is that inside of definitions the need for knowing the definition is small.

Maybe it's possible to generate equation lemmas for let recs on demand (probably a big project). If that were to happen, then in that future we could keep the let rec tactic being the let rec term. Perhaps that's reason enough to not pursue have rec?

[Eric Wieser]

I guess there's a related weaker proposal that is "make have permit the same syntax as let" (both rec and pattern matching), and leave dividing the semantics to a separate RFC