let rec and refine

Stream: lean4

[Alex Sanchez-Stern]

Are there plans to allow using let rec with refine? Like:

def foo: Nat -> Nat := by {
   refine let rec f (n : Nat): Nat := ?_; f
}

Ideally this should produce a goal with n : Nat and f: Nat -> Nat in the context and Nat as the goal, though not sure if this interacts with the termination checker in a weird way. Right now it just gives an error on the ?_ saying "don't know how to synthesize placeholder".

I'm essentially trying to use this to produce a computable recursive function in tactic mode, because of the limitations of functions generated using induction. Writing a top level recursive definition doesn't work because I'm trying to build some machinery for automatically synthesizing Equivs between certain types.

[Robin Arnez]

Well, let rec more or less defines a top-level recursive definition though

[Alex Sanchez-Stern]

Sure, but it can be generated using tactics in a way that top-level recursive definitions can't. If necessary, I'll go up a level and use more general metaprogramming constructs, but this seems like a reasonable thing to support at the tactic level.

[Wrenna Robson]

My feeling is I don't know what you're doing exactly but you almost certainly shouldn't do it like this.

[Alex Sanchez-Stern]

You're saying, it shouldn't be possible to prove two types Equiv just using tactics? Or that it only shouldn't be possible when the types are inductive? For non-recursive types like structures it works just fine.

[Aaron Liu]

You shouldn't use tactics to construct data

[Yves Jäckle]

@Alex Sanchez-Stern
You can get a sort of computable induction with this workaround:

universe u

@[elab_as_elim]
def Nat.compRec {motive : Nat → Sort u}
  (zero : motive Nat.zero) (succ : (n : Nat) → motive n → motive n.succ)
  (t : Nat) : motive t :=
  match t with
  | 0 => zero
  | .succ n => succ n (Nat.compRec zero succ n)


def factorial : Nat → Nat := fun n => by {
  induction n using Nat.compRec with
  | zero => exact 1
  | succ n sofar => exact sofar*(n+1)
}

#eval factorial 2
#eval factorial 3
#eval factorial 4

[Robin Arnez]

You shouldn't do that though...

[Robin Arnez]

There's much better support for functions written with recursion.

[Alex Sanchez-Stern]

I mean, I wouldn't try to commit something with tactic-written functions to mathlib, but there are a lot of different applications of Lean where being able to prove types equivalent purely using bounded automation is useful. I care a lot about being able to use the tooling in a way that fully respects the curry-howard correspondence and doesn't have things you can only write in "proof style" or "program style"

[Robin Arnez]

You can also create global declarations using tactics (including recursive ones), if that's part of the concern. For that you can see docs#Lean.Elab.addPreDefinitions

[Alex Sanchez-Stern]

Ah, that does seem useful, thanks!