One place where you can look for results of the translations is https://github.com/digama0/mm0/blob/build/mm0-lean/mm0/set/set.lean#L7625 , which is the output of the MM0 -> Lean translation. The variable names are currently kind of garbage because they aren't preserved through the translation process, and there are no notations so it's all direct references to the metamath internal names for the syntax constructors, but you should be able to see the general shape I outlined in the previous post and you can probably infer a lot more by looking around and comparing the theorems there to the original theorems from set.mm (note that hyphens become underscores in the translation).
The Haskell project is designed to be run using Stack, which ensures a consistent build environment. I believe it is possible to use ghc directly, but only if you give it a mountain of command line options. If your docker build supports stack, then the following should work: stack build mm0-hs stack exec mm0-hs which should produce a short error/help message detailing mm0-hs's command line options (of which to-hol is the most useful one for the present purpose). By the way, check out https://github.com/digama0/mm0/blob/build/mm0-lean/mm0/set/post.lean#L539 , which is a *complete* translation of dirith. It's a proof of Dirichlet's theorem in lean, in fully lean-native syntax, by modeling ZFC inside lean and translating the statement (including natural numbers, gcd, divisibility and infinitude) from the metamath notions to the analogous lean notions. On Sun, Jun 23, 2019 at 8:52 PM Cris Perdue <[email protected]> wrote: > Thanks Mario for your diligent efforts to explain your work on > translations from MM / MM0 to other logical languages, HOL in particular. I > can't say at this point that I properly understand everything you have > said, but it does look like the results of translation may indeed match > what I would hope for in a translation to HOL. I would like to explore this > further. Having Metamath theorems and proofs available for consumers of HOL > looks promising and interesting from my point of view. > > You refer to using the command mm0-hs to-hol in your repository. I am not > a Haskell user and am not exactly set up to run Haskell on the Mac > computers I use. On the other hand I do have Docker set up, and have > downloaded an official Haskell image from Docker Hub, which I expect I can > use to run scripts such as this one. The description at > https://hub.docker.com/_/haskell/ states that: > > This image ships a minimal Haskell toolchain (ghc and cabal-install) from > the upstream downloads.haskell.org > <https://launchpad.net/~hvr/+archive/ubuntu/ghc> Debian repository as > well as the Stack tool (https://www.haskellstack.org/). > > Can you give ghc command(s) to build the translator? I think I can figure > out how to run ghc commands within the Docker image, and work with files on > the host filesystem. And then, would I run the compiled Haskell in a > specific directory, e.g. one containing set.mm or an MM0 counterpart? > > Frankly, right now I would find translations of *statements* in Metamath > (or MM0) to statements in HOL more interesting than translations of the > proofs. OpenTheory claims to be low-level and surely not the only option > for translation of the proofs. > > You may already have files with the results of the translation(s). If some > of these might be available, perhaps that would be a good next step for me > rather than recreating the translations. What do you see as reasonable > options? > > Thanks much, > Cris > > > > On Tue, Jun 18, 2019 at 3:06 PM Mario Carneiro <[email protected]> wrote: > >> >> >> On Tue, Jun 18, 2019 at 6:01 PM Mario Carneiro <[email protected]> wrote: >> >>> In statements, this means that an application "wff x ph" is translated >>> to "wff (\x. ph x)" where "\x." is a lambda over x. >>> >> >> Oops, typo. That should read: >> >> In statements, this means that an application "wal x ph" is translated to >> "wal (\x. ph x)" where "\x." is a lambda over x. >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/CAFXXJSs9yPXUUBTGgGbUFETYr9d94mibpjk-kzK2z%3DM_LoA0VA%40mail.gmail.com >> <https://groups.google.com/d/msgid/metamath/CAFXXJSs9yPXUUBTGgGbUFETYr9d94mibpjk-kzK2z%3DM_LoA0VA%40mail.gmail.com?utm_medium=email&utm_source=footer> >> . >> > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/CAOoe%3DWJQ%3DPnZhYWRKP%3DjJsiEH7atLk7sEDQj8%3DfDbbn2ojnRjQ%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAOoe%3DWJQ%3DPnZhYWRKP%3DjJsiEH7atLk7sEDQj8%3DfDbbn2ojnRjQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvkDFw3Vw2rSAc1a-hDJ87wK%3Dcc_mmuMG4Ajb2S%3Ddod6w%40mail.gmail.com.
