## Stream: general

### Topic: rec_fn_macro

#### Ben Sherman (May 21 2018 at 18:27):

I just updated Lean from 3.3.0 to 3.4.1, and now when I write this code:

axiom R : Type

inductive Sampler : Type
| Ret : Sampler
| BindUniform : (R → Sampler) → Sampler

def Bind : Sampler → (ℕ → Sampler) → Sampler
| Sampler.Ret f := f 0
| (Sampler.BindUniform k) f := Sampler.BindUniform (λ x, Bind (k x) f)


I get the error rec_fn_macro only allowed in meta definitions in the definition of Bind. Is this a bug? Should I submit it as a Github issue? Or do I just not understand what's going on?

#### Andrew Ashworth (May 21 2018 at 18:50):

whether or not it's a bug, lean 3.4.1 is the last release in the 3xx series and only critical issues are going to be fixed

#### Andrew Ashworth (May 21 2018 at 19:01):

if you change out axiom R for variable R do you get a more educational error message?

#### Andrew Ashworth (May 21 2018 at 19:07):

This is some kind of universe problem, I bet

#### Andrew Ashworth (May 21 2018 at 19:11):

maybe not. I just pasted it into my vscode and replaced axiom R with variable R. If you #print Sampler you get that the Sampler type is Type u -> Type u. Your definition is type incorrect. Now I'm confused why it ever worked in 3.3.0...

#### Andrew Ashworth (May 21 2018 at 19:13):

inductive Sampler : Type u₁ → Type u₁
constructors:
Sampler.Ret : Π (R : Type u₁), Sampler R
Sampler.BindUniform : Π {R : Type u₁}, (R → Sampler R) → Sampler R


#### Andrew Ashworth (May 21 2018 at 19:14):

huh, interesting. The definition is correct if you use axiom...

#### Kevin Buzzard (May 21 2018 at 19:30):

I guess a variable is something which, if mentioned in a definition, secretly appends itself as a "forall R : type" in front of definitions

#### Ben Sherman (May 21 2018 at 19:30):

Yeah, if I switch to using a variable or a parameter in a section, the definition goes through fine. And I don't think Sampler becomes universe-polymorphic in any case

#### Kevin Buzzard (May 21 2018 at 19:30):

whereas perhaps with an axiom this does not happen.

#### Kevin Buzzard (May 21 2018 at 19:31):

But isn't the error with Bind simply because Lean can't prove that the definition "terminates"?

#### Kevin Buzzard (May 21 2018 at 19:32):

cf the meta def of that 91 function in Programming In Lean, where the definition is OK but this is too hard for Lean to spot so you have to make it meta

#### Kevin Buzzard (May 21 2018 at 19:33):

axiom R : Type
variable S : Type

theorem X : R = R := rfl
theorem Y : S = S := rfl

#check X -- R = R
#check Y -- ∀ (S : Type), S = S


#### Kevin Buzzard (May 21 2018 at 19:35):

The axiom makes a new constant, like quotient.sound or whatever -- when you mention quotient.sound you don't get random "forall quotient.sound" hypotheses appearing in theorems

#### Kevin Buzzard (May 21 2018 at 19:35):

but the variable gets inserted. I guess you guys both know this.

#### Ben Sherman (May 21 2018 at 19:36):

@Kevin Buzzard No, this is actually a primitive recursive definition:

protected eliminator Sampler.rec : Π {real : Type} {C : Sampler real → Sort l},
C (Sampler.Ret real) →
(Π (a : real → Sampler real), (Π (a_1 : real), C (a a_1)) → C (Sampler.BindUniform a)) →
Π (n : Sampler real), C n


Notice how the inductive hypothesis allows you to apply the continuation to any argument.

#### Kevin Buzzard (May 21 2018 at 19:37):

I am suggesting that your definition of Bind relies on evaluating Bind elsewhere, does it not?

#### Kevin Buzzard (May 21 2018 at 19:38):

And with the definition of nat, Lean can use some recursion principle to check that the definition is good.

#### Kevin Buzzard (May 21 2018 at 19:40):

