Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    Stef O'Rear
    @sorear
    Ask anywhere, we were all newbies once
    Giovanni Mascellani
    @giomasce
    Thank you. Basically I am trying to write some proofs in Metamath and I continue running on things that appear to be trivial to me, but that I don't know how to tell Metamath (I am a math PhD student, but not a logician). For example, many theorems can come under two different forms: 1) using Metamath hypotheses and thesis, like in "|- ph & |- ps => |- ch"; 2) expressing everything in one implication, like in "|- ( ph /\ ps ) -> ch". In general I find it easy to pass from 2 to 1, but do not know how to pass from 1 to 2. Is there a way or is number 2 actually more powerful?
    ("pass from 2 to 1" means "if I have a theorem expressed in form 2 I know how to prove the equivalent theorem in form 1")
    Stef O'Rear
    @sorear
    There's no way in general. number 2 is more powerful. (there are some tricks that can be used in a subset of cases, look at theorem "dedth" and http://us.metamath.org/mpegif/mmdeduction.html , but those tricks are deprecated; new results are almost always done in method 2). The link has useful background regardless.
    Giovanni Mascellani
    @giomasce
    Thank you.
    Giovanni Mascellani
    @giomasce
    Another question: ax-13 says that "|- ( x = y -> ( x e. z -> y e. z ) )". Is there an equivalent result for classes? For example, "|- ( ( A e. _V /\ A = B ) -> ( A e. z -> B e. z ) )". I tried to prove it, but could not.
    Stef O'Rear
    @sorear
    @giomasce That follows from eleq1 and prepositional logic
    Giovanni Mascellani
    @giomasce
    Thanks again. One of the major challenges I am facing while learning Metamath is to have a grip on the set.mm database. It is very difficult to find the needed theorems at the beginning.
    tirix
    @tirix
    Hi there! Something not substantial : ~ pwundif does not seem to bring much. It states |- ~P ( A u. B ) = ( ( ~P ( A u. B ) \ ~P A ) u. ~P A ), but that could be simply derived from |- A = ( ( A \ B ) u. B ), no need to involve power set here...
    Stef O'Rear
    @sorear
    @tirix your second statement is not true without an assumption that B C_ A ( ~ undif ), or in this case ~P A C_ ~P ( A U. B ), which you would have to get from probably ~ ssun1 and ~ sspwb; Norm always likes shorter versions of proofs, and this seems like a relatively easy one to put together
    tirix
    @tirix
    @sorear Exactly! In that case, there's even ~ pwunss. The proof can be much shorter, like :
    ( cun cpw cdif undif1 wss wceq pwunss unss mpbir simpli ssequn2 wa mpbi eqtr2i ) ABCDZADZERCQRCZQQRFRQGZSQHTBDZQGZTUBNRUACQGABIRUAQJKLRQMOP
    Stef O'Rear
    @sorear
    @tirix Send that to Norm, not me
    tirix
    @tirix
    @sorear Will do!
    Marnix Klooster
    @marnix
    So... after a long time of silence, I've found me a use for this channel. Some of you may have seen emails from me on the Metamath mailing list, about a 'calculational proof format'. Those didn't really generate much response as far as I remember, but this might be more suitable for a chat format like here. So I'd like to throw out some ideas and see what you think.
    This will be a fair bit of monologue at first, but hopefully that will change soon. :-)
    Let me start with a stake in the ground, and as an example let me use the proof for 'reccot' (tan=1/cot) from David Wheeler's nice mmj2 video (https://youtu.be/Rst2hZpWUbU?t=296).

    The stake is this: I shouldn't need to write down more than the essence of this argument (see also reccot), which is

    In the context  |- ( ( A e. CC /\ ( sin ` A ) =/= 0 /\ ( cos ` A ) =/= 0 ) -> ... ) , we have
    
       ( 1 / ( cot ` A ) )
    =     "by (cotval)"
       ( 1 / ( ( cos ` A ) / ( sin ` A ) ) )
    =     "by (recdiv) using (sincl) and (coscl)"
       ( ( sin ` A ) / ( cos ` A ) )
    =     "by (tanval)"
       ( tan ` A )

    All other steps that are needed, are fully generic rules for transitivity, "windowing" rules (here: oveq2d used in the first step), context manipulation rules, and commutativity rules (not in this specific proof). Automation should be able to find those steps.

    So that's my stake-in-the-ground. Note that mmj2 is of course already quite a step up from metamath.exe's proof assistant mode, on the way towards that goal. But having more automation would be very welcome. And I think that a 'calculational proof format' could simplify/guide that automation effort.
    Marnix Klooster
    @marnix
    So there are two things I'd like to have. First, I'd have to have some tool or environment (like mmj2) which is such a proof assistant-- and that environment should be extensible, to also support, e.g., Mario Carneiro's arithmetic proof search algorithms.
    Second, I'd like to have some way in which to mark/store/annotate set.mm proofs so that the calculational (or arithmetical, or whatever) essence of the Metamath proof is kept, in such a way that that essence can also be used in other ways and by other tools.
    Let me focus on the first for now: an extensible Metamath proof assistant with a 'calculational' focus. My idea is to use DrRacket for this, an IDE for the Racket language (https://racket-lang.org/).
    So we could create a Racket language (#lang mmcalc?) which allows import set.mm, parsing it using specific $j-like rules, and then give a calculation like the one above, and then e.g. output the resulting proof to a .mm file.
    And then we can also allow partial proofs, so that running the code would list the sub-goals that still need to be filled in. And when running in the DrRacket IDE, we can use the https://github.com/david-christiansen/todo-list tool to give the user a nice list of those sub-goals. And that DrRacket IDE would then of course also have commands / shortcuts to complete proofs, search for relevant statements, etc.
    (end of initial monologue :-) what do you think so far? does this match in any way what others here have been thinking about?)
    Mario Carneiro
    @digama0

    I've been thinking about something similar for a long time. I work primarily with lean now, and the "plain proof" mode there includes the concept of a calc block, which would look like:

    calc 1 / cot A
        = 1 / (cos A / sin A) : by rw cotval
    ... = sin A / cos A : by rw recdiv
    ... = tan A : by rw tanval

    which is clearly very similar in spirit to your version. I've wanted a proof interface for metamath in lean for a long time now, and some recent developments are making this more practical, but it's certainly a long term project with no completion date right now.

    Marnix Klooster
    @marnix
    That sounds like something I should look at, thanks! For my future reference: https://leanprover.github.io/reference/expressions.html#structured-proofs
    Giovanni Mascellani
    @giomasce
    Hi! I think there is a general trick to replace a $d x A or $d x ph$ condition in a theorem with the corresponding F/_ x A or F/ x ph, but I do not remember it. Can anybody help me?
    (in this specific case, I would like to do that for sbcex2 and its universal counterpart)
    Anarchos
    @Sylvain78
    I would like to know why is set.mm so big, and not split in other files which could be included ?
    Mario Carneiro
    @digama0
    @Sylvain78 As you can probably see from the frequency of messages, this chat room is basically dead. I would recommend you ask your question at https://groups.google.com/g/metamath for better visibility
    tirix
    @tirix
    In short, I think Norm wished to keep the database completely self-contained, and felt better with a single date at the top as a version marker for the whole.
    Mario Carneiro
    @digama0
    The short answer to your question is that it was Norm's preference; it makes some kind of text searches simpler and as long as you have a good editor it's still possible to work with it just as well