[opentheory-users] a standalone tactic translating numeral encodings

[Ramana Kumar]

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/20120820/439122d7/attachment.htm>