Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
The PR experiments an implementation of the proposition made in CEP #42 of attributes sealed and unsealed that allows to indicate the opacity of a definition defined non-interactively, and that provides the current role of Qed/Defined without having to break the intuitive matching of keywords Theorem/Qed and Definition/Defined.
The main changes are:
the "opaque" value is now part of the Declare.Info.t while it was before passed as a standalone argument or stored in the program obligation state -> a better idea would be to have them in the CInfo.t actually, since they can be different for different components of a block of definitions
at Qed/Defined time, a check is done to determine if there is an attribute which takes precedence over the Qed/Defined keyword`;
for non-interactive declaration, either the default value associated to the kind of the declaration is used, or, in some cases, a specific opacity is decided upfront.
At the current time, there is a warning in case of a sealed/Defined or unsealed/Qed mismatch, as well as when the attribute is defined and there is mismatch Theorem/Defined or Definition/Qed. But the warning is deactivated because it is too much work to adapt the stdlib to the warning.
proux01
commented
2 days ago
The PR experiments an implementation of the proposition made in CEP #42 of attributes
sealedandunsealedthat allows to indicate the opacity of a definition defined non-interactively, and that provides the current role ofQed/Definedwithout having to break the intuitive matching of keywordsTheorem/QedandDefinition/Defined.The main changes are:
Declare.Info.twhile it was before passed as a standalone argument or stored in the program obligation state -> a better idea would be to have them in theCInfo.tactually, since they can be different for different components of a block of definitionsQed/Definedtime, a check is done to determine if there is an attribute which takes precedence over theQed/Definedkeyword`;At the current time, there is a warning in case of a
sealed/Definedorunsealed/Qedmismatch, as well as when the attribute is defined and there is mismatchTheorem/DefinedorDefinition/Qed. But the warning is deactivated because it is too much work to adapt the stdlib to the warning.