Misc cbv* and equality theorems

[GinoGiotto]

This PR is meant to "fill the gaps" of missing equality inferences and adjust a few theorems that are going to be used in the justification theorem prover. Specifically:

Main:

• Fix inaccurate comments in equality theorems about ~df-mo and ~df-eu.
• Remove DV conditions from equality inferences (without increasing axiom usage).
• Avoid axioms in equality theorems (no OLD versions and no revision tags where the original proof was just a direct application of the corresponding theorem with nonfreeness hypotheses).
• Add a few $j tags.

Mathboxes:

• Add equality inferences and equality deductions.
• Add cbv* theorems.
• Remove DV conditions from equality inferences (without increasing axiom usage).

[tirix]

I see you've removed ~ prodeq1iOLD which is just the application of ~ prodeq1i and ~ ax-mp:
I'm not versed into axiom avoidance, but does that mean that ~ ax-mp uses ax-10, etc. ?
That seems off.

The shorter proof with just ~ prodeq1i and ~ ax-mp should be preferred.

[GinoGiotto]

Hi Thierry, so sorry I didn't answer before. I'm not sure I understand your concern, let me know if I got it wrong:

I see you've removed ~ prodeq1iOLD which is just the application of ~ prodeq1i and ~ ax-mp:

Theorem ~ prodeq1iOLD is not removed, the commit diff shows that it is placed below ~ prodeq1i. Maybe you meant replacing the original proof with the new one?

I'm not versed into axiom avoidance, but does that mean that ~ ax-mp uses ax-10, etc. ?
That seems off.

In this PR I removed ax-10 ax-11 and ax-12 from ~ prodeq1 (without the "i" suffix), so if it was for axiom usage alone it could be used in the proof of ~ prodeq1i. The issue however, is not axiom usage, but DV conditions (as the revision message of ~ prodeq1i says).

In particular, the proof revision of ~ prodeq1i allows to change the original:

 ${
    $d k A $.  $d k B $.
    prodeq1iOLD.1 $e |- A = B $.
    prodeq1iOLD $p |- prod_ k e. A C = prod_ k e. B C $= ... $.
  $}

To the stronger:

 ${
    prodeq1i.1 $e |- A = B $.
    prodeq1i $p |- prod_ k e. A C = prod_ k e. B C $= ... $.
  $}

The shorter proof with just ~ prodeq1i and ~ ax-mp should be preferred.

Afaik The DV conditions on ~ prodeq1 (without the "i" suffix) are not removable, so we can't use it directly in the proof of ~ prodeq1i.

[tirix]

Thanks, I see now!
I was indeed looking at the axiom usage, and did not see that the DV conditions were dropped.

[tirix]

Ok, then another naive comment:
I see df-sum does not seem to have this issue (no DV conditions on k, A and k, B in sumeq1).
Could maybe this new version of df-prod avoid DV conditions on prodeq1?

    df-prod $a |- prod_ k e. A B =
    ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\
      E. n e. ( ZZ>= ` m )
         E. y ( y =/= 0 /\
               seq n ( x. , ( l e. ZZ |-> if ( l e. A , [_ l / k ]_ B , 1 ) ) ) ~~> y ) /\
      seq m ( x. , ( l e. ZZ |-> if ( l e. A , [_ l / k ]_ B , 1 ) ) ) ~~> x ) \/
      E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\
       x =
       ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) $.

(I simply replaced k by a new variable l, and B by [_ l / k ] B, as is done in df-sum)

[GinoGiotto]

Maybe it works, but the problem is that df-prod is not the only definition to have this issue. Other examples are iineq1 or disjeq1 or even the basic rabeq. Perhaps one could open an issue to make it a requirement for every definition that has both setvars and classes on the LHS (they are not that many). On the other hand, some people may find this not aesthetically pleasing to look at:

df-iinNEW $a |- |^|_ x e. A B = { y | A. v e. [_ v / x ]_ A y e. [_ v / x ]_ B } $.

If the proposal is only for df-prod because in this specific case the proof is too long, I may be ok with it, but I'm not sure if we should generalize it to other definitions then.