Presumably the error means "I find myself trying to prove that this definition of Bind has a decent recursor but I find myself trying to write some induction over functions, so I give up, make me meta so I don't have to worry about this sort of thing and can just be untrusted code"

heh

#### Kevin Buzzard (May 21 2018 at 19:41):

making the definition of Bind meta doesn't make the error go away :-)

#### Ben Sherman (May 21 2018 at 19:44):

So the definition works if I apply the recursor directly:

axiom real : Type

inductive Sampler : Type
| Ret : Sampler
| BindUniform : (real → Sampler) → Sampler

def Bind (x : Sampler) : (ℕ → Sampler) → Sampler
:= @Sampler.rec_on (λ _, (ℕ → Sampler) → Sampler) x
(λ f, f 0)
(λ k ih f, Sampler.BindUniform (λ x, ih x f))


So, even though the definition is primitive recursive, it does look to be something to do with it failing in figuring out the recursion scheme.

#### Kevin Buzzard (May 21 2018 at 20:08):

I am really confused by that recursor

#### Kevin Buzzard (May 21 2018 at 20:09):

(Π (a_1 : R), C (a a_1))

#### Kevin Buzzard (May 21 2018 at 20:12):

inductive Sampler : Type
| Ret : Sampler
| BindUniform : (ℤ → Sampler) → Sampler

def Bind : Sampler → (ℕ → Sampler) → Sampler
| Sampler.Ret f := f 0
| (Sampler.BindUniform k) f := Sampler.BindUniform (λ x, Bind (k x) f)


That works fine

#### Kevin Buzzard (May 21 2018 at 20:13):

replacing the constant with an explicit type

#### Kevin Buzzard (May 21 2018 at 20:22):

The definition with rec_on looks a bit funny to me -- k doesn't seem to play a role

oh I see

#### Kevin Buzzard (May 21 2018 at 20:23):

ih x is Bind (k x)

#### Kevin Buzzard (May 21 2018 at 20:24):

that's the role of ih

#### Ben Sherman (May 21 2018 at 20:26):

@Kevin Buzzard Yes, exactly!

#### Kevin Buzzard (May 21 2018 at 20:27):

so I finally understand the question :-)

#### Kevin Buzzard (May 21 2018 at 20:28):

so it is a bit weird that it will work for a concrete type like the integers but won't work for the constant, or at least it's weird to me

#### Ben Sherman (May 21 2018 at 20:28):

Right, and if you change from axiom to parameter or variable, it works again. So I'm thinking it's a bug.

#### Kevin Buzzard (May 21 2018 at 20:29):

well, with variable you change the type

#### Kevin Buzzard (May 21 2018 at 20:29):

so you have to fiddle with everything

#### Ben Sherman (Nov 08 2018 at 02:04):

I'm having another issue with rec_fn_macro: I've reduced it to this bug this time:

import analysis.real
def foo : bool → list ℝ
| tt := list.nil
| ff := 1/2 :: foo tt


I get the error:

equation compiler failed to generate bytecode for 'foo._main'
nested exception message:
code generation failed, VM does not have code for 'real.division_ring'


If I try to mark foo as noncomputable, I instead get an error about a failure to prove the recursion well-founded.
Does anyone have any idea for how to get around this issue?
In my actual code, I'm getting a rec_fn_macro issue that appears nonlocally - it's failing for a definition that calls some other function bar that involves division on ℝ. If I redefine bar as sorry, there is no longer any issue. But it doesn't even help for me to mark bar as irreducible.

#### Mario Carneiro (Nov 08 2018 at 02:09):

I don't see the issue. This is certainly noncomputable, and that's the error you get if you don't mark it so. And it is failing to prove the recursion is well founded because the default well founded instance on bool has tt and ff incomparable, so you can't do any recursion.

#### Mario Carneiro (Nov 08 2018 at 02:10):

perhaps you have oversimplified your example?

#### Ben Sherman (Nov 08 2018 at 02:15):

Thanks! I didn't know that details about the well-foundedness. Then I indeed oversimplified my example - originally it was nat. Let me backtrack with a revised example.

Last updated: May 17 2021 at 21:12 UTC