Definition of the structure product (df-prds)

[zwang123]

The definition of the structure product df-prds includes d e. ( c h ( 2nd ` a ) ) but I suppose this should be d e. ( ( 2nd ` a ) h c )?

Because it seems to me that ( x ( Hom ` c ) y ) is the hom-class of morphisms from x to y from observing the definition df-cat.
If this is the case, e should be a morphism from ( 1st ` a ) to ( 2nd ` a ), and d should be a morphism from ( 2nd ` a ) to c in the definition (pasted below).

        <. ( comp ` ndx ) , ( a e. ( v X. v ) , c e. v |->
           ( d e. ( c h ( 2nd ` a ) ) , e e. ( h ` a ) |-> ( x e. dom r |->
             ( ( d ` x ) ( <. ( ( 1st ` a ) ` x ) , ( ( 2nd ` a ) ` x ) >.
               ( comp ` ( r ` x ) ) ( c ` x ) ) ( e ` x ) ) ) ) ) >.

Apologize if I misunderstood. But if this is actually an error, how was it not detected by verifications?

Update: created a TODO list for this issue.

[icecream17]

I think you are probably right, though this error would not be detected as this component is never used: https://us.metamath.org/mpeuni/prdsco.html

@sorear @tirix

[zwang123]

Understandable. Is it possible to automatically verify theorems or definitions not referenced by others lest such things happen again, by, for example, adding some examples?

[icecream17]

Usually examples are not automatically made, but they are indeed very effective in ensuring definitions are at least correct enough to have all the properties proven

[david-a-wheeler]

We can verify that a theorem verifies against the definitions it uses, but we can't directly verify that a given definition is the "right" definition except by proving that it has the expected properties.

I agree with @icecream17 that examples are an excellent way to verify that a definition has certain properties that you expect. They also help illustrate how to use the definition.

The "conventions" section even enshrines this. If you look at point "Definitions (df-...)" it says: "We encourage definitions to include hypertext links to proven examples."

[zwang123]

Maybe I can do a quick fix to this. But this is the first time so I am not sure if I fully comprehend the rules though I read some pages...

[icecream17]

Note: I am now closer to 99% sure this change is correct by comparing prdsco with df-comf

Since metamath also proves expressions are syntactically valid (in steps that are hidden on the website, and done automatically when typing in an essential step), one would have to additionally "revise" reldmprds, prdsval, and 11 component theorems, even though all the steps are the same (including prdsval and prdsco!)

Which is a lot harder to do as a beginner, but as an example there is: https://github.com/metamath/set.mm/pull/931/files

1. In the comment of df-prds and prdsco (and optionally other theorems) add (Revised by [name], xx-Aug-2024.)
2. Fix the conclusion (and hypotheses) of df-prds, prdsval, and prdsco
3. Reprove reldmprds, prdsval, and the 11 component theorems

[icecream17]

Now that I think about it, it is decently common to have to revise proofs in this way. There has to be a way to automate this, since metamath.exe supports submitting commands

(the command file would look like:)

prove theorem
assign last theorem2

assign last theorem3

...

So all one needs is a list "theorem2" "theorem3", etc. (duplicates may happen since theorems may be used multiple times in a proof). I do not know any way to do this, however

[zwang123]

Note: I am now closer to 99% sure this change is correct by comparing prdsco with df-comf

Since metamath also proves expressions are syntactically valid (in steps that are hidden on the website, and done automatically when typing in an essential step), one would have to additionally "revise" reldmprds, prdsval, and 11 component theorems, even though all the steps are the same (including prdsval and prdsco!)

Which is a lot harder to do as a beginner, but as an example there is: https://github.com/metamath/set.mm/pull/931/files

1. In the comment of prdsco and prdsco (and optionally other theorems) add (Revised by [name], xx-Aug-2024.)
2. Fix the conclusion (and hypotheses) of df-prds, prdsval, and prdsco
3. Reprove reldmprds, prdsval, and the 11 component theorems

Thanks for figuring it out. After solving many technical issues (e.g., lamp doesn't seem to work with vars containing . like .+ and .<_; the heap memory size for mmj bat is too small, etc ), I think I can work on this.
(Already done for df-prds, reldmprds, and prdsval.)

Now that I think about it, it is decently common to have to revise proofs in this way. There has to be a way to automate this

It would be excellent to have such a thing and release it as a public API. But for now I think I can handle it manually thanks to its small scale.

[zwang123]

I have finished fixing the definition. At least I think I have done so. The remaining task is to add examples for the definition, which could be a little out of scope for a first-time (or second-time) contributor.

I created a TODO list for future reference. Please remind if anything is missing.

TODO list

• Fixing the definition, df-prds -> (Fix df-prds #4138)
• Adding examples for df-prds
• Automating proof changes like this (optional)
• Forcing proven examples for new definitions? (e.g., setting it as a rule) (optional)
• Variables containing . for lamp (optional)
• Max heap size for mmj (looks like it is fixed to 1280M in latest branch; maybe need to update the link in this page) (optional)
• Blank lines not detected in metamath.exe formatting (this change was not forced by the program) (optional)