Re: [isabelle] Proof by analogy and proof stability in Isabelle
> Next, I will discuss proof stability in Isabelle.
> I was in USA recently, installed the same version of Isabelle there, and tried to compile my theory. In three places the compilation fails, because “auto” did not perform the job for some reason. I fix this by adding a little bit more explanation, but it may be not so simple next time. As a mathematician, I know that if I prove something, this is
> proved forever. For this reason I would prefer to have a proof which is extremely stable, even if non-readable.
Auto is deterministic and insensitive to the country it is run in. It is
sensitive to the version of Isabelle and the theories you run your
theories on top of.
> What is proof “by auto”? This is a sequence of some logical steps, which should be (I am sure) easy to unpack. Can I, after proving some lemma, get a fully unpacked version of proof, which is non-readable for human,
> but will be compiled in any version of Isabelle? Moreover, if the proofs of intermediate lemmas will also be unpacked, this proof would remain correct even if some intermediate lemmas disappear in the new version! If I will spend 5-6 month to prove a major result, I want to have such a proof for it, save it on my computer, and this would be like
> a “proof certificate”, extremely stable and valid forever (I know that if I submit the proof to Isabelle archive then somebody will take care, but this do not make me completely happy). Moreover, I need such a low-level proof for some other reasons, connected with proof analysis, and ideas about translation between different theorem provers. So, the question is, can I get somehow such a low-level stable proof of my lemmas? If yes, how? If no, the suggestion is to provide users with such a possibility.
Such an approach is feasible only in principle. You could write all the
proof objects out to a file, expanding all proofs of lemmas used.
Isabelle's proof terms even have a concrete syntax for that. This would
give you a stable but gigantic proof. The requirements in terms of time
and space would make it impossible to process these proofs effectively.
And you would have lost the readable version.
This archive was generated by a fusion of
Pipermail (Mailman edition) and