Zulip Chat Archive

Stream: new members

Topic: CD editor with Lean proof logic


view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:05):

@Patrick Massot I'm making a commutative diagram editor, that assists you or offers options for the next step to take in proving something.

The graphical part is already written (last year's personal project) in PyQt5 and it's very nice. It even stores the undo/redo stack so even if you restart your machine, you can still undo from where you left off. Things it would assist with would be stuff like:

If I take an element 'x' at this module (a node), then there should be an element 'f(x)' in this other mapped to module. And so on.

I used to have videos up on YT showing its capabilities. I'll work on it this week and post a video for you to get a better idea of it.

view this post on Zulip Patrick Massot (Aug 24 2019 at 08:09):

So you want your software to write Lean code and simply ask Lean to check it? It looks like you could even get away with using lean in command line mode (although using the Lean server would be faster for incremental changes)

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:09):

Yes, I think server mode for now, but I will try both.

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:10):

I guess the "proof ideas" have to come from my app?

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:11):

I'm not 100% sure how Lean works, I will learn more about it this coming week

view this post on Zulip Patrick Massot (Aug 24 2019 at 08:11):

It depends on the proof. Again it would help to have a full example of some proof you'd like your software to handle

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:12):

I have an image on MSE

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:12):

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:12):

That's done in Paint3D not the app

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:14):

BananaCats_IsomorphismArrow.png

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:15):

There's one version's screenshot. It also supports nodes within nodes, but I'm thinking of defeaturing that for the sake of graphics scene speed in PyQt5.

view this post on Zulip Patrick Massot (Aug 24 2019 at 08:16):

About the drawing part, are you aware of https://tikzcd.yichuanshen.de/?

view this post on Zulip Patrick Massot (Aug 24 2019 at 08:16):

About your first picture, I'm afraid I don't understand the statement

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:16):

Yep, I've used that before. The editing in BananaCats is a lot easier.

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:17):

Oh it's a visual proof of (part of) Yoneda's lemma, but obviously not 100% visual since there's that added remark at the bottom.

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:19):

I'm thinking of breaking the proofs up into "slides" (actually application tabs).
So you'd click a button to functor, enter in the functors name, and it pops open the functored diagram.

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:19):

Also supports positional reflection of arrows / nodes, so if you modify the source diagram, you can optionally (by default) automatically position the parts of the target diagram.

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:22):

As far as "diagram rules" go, I'm not sure precisely how I'll accomplish that. I've heard of Double-Pushout Rewriting of graphs, but it's scope is limited to adhesive categories (a lot of which are the usual categories). But I'm sure Lean will help a lot with the logic part. Rule intro / elimination etc. I have to figure out a way to encode the diagrams into Lean code eventually.

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:25):

Also will support drag-n-drop between app instances, and drag-n-drop of an image and text into the browser (for posting on say MSE).

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:26):

Drag-n-drop of the objects in the scene already works, that's how I do copy/paste actually.

view this post on Zulip Daniel Donnelly (Aug 24 2019 at 08:26):

:slight_smile:


Last updated: May 08 2021 at 04:14 UTC