Custom equation compiler

Stream: general

[Praneeth Kolichala]

While working on my computability refactor using trees, I am trying to automate as many primrec lemmas as possible. Ultimately, the dream is to be able to write something like derive primrec [list.foldr, list.sum, list.map] and have a tactic automatically prove that they are primitive recursive based on their structure.

To this end, I've written a generic recursion template tentatively called stack_rec -- because it explicitly keeps track of the arguments that would traditionally go on a stack. The idea is that pre does explicit preprocessing before passing arguments to the inductive hypothesis, and post does the post-processing given the result from the inductive step. For example the definition of stack_rec for a list is:

variables {α β : Type} {γ : Type*} (base : α → β) (pre : γ → list γ → α → α)
  (post : β → γ → list γ → α → β)

@[simp] def stack_rec : list γ → α → β
| [] a := base a
| (x :: xs) a := post (stack_rec xs (pre x xs a)) x xs a

And an example implementation is:

def nth_stack_rec {γ} (x : list γ) (n : ℕ) : option γ :=
x.stack_rec (λ _, none) (λ hd tl (n : ℕ), n.pred) (λ ih hd tl n, if n = 0 then some hd else ih) n

In other words, we preprocess by the argument n to the inductive hypothesis by subtracting 1. This corresponds directly to the definition:

def nth' : list γ → ℕ → option γ
| [] _ := none
| (hd :: tl) n := if n = 0 then some hd else let ih := nth' tl n.pred in ih

My question is, is there a way to take a recursively defined function and automatically put it in the stack_rec form? Obviously, not all Lean-defined functions can be written with stack_rec, but can we write a tactic that works on "usual" cases? The issue is that rewriting every function using stack_rec and proving their equivalence is cumbersome, but also requires no creativity and seems very routine. However, inspecting what the equation compiler outputs, it seems to use brec and below, rather than the usual rec. And there isn't much documentation on brec and what it does.

What would be the best way of finding the equivalent rec definition of a function, if one is available? (Going from rec to stack_rec seems quite doable).

[Junyan Xu]

brec and below (and I think all those auto-generated stuff) use rec under the hood; you can see by using #print (but I admit I can't immediately make sense of the output; I wasn't aware of their existence before):

#print list.brec_on
#print list.below
#print nat.brec_on
#print nat.below

@[reducible]
protected def list.brec_on : Π {T : Type u} {motive : list T → Sort l} (n : list T), (Π (n : list T), list.below T n → motive n) → motive n :=
λ {T : Type u} {motive : list T → Sort l} (n : list T) (F : Π (n : list T), list.below T n → motive n),
  (list.rec ⟨F list.nil punit.star, punit.star⟩
     (λ (hd : T) (tl : list T) (ih : pprod (motive tl) (list.below T tl)),
        ⟨F (hd :: tl) ⟨ih, punit.star⟩, ⟨ih, punit.star⟩⟩)
     n).fst

@[reducible]
protected def list.below : Π (T : Type u) {motive : list T → Sort l}, list T → Sort (max 1 l) :=
λ (T : Type u) {motive : list T → Sort l} (n : list T),
  list.rec punit (λ (hd : T) (tl : list T) (ih : Sort (max 1 l)), pprod (pprod (motive tl) ih) punit) n

@[reducible]
protected def nat.brec_on : Π {motive : ℕ → Sort l} (n : ℕ), (Π (n : ℕ), nat.below motive n → motive n) → motive n :=
λ {motive : ℕ → Sort l} (n : ℕ) (F : Π (n : ℕ), nat.below motive n → motive n),
  (nat.rec ⟨F 0 punit.star, punit.star⟩
     (λ (n : ℕ) (ih : pprod (motive n) (nat.below motive n)),
        ⟨F n.succ ⟨ih, punit.star⟩, ⟨ih, punit.star⟩⟩)
     n).fst

@[reducible]
protected def nat.below : (ℕ → Sort l) → ℕ → Sort (max 1 l) :=
λ (motive : ℕ → Sort l) (n : ℕ),
  nat.rec punit (λ (n : ℕ) (ih : Sort (max 1 l)), pprod (pprod (motive n) ih) punit) n

[Praneeth Kolichala]

It seems like these are trying to simulate a kind of strong induction, but I can't quite figure it out. Is there any documentation on what they actually do? Why are they multiplying by punit in nat.below and list.below (maybe for universe reasons?)