Re: [isabelle] Proof by analogy and proof stability in Isabelle
This is the killer, I believe:
"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!"
Otherwise replaying proofs is uncritical.
Paul Jackson wrote:
>> Bodgan Greshuk wrote:
>>> 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.
> Tobias Nipkow <nipkow at in.tum.de> wrote:
>> 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.
> Hi Tobias,
> Jaroslav Sevcik implemented a proof recording and replay mechanism for
> HOL Light: see the section headed "HOL light proof replay" on his (ex)
> homepage http://homepages.inf.ed.ac.uk/s0566973/. He remarks there that
> proof replay cut the start-up time of HOL Light, which involves loading
> a lot of background theories, by about 50%.
> I was under the impression too that Coq stores proof terms and uses them
> for proof reconstruction.
> Is what you and Bogdan are discussing somehow different?
This archive was generated by a fusion of
Pipermail (Mailman edition) and