Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

List stmt #150

Merged
merged 4 commits into from
Jun 1, 2024
Merged

List stmt #150

merged 4 commits into from
Jun 1, 2024

Conversation

tirix
Copy link
Collaborator

@tirix tirix commented Nov 26, 2023

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
Copy link

GinoGiotto commented Nov 27, 2023

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
Copy link
Collaborator Author

tirix commented Nov 27, 2023

What do you think?

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

@GinoGiotto
Copy link

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.

@tirix tirix merged commit 96b778d into metamath:main Jun 1, 2024
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants