The theorem itexp (soon to be itgpow) (was: Help with beginning to contribute to set.mm)

[Benoit]

Jon wrote:

>Hi Benoit. I made some changes to itexp as you suggested, I changed the
>conditions so it works with NN0 and I changed the name to itgexp as "itg" seems
>to be the common abbreviation for integral. I am very happy to change to either
>itgmon or itgpow, it's fine with me, however I think that it should definitely match
> dvexp and maybe also the exp theorems in Glauco's Mathbox. So I think I am
>very happy to change and I think someone with more authority than me would
>need to make the change global and do I find replace in all theorems that rely
>on dvexp etc if this change is to happen.

That's great for NN0 !  As for labels, let's see what the other thread gives. I would use itgpow and dvpow.

>I'm afraid at the moment I don't want to start on replacing everything with
> (ph ->, that sounds like quite a lot of tricky work, I might get to it in the future
>though. I can see that a lot of thought has gone into deduction vs inference etc.
> Is it good practice in general to write everything in deduction form ( I mean
>starting with "( ph ->" )?

It's true that this sounds like a long boring work... unless experienced users know of a faster way??
So yes, it is generally good practice to write theorem in deduction form, if nothing else because it's trivial to get the inference form from it, but harder to go the other way around: you learnt it the hard way!  And it's more widely applicable. Even better are closed forms, although it's probably not worth the effort for longer proofs: deduction form is generally enough.  I think it's explained in the metamath.pdf book, but here is a summary:
If you have a theorem in closed form
  |- PH -> PS
then you get the deduction form
  |- ( ph -> PH) => |- ( ph -> PS )
by using ~syl, as well as the inference form
  |- PH => |- PS
by using ax-mp.
If you have a theorem in deduction form
  |- ( ph -> PH) => |- ( ph -> PS )
then you get the inference form by using the deduction form above with T. substituted for ph, and use trud (this is why I told you above that the presence of T. as an antecedent and the uses trud in your proof of itgpow shows that parts of the proof are in deduction style).
*IF* there are no dv conditions (e.g $d ph x $. if PH contains x) that forbid you from doing so, you can also substitute PH for ph, use id, and recover the closed form.

> To anyone, I am a little stuck with this next theorem

Please, start a new thread "...  (was: Help with beginning to contribute to set.mm)".  By the way, the theorem looks false to me: what if C is a non-measurable subset? Or simply RR ?  It looks like your B is ( A X. C ).

Benoit

[Thierry Arnoux]

Hi Jon & Benoît,

I've created the deduction version of that theorem (whatever we choose to name it). It is not a particularly hard task, just a bit long and a bit boring as explained by Benoît.  This is typically the kind of task that could be easily automated.

About this:

h1::subarea.1      |- A e. dom area

h2::subarea.2      |- C C_ RR

h3::subarea.3      |- B = { <. x , y >. | ( <. x , y >. e. A /\ x e. C ) }

!qed::                    |- B e. dom area

I believe what you need is 

h1::subarea.1      |- A e. dom area

h2::subarea.2      |- ( x e. dom A -> C C_ RR )

h3::subarea.3      |- B = { <. x , y >. | ( <. x , y >. e. A /\ y e. C ) }

!qed::                    |- B e. dom area

Also, why not try directly with the deduction version this time? ;-)
(or at least the closed version)

BR,
_
Thierry

[Benoit]

On Friday, June 14, 2019 at 3:24:42 PM UTC+2, Thierry Arnoux wrote:

Hi Jon & Benoît,

I've created the deduction version of that theorem (whatever we choose to name it). It is not a particularly hard task, just a bit long and a bit boring as explained by Benoît.  This is typically the kind of task that could be easily automated.

Thanks a lot !
 

h1::subarea.1      |- A e. dom area

h2::subarea.2      |- ( x e. dom A -> C C_ RR )

h3::subarea.3      |- B = { <. x , y >. | ( <. x , y >. e. A /\ y e. C ) }

!qed::                    |- B e. dom area

It looks false: what if C is not measurable ? (e.g. take A to be the unit square and C a non-measurable subset of [0,1])

