Add hypothesis and dv usage qualifiers to VERIFY PROOF #92

jamesjer · 2022-06-27T19:31:10Z

Regarding the discussion at metamath/set.mm#2648, here is one way metamath-exe could be enhanced to show some unused elements of metamath databases. This PR adds the following qualifiers to VERIFY PROOF:

/DISJOINT_VARS checks for unused non-dummy dvs
/ALL_DISJOINT_VARS check for all unused dvs
/ESSENTIAL checks for unused $e statements
/FLOATING checks for unused $f statements
/HYPOTHESES is /ESSENTIAL and /FLOATING combined

wlammen · 2022-06-28T05:13:55Z

Can look into this, but probably not before weekend.

wlammen · 2022-07-02T10:05:35Z

src/mmveri.h

@@ -11,14 +11,24 @@

 #include "mmdata.h"

-char verifyProof(long statemNum);
+/* Flags for verifyProof */


When declaring new constants, comment their semantics at this point. All development environments I know of will automatically look up that lines and present an excerpt to the developer on request.

wlammen · 2022-07-02T10:06:39Z

src/mmveri.h

-  long statementNum, long step, flag unkHypFlag);
+  long statementNum, long step, flag unkHypFlag,
+    /* For checking for unused $d conditions: */
+  flag verifyFlag, nmbrString *djRVar, nmbrString *djOVar);


A comment starting with /*! is a typical doxygen command. Try to follow that scheme and use /param to explain the parameters you introduced. How does your addition affect the error behaviour? Will it throw exceptions not seen before? Can you establish pre- / post-conditions or invariants with respect to your added code? Use doxygen /pre /post and /invariant tags to describe these and allow test code designers to write a test suite later.

wlammen · 2022-07-02T10:10:16Z

src/mmveri.c

@@ -18,11 +18,16 @@ struct getStep_struct getStep = {0, 0, 0, 0, 0,
    NULL_PNTRSTRING};

 /* Verify proof of one statement in source file.  Uses wrkProof structure.
-   Assumes that parseProof() has just been called for this statement. */
+   Assumes that parseProof() has just been called for this statement.


Suggest to convert this into a doxygen style comment starting with /*! . Use tags to categorize the individual portions of the comment.

wlammen · 2022-07-02T10:10:50Z

src/mmveri.c

@@ -18,11 +18,16 @@ struct getStep_struct getStep = {0, 0, 0, 0, 0,
    NULL_PNTRSTRING};

 /* Verify proof of one statement in source file.  Uses wrkProof structure.
-   Assumes that parseProof() has just been called for this statement. */


This is a typical pre-condition, so mark it with /PRE

wlammen · 2022-07-02T10:12:24Z

src/mmveri.c

@@ -18,11 +18,16 @@ struct getStep_struct getStep = {0, 0, 0, 0, 0,
    NULL_PNTRSTRING};

 /* Verify proof of one statement in source file.  Uses wrkProof structure.
-   Assumes that parseProof() has just been called for this statement. */
+   Assumes that parseProof() has just been called for this statement.
+   If verifyFlag includes VERIFY_DVS, check for unused $d conditions on nondummy


This describes the second parameter, so start the line with /PARAM verifyFlag

wlammen · 2022-07-02T13:40:28Z

src/mmveri.c

@@ -103,6 +136,14 @@ char verifyProof(long statemNum)
      g_WrkProof.mathStringPtrs[step] =
          g_Statement[stmt].mathString;

+      if (verifyFlag & VERIFY_ESSENTIAL) {


I don't see where the usage of a $f is registered. If I call verifyProof with VERIFY_FLOATING, how is the reference of a floating hypothesis recorded in essVar?

wlammen · 2022-07-02T13:46:23Z

src/mmveri.c

 /* Returns 0 if proof is OK; 1 if proof is incomplete (has '?' tokens);
   returns 2 if error found; returns 3 if not severe error
   found; returns 4 if not a $p statement */
-char verifyProof(long statemNum)
+char verifyProof(long statemNum, flag verifyFlag)


This function is way to long, and the loop traversing the proof steps has several 'continue' shortcuts built in. Without interspersed post-condition assertions I find it hard to check for correctness. Consider extracting blocks of code to separate helper routines with a telling name.

wlammen · 2022-07-02T13:48:39Z

src/mmveri.c

+	  printLongLine(g_Statement[g_Statement[statemNum].reqHypList[i]].labelName,
+			"", " ");
+	}
+      }


Indentation is out of order?

wlammen · 2022-07-02T13:59:04Z

src/mmcmds.c

