[opentheory-users] Scalable LCF-style proof translation

[Joe Leslie-Hurd]

Hi Alex,

> - So far, we haven't really tried to use the OpenTheory exporter from HOL
> Light on Flyspeck, mainly because it seemed to rely on all those annotations
> present in the sources, and having to put in these commands into the
> Flyspeck sources did not seem very attractive.

I'm sure it would be possible to implement an auto-export mode for
OpenTheory, perhaps using the theorem database as you did.

However, before attempting Flyspeck theorems I'd like to verify that
the OpenTheory article format is not causing a 10x space blow-up!

>> Cezary, Alex: Would it be possible to share this proof trace in the
>> two formats, so I can see what difference is responsible for the
>> blow-up?
>
> I must pass this question on to Cezary, who made this specific experiment.
> I'm not even sure whether this is before or after compression...

Cezary: I'd be most grateful if you could send me the data files you
used for this experiment.

> But just
> looking at the list of OpenTheory commands, it seems to me that building up
> substitutions as nested lists on the stack is rather complicated.

My gut feeling is that the list construction tax (cons and nil
commands) will occupy negligible space, but I'm prepared for the data
to prove me wrong.

Incidentally, how does your format encode lists (substituions or the
list of types that are an argument to type operators)?

> However, I have some further questions:
>
> - I wonder which of the offline processing that we do currently is actually
> done similarly by the existing opentheory infrastructure. By looking at some
> opentheory tool help texts, I couldn't see the answer to this question. Most
> of the commands seem to be concerned with package management, which is
> unrelated. Currently, we do
>
>   -- mark the last occurrence of any given object, to ensure deletion
>   -- strip material that is not relevant for some "exported" theorem

The opentheory tool post-processes articles extracted from theorem
provers, for compression and neatness purposes. To that end it does
both of the things you call out.

> - Do the existing exporters make use of the stack in any significant way
> apart from what is necessary to construct objects?

No.

> How does the HOL Light
> exporter deal with sharing (between terms)?

It adds every type, term and theorem to a dictionary, so each is only
exported once (per theory, when the dictionaries are reset).

> I assume for the HOL4 exporter
> this is not an issue, since sharing can be observed directly. Is this
> correct?

That's a question for Ramana, who's the maintainer of the HOL4
import/export infrastructure.

> - If I want to play with the tools, i.e., export some small theorem from HOL
> Light, apply some mapping (aka theory interpretation) and re-import into
> HOL4... Are there any step by step instructions that I can follow?

This FAQ describes the steps for exporting from HOL Light:

http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light

Ramana: I know I just asked you in another thread for some notes on
exporting from HOL4, but if you also made notes for importing I'd
create two new FAQs to put them in!

Cheers,

Joe