Fixes

[GinoGiotto]

This PR addresses most issues in #1, specifically:

• Distinct variable conditions errors.
• Parsing errors:
  • Two theorems have the same name, I don't know the label convention for this database, so I simply renamed the second one kcl instead of kcd ("c" and "l" are respectively the first and last letters of "conditional").
  • two was not declared, I suppose it was meant to be bool since it's the type with two elements.
  • 1st and 2nd were not declared, so I added them as costants.

The only issues of #1 that are not fixed are:

?Error on line 1101 of file "dtt.mm" at statement 509, label "0val", type "$p":
    wk wa tyld tyde mp2an detr4i ) ABCDHEIJZKLMZNLMZABCDEIFADOLMBUCUDZCUKIKLM
                                     ^
At proof step 3, statement "ol" requires 3 hypotheses but the RPN stack
contains only 2 entries: "A" (step 1) and  "B" (step 2).
.
?Error on line 1131 of file "dtt.mm" at statement 516, label "k1s", type "$p":
    wk wa tyld tyde mp2an detr4i ) ABCDHEIJZKLMZNLMZABCDEIFADOLMBUCUDZCUKIKLM
                                   ^
At proof step 1, statement "ol" requires 3 hypotheses but the RPN stack is
empty.

?Error on line 1147 of file "dtt.mm" at statement 521, label "de1s", type "$p":
      ZGUKUMPULQRSUEUJUKPAUJUMUKUIITIUITUJUMPEUAUIUBUIIUFUGQUHRS $.
          ^^
This compressed label reference is outside the range of the label list.  The
compressed label value is 32 but the largest label defined is 31.
....
Warning: The following $p statement(s) were not proved:  k1r, kpaird

Metamath-exe doesn't let me visualize a different proof format if it contains errors. Is it possible to make a faulty proof human-readable? Without that feature I don't know how to fix those issues.

I also updated some latex definitions according to the recent format changes done in set.mm metamath/set.mm#3067 metamath/set.mm#3091 (comment)

Dates below proofs are outdated according to https://groups.google.com/g/metamath/c/YM3nojVoaqk/m/UvicrL5XBAAJ so I removed them and added a corresponding tag when missing. I only have doubts for three instances:

$( The type of the zero recursor.
   (Contributed by Mario Carneiro, 14-Mar-2016.) $)
  0val $p |- ( A : Type i |= zero.rec i A : ( zero -> A ) ) $=
    ( ol uu0 uimax tty mt om tpp tv wde df-pp a1i kdetrd wule ax-imax0 ax-0le
    wk wa tyld tyde mp2an detr4i ) ABCDHEIJZKLMZNLMZABCDEIFADOLMBUCUDZCUKIKLM
    ZGUKUMPULQRSUEUJUKPAUJUMUKUIITIUITUJUMPEUAUIUBUIIUFUGQUHRS $.
    $( [26-Feb-2016] $)

${
    dett.1 $e |- ( ph |= OA : Type i ) $.
    dett.2 $e |- ( ph |= A : OA ) $.
    dett.3 $e |- ( ph |= B : OA ) $.    
    $( The equality rule for the conditional, true case.
       (Contributed by Mario Carneiro, 14-Mar-2016.) $)
    dett $a |- ( ph |= cond i tt A B := A ) $.
      $( [26-Feb-2016] $)

    $( The equality rule for the conditional, false case.
       (Contributed by Mario Carneiro, 14-Mar-2016.) $)
    deff $a |- ( ph |= cond i ff A B := B ) $.
      $( [26-Feb-2016] $)
  $}

Which date should stay between 26-Feb-2016 and 14-Mar-2016?

There was also an unmatched bracket that I fixed by looking at similar theorems. In any case I splitted all these changes in commits, so they should be easier to review.

[jorge-agra]

Hi @GinoGiotto ,

if you need the steps of the proofs, up until the error, I can provide you that, but you might need to build the proofs in error from scratch.

Best regards.

[GinoGiotto]

(I accidentally pressed the close button).

Hi @jorge-agra

Thank you for your availability, indeed some proof steps might help, but I would probably still need some time since my understanding of dependent type theory is very limited (I actually wanted to use this database for learning). My main focus was to fix the issues I've found with metamath-exe in #1, but beyond that I'm not sure how much I'll be able to achieve, especially if I'm dealing with building proofs from scratch.

In any case some proof steps could be useful as well for someone else that would like to embark on this challenge. Eventually even the commands that generated those steps might be supportive.

Regards