Also, why not try directly with the deduction version this time? ;-)

Indeed !

Benoit

[Jon P]

Wow Theirry that is really cool :) Yeah nice theorem to have. Should it maybe be itgexpd for deduction? Do you think it is wise to have both versions or just the deduction one?

Re this:

h1::subarea.1      |- A e. dom area

h2::subarea.2      |- C C_ RR

h3::subarea.3      |- B = { <. x , y >. | ( <. x , y >. e. A /\ x e. C ) }

!qed::                    |- B e. dom area

what I'm trying to do is use this with iocunico to split a triangle into two halves. So for example C might be ( -oo (,] Q ) and just be the left half of the triangle. So yeah B is only meant to be this left side. I am not so sure whether your version does this, I am a bit confused. 

I think it will be ok if C is some crazy set because at each point x e. C the other properties of dmarea will hold, though I am sure I may well be wrong :)

Yeah I am happy to try to do it in deduction form :)

[Thierry Arnoux]

Hi Jon,

You can rename it as you see fit! Adding a “d” is indeed the practice.

At first I misunderstood what you wanted to do. You want a theorem that states that if a surface has an area, so has a subset of that surface.
Benoit is right, you will need additional conditions on you C for that, like probably
‘ C e. dom vol ‘
Note also that your set B can be written as ‘ B = ( A i^i ( C X. RR ) ) ‘. This is shorter and does not require a free variable.

BR,
_
Thierry

[Benoit]

I think that the inference version is not worth keeping: the deduction version is enough, and easily implies the inference form.  For the sake of illustration, here is a proof of itexp from itgexp (current labeling), using "trud" at its last step, as hinted above:

---------Clip out the proof below this line to put it in the source file:
      ( cicc co cv cexp citg c1 caddc cmin wtru cr wcel a1i cdiv cle wbr cn cn0
      wceq nnnn0 syl itgexp trud ) ABCIJAKDLJMCDNOJZLJBUKLJPJUKUAJUFQABCDBRSQET
      CRSQFTBCUBUCQGTQDUDSZDUESULQHTDUGUHUIUJ $.
---------The proof of "itexp" (186 bytes) ends above this line.

You can paste it to see how it looks in uncompressed format.

Since only the deduction form will remain, is the suffixed "d" still necessary?  Depending on Thierry's (or someone else's) answer, I suggest you (Jon) relabel it either itgpow or itgpowd, and remove the inference version (if you want: this is your mathbox, after all!).

