- Join over
**1.5M+ people** - Join over
**100K+ communities** - Free
**without limits** - Create
**your own community**

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.

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")

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.

@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
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.

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

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?)

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.

That sounds like something I should look at, thanks! For my future reference: https://leanprover.github.io/reference/expressions.html#structured-proofs

(in this specific case, I would like to do that for

`sbcex2`

and its universal counterpart)