VM unreachable instruction has been reached

Stream: general

[Jiatong Yang]

I get "VM unreachable instruction has been reached" when I eval n. i know, of course, that n can't be calculated. But why I get this instead of "noncomputable" ?

axiom contra : false
def n : ℕ := contra.elim
#eval n

[Alex J. Best]

Noncomputable simply means that lean cannot generate executable code for the function.
The first thing to note is that docs#false.elim is a computable function, its code looks like this (in pseudo-code):

def false.elim(a : false):
-- check if a is any of the constructors of false
-- oh wait there are none
-- ok we are done
unreachable

this is a well defined function with executable code, albeit slightly useless..
You can see the code generated for any def using the opton set_option trace.compiler.code_gen true, it is

[compiler.optimize_bytecode]  false.elim 2
0: unreachable
1: ret

so if this function is ever called with an argument (which should be impossible) we get unreachable.
Now the reason you may be surprised by this is that axioms usually aren't computable either, we get some error about VM does not have code for blah instead.
What's happening is that false.elim is inlined and the compiler is smart enough to realise it doesn't really matter what the input is and so gets rid of the use of the axiom, leaving you with something like

def n():
-- check if _ is any of the constructors of false
-- oh wait there are none
-- ok we are done
unreachable

maybe the short answer is that if you add false as an axiom you are not really doing anything the system was designed for...

[Kyle Miller]

I believe the axiom is eliminated for another reason than inlining in this case, which is that contra is a proof, which is erased because proofs are computationally irrelevant. In any case, false.elim certainly is being inlined.

[Alex J. Best]

Good point, I forgot false was a Prop :grinning:!