Hott3: Theorems, lemmas, axioms

Stream: general

[Thomas Eckl]

It is annoying that in the hott3-mode you cannot freely use theorem, lemma, axiom because no conclusion is of type Prop (in the sense of Sort 0), so Lean3 will from time to time produce a code generation failed, VM does not have code for ... message. For me, labelling facts as Theorems, Lemmas, Axioms and so on is a useful way to organise code and make it more readable.

I am wondering whether one can redefine their usage, maybe in the hott attribute, in the following way: You are allowed to use them if the conclusion is of type Prop in the HoTT sense, or if the type satisfies is_prop (maybe relying on the class-instance mechanism). Is there anything which prevents you from doing it, like protected names etc? I did not do much meta-programming up to now, so don't want to start something which is hopeless anyway.

Here is also a related and more immediate problem: At one point in my code Lean complained that VM does not have code for 'hott.trunc.is_trunc_trunc'. Now, hott.trunc.is_trunc_trunc is declared as an axiom in init.hit of the hott3 library. Shouldn't that be changed to a constant, as it was in the Lean2 Hott library? Or is there a reason for calling it an axiom now? If not, what's the best way to correct it? If I change it in my init.hit file, do I have to recompile the hott3 library? And shall I raise an issue in GiTHub?

[Sebastian Ullrich]

axiom and constant are synonyms in Lean 3

[Sebastian Ullrich]

It's been a while, but can't you use noncomputable theory (after the imports) to ignore the code generation error?

[Thomas Eckl]

Neither adding noncomputable theory at the top of the file nor noncomputable in front of the def removes the code generation error. Is that a problem? Or does the noncomputable just prevent Lean to complain on (noncomputable) future uses of the definition?

[Floris van Doorn]

It is not easy to redefine what def does vs lemma/theorem. That is hard-coded in C++, so that would require a change in Lean itself. I agree it is annoying that you have to call everything def instead of freely choosing lemma/theorem.

About the VM error: I don't know what causes that. Writing hott_theory automatically marks that file as noncomputable theory, and that should solve it. I remember that I've seen that error for incomplete definitions, or definitions with also some other error. If that was not the case, could you post a #mwe?

[Thomas Eckl]

When trying to minimise the code and erasing some let ... in the VM error vanished. No explanation for this, but who cares ... Your hint helped, and I will live with def.