Add dcand to iset.mm, deprecate old form dcan2

[david-a-wheeler]

No description provided.

[david-a-wheeler]

The dcand proof is lame, but it is valid. I'm sure it can be simplified, but I figured I'd start with "the simplest thing that would work".

i ran some minimizations, and they ended up with validation errors. That is weird. I need to investigate.

[jkingdon]

I believe the failures on this branch are also the ones happening on the develop branch which are fixed by #4393

[david-a-wheeler]

@jkingdon - you're right! I also had to regen the discouraged file, because we have some dcan2 uses, but I can fix that later. I want to clean up the dcand proof; it's correct but I believe it's overly complicated.

[benjub]

I did some propcalc proofs recently, so my "metamath-fu" temporarily got a bit higher, and I found the following. Do whatever you want with it:

    dcand $p |- ( ph -> DECID ( ps /\ ch ) ) $=
        ( wa wn wo wdc df-dc id intnanrd orim2i sylbi syl intnand sylanbrc sylibr
      ordir ) ABCFZTGZHZTIABUAHZCUAHZUBABIZUCDUEBBGZHUCBJUFUABUFBCUFKLMNOACIZUD
      EUGCCGZHUDCJUHUACUHCBUHKPMNOBCUASQTJR $.

[david-a-wheeler]

I bow to your "metamath-fu" :-). Added.

[jkingdon]

A few of the proofs, like lgscllem , lgsval , nninfdclemp1 , ctiunctlemudc , 1arith , and infpnlem2 , pcmptdvds , pclemdc , nnwosdc get a lot longer and the compressed proof contains some repetitive characters (which I suppose isn't the real problem, just might be a hint about why the proofs got long).

At first I thought this would be a non-blocking comment but I don't know, they are a lot longer. Is fixing this just as simple as running scripts/minimize ?

[avekens]

A few of the proofs, like lgscllem , lgsval , nninfdclemp1 , ctiunctlemudc , 1arith , and infpnlem2 , pcmptdvds , pclemdc , nnwosdc get a lot longer and the compressed proof contains some repetitive characters (which I suppose isn't the real problem, just might be a hint about why the proofs got long).

At first I thought this would be a non-blocking comment but I don't know, they are a lot longer. Is fixing this just as simple as running scripts/minimize ?

I agree that the reason of the much longer proofs should be investigated first. I haven't seen such a repetition of characters in a proof before.

[GinoGiotto]

I agree that the reason of the much longer proofs should be investigated first. I haven't seen such a repetition of characters in a proof before.

Those are definitely repeated steps, which should be easily fixable with a minimization process. In the case of nnwosdc, there is a repeated application of 3bitr2d. After minimization the proof becomes:

    $( Well-ordering principle: any inhabited decidable set of positive
       integers has a least element (schema form).  (Contributed by NM,
       17-Aug-2001.)  (Revised by Jim Kingdon, 25-Oct-2024.) $)
    nnwosdc $p |- ( ( E. x e. NN ph /\ A. x e. NN DECID ph ) ->
                  E. x e. NN ( ph /\ A. y e. NN ( ps -> x <_ y ) ) ) $=
      ( vw vj cn wrex wdc wral wa cv wcel wex wi sylibr weq nfcv wal wss rabn0m
      w3a cle wbr ssrab2 biantrur sylbb1 wsb wn wo animorrl df-dc nfs1v sbequ12
      crab nfdc dcbid impcom dcand elrabf dcbii ralrimiva anim12i df-3an nfrab1
      rspc nnwofdc df-rex rabid df-ral 3bitr2d elrab imbi1i bitri albii anbi12i
      impexp exbii anbi2i anass bitr3i bitr4i 3bitri sylib syl ) ACHIZAJZCHKZLZ
      ACHUPZHUAZFMWKNFOZGMZWKNZJZGHKZUCZABCMZDMZUDUEZPZDHKZLZCHIZWJWLWMLZWQLWRW
      GXFWIWQWMWGXFACFHUBWLWMACHUFUGUHWIWPGHWIWNHNZLZXGACGUIZLZJWPXHXGXIXHXGXGU
      JZUKXGJWIXGXKULXGUMQXGWIXIJZWHXLCWNHXICACGUNZUQCGRAXIACGUOZURVGUSUTWOXJAX
      ICWNHCWNSCHSXMXNVAVBQVCVDWLWMWQVEQWRXADWKKZCWKIZXECDFWKGACHVFDWKSVHXPWSWK
      NZXOLZCOWSHNZALZWTHNZXBPZDTZLZCOZXEXOCWKVIXRYDCXQXTXOYCACHVJXOWTWKNZXAPZD
      TYCXADWKVKYGYBDYGYABLZXAPYBYFYHXAABCWTHCDRABABEEEVLVMVNYABXAVRVOVPVOVQVSY
      EXSXDLZCOXEYDYICYDXTXCLYIXCYCXTXBDHVKVTXSAXCWAWBVSXDCHVIWCWDWEWF $.

And this proof has the same amount of lines as the original one.

[david-a-wheeler]

Weird. I did run minimize on this. Maybe I should just add dcand, note that existing dcan2 uses are deprecated, and then remove existing uses of dcan2 separately. It would probably be a cleaner commit anyway.

[jkingdon]

Weird. I did run minimize on this. Maybe I should just add dcand, note that existing dcan2 uses are deprecated, and then remove existing uses of dcan2 separately. It would probably be a cleaner commit anyway.

Maybe the arguments to minimize or something?

Anyway, seems like this should be fixable either in the way described above or some other way (seems like either one could work).