List stmt

[tirix]

Adds a --list-statements option which lists all statements in the given database. This takes less than one second on set.mm on my machine. This is a very simple implementation which just lists the statement label, and then the corresponding statement, as follows:

idi.1: |- ph
idi: |- ph
a1ii.1: |- ph
a1ii.2: |- ps
a1ii: |- ph
wn: wff -. ph
wi: wff ( ph -> ps )
min: |- ph
maj: |- ( ph -> ps )
ax-mp: |- ps
...

Floats $f are not included but could easily be added. (based on the split-crate PR #149)

[GinoGiotto]

Nice! Thank you for this.

So since this command is designed to print a list of statements, I think it would make sense to apply my suggestion here. It does not have to be implemented if there is no interest for it (besides me, which I'm interested), but I think it has some advantages which I described below.

Basically I'm proposing to imitate the behaviour of metamath-exe (with the speed advantage of metamath-knife):

MM> SHOW STATEMENT *
34 idi.1 $e |- ph $.
35 idi $p |- ph $= ... $.
-------------------------------------------------------------------------------
38 a1ii.1 $e |- ph $.
39 a1ii.2 $e |- ps $.
40 a1ii $p |- ph $= ... $.
-------------------------------------------------------------------------------
42 wn $a wff -. ph $.
-------------------------------------------------------------------------------
43 wi $a wff ( ph -> ps ) $.
-------------------------------------------------------------------------------
45 min $e |- ph $.
46 maj $e |- ( ph -> ps ) $.
47 ax-mp $a |- ps $.
-------------------------------------------------------------------------------
49 ax-1 $a |- ( ph -> ( ps -> ph ) ) $.
-------------------------------------------------------------------------------
50 ax-2 $a |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) ) $.
-------------------------------------------------------------------------------
51 ax-3 $a |- ( ( -. ph -> -. ps ) -> ( ps -> ph ) ) $.
-------------------------------------------------------------------------------

Specifically:

• Show the $e $a $p keywords for every statement.
• Group statements in frames (I'm referring to the metamath concept of "frame", described from page 129 of the metamath book).
• Show dv conditions for every frame.
• $f statements are not showed by default on metamath-exe unless the /FULL option is active. It think it's ok to just ignore them for now.
• Differently from metamath-exe, I think the running index is not too important.

The advantage of this formatting resides in making clear the rules of inferences to which the $e hypotheses belong to. Showing dv conditions allow the user to differentiate identical statements, like ax13v and ax13w .

Example:

  ${
    pm5.21ni.1 $e |- ( ph -> ps ) $.
    pm5.21ni.2 $e |- ( ch -> ps ) $.
    $( Two propositions implying a false one are equivalent.  (Contributed by
       NM, 16-Feb-1996.)  (Proof shortened by Wolf Lammen, 19-May-2013.) $)
    pm5.21ni $p |- ( -. ps -> ( ph <-> ch ) ) $=
      ( wn con3i 2falsed ) BFACABDGCBEGH $.

    ${
      pm5.21nii.3 $e |- ( ps -> ( ph <-> ch ) ) $.
      $( Eliminate an antecedent implied by each side of a biconditional.
         (Contributed by NM, 21-May-1999.) $)
      pm5.21nii $p |- ( ph <-> ch ) $=
        ( wb pm5.21ni pm2.61i ) BACGFABCDEHI $.
    $}
  $}

With the current implementation the output is:

pm5.21ni.1: |- ( ph -> ps )
pm5.21ni.2: |- ( ch -> ps )
pm5.21ni: |- ( -. ps -> ( ph <-> ch ) )
pm5.21nii.3: |- ( ps -> ( ph <-> ch ) )
pm5.21nii: |- ( ph <-> ch )

Which does not make clear the membership of $e statements, since we can't know from here that pm5.21ni.1 is an hypothesis of pm5.21nii as well.

While with metamath-exe the membership is perfectly clear:

1366 pm5.21ni.1 $e |- ( ph -> ps ) $.
1367 pm5.21ni.2 $e |- ( ch -> ps ) $.
1368 pm5.21ni $p |- ( -. ps -> ( ph <-> ch ) ) $= ... $.
-------------------------------------------------------------------------------
1366 pm5.21ni.1 $e |- ( ph -> ps ) $.
1367 pm5.21ni.2 $e |- ( ch -> ps ) $.
1370 pm5.21nii.3 $e |- ( ps -> ( ph <-> ch ) ) $.
1371 pm5.21nii $p |- ( ph <-> ch ) $= ... $.

What do you think?

[tirix]

What do you think?

Sure, I've pushed a commit with the changes for that format.

[GinoGiotto]

Sure, I've pushed a commit with the changes for that format.

That was fast! This would have definitely taken months for me even to start making sense of rust. So thank you for that.

This is how the new output appears to me:

idi.1 $e |- ph
idi $p |- ph
-------------------------------------------------------------------------------
a1ii.1 $e |- ph
a1ii.2 $e |- ps
a1ii $p |- ph
-------------------------------------------------------------------------------
wn $a wff -. ph
-------------------------------------------------------------------------------
wi $a wff ( ph -> ps )
-------------------------------------------------------------------------------
min $e |- ph
maj $e |- ( ph -> ps )
ax-mp $a |- ps
-------------------------------------------------------------------------------
ax-1 $a |- ( ph -> ( ps -> ph ) )
-------------------------------------------------------------------------------
ax-2 $a |- ( ( ph -> ( ps -> ch ) ) -> ( ( ph -> ps ) -> ( ph -> ch ) ) )
-------------------------------------------------------------------------------
ax-3 $a |- ( ( -. ph -> -. ps ) -> ( ps -> ph ) )
-------------------------------------------------------------------------------
...

Which looks good. I explored around and I didn't find obvious problems. In your output dv conditions are listed pair by pair, which is even better for extracting data (in general the more standardized the output is, the easier is for me to use it).

An other observation is that dv conditions of dummy vars are ignored, which I think it's the correct behaviour since those are related to proofs only, not to statements (and indeed even metamath-exe ignores them, you can checkout theorem axc14 as an example).

Therefore I've nothing to complain. Approve.