Revisited local and global monotonicity #4794
Conversation
|
|
The comment section of ax6er should end like this: |
set.mm
Outdated
|
|
||
| $( | ||
| This theorem is proved but it depends on 7 theorems from Thierry Arnoux's | ||
| mathbox. Therefore, I'm putting it in comments for now. |
There was a problem hiding this comment.
... then these 7 theorems could/should be moved to main. Alternatively, ~boolesineq can be moved to TA's mathbox (if @tirix agrees), as long as it not used in another mathbox.
There was a problem hiding this comment.
Ok for me to move to my mathbox if you'd like, I think that would be better than commenting out since the theorem will be "alive" and benefit of global changes like renames, etc.
I suppose the 7 theorems are just the first layer of the onion and more theorems from Measure Theory would be possibly pulled, so the question is about "moving Measure Theory to main": Glauco also has his own development of Measure Theory in his mathbox and ideally we would have a deep discussion about which is better, and either choose one to move, or move a merged version.
There was a problem hiding this comment.
I'm also OK with such a move! Though I think a global section on probability theory should be considered sometime (but not too hastily as some conventional formalizations can be weaker than other ones).
|
@ProgramCrafter You need to resolve the merge conflicts first, before we can add this to set.mm |
|
The conflicts are trivial to solve, but:
|
|
|
By the way should I add this change-set entry? |
I don't think it's mandatory as it does not impact "main", but I'd suggest you do it anyway for keeping the record. |
|
What do you mean by |
|
It named a list of theorems to expand database actually. In my experiments it wasn't capable of writing valid Metamath syntax even for expressions 😢 (guess something more agentic or with a special tool could prove theorems tho). |
|
Thanks! Even that is actually interesting. I'm still curious if it suggested any other theorem! FYI there is a wiki page about automated proving. |
|
I've got why it failed the first time! Metamath is very non-famous actually, but LLM could somewhat infer the language from actual examples. It suggests quite a bunch: |
Co-authored-by: Steven Nguyen <[email protected]>
There was a problem hiding this comment.
A good reason must be given why the theorem ~ax6er is used in the proof of ~ormkglobd! If it can be replaced by ~ax6ev, then this would be preferred. If not, maybe a theorem ~ax6erv can be proven (reversed version of ~ax6ev, such as ~ax6er is the reversed version of ~ax6e).
| @@ -20730,6 +20738,11 @@ theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the | |||
| ax6 $p |- -. A. x -. x = y $= | |||
| ( weq wex wn wal ax6e df-ex mpbi ) ABCZADJEAFEABGJAHI $. | |||
|
|
|||
| $( Commuted form of ~ ax6e . (Contributed by BJ, 15-Sep-2018.) | |||
| (New usage is discouraged.) $) | |||
There was a problem hiding this comment.
Why was this used and moved to main, although its usage is declared to be discouraged? There should be a very good reason for using such a theorem! The comment of ~ ax6e, which is also discouraged to be used, says that ~ax6ev should be used instead. Why is this not possible (in the proof of ~ormkglobd)?
@benjub this theorem was in your mathbox before. What was your intention to create it? Why is it used in the proof of ~exlimiieq2 (only)?
There was a problem hiding this comment.
I tried to inline its proof and use ax6ev (with appropriate $d conditions), and metamath-exe did not report any error nor unified the proof correctly (i.e. treated the full theorem as unproved). Should be possible though.
@avekens I'm OK if you amend the proof to avoid usage of ~ ax6er too.
There was a problem hiding this comment.
There is aready a reversed version of ~ax6ev in set.mm: ~ax6evr. This should be applicable instead of ~ax6er resp. ~ax6ev.
There was a problem hiding this comment.
Quite surprisingly metamath-exe just failed to unify setvar assignments automatically!
6723 vx=? $? setvar k
6724 vy=? $? setvar b
6725 exlimiiv.2=ax6evr $p |- E. k b = k
6726 syl2anc.3=exlimiiv $p |- ( ( ph /\ b e. ( 0 ..^ T ) ) -> ( B
` b ) R ( B ` ( b + 1 ) ) )
6727 sotrd.6=syl2anc $p |- ( ( ( ph /\ k e. ( 0 ..^ T ) ) /\ ( b
e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) R ( B ` b ) ) -> ( B ` b ) R (
B ` ( b + 1 ) ) )
6728 fzindd.6=sotrd $p |- ( ( ( ph /\ k e. ( 0 ..^ T ) ) /\ ( b
e. ZZ /\ ( k + 1 ) <_ b /\ b < T ) /\ ( B ` k ) R ( B ` b ) ) -> ( B ` k ) R (
B ` ( b + 1 ) ) )
MM-PA> assign 6724 vb
MM-PA> assign 6723 vk
CONGRATULATIONS! The proof is complete. Use SAVE NEW_PROOF to save it.
Note: The Proof Assistant does not detect $d violations. After saving
the proof, you should verify it with VERIFY PROOF.
MM-PA> save new_p
/ or nothing <nothing>?
The new proof of "ormkglobd" has been saved internally.
Remember to use WRITE SOURCE to save changes permanently.
MM-PA> q
Exiting the Proof Assistant. Type EXIT again to exit Metamath.
MM> ve pr *
0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%
..................................................
All proofs in the database were verified in 4.29 s.
There was a problem hiding this comment.
Yeah I think automatic one step proofs and unifications happen when doing improve all
No description provided.