Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
    Mario Carneiro
    @digama0

    Grand Opening of the Metamath chat room!

    If you prefer the chat experience to a mailing list (i.e. you send three one word emails in a row), this may be for you. This chat room is intended for quick questions or remarks relating to metamath in some way, and is associated with the github "metamath" organization (which hosts the set.mm repository).

    I'm not sure if it will get any use, but it doesn't hurt to open it up and see who likes it!

    I would ask that anything really substantial goes on the mailing list, though (or at least is repackaged into a post on the mailing list), so that we don't get any further fracturing of the knowledge which is distributed across several media.

    I know that there are many people who like to lurk on the list, and I hope that the new format will make it easier to contribute.

    jn1z
    @jn1z
    As one of the lurkers, I'll volunteer that it's an Interesting idea. IIRC, Coq has/had a chatroom also (where I discovered in real-time that their declarative feature was known to be horribly broken)
    Giovanni Mascellani
    @giomasce
    Hi everybody. I am trying to learn Metamath to add a few proofs to set.mm. Is this a good place for newbie questions?
    Stefan 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")
    Stefan 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.
    Stefan 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...
    Stefan 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
    Stefan 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)