consider marking as noncomputable... again

Stream: lean4

[Edward van de Meent]

i was trying to formalize the fact that an inductive Fix as described in the new (unfinished) reference manual at the example at 3.2.4.3.2.2, does indeed give a contradiction. While doing so, i came across this gem of an error message:

set_option autoImplicit false

universe u u2

axiom Fix' : (Type u → Type u) → Type u
axiom Fix'.mk : {f:Type u → Type u} → f (Fix' f) → Fix' f

axiom Fix'.rec : {f:Type u → Type u} → {motive : Fix' f → Sort u2} →
  (mk: (a:f (Fix' f)) → motive (Fix'.mk a)) → (a:Fix' f) → motive a

def Bad' := Fix' (fun a => a → a)

noncomputable unsafe def Bad'.rec {motive : Bad'.{u} → Sort u2}
-- failed to compile definition, consider marking it as 'noncomputable'
    (mk: (a:Bad'.{u} → Bad'.{u}) → ((b:Bad'.{u}) → motive (a b)) → motive (Fix'.mk a))
    (a:Bad'.{u}) : motive a :=
  Fix'.rec (f := fun a => a → a) (fun v => mk v (fun b => Bad'.rec mk (v b))) a

i understand i'm trying to do something that should be hard to do with lean, (unsoundness and all that), but i'd at the very least hope that proving this is unsound should be possible somehow...

[Kim Morrison]

set_option autoImplicit false

universe u u2

axiom Fix' : (Type u → Type u) → Type u
axiom Fix'.mk : {f:Type u → Type u} → f (Fix' f) → Fix' f

axiom Fix'.rec : {f:Type u → Type u} → {motive : Fix' f → Sort u2} →
  (mk: (a:f (Fix' f)) → motive (Fix'.mk a)) → (a:Fix' f) → motive a

def Bad' := Fix' (fun a => a → a)

noncomputable section

unsafe def Bad'.rec {motive : Bad'.{u} → Sort u2}
-- failed to compile definition, consider marking it as 'noncomputable'
    (mk: (a:Bad'.{u} → Bad'.{u}) → ((b:Bad'.{u}) → motive (a b)) → motive (Fix'.mk a))
    (a:Bad'.{u}) : motive a :=
  Fix'.rec (f := fun a => a → a) (fun v => mk v (fun b => Bad'.rec mk (v b))) a

end

#check Bad'.rec

[Edward van de Meent]

thanks! still, i'm curious why this version doesn't give the warning?

[Kyle Miller]

It seems that the code ignores noncomputable when you do unsafe. There should probably be a warning when you use noncomputable here since there's no point in making the definition. The only thing you can do with unsafe code is evaluate it.

[Eric Wieser]

You can also inspect its type with type_of%!

[Mario Carneiro]

You can also typecheck it. I think the existing "linter error" saying that you shouldn't use unsafe theorem is too aggressive

[Edward van de Meent]

Wait, is there an issue with the type?

[Mario Carneiro]

I don't think so

[Edward van de Meent]

Then how does inspecting the type help?

[Mario Carneiro]

I guess it's just a general comment about things you can do with unsafe noncomputable definitions

[Mac Malone]

Kyle Miller said:

It seems that the code ignores noncomputable when you do unsafe. There should probably be a warning when you use noncomputable here since there's no point in making the definition.

I (with approval) removed a previous error on noncomputable unsafe in lean4#3647, because I make use of it in Alloy to generate opaque definitions without code and then attach the code later. While that works now, it seems I missed somewhere else in the code were unsafe definitions ignore noncomputable.