This project is currently an implementation of a proof-checker. But it is planned to be extended; for example, to support algorithm extraction from intuitionistic proofs, which is considered to be an interesting feature.
0
stars
0
forks
source link
Its time to start making a template proof library #3
There were proposed several names for the library: STTL (standard template theorem library), STL, mb STLL.
It is a big deal to implement, not because it is hard (it is not), but because it is probably large.
I hope a library is possible that allows to avoid, e.g., exponential growth of proof size relative to human-checkable proof size; maybe, even polynomial blow-up may be avoided, but I am not sure.
For that purpose it proved useful to state lemmata as templates, that take a hypothesis as their argument as well, and work under it till the result. Note that two- or many- hypotheses templates are not necessary, as the corresponding merging/splitting mechanisms have already been partionally implemented on the very first test proof part (as "merging_hypotheses" and "splitting_hypotheses"). I am sure some utilities to shuffle hypotheses or like may be implemented as well, and then a one-hypothesis-templated lemma may be used just conjuncting the many hypotheses we now have, then applying, then splitting if needed
As for now, there are only two generic types of lemmas: for propositinal variables, and for natural numbers (assuming PA). But they may well be written as templates on formulas, as well; for example, some custom rules of inference that are implemented using standard. Many things can be done, and of course, other types of lemmata/theorems are also appreciated.
There were proposed several names for the library: STTL (standard template theorem library), STL, mb STLL.
It is a big deal to implement, not because it is hard (it is not), but because it is probably large. I hope a library is possible that allows to avoid, e.g., exponential growth of proof size relative to human-checkable proof size; maybe, even polynomial blow-up may be avoided, but I am not sure.
For that purpose it proved useful to state lemmata as templates, that take a hypothesis as their argument as well, and work under it till the result. Note that two- or many- hypotheses templates are not necessary, as the corresponding merging/splitting mechanisms have already been partionally implemented on the very first test proof part (as "merging_hypotheses" and "splitting_hypotheses"). I am sure some utilities to shuffle hypotheses or like may be implemented as well, and then a one-hypothesis-templated lemma may be used just conjuncting the many hypotheses we now have, then applying, then splitting if needed
As for now, there are only two generic types of lemmas: for propositinal variables, and for natural numbers (assuming PA). But they may well be written as templates on formulas, as well; for example, some custom rules of inference that are implemented using standard. Many things can be done, and of course, other types of lemmata/theorems are also appreciated.