Proofs are broken since this morning.

[metakunt]

I have tried to use mmj2 for proofs. So far so good. But in the morning it generates me wrong proofs that give issues when i try to import the results into set.mm.

$( <MM> <PROOF_ASST> THEOREM=syllogism LOC_AFTER=

h1::syllogism.1 |- ( ph -> M e. ZZ ) 
h2::syllogism.2 |- ( ph -> N e. ZZ ) 
h3::syllogism.3 |- ( ph -> M <_ N ) 
h4::syllogism.4 |- ( ph -> K e. NN0 ) 
h5::syllogism.5 |- ( ( ph /\ k e. ( M ... ( N + K ) ) ) -> A e. CC ) 
10:2:zred          |- ( ph -> N e. RR )
11:10:ltp1d        |- ( ph -> N < ( N + 1 ) )
12::fzdisj         |- (  N < ( N + 1 )
                      ->   ( ( M ... N ) i^i ( ( N + 1 ) ... ( N + K ) ) )
                         = (/) )
13:11,12:syl       |- (  ph
                      ->   ( ( M ... N ) i^i ( ( N + 1 ) ... ( N + K ) ) )
                         = (/) )
14:4:nn0zd         |- ( ph -> K e. ZZ )
15:2,14:zaddcld    |- ( ph -> ( N + K ) e. ZZ )
16::nn0addge1      |- ( ( N e. RR /\ K e. NN0 ) -> N <_ ( N + K ) )
17:10,4,16:syl2anc |- ( ph -> N <_ ( N + K ) )
18::elfz4          |- (  (  ( M e. ZZ /\ ( N + K ) e. ZZ /\ N e. ZZ )
                         /\ ( M <_ N /\ N <_ ( N + K ) ) )
                      -> N e. ( M ... ( N + K ) ) )
19:1,15,2,3,17,18:syl32anc    
                   |- (  ph
                      -> N e. ( M ... ( N + K ) ) )
20::fzsplit        |- (  N e. ( M ... ( N + K ) )
                      ->   ( M ... ( N + K ) )
                         = ( ( M ... N ) u. ( ( N + 1 ) ... ( N + K ) ) ) )
21:19,20:syl       |- (  ph
                      ->   ( M ... ( N + K ) )
                         = ( ( M ... N ) u. ( ( N + 1 ) ... ( N + K ) ) ) )
22::fzfid          |- ( ph -> ( M ... ( N + K ) ) e. Fin )
qed:13,21,22,5:fprodsplit 
                   |- (  ph
                      ->   prod_ k e. ( M ... ( N + K ) ) A
                         = ( prod_ k e. ( M ... N ) A
                             x.
                             prod_ k e. ( ( N + 1 ) ... ( N + K ) ) A ) )

$=  ( syllogism.2 syllogism.1 syllogism.4 syllogism.3 syllogism.5 cfz
    co caddc wbr wceq syl wcel cz cle c1 clt cin c0 zred ltp1d fzdisj
    cun nn0zd zaddcld cr cn0 nn0addge1 syl2anc elfz4 syl32anc fzsplit
    fzfid fprodsplit ) AEFLMZFUANMZFDNMZLMZBEVBLMZCAFVAUBOUTVCUCUDPAF
    AFGUEZUFEFVAVBUGQAFVDRZVDUTVCUHPAESRVBSRFSREFTOFVBTOZVFHAFDGADIUI
    UJGJAFUKRDULRVGVEIFDUMUNFEVBUOUPFEVBUQQAEVBURKUS $.
$d K k 
$d M k 
$d N k 
$d k ph 
$) 

And here is the metamath output

