CD editor with Lean proof logic

Stream: new members

[Daniel Donnelly]

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

[Patrick Massot]

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)

[Daniel Donnelly]

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

[Daniel Donnelly]

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

[Daniel Donnelly]

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

[Patrick Massot]

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

[Daniel Donnelly]

I have an image on MSE

[Daniel Donnelly]

[Daniel Donnelly]

That's done in Paint3D not the app

[Daniel Donnelly]

BananaCats_IsomorphismArrow.png

[Daniel Donnelly]

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.

[Patrick Massot]

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

[Patrick Massot]

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

[Daniel Donnelly]

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

[Daniel Donnelly]

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.

[Daniel Donnelly]

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.

[Daniel Donnelly]

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.

[Daniel Donnelly]

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.

[Daniel Donnelly]

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

[Daniel Donnelly]

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

[Daniel Donnelly]

:slight_smile: