search

uds-psl / coq-library-undecidability

A library of mechanised undecidability proofs in the Coq proof assistant.
Mozilla Public License 2.0
111 stars 30 forks source link

Avoiding Let ... Qed #102

Open mrhaandi opened 3 years ago

mrhaandi commented 3 years ago

As pointed out in (https://github.com/coq/coq/issues/10459) and (https://github.com/coq/coq/issues/13584), semantics of Let ... Qed. are not coherent / future proof, and also slow down interface file vos compilation.

Currently, the library contains many such constructions, mostly concentrated in H10, MuRec, and TRAKHTENBROT. @DmxLarchey

Arguably, unless absolutely necessary, Let ... Qed should be replaced by (Local) Fact/Lemma/Theorem for less potential trouble in future, and faster compilation.

DmxLarchey commented 3 years ago

Well the fact that Let ... Qed is transparent in some way is a Coq bug. In general, I am not in favor of working around bugs, though this one might perhaps not be fixed anytime soon.

I could replace Let ... Qed with Local Fact ... Qed but this is not an ideal substitute since Local definitions are only local to the file (or module), they are not local to the section. This is the main reason I did use them in the first place. Obviously, 

Local Fact H : a = b. ... Qed.

is not a good naming convention but

Let H : a = b. ... Qed.

is fine since scope of the name H is limited to the current section. This is a way to split long proofs with lots of intermediate results into several lemmas that have not enough generality to justify their visibility outside of the proof.

So I could make an effort if the Let definition creates a critical bottleneck w.r.t. compilation time but I do not think it is a good practice in general, until I find some replacement for Let that has the same naming scope.

Right now, I do think the major bottleneck is still the automated construction of L terms.