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.
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
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.
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.
#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.
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.
sbcex2
and its universal counterpart)