Add some of the tests from metamath-test (#57)

- Does not include anything which took a long time to run
- Does not include versions of set.mm and the like - we check those
elsewhere
- Emphasis is on failure tests

Author: jkingdon

tests/anatomy-bad1.expected

@@ -0,0 +1,16 @@
+MM> READ "anatomy-bad1.mm"
+Reading source file "anatomy-bad1.mm"... 699 bytes
+699 bytes were read into the source buffer.
+The source has 8 statements; 1 are $a and 1 are $p.
+No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
+if you want to check them.
+MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
+..................................................
+?Error on line 29 of file "anatomy-bad1.mm" at statement 8, label "wnew", type
+"$p":
+wnew $p wff ( s -> ( r -> p ) ) $= ws wr wp w2 ws $.
+                                               ^^
+After proof step 5 (the last step), the RPN stack contains 3 entries: "ws"
+(step 1), "w2" (step 4), and  "ws" (step 5).  It should contain exactly one
+entry.
+

tests/anatomy-bad1.in

@@ -0,0 +1 @@
+verify proof *

tests/anatomy-bad1.mm

@@ -0,0 +1,30 @@
+$( anatomy.mm $)
+
+$(
+                      PUBLIC DOMAIN DEDICATION
+
+This file is placed in the public domain per the Creative Commons Public
+Domain Dedication. http://creativecommons.org/licenses/publicdomain/
+
+Norman Megill - email: nm at alum.mit.edu
+
+$)
+
+
+$( This file is the introductory formal system example described
+   in Chapter 4 of the Metamath book, "Anatomy of a proof". $)
+
+$( Declare the constant symbols we will use $)
+$c ( ) -> wff $.
+$( Declare the metavariables we will use $)
+$v p q r s $.
+$( Declare wffs $)
+wp $f wff p $.
+wq $f wff q $.
+wr $f wff r $.
+ws $f wff s $.
+w2 $a wff ( p -> q ) $.
+
+$( Prove a simple theorem. $)
+wnew $p wff ( s -> ( r -> p ) ) $= ws wr wp w2 ws $.
+

tests/anatomy-bad2.expected

@@ -0,0 +1,15 @@
+MM> READ "anatomy-bad2.mm"
+Reading source file "anatomy-bad2.mm"... 696 bytes
+696 bytes were read into the source buffer.
+The source has 8 statements; 1 are $a and 1 are $p.
+No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
+if you want to check them.
+MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
+..................................................
+?Error on line 29 of file "anatomy-bad2.mm" at statement 8, label "wnew", type
+"$p":
+wnew $p wff ( s -> ( r -> p ) ) $= ws wr wp w2 $.
+                                            ^^
+After proof step 4 (the last step), the RPN stack contains 2 entries: "ws"
+(step 1) and  "w2" (step 4).  It should contain exactly one entry.
+

tests/anatomy-bad2.in

@@ -0,0 +1 @@
+verify proof *

tests/anatomy-bad2.mm

@@ -0,0 +1,30 @@
+$( anatomy.mm $)
+
+$(
+                      PUBLIC DOMAIN DEDICATION
+
+This file is placed in the public domain per the Creative Commons Public
+Domain Dedication. http://creativecommons.org/licenses/publicdomain/
+
+Norman Megill - email: nm at alum.mit.edu
+
+$)
+
+
+$( This file is the introductory formal system example described
+   in Chapter 4 of the Metamath book, "Anatomy of a proof". $)
+
+$( Declare the constant symbols we will use $)
+$c ( ) -> wff $.
+$( Declare the metavariables we will use $)
+$v p q r s $.
+$( Declare wffs $)
+wp $f wff p $.
+wq $f wff q $.
+wr $f wff r $.
+ws $f wff s $.
+w2 $a wff ( p -> q ) $.
+
+$( Prove a simple theorem. $)
+wnew $p wff ( s -> ( r -> p ) ) $= ws wr wp w2 $.
+

tests/anatomy-bad3.expected

@@ -0,0 +1,15 @@
+MM> READ "anatomy-bad3.mm"
+Reading source file "anatomy-bad3.mm"... 696 bytes
+696 bytes were read into the source buffer.
+The source has 8 statements; 1 are $a and 1 are $p.
+No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
+if you want to check them.
+MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
+..................................................
+?Error on line 29 of file "anatomy-bad3.mm" at statement 8, label "wnew", type
+"$p":
+wnew $p wff ( s -> ( r -> p ) ) $= wr wp w2 w2 $.
+                                            ^^
+At proof step 4, statement "w2" requires 2 hypotheses but the RPN stack
+contains only one entry, "w2" (step 3).
+

tests/anatomy-bad3.in

@@ -0,0 +1 @@
+verify proof *

tests/anatomy-bad3.mm

@@ -0,0 +1,30 @@
+$( anatomy.mm $)
+
+$(
+                      PUBLIC DOMAIN DEDICATION
+
+This file is placed in the public domain per the Creative Commons Public
+Domain Dedication. http://creativecommons.org/licenses/publicdomain/
+
+Norman Megill - email: nm at alum.mit.edu
+
+$)
+
+
+$( This file is the introductory formal system example described
+   in Chapter 4 of the Metamath book, "Anatomy of a proof". $)
+
+$( Declare the constant symbols we will use $)
+$c ( ) -> wff $.
+$( Declare the metavariables we will use $)
+$v p q r s $.
+$( Declare wffs $)
+wp $f wff p $.
+wq $f wff q $.
+wr $f wff r $.
+ws $f wff s $.
+w2 $a wff ( p -> q ) $.
+
+$( Prove a simple theorem. $)
+wnew $p wff ( s -> ( r -> p ) ) $= wr wp w2 w2 $.
+

tests/anatomy.expected

@@ -0,0 +1,9 @@
+MM> READ "anatomy.mm"
+Reading source file "anatomy.mm"... 699 bytes
+699 bytes were read into the source buffer.
+The source has 8 statements; 1 are $a and 1 are $p.
+No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
+if you want to check them.
+MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
+..................................................
+All proofs in the database were verified.