Zulip Chat Archive

Stream: general

Topic: rec_fn_macro


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Andrew Ashworth (May 21 2018 at 19:07):

This is some kind of universe problem, I bet

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip Andrew Ashworth (May 21 2018 at 19:14):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 21 2018 at 19:30):

whereas perhaps with an axiom this does not happen.

view this post on Zulip 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"?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 21 2018 at 19:35):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 21 2018 at 19:37):

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

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (May 21 2018 at 19:40):

heh

view this post on Zulip Kevin Buzzard (May 21 2018 at 19:41):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 21 2018 at 20:08):

I am really confused by that recursor

view this post on Zulip Kevin Buzzard (May 21 2018 at 20:09):

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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (May 21 2018 at 20:12):

That works fine

view this post on Zulip Kevin Buzzard (May 21 2018 at 20:13):

replacing the constant with an explicit type

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 21 2018 at 20:23):

oh I see

view this post on Zulip Kevin Buzzard (May 21 2018 at 20:23):

ih x is Bind (k x)

view this post on Zulip Kevin Buzzard (May 21 2018 at 20:24):

that's the role of ih

view this post on Zulip Ben Sherman (May 21 2018 at 20:26):

@Kevin Buzzard Yes, exactly!

view this post on Zulip Kevin Buzzard (May 21 2018 at 20:27):

so I finally understand the question :-)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 21 2018 at 20:29):

well, with variable you change the type

view this post on Zulip Kevin Buzzard (May 21 2018 at 20:29):

so you have to fiddle with everything

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 08 2018 at 02:10):

perhaps you have oversimplified your example?

view this post on Zulip 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