I just did some minimization and rewrapping of some of your proofs (it's one of the later commits of the pending PR #926).  May I suggest that in the future you use

  MM-PA> minimize * /no *

when your proofs are done, to minimize them without introducing dependencies on new axioms or definitions.  Also, just before doing a PR, as indicated in https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md, you can do a general check and rewrap by typing

  $ ./metamath 'read set.mm' 'write source set.mm /rewrap' erase 'read set.mm' 'save proof */compressed/fast' 'verify markup */file_skip/top_date_skip' 'verify proof *' 'write source set.mm' quit

It rewraps everything except for the statements, i.e. in between $p ... $= (and $a..., $e... ).  For these, you have to break lines manually.  At least, do a line break after "$=".  Never use tabulations.  If the line of the statement needs to be broken, then break it after operators which are "high in the parsing tree" (I don't know how to say it precisely and concisely, but you see what I mean).

Benoit

[Jon P]

Awesome, thanks for the help :)

I agree with you Benoit that exp is a nice word for Euler's constant and related function so I've relabeled the theorem as itgpowd (I think d is consistent as it is a deduction theorem). I think it would be good to change dvexp etc too but I don't think I can do that. I removed the non-deduction version as I agree it is not so useful.

When you say to use "  MM-PA> minimize * /no *" when should I use that? I do proofs in mmj2, do I need to load them in metamath.exe somehow?

When following the list of instructions: https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md I get this error, not sure what is happening, maybe it is not important to verify markup

MM> verify markup */file_skip/top_date_skip

                                                ^^^^^^^^^^^^^

?Expected DATE_SKIP, FILE_SKIP, or VERBOSE.

MM>

It is happy if I use: MM> verify markup */file_skip/date_skip

How long is the character line in set.mm, it looks like 79 characters long, is that right? Seems like an unusual choice for the length. I understand about high in the tree I think, e.g in ((A = B) -> (C = (D + F)) the -> is high and the D+F is low.

A more general philosophical question: is there some thing about how "it must be deduction form all the way down" in the sense that if I do some proof A in non-deduction form and then B relies on A then B cannot be in deduction form. Does this mean it's important to build the whole tree in deduction form? I have the proofs arearect and areaquad and I guess I would need to go back and put them in deduction form, which maybe isn't so hard.

[Benoit]

When you say to use "  MM-PA> minimize * /no *" when should I use that? I do proofs in mmj2, do I need to load them in metamath.exe somehow?

It is not mandatory, so do not do it if it's a hassle.  Yes, it is done in the metamath program once the proof is finished.  As for me, when doing a long proof, I have three windows open: mmj2, a text editor with set.mm, and the metamath program (actually, I also have a web browser since metamath.org/mpeuni can be useful).  When I finish the proof in mmj2 (i.e. when after a ctrl+U, the compressed proof appears), I copy-paste the proof in the text editor (together with the generated $d conditions, if any), and in the metamath program, I run:
  MM> er     [for "erase"]
  MM> r set.mm   ["r" for "read"]
  MM> pr xxx  [to open the proof assistant with said theorem]
  MM-PA> min */no *
and if the program indicates that some minimization has been done, then either
  MM-PA> sh n/c  [to show the new proof in compressed format and copy-paste it in the text editor]
or
  MM-PA> sa n/c  [to have the metamath program save the new proof internally]
  MM-PA> exi
  MM> wr so set.mm/rew [to write the new proof, and rewrap]
Of course, if you do several proofs at a time, then some operations need be done for each proof and some only once, and you can guess which ones, with possibly a few trials and errors.  For shorter proofs, I do not use mmj2, but only the metamath program.

Side note: MM> min */no * is to avoid introducing new dependencies on axioms or definitions.  If you only want to avoid dependencies on new axioms, then use MM> min */no ax-*, and if you do not care at all, use MM> min *

For all of these commands, look at the metamath help by typing MM> help [command] , especially to learn about the available options.
 

When following the list of instructions: https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md I get this error, not sure what is happening, maybe it is not important to verify markup

MM> verify markup */file_skip/top_date_skip

                                                ^^^^^^^^^^^^^

?Expected DATE_SKIP, FILE_SKIP, or VERBOSE.

MM>

It is happy if I use: MM> verify markup */file_skip/date_skip

This is probably because you use an older version of the metamath program, which did not have the top_date_skip option.  If it's not a hassle, then install the newest version of the program.  Else, using /date_skip is ok: it will not check date consistencies in "Contributed ...", but if you entered them carefully, this is no problem.
 

How long is the character line in set.mm, it looks like 79 characters long, is that right? Seems like an unusual choice for the length. I understand about high in the tree I think, e.g in ((A = B) -> (C = (D + F)) the -> is high and the D+F is low.

Yes, 79.  I think 80 is standard and metamath's convention is 79 maybe because the 80th is actually a non-printable "line break" character, or something like that?  You got it right for the "high" operators.  I have to add that I wrote earlier "break after the binary operator" while Norm told me he prefers "break before"; there is no universal convention.

A more general philosophical question: is there some thing about how "it must be deduction form all the way down" in the sense that if I do some proof A in non-deduction form and then B relies on A then B cannot be in deduction form. Does this mean it's important to build the whole tree in deduction form? I have the proofs arearect and areaquad and I guess I would need to go back and put them in deduction form, which maybe isn't so hard.

I think the above exchanges show that closed and deduction forms are more applicable, while inference forms are less applicable.  So go directly for the deduction form (unless the proof is short enough that you can prove the closed form).  I think you can state more general rules like the one you wrote.  For arearect and areaquad, I would say: wait until you need the deduction form.

Benoit