rec_fn_macro

Stream: general

[Ben Sherman]

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]

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]

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

[Andrew Ashworth]

This is some kind of universe problem, I bet

[Andrew Ashworth]

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]

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]

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

[Kevin Buzzard]

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]

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]

whereas perhaps with an axiom this does not happen.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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

[Ben Sherman]

@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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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"

[Kevin Buzzard]

heh

[Kevin Buzzard]

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

[Ben Sherman]

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]

I am really confused by that recursor

[Kevin Buzzard]

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

[Kevin Buzzard]

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)

[Kevin Buzzard]

That works fine

[Kevin Buzzard]

replacing the constant with an explicit type

[Kevin Buzzard]

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

[Kevin Buzzard]

oh I see

[Kevin Buzzard]

ih x is Bind (k x)

[Kevin Buzzard]

that's the role of ih

[Ben Sherman]

@Kevin Buzzard Yes, exactly!

[Kevin Buzzard]

so I finally understand the question :-)

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

well, with variable you change the type

[Kevin Buzzard]

so you have to fiddle with everything

[Ben Sherman]

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]

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]

perhaps you have oversimplified your example?

[Ben Sherman]

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.