Revisited local and global monotonicity #4794
Conversation
|
|
The comment section of ax6er should end like this: |
|
@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).
set.mm
Outdated
| @@ -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
|
Please move ax6er back tio BJ mathbox (and remove discouraged tag), so restore it as it was before. |
There was a problem hiding this comment.
(wait I cannot request changes on my own PR?
it will probably be a draft until @benjub 's answer)
set.mm
Outdated
| @@ -578732,6 +578727,11 @@ References are made to the second edition (1927, reprinted 1963) of | |||
| ( wal wi 2sp gen2 nfa2 nfa1 2stdpc5 ax-mp ) ACDZBDZAEZBDCDMABDCDENCBABCFGMA | |||
| CBACBHLBIJK $. | |||
|
|
|||
| $( Commuted form of ~ ax6e . (Could be placed right after ~ ax6e ). | |||
There was a problem hiding this comment.
Apparently it could not be placed right after ~ ax6e .
| @@ -131,6 +132,9 @@ Date Old New Notes | |||
| 30-Apr-25 idomrootle [same] Moved from SO's mathbox to main set.mm | |||
| 30-Apr-25 ply1ascl0 [same] Moved from TA's mathbox to main set.mm | |||
| 30-Apr-25 hashf1dmcdm [same] Moved from BT's mathbox to main set.mm | |||
| 30-Apr-25 sotrd [same] Moved from SF's mathbox to main set.mm | |||
| 30-Apr-25 ax6er [same] Moved from BJ's mathbox to main set.mm | |||
There was a problem hiding this comment.
I think after this entry is removed (ax6er is not moved from BJ's mathbox anymore), this PR will be fine.
No description provided.