From 3441655a126f9799f40f50e52b08dc10cab48a57 Mon Sep 17 00:00:00 2001 From: Gino Giotto Date: Fri, 17 Nov 2023 00:41:17 +0100 Subject: [PATCH 1/3] add test cases about minimization --- tests/min_found.expected | 29 +++++++++++++++++++++++++++++ tests/min_found.in | 4 ++++ tests/min_found.mm | 31 +++++++++++++++++++++++++++++++ tests/min_not_found.expected | 24 ++++++++++++++++++++++++ tests/min_not_found.in | 4 ++++ tests/min_not_found.mm | 31 +++++++++++++++++++++++++++++++ 6 files changed, 123 insertions(+) create mode 100644 tests/min_found.expected create mode 100644 tests/min_found.in create mode 100644 tests/min_found.mm create mode 100644 tests/min_not_found.expected create mode 100644 tests/min_not_found.in create mode 100644 tests/min_not_found.mm diff --git a/tests/min_found.expected b/tests/min_found.expected new file mode 100644 index 00000000..784f4b41 --- /dev/null +++ b/tests/min_found.expected @@ -0,0 +1,29 @@ +MM> READ "min_found.mm" +Reading source file "min_found.mm"... 775 bytes +775 bytes were read into the source buffer. +The source has 18 statements; 5 are $a and 2 are $p. +SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database. +No errors were found. However, proofs were not checked. Type VERIFY PROOF * +if you want to check them. +MM> Continuous scrolling is now in effect. +MM> 0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100% +.................................................. +All proofs in the database were verified in x.xx s. +MM> Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit. +You will be working on statement (from "SHOW STATEMENT th2"): +18 th2 $p D $= ... $. +Note: The proof you are starting with is already complete. +MM-PA> Bytes refer to compressed proof size, steps to uncompressed length. +Scanning forward through statements... +Proof of "th2" decreased from 24 to 15 bytes using "in1". +Scanning backward through statements... +Proof of "th2" decreased from 24 to 15 bytes using "in1". +The forward scan results were used. +MM-PA> Proof of "th2": +---------Clip out the proof below this line to put it in the source file: + ( ax-1 in1 ) AB $. +---------The proof of "th2" (15 bytes) ends above this line. +MM-PA> EXIT +Warning: You have not saved changes to the proof of "th2". +Do you want to EXIT anyway (Y, N) ? Y +Exiting the Proof Assistant. Type EXIT again to exit Metamath. diff --git a/tests/min_found.in b/tests/min_found.in new file mode 100644 index 00000000..b2c80251 --- /dev/null +++ b/tests/min_found.in @@ -0,0 +1,4 @@ +verify proof * +prove th2 +minimize * /allow * +show new /compressed diff --git a/tests/min_found.mm b/tests/min_found.mm new file mode 100644 index 00000000..e051f936 --- /dev/null +++ b/tests/min_found.mm @@ -0,0 +1,31 @@ +$( A shortening found by the minimizer. The comparison with min-not-found.mm + suggests that the minimizer's ability to detect this one depends on the + presence of statement "A" in at least one of the steps of the minimized + proof. Axiom ax-3 and costant C are not used here, but they are kept + anyway to lessen the amount of differences with min-found.mm. $) + + $c A B C D $. + + ax-1 $a A $. + ax-2 $a B $. + ax-3 $a C $. + + ${ + in1.1 $e A $. + in1 $a D $. + $} + + ${ + in2.1 $e B $. + in2.2 $e A $. + in2.3 $e B $. + in2.4 $e B $. + in2.5 $e B $. + in2 $a D $. + $} + + $( Minimized proof, found automatically. (New usage is discouraged.) $) + th1 $p D $= ( ax-1 in1 ) AB $. + + $( Non-minimized proof. $) + th2 $p D $= ( ax-2 ax-1 in2 ) ABAAAC $. diff --git a/tests/min_not_found.expected b/tests/min_not_found.expected new file mode 100644 index 00000000..12f8f8ba --- /dev/null +++ b/tests/min_not_found.expected @@ -0,0 +1,24 @@ +MM> READ "min_not_found.mm" +Reading source file "min_not_found.mm"... 762 bytes +762 bytes were read into the source buffer. +The source has 18 statements; 5 are $a and 2 are $p. +SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database. +No errors were found. However, proofs were not checked. Type VERIFY PROOF * +if you want to check them. +MM> Continuous scrolling is now in effect. +MM> 0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100% +.................................................. +All proofs in the database were verified in x.xx s. +MM> Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit. +You will be working on statement (from "SHOW STATEMENT th2"): +18 th2 $p D $= ... $. +Note: The proof you are starting with is already complete. +MM-PA> Bytes refer to compressed proof size, steps to uncompressed length. +Scanning forward through statements... +No shorter proof was found. +MM-PA> Proof of "th2": +---------Clip out the proof below this line to put it in the source file: + ( ax-2 ax-3 in2 ) ABAAAC $. +---------The proof of "th2" (24 bytes) ends above this line. +MM-PA> EXIT +Exiting the Proof Assistant. Type EXIT again to exit Metamath. diff --git a/tests/min_not_found.in b/tests/min_not_found.in new file mode 100644 index 00000000..b2c80251 --- /dev/null +++ b/tests/min_not_found.in @@ -0,0 +1,4 @@ +verify proof * +prove th2 +minimize * /allow * +show new /compressed diff --git a/tests/min_not_found.mm b/tests/min_not_found.mm new file mode 100644 index 00000000..0c0d4f87 --- /dev/null +++ b/tests/min_not_found.mm @@ -0,0 +1,31 @@ +$( A shortening not found by the minimizer. The comparison with min-found.mm + suggests that the minimizer's inability to detect it is due to the absence + of statement "C" in any of the steps of the minimized proof. The + shortening is detected if proveFloating is set to 1 in minimizeProof, + which allows absent "$e" statements to be found. $) + + $c A B C D $. + + ax-1 $a A $. + ax-2 $a B $. + ax-3 $a C $. + + ${ + in1.1 $e A $. + in1 $a D $. + $} + + ${ + in2.1 $e B $. + in2.2 $e C $. + in2.3 $e B $. + in2.4 $e B $. + in2.5 $e B $. + in2 $a D $. + $} + + $( Minimized proof, not found automatically. (New usage is discouraged.) $) + th1 $p D $= ( ax-1 in1 ) AB $. + + $( Non-minimized proof. $) + th2 $p D $= ( ax-2 ax-3 in2 ) ABAAAC $. From f5de6df9b06428a2921c6b5db2f05c303c4cd6ab Mon Sep 17 00:00:00 2001 From: Gino Giotto Date: Fri, 17 Nov 2023 01:04:02 +0100 Subject: [PATCH 2/3] corrections --- tests/min_found.expected | 4 ++-- tests/min_found.mm | 10 +++++----- tests/min_not_found.expected | 4 ++-- tests/min_not_found.mm | 6 +++--- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/tests/min_found.expected b/tests/min_found.expected index 784f4b41..320e8bfa 100644 --- a/tests/min_found.expected +++ b/tests/min_found.expected @@ -1,6 +1,6 @@ MM> READ "min_found.mm" -Reading source file "min_found.mm"... 775 bytes -775 bytes were read into the source buffer. +Reading source file "min_found.mm"... 761 bytes +761 bytes were read into the source buffer. The source has 18 statements; 5 are $a and 2 are $p. SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database. No errors were found. However, proofs were not checked. Type VERIFY PROOF * diff --git a/tests/min_found.mm b/tests/min_found.mm index e051f936..5592a6c5 100644 --- a/tests/min_found.mm +++ b/tests/min_found.mm @@ -1,8 +1,8 @@ -$( A shortening found by the minimizer. The comparison with min-not-found.mm - suggests that the minimizer's ability to detect this one depends on the - presence of statement "A" in at least one of the steps of the minimized - proof. Axiom ax-3 and costant C are not used here, but they are kept - anyway to lessen the amount of differences with min-found.mm. $) +$( A shortening found by the minimizer. The comparison with min_not_found.mm + suggests that the minimizer's ability to detect it depends on the presence + of statement "A" in the steps of the minimized proof. The costant C and + axiom ax-3 are not used here, but they are kept anyway to lessen the amount + of differences with min_not_found.mm. $) $c A B C D $. diff --git a/tests/min_not_found.expected b/tests/min_not_found.expected index 12f8f8ba..673dbf56 100644 --- a/tests/min_not_found.expected +++ b/tests/min_not_found.expected @@ -1,6 +1,6 @@ MM> READ "min_not_found.mm" -Reading source file "min_not_found.mm"... 762 bytes -762 bytes were read into the source buffer. +Reading source file "min_not_found.mm"... 787 bytes +787 bytes were read into the source buffer. The source has 18 statements; 5 are $a and 2 are $p. SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database. No errors were found. However, proofs were not checked. Type VERIFY PROOF * diff --git a/tests/min_not_found.mm b/tests/min_not_found.mm index 0c0d4f87..8799ec1b 100644 --- a/tests/min_not_found.mm +++ b/tests/min_not_found.mm @@ -1,8 +1,8 @@ -$( A shortening not found by the minimizer. The comparison with min-found.mm +$( A shortening not found by the minimizer. The comparison with min_found.mm suggests that the minimizer's inability to detect it is due to the absence of statement "C" in any of the steps of the minimized proof. The - shortening is detected if proveFloating is set to 1 in minimizeProof, - which allows absent "$e" statements to be found. $) + shortening is detected if proveFloating is set to 1 in replaceStatement + called by minimizeProof, which allows absent $e statements to be found. $) $c A B C D $. From b3d544cef88df4ca4e28119c2f98cc5851211795 Mon Sep 17 00:00:00 2001 From: Gino Giotto Date: Fri, 17 Nov 2023 02:50:16 +0100 Subject: [PATCH 3/3] typo --- tests/min_not_found.expected | 4 ++-- tests/min_not_found.mm | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/min_not_found.expected b/tests/min_not_found.expected index 673dbf56..f631f63f 100644 --- a/tests/min_not_found.expected +++ b/tests/min_not_found.expected @@ -1,6 +1,6 @@ MM> READ "min_not_found.mm" -Reading source file "min_not_found.mm"... 787 bytes -787 bytes were read into the source buffer. +Reading source file "min_not_found.mm"... 788 bytes +788 bytes were read into the source buffer. The source has 18 statements; 5 are $a and 2 are $p. SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database. No errors were found. However, proofs were not checked. Type VERIFY PROOF * diff --git a/tests/min_not_found.mm b/tests/min_not_found.mm index 8799ec1b..3b67065f 100644 --- a/tests/min_not_found.mm +++ b/tests/min_not_found.mm @@ -24,7 +24,7 @@ in2 $a D $. $} - $( Minimized proof, not found automatically. (New usage is discouraged.) $) + $( Minimized proof, not found automatically. (New usage is discouraged.) $) th1 $p D $= ( ax-1 in1 ) AB $. $( Non-minimized proof. $)