[opentheory-users] a standalone tactic translating numeral encodings

[Michael Norrish]

Can you prepend the OT theory file with one that defines the bit0 and bit1 
constants in terms of bit2 and bit1, thereby "masking" out those definitions 
when the two articles are merged?  I assume your existing numconv code would 
give you something that you could append to the OT article to mask the 
occurrences of bit0 and bit1 in the output theorems.

Michael

On 18/10/12 03:10, Ramana Kumar 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
> <mailto: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
>     <mailto: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
>         <mailto: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
>         <mailto: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 <mailto:opentheory-users at gilith.com>
>          >> http://www.gilith.com/opentheory/mailing-list
>          >>
>          >
>          >
>          > _______________________________________________
>          > opentheory-users mailing list
>          > opentheory-users at gilith.com <mailto:opentheory-users at gilith.com>
>          > http://www.gilith.com/opentheory/mailing-list
>          >
>
>         _______________________________________________
>         opentheory-users mailing list
>         opentheory-users at gilith.com <mailto: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
>