[opentheory-users] a standalone tactic translating numeral encodings

[Ramana Kumar]

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
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20121017/02a8587b/attachment.html>