-      if (verifyFlag) {
-        if (verifyProof(i) >= 2) errorFound = 1;
+      if (verifyFlag & VERIFY_FULL) {
+        if (verifyProof(i, verifyFlag) >= 2) errorFound = 1;


It seems that VERIFY_FULL is ignored in verifyProof. Why is this flag submitted to this function?

wlammen · 2022-07-02T14:00:49Z

src/mmcmds.c

-/* If verify = 0, parse the proofs only for gross error checking.
-   If verify = 1, do the full verification. */
+/* If verifyFlag = VERIFY_NONE, parse the proofs only for gross error checking.
+   If verifyFlag includes VERIFY_FULL, do the full verification.


It seems this flag only controls a progress bar and a couple of result print outs. Please be more specific.

jamesjer · 2022-07-09T04:43:26Z

I haven't finished doing everything you requested yet. In particular, I have not done any refactoring of verifyProof. I'm pushing an update anyway so you can see my progress. I am traveling starting tomorrow, so won't get back to this probably until July 11 at the earliest.

Note that I removed checking for unused $f statements, since that doesn't seem to make any sense.

wlammen · 2022-07-09T05:21:02Z

Hmm. trujust is an example with local $f instructions. Were something like vz.tru \$f setvar z $. added, that would be a redundant floating hypothesis. I thought you had such a scenario in mind.

jkingdon · 2022-08-27T04:54:14Z

How does the distinct variable part compare to https://github.com/metamath/set.mm/blob/develop/scripts/check-dvs.py ?

jamesjer · 2024-01-01T00:40:25Z

I apologize for leaving this hanging. @jkingdon the script in question checks for variables that aren't mentioned at all in the theorem or proof. This PR, on the other hand, shows you dvs that the verifier never accessed while checking the proof, which implies that the verifier would still succeed if the dvs weren't present at all.

@wlammen , that would be useful, but the code in the original version of this PR checked for unused $f statements globally, which produced voluminous, and not at all useful, output. I'll have to think about how to constrain it to local $f statements.

benjub · 2024-01-01T16:41:30Z

src/metamath.c

-      } else {
-        verifyProofs(g_fullArg[2],1); // Parse and verify
-      }
+      i = (switchPos("SYNTAX_ONLY") != 0) ? 0 : 1;


Here and below, isn't our convention to write conditions as (switchPos("SYNTAX_ONLY")) instead of (switchPos("SYNTAX_ONLY") != 0) ?

Yes, you are right. I have changed the code accordingly.

GinoGiotto · 2024-01-03T12:18:53Z

I heavily used these functionalities to optimize https://groups.google.com/g/metamath/c/OB2_9sYgDfA and they are quite amazing. While the Python script found this PR as result (which is about 50 or so eliminable dv conditions), the /DISJOINT_VARS option currently finds 14,406 dv conditions that can be eliminated in set.mm.

Only problem is that the /FLOATING and the /HYPOTHESES options currently do not work @jamesjer and they don't even appear in the list of valid options.

But once everything is settled I'm strongly in favour of merging this PR.

EDIT: I just read above that checking for unused $f statements was intentionally removed, therefore it's ok with me.

/DISJOINT_VARS checks for unused non-dummy dvs /ALL_DISJOINT_VARS check for all unused dvs /ESSENTIAL checks for unused $e statements

jamesjer · 2024-01-03T22:31:14Z

@GinoGiotto Thank you for the comments. I will note that we should be cautious about removing anything based on these checks. Some "unused" dvs and essential hypotheses are there on purpose, even if the verifier doesn't use them when verifying. For example, ax6v has an unused dv that is the entire point of ax6v, and a1ii has an unused $e on purpose.

GinoGiotto · 2024-01-03T23:59:15Z

Some "unused" dvs and essential hypotheses are there on purpose, even if the verifier doesn't use them when verifying.

I know :-)

Indeed I was thinking that an exception list might be a good idea. For dv conditions a good rule of thumb could be to exclude checking those theorems with a label ax*v, which are usually weakened to show that the original axiom ax-* was provable from them. A quick search shows that the following label list ax6v, ax7v, ax7v1, ax7v2, ax8v, ax8v1, ax8v2, ax9v, ax9v1, ax9v2, ax12v, ax13v should be comprehensive enough for now.

icecream17 · 2024-08-05T15:39:28Z

Perhaps we could have a list of such theorems in the set.mm repo. This way, if someone wants to add extra DVs or hypotheses in a mathbox theorem for some reason, metamath.exe wouldn't have to change, and people wouldn't need to reinstall it.

I am very interested in this pr; both the DV and hypothesis checker seems very useful

jkingdon · 2024-08-05T20:03:55Z

Perhaps we could have a list of such theorems in the set.mm repo.

I think this would be required if we want to move forward with this (perhaps in $j directives or some similar mechanism).

I can think of a few examples in iset.mm which aren't in the list posted in this issue and I expect we'll add more in the future.

tirix · 2024-08-06T06:40:16Z

I'm probably often using too many DV conditions, this seems kind of wrong, but since this is completely unchecked, there is no easy way to fix this, and this PR would help.

GinoGiotto · 2024-08-06T08:03:37Z

I think this would be required if we want to move forward with this (perhaps in $j directives or some similar mechanism).

Using $j directives is a good idea, they wouldn't be invasive since there probably aren't many theorems to be excluded. If there aren't other known issues, I encourage moving forward with this PR.

In set.mm there is also axsep to be added in the list.

benjub · 2024-08-07T16:15:22Z

The $j-mechanism sounds good. So, there are two cases, like

$( $j intentional-hypothesis 'blabla'; $)
$( $j intentional-DV-condition 'x y A'; $)

?

For the second item, since DV conditions do not have labels, there is no canonical way to refer to them in a $j-statement. For instance, if I write $d y x $. (resp. $d y A x $.), will a mention to 'y x' be accepted ? Or should it be exactly the string 'y x' (resp. 'y A x') and nothing else ?

Also, in both cases, some hypotheses or DV conditions may be intentional for some theorems and not others, a situation which may arise in the case of long scopes. This is one more reason to avoid long scopes, which are error-prone.

icecream17 · 2024-08-09T15:30:13Z

I think $j DVs should be able to just list what intentional extra DVs there are, like normal DVs, independent of however the actual DVs are written

jamesjer mentioned this pull request Jun 27, 2022

Theorems which don't use some of their hypotheses metamath/set.mm#2648

Open

wlammen suggested changes Jul 2, 2022

View reviewed changes

jamesjer force-pushed the master branch from a7b6967 to 2b90467 Compare July 9, 2022 04:40

benjub mentioned this pull request Sep 26, 2022

Manpage #98

Merged

jamesjer force-pushed the master branch from 2b90467 to cad7fde Compare January 1, 2024 00:35

benjub reviewed Jan 1, 2024

View reviewed changes

Add hypothesis and dv usage qualifiers to VERIFY PROOF

9b14a9d

/DISJOINT_VARS checks for unused non-dummy dvs /ALL_DISJOINT_VARS check for all unused dvs /ESSENTIAL checks for unused $e statements

jamesjer force-pushed the master branch from cad7fde to 9b14a9d Compare January 3, 2024 22:27

GinoGiotto mentioned this pull request Mar 19, 2024

Discourage indirect usage of ax-13? metamath/set.mm#3879

Closed

GinoGiotto mentioned this pull request Oct 14, 2024

Remove DV conditions metamath/set.mm#4289

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add hypothesis and dv usage qualifiers to VERIFY PROOF #92

Add hypothesis and dv usage qualifiers to VERIFY PROOF #92

jamesjer commented Jun 27, 2022

wlammen commented Jun 28, 2022

wlammen Jul 2, 2022

wlammen Jul 2, 2022

wlammen Jul 2, 2022

wlammen Jul 2, 2022

wlammen Jul 2, 2022

wlammen Jul 2, 2022

wlammen Jul 2, 2022

wlammen Jul 2, 2022

wlammen Jul 2, 2022

wlammen Jul 2, 2022

jamesjer commented Jul 9, 2022

wlammen commented Jul 9, 2022 •

edited

Loading

jkingdon commented Aug 27, 2022

jamesjer commented Jan 1, 2024

benjub Jan 1, 2024

jamesjer Jan 3, 2024

GinoGiotto commented Jan 3, 2024 •

edited

Loading

jamesjer commented Jan 3, 2024

GinoGiotto commented Jan 3, 2024 •

edited

Loading

icecream17 commented Aug 5, 2024

jkingdon commented Aug 5, 2024

tirix commented Aug 6, 2024

GinoGiotto commented Aug 6, 2024

benjub commented Aug 7, 2024

icecream17 commented Aug 9, 2024

Add hypothesis and dv usage qualifiers to VERIFY PROOF #92

Are you sure you want to change the base?

Add hypothesis and dv usage qualifiers to VERIFY PROOF #92

Conversation

jamesjer commented Jun 27, 2022

wlammen commented Jun 28, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jamesjer commented Jul 9, 2022

wlammen commented Jul 9, 2022 • edited Loading

jkingdon commented Aug 27, 2022

jamesjer commented Jan 1, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

GinoGiotto commented Jan 3, 2024 • edited Loading

jamesjer commented Jan 3, 2024

GinoGiotto commented Jan 3, 2024 • edited Loading

icecream17 commented Aug 5, 2024

jkingdon commented Aug 5, 2024

tirix commented Aug 6, 2024

GinoGiotto commented Aug 6, 2024

benjub commented Aug 7, 2024

icecream17 commented Aug 9, 2024

wlammen commented Jul 9, 2022 •

edited

Loading

GinoGiotto commented Jan 3, 2024 •

edited

Loading

GinoGiotto commented Jan 3, 2024 •

edited

Loading