Reorganized Peano Directory

[Paul Merrell]

I just checked in a massive reorganization of the peano directory. I've kept the old version around because I did not finish getting everything in and I'm having a few issues with the new directory.

I've split peano_thms into more manageable and reasonable pieces. I've also reorganized the construction of the integers and rational numbers. I've created an interface file for the core components common to natural, integer, and rational arithmetic. We first prove it using the Peano axioms, then in the construction of the integers, and then in the construction of the rationals.

This gets tricky because I'm using the same theorem first proved for natural numbers to prove it for the integers. I'm using prefixes to avoid naming conflicts. (I only just discovered that they existed.) So I have two version of the operators (+ & n.+) and I have two versions of the theorems (addcom & n.addcom), but I don't want two different kinds so I'm using kindbind. This is causing problems. I haven't seen prefixes or kindbind used anywhere else, so this may be a new test for our verifier.

I've used kindbind to merge nat and n.nat, but I get errors like "expected nat got n.nat". I think we need to change the python verifier a little. The Javascript verifier doesn't have this problem. If I disable a couple of those checks everything verifies. The problem files are:

 peano_new/arithmetic/negative_min.gh

 peano_new/arithmetic/division_NaN.gh

 peano_new/arithmetic/division_min.gh

Paul

[Jim Kingdon]

Teaching those kind checks about kindbind makes sense to me.

I assume you found the kind tests in testsuite? There seem to be four test cases which hit the kind checks that were giving you problems. If the kind checks are put back, but with more kindbind smarts, then those tests would again pass, I suspect.

--
You received this message because you are subscribed to the Google Groups "Ghilbert" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ghilbert+u...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.

[Paul Merrell]

I fixed the tests. I updated verify.py to be smarter about kindbind. All the peano files pass.

The verify_all.py test has never worked for me. Certain files in general are giving me trouble. I'm using a Windows machine. It complains about Basic_operations_of_Zermelo-Fraenkel_set_theory.gh. I think it's because the "dash" character in the file name is not a standard dash -. Zermelo-Fraenkel_set_theory has the same problem.

Paul

[Jim Kingdon]

Cool! The fixed verify.py looks good.

As for the filenames, yes, that is an en dash (not a hyphen). Are you using NTFS or FAT? ( http://msdn.microsoft.com/en-us/library/windows/desktop/dd317748%28v=vs.85%29.aspx ). Not sure I know Windows well enough to really be sure what is going on.

As for the choice of en dash versus hyphen, it seems that style guides differ on this point (see https://en.wikipedia.org/wiki/Dash#Relationships_and_connections ). I'm also not sure I care as much in filenames as I would in the contents of the files themselves. Although I do sort of imagine we'll eventually run across something like β-completeness (not a real example) or something else where we'll wish we can use a full character set in filenames.

I checked in a few fixes to make verify_all.py work. Will be cool if we can get it working for you too, one way or another.

[Paul Merrell]

I've done more reorganization. Now the theorems for natural numbers, integers, rationals, reals, and complex numbers are in separate directories. There is a common directory for theorems that are true for several kinds of numbers. Next, I'll be working on a way to export theorems in one directory to another.

I've also added complex numbers. We don't really have real number working, but since everything is modular I decided to skip over that part.

I made a ton of changes. I checked everything several times, but I may have missed a mistake since verify_all is not working for me. I'm not sure if I have NTFS or FAT, but we shouldn't use en dashes if it break things.

Paul

[Jim Kingdon]

> I'm not sure if I have NTFS or FAT, but we shouldn't use en dashes if
it break things.

It's OK with me if you want to rename that file.

[Paul Merrell]

I renamed some files in the general directory. I got everything to verify for the first time on my machine. I migrated more theorems into the new peano directory and added some theorems related to real numbers (skipping the construction of real numbers). Next I plan to work on some typesetting. I going to see if I can get LaTex to work with Ghilbert. We really need something better for displaying fractions, square roots, binomial coefficients, summations, etc.

Paul

On Thu, Feb 6, 2014 at 8:32 AM, Jim Kingdon <jkingd...@gmail.com> wrote:

> I'm not sure if I have NTFS or FAT, but we shouldn't use en dashes if it break things.

It's OK with me if you want to rename that file.

--
You received this message because you are subscribed to the Google Groups "Ghilbert" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ghilbert+unsubscribe@googlegroups.com.

[Jim Kingdon]

MathML might be a bit more natural, as I have read that it is more logical and LaTeX is more typographical. But either one would probably work. There's a comparison at http://www.mathjax.org/about/latex-and-mathml/ . There's also ASCIIMathML: http://www1.chapman.edu/~jipsen/mathml/asciimath.html

Depends a bit on how we are using it (like is the LaTeX/whatever just generated from the ghilbert, and noone ever sees it except when they are adding new rules for typesetting new terms, or it is a bit more hands-on?).

To unsubscribe from this group and stop receiving emails from it, send an email to ghilbert+u...@googlegroups.com.

For more options, visit https://groups.google.com/groups/opt_out.

--
You received this message because you are subscribed to the Google Groups "Ghilbert" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ghilbert+u...@googlegroups.com.