[opentheory-users] a standalone tactic translating numeral encodings

[Joe Leslie-Hurd]

Hi Ramana,

Since HOL4 has a different set of numerals from the OpenTheory
standard bit0 and bit1, I'd recommend building the numeral conversion
into the HOL4 interface - that way you'll have the theorem prover
infrastructure available to process general article files.

If you choose this route then you can import OpenTheory theories into
HOL4 as follows:

1. Define a bit0 constant that doubles its argument.

2. Read the theory binding the standard bit0 constant to the defined
constant in step 1.

3. When you need to import a theorem, first rewrite it using your
numconv and then look for a HOL4 theorem that matches.

4. Post-process the resulting set of theorems using numconv and make
them available inside HOL4.

Cheers,

Joe

On Wed, Oct 17, 2012 at 9:10 AM, Ramana Kumar <ramana at xrchz.net> wrote:
> Hi,
>
> I'm in the process of importing a package from HOL Light into HOL4.
> I've generated an OpenTheory article, which uses the Number.Natural.bit0,
> which HOL4 doesn't understand.
> I have the numconv tool, which does conversion from bit0/bit1 numbers to
> bit1/bit2 numbers, but it doesn't work on whole articles yet.
> I would like input on how to design it so that it will.
>
> Here is what numconv does:
>
> Translate numeral representations within a term, producing a theorem |-
> t[rep1] = t[rep2].
> The input term is represented by a simple article with a single theorem
> containing the term.
> The output theorem is represented by an ordinary article, based on axioms in
> the standard library, and a few extra ones about bit2 if necessary.
>
> What I would like:
>
> A tool to convert all numeral representations throughout an article, i.e.
> turn an article based on the standard library into one that only uses
> numeral constants relevant to the desired representation.
>
> Ideas on a good route to achieve that?
>
> Cheers,
> Ramana
>
>
> On Mon, Aug 20, 2012 at 8:52 PM, Ramana Kumar <ramana at xrchz.net> wrote:
>>
>> I have rewritten my standalone conversion between Norrish numerals and
>> binary numerals.
>>
>> The code now lives here: https://gitorious.org/hol/ot/trees/master (it is
>> numconv.hs)
>>
>> Changes/Features:
>>
>> Now translates in both directions: Norrish -> Binary and Binary -> Norrish
>> Translates numerals recursively within any term (doesn't require a bare
>> numeral as input)
>> Optional "rule mode" proves t |- t' rather than |- t = t'; maybe useful
>> for converting numerals in an already proved theorem and composing the
>> resulting articles.
>> Refactored into several reusable Haskell modules
>> Cleaned up code; it now doesn't emit any warnings with ghc's -Wall.
>>
>> I haven't tested it very much, especially in the from-binary direction.
>> Test articles and use cases would be appreciated. The axioms in that
>> direction are probably not in the standard library, but they are provable in
>> HOL4...
>>
>> The next task I want to do is figure out how best to create a kind of
>> "compatibility theory package" that would include those theorems (and other
>> common prover-specific theorems) that can be added to the "requires:" of a
>> package for easy use of packages coming out of specific provers.
>>
>> I look forward to your comments and tests for numconv :)
>> And if you have ideas for other standalone proof tools, the OpenTheory
>> Haskell modules are free to use.
>>
>>
>> On Fri, Apr 6, 2012 at 9:31 PM, Joe Hurd <joe at gilith.com> wrote:
>>>
>>> Yep, looks like it works fine now, in case we ever need to de-Norrish
>>> some numerals from HOL Light.
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>> On Thu, Apr 5, 2012 at 11:25 PM, Ramana Kumar <ramana.kumar at gmail.com>
>>> wrote:
>>> > My code works fine on this article. The problem was my CGI script. It
>>> > should
>>> > be fixed now.
>>> > (It had a call to runhaskell n2b.hs which got confused when called from
>>> > another directory, so now I've given it an absolute path to n2b.hs.)
>>> >
>>> > On Thu, Apr 5, 2012 at 11:10 PM, Joe Hurd <joe at gilith.com> wrote:
>>> >>
>>> >> Hi Ramana,
>>> >>
>>> >> > My guess is that you're generating an article with HOLLight.BIT2
>>> >> > rather
>>> >> > than
>>> >> > Number.Natural.bit2, but I haven't actually run your attempt.
>>> >> > If that's not the problem it would be helpful if you could send me
>>> >> > the
>>> >> > article that gets passed to the web tactic (or maybe I should have
>>> >> > some
>>> >> > infrastructure for saving it...)
>>> >>
>>> >> I've attached the article encoding the goal: FYI the opentheory
>>> >> summary for it is:
>>> >>
>>> >> $ opentheory info n2b-goal.art
>>> >> 3 input type operators: -> bool Number.Natural.natural
>>> >> 5 input constants: F Function.K Number.Natural.bit1
>>> >> Number.Natural.bit2
>>> >>  Number.Natural.zero
>>> >> 1 assumption:
>>> >>  |- Function.K F
>>> >>       (Number.Natural.bit2 (Number.Natural.bit1 (Number.Natural.bit2
>>> >> 0)))
>>> >> 1 theorem:
>>> >>  |- Function.K F
>>> >>       (Number.Natural.bit2 (Number.Natural.bit1 (Number.Natural.bit2
>>> >> 0)))
>>> >>
>>> >> > The function n2b near the top of the file is the algorithm.
>>> >> > It's been a while, so let's see if I can figure out the algorithm
>>> >> > just
>>> >> > by
>>> >> > reading that code...
>>> >>
>>> >> Your algorithm looks absolutely fine, and should scale up to any size
>>> >> of natural number that a theorem prover could conceivably process.
>>> >>
>>> >> Cheers,
>>> >>
>>> >> Joe
>>> >>
>>> >> _______________________________________________
>>> >> opentheory-users mailing list
>>> >> opentheory-users at gilith.com
>>> >> http://www.gilith.com/opentheory/mailing-list
>>> >>
>>> >
>>> >
>>> > _______________________________________________
>>> > opentheory-users mailing list
>>> > opentheory-users at gilith.com
>>> > http://www.gilith.com/opentheory/mailing-list
>>> >
>>>
>>> _______________________________________________
>>> opentheory-users mailing list
>>> opentheory-users at gilith.com
>>> http://www.gilith.com/opentheory/mailing-list
>>
>>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>