$ ./rewrap.sh
Metamath - Version 0.199.pre 29-Jan-2022      Type HELP for help, EXIT to exit.
MM> read D:\metamath\set.mm\set.mm
Reading source file "D:\metamath\set.mm\set.mm"... 44359149 bytes
44359149 bytes were read into the source buffer.
The source has 212383 statements; 2812 are $a and 42097 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> write source D:\metamath\set.mm\set.mm /rewrap
The input file will be renamed D:\metamath\set.mm\set.mm~1.
Writing "D:\metamath\set.mm\set.mm"...
212383 source statement(s) were written.
MM> erase
Metamath has been reset to the starting state.
MM> read D:\metamath\set.mm\set.mm
Reading source file "D:\metamath\set.mm\set.mm"... 44359149 bytes
44359149 bytes were read into the source buffer.
The source has 212383 statements; 2812 are $a and 42097 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> save proof */compressed/fast
Reformatting and saving (but not recompressing) all proofs...
Remember to use WRITE SOURCE to save changes permanently.
MM> write source D:\metamath\set.mm\set.mm
The input file will be renamed D:\metamath\set.mm\set.mm~1.
Writing "D:\metamath\set.mm\set.mm"...
212383 source statement(s) were written.
MM> verify proof *
0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
........................................?Error at statement 173145, label "prodsplit", type "$p":
      cr cn0 ) AEFLMZFUANMZFDNMZLMZBEVBLMZCAFVAUBOUTVCUHUCPAFAFGUDZUEEFVAVBUFQA
                                                                ^^
The hypotheses of statement "zred" at proof step 37 cannot be unified.
  Hypothesis 1:  wff ph
  Step 34:  wff ph
  Hypothesis 2:  class A
  Step 35:  class N
  Hypothesis 3:  |- ( ph -> A e. ZZ )
  Step 36:  |- ( ph -> M e. ZZ )
..........
MM> quit

This is how I converted the proof to metamath

  ${
    $d M k $.  $d N k $.  $d K k $.  $d ph k $.
    prodsplit.1 $e |- ( ph -> M e. ZZ ) $.
    prodsplit.2 $e |- ( ph -> N e. ZZ ) $.
    prodsplit.3 $e |- ( ph -> M <_ N ) $.
    prodsplit.4 $e |- ( ph -> K e. NN0 ) $.
    prodsplit.5 $e |- ( ( ph /\ k e. ( M ... ( N + K ) ) ) -> A e. CC ) $.
    $( Product split into two factors, original by icecream.  (Contributed by
       metakunt, 21-Apr-2024.) $)
    prodsplit $p |- ( ph
                      -> prod_ k e. ( M ... ( N + K ) ) A
                      = ( prod_ k e. ( M ... N ) A
                          x.
                      prod_ k e. ( ( N + 1 ) ... ( N + K ) ) A ) ) $=
      ( cfz co caddc wbr wceq syl wcel cz cle c1 clt c0 zred ltp1d fzdisj nn0zd
      cin cun zaddcld nn0addge1 syl2anc elfz4 syl32anc fzsplit fzfid fprodsplit
      cr cn0 ) AEFLMZFUANMZFDNMZLMZBEVBLMZCAFVAUBOUTVCUHUCPAFAFGUDZUEEFVAVBUFQA
      FVDRZVDUTVCUIPAESRVBSRFSREFTOFVBTOZVFHAFDGADIUGUJGJAFURRDUSRVGVEIFDUKULFE
      VBUMUNFEVBUOQAEVBUPKUQ $.
  $}

This is the second proof that's broken. And I have no clue what is the cause. Another broken proof is found in https://github.com/metamath/set.mm/pull/3939 I'd hope to know why it breaks so I can avoid it in the future. MMJ2 seems to output a proof, so I'd hope that works.

[digama0]

Your first code block shows a theorem by the name of syllogism, but you are proving a different theorem, prodsplit. mmj2 uses some information regarding the positioning of a theorem in context so I don't recommend writing the theorem signature directly in mmj2. Instead, first create the theorem signature in the mm file but put ... $= ? $. for the proof, then load the mm file and open the theorem in mmj2; do the proof there, without changing the header line (and mmj2 will enforce that the hypotheses and QED step match what is in the mm file).

Generation of new theorems directly from mmj2 doesn't quite work correctly; you can see ( syllogism.1 ... appearing in the compressed proof but those hypotheses (1) shouldn't show up in compressed proofs and (2) don't exist in the first place because the theorem is called prodsplit, not syllogism, so the resulting proof will not check.

[metakunt]

How do I do that? I have never used a mm file before and I couldn't find good documentation that explains the basics.

The easiest I've found was to somehow get mmj2 running. So far I've copy pasted all proofs back to the main set.mm file.

That also explains why I could likely just copy paste a proof without hypotheses.

Would this be a mm file?

${
    prodsplit.1 $e |- ( ph -> M e. ZZ ) $.
    prodsplit.2 $e |- ( ph -> N e. ZZ ) $.
    prodsplit.3 $e |- ( ph -> M <_ N ) $.
    prodsplit.4 $e |- ( ph -> K e. NN ) $.
    prodsplit.5 $e |- ( ( ph /\ k e. ( M ... ( N + K ) ) ) -> A e. CC ) $.
    prodsplit $p |- ( ph ->
      ( prod_ k e. ( M ... N ) A x. prod_ k e. ( ( N + 1 ) ... ( N + K ) ) A )
      = prod_ k e. ( M ... ( N + K ) ) A ) $=
$}

And if so, how do I load it into mmj2. I've tried to name the file prodsplit.mm and prodsplit.mmp. But the first one didn't load and the second one just looked really weird in mmj2

[digama0]

Yes, that is what the theorem statement would look like, except that you did not close the statement, you need to add ? $. after the $=. (Normally there would also be a comment before the statement.) The easiest way to get all the fiddly details right is to just copy and paste from another statement in set.mm .

To load a database (which is needed for mmj2 to work at all), you need to specify the path to the file in the RunParms.txt. See https://github.com/digama0/mmj2/blob/master/quickstart.md .

[metakunt]

Yeah, I still don't know what I need to do to do import a file in mmj2.

First if the file is wrong, what is missing. So far I have understood that ? $. is missing. So this file should work

${
    prodsplit.1 $e |- ( ph -> M e. ZZ ) $.
    prodsplit.2 $e |- ( ph -> N e. ZZ ) $.
    prodsplit.3 $e |- ( ph -> M <_ N ) $.
    prodsplit.4 $e |- ( ph -> K e. NN ) $.
    prodsplit.5 $e |- ( ( ph /\ k e. ( M ... ( N + K ) ) ) -> A e. CC ) $.
    prodsplit $p |- ( ph ->
      ( prod_ k e. ( M ... N ) A x. prod_ k e. ( ( N + 1 ) ... ( N + K ) ) A )
      = prod_ k e. ( M ... ( N + K ) ) A ) $= ? $.
$}

i've tried, this is how it looks and I am doing something wrong. I did specify the database in RunParms.txt This is my RunParms.txt

LoadFile,set.mm
VerifyProof,*
Parse,* 
ProofAsstUnifySearchExclude,biigb,xxxid,dummylink
ProofAsstProofFolder,myproofs
TheoremLoaderMMTFolder,myproofs
ProofAsstDeriveAutocomplete, yes
ProofAsstUseAutotransformations, yes,no,yes
RunProofAsstGUI
RunMacro,definitionCheck,ax-*,df-bi,df-clab,df-cleq,df-clel
*done

And this is my script to start mmj2

java -Xms128M -Xmx2048M -jar mmj2.jar RunParms.txt Y "" d:\metamath\set.mm ""

It points to the correct, and only, set.mm database I have on my disk.

Or do you mean that I have to put the incomplete theorem in set.mm and work the proof from there?

[digama0]

Or do you mean that I have to put the incomplete theorem in set.mm and work the proof from there?

Yes. Go to the place in set.mm where you would like your theorem to live eventually (e.g. in your mathbox), add the theorem, and then start up mmj2 pointing to your copy of set.mm. Then use the navigation commands in mmj2 to open the "prodsplit" theorem, and it will create a worksheet for the theorem which you can then edit as normal. Most likely you can just copy the proof steps from the first version at that point, and mmj2 will generate the completed proof on a line starting with $=, which you then copy back into set.mm, replacing the ?.

[metakunt]

It worked. Thank you very much.