More weirdness with universe levels: max (u + 1) v not > 0?

Stream: new members

[Perrin Alaine-Sedano]

Hi, so I was playing around with exercise 3 in Induction and Recursion to define WellFounded.fix and got another weird error with universe levels. I realized that using Acc seemingly wouldn't work because it's of type Prop and thus can only eliminate to Prop. So I decided to define my own version like so:

inductive AccAttack {α : Sort u} (r : α → α → Prop) : α → Sort max 1 u where
  | intro (x : α) (h : ∀ y : α, r y x → AccAttack r y) : AccAttack r x

and then

inductive myBelow {α : Sort u} {r : α → α → Prop} (motive : {a : α} → AccAttack r a → Sort v) : AccAttack r a → Sort (max (u + 1) v) where
  | intro {a : α} {h : ∀ y, r y a → AccAttack r y} : (∀ (y : α) (hrya : r y a), myBelow motive (h y hrya)) → (∀ (y : α) (hrya : r y a  ), motive (h y hrya)) → (t : AccAttack r a) → myBelow motive t

I tried to define my own brecOn like this:

def accAttackBrecOn {α : Sort u} {r : α → α → Prop} {motive : {a : α} → AccAttack r a → Sort v} (f : {a : α} → (t : AccAttack r a) → myBelow motive t → motive t) {a : α} (t : AccAttack r a) : motive t :=
  let rec buildBelow {x : α} (t : AccAttack r x) : myBelow motive t :=
    match t with
    | AccAttack.intro x hy_ryx_accry => myBelow.intro
        (λ (y : α) (hrya : r y x) ↦ buildBelow (hy_ryx_accry y hrya))
        (λ (y : α) (hrya : r y x) ↦ f (hy_ryx_accry y hrya) (buildBelow (hy_ryx_accry y hrya)))
        (AccAttack.intro x hy_ryx_accry)

It gives a failure to prove termination error for buildBelow, saying

Cannot use parameter t:
  invalid universe level, max (u+1) v is not greater than 0

Except, isn't max (u+1) v always guaranteed to be greater than 0? It's not imax.

If I change it to Type (max u v) it works fine.

[Kyle Miller]

That "is not greater than 0" comes from an error generated by trying to decrement 1 from a universe level. I'm guessing some step is trying to turn Sort foo to Type foo' by solving for a foo' such that foo = foo' + 1 (with foo being max (u + 1) v).

[Kyle Miller]

So, yes, max (u + 1) v is greater than 0, but it can't see that by decrementing.

I'm not sure which part exactly is doing this, though the "cannot use parameter" error seems to be docs#Lean.Elab.Structural.tryAllArgs, part of the structural recursion system.

[Perrin Alaine-Sedano]

Kyle Miller

Thanks for explaining! Do you think my whole approach to solving this exercise is on the right track?

[Kyle Miller]

It might be cheating to use recursion to define your own brecOn, since that lets you take advantage of however Lean de-recursifies it. Maybe it would be better to use recursors directly?

[Kyle Miller]

(Regarding Sort (max 1 u), there was a recent discussion about "why doesn't use Lean use this instead of Sort (u + 1)?" This decrement failure is an interesting reason why not.)

[Perrin Alaine-Sedano]

@Kyle Miller Thanks. Is there a way I could do this using the built-in Acc instead? I thought of trying to use termination_by and decreasing_by but I'm not really sure how. For instance if sizeOf is a function from the type to Nat but it's not possible to eliminate Acc to anything but Prop then can it not be defined for Acc?

[Kyle Miller]

Perrin Alaine-Sedano said:

I realized that using Acc seemingly wouldn't work because it's of type Prop and thus can only eliminate to Prop.

Did you check that Acc.rec doesn't allow large elimination?

[Perrin Alaine-Sedano]

@Kyle Miller I think it does but it says it’s not supported by the code generator and I’d have to make the function non computable. I wanted to see if I could avoid this. Btw, is the reason Acc.rec and WellFounded.fix are non computable exactly this issue I’ve been running into, that inductive types of type Prop only eliminate to other types of type Prop?

[Kyle Miller]

No, noncomputability is an independent issue. That's simply that the current code generator doesn't support the recursors. Not even Nat.rec is supported (except by virtue of there being a @[csimp] lemma that replaces it with a compiled function that implements it).

You can check that Acc.rec has large elimination: the motive argument takes values in Sort u rather than just Prop.

[Perrin Alaine-Sedano]

@Kyle Miller Oh, okay. Is there any way to use large elimination with Acc then without making it noncomputable? If I can't use Acc.rec directly I've tried pattern matching and it gives errors about the resulting type not being Prop, it seems like it's using brecOn by default

[Kyle Miller]

Can you say why you want the function to be noncomputable? That's just an extra hoop to jump through that doesn't have theoretical significance, and it's something you can probably solve afterwards with @[csimp] lemmas.

I'd think a good first step is to use recursors directly (and avoid using match or recursive definitions, since these invoke high-powered machinery that can make use of Acc on your behalf) as an exercise to define WellFounded.fix.

[Kyle Miller]

Of course, it all depends on what your learning goals are. I just wouldn't worry about computability if you don't have a noncomputable version yet.

[Perrin Alaine-Sedano]

@Kyle Miller I want it to be computable, not noncomputable, which is why I was trying to avoid Acc.rec since it isn't supported by the code generator. Maybe I am overthinking all this though and should focus on the basics

[Kyle Miller]

I hear that, but I'm curious why you want computability. That's not a theoretical property. It's just a property of whether the code generator as it is implemented can compile it to C.

[Perrin Alaine-Sedano]

@Kyle Miller Partly just perfectionism I guess lol. Although also thought noncomputable might mean it can't be verified as correct by the kernel? Am I wrong about that?

[Kyle Miller]

Yes, that's wrong, and why I've been mentioning the code generator so much :-)

[Perrin Alaine-Sedano]

@Kyle Miller Ah okay. Thanks for clearing that up. So a noncomputable function can still type check correctly, can it not be run?

[Kyle Miller]

It can't be compiled into executables, that's all.

It still can be "run" inside the kernel.

[Kyle Miller]

Sometimes noncomputable is indicative of truly unrunnable definitions, because of the axiom of choice for example, but not here.

[Perrin Alaine-Sedano]

@Kyle Miller Oh okay. There's still a ton I have to learn about this. Is the only disadvantage then that it would be much slower than an executable?

[Kyle Miller]

Sure, if you're wanting to evaluate functions.

This has no bearing on kernel reasoning though (unless you accept using tactics like native_decide, which let the kernel call out to the compiler for answers)

[Perrin Alaine-Sedano]

@Kyle Miller Thanks! Sorry to be asking a ton of questions. There's one more thing I was wondering, is the fact that it's possible to do large elimination with Acc an instance of subsingleton elimination like I found here?

[Kyle Miller]

What I know about type theory I've picked up from using Lean, but that's my understanding!