Is there a limit to complexity of custom block?

[michaelgwelch]

I wanted to prove the identity (∀x P(x)) → ⏊ ≡ ∃x(P(x) → ⏊)

and make a custom block out of it. My first attempt used two instances of my proof by contradiction custom block. Once I multi-selected the custom blocks the "new custom block" disappeared. So I assumed I could used custom blocks in the definition of a custom block.

So I rewrote the proof using just the built-in proofs. As soon as I get near to selecting all of the blocks then the new custom block disappears. Due to complexity?

For reference this is my proof. Would love to create a custom block out of this to finish the proof I asked about a few days ago.

[nomeata]

Yes, there are limits to the complexity, because not every proposition is expressible by our block format, but they are not clearly defined (yet), and the system does not provide any feedback.

Sometimes it may help to select further blocks, as it simplifies the “interface”. It may of course also be simply a bug. But to root that out, it would be helpful if you could provide a minimal example of a set of blocks where you want to create a custom block from, but can’t.

Also, when you select blocks, in order to calculate the custom block, the system pretends that all other blocks have been removed and checks that graph. So to see if that works, detach all the blocks that you do not want to be part of the custom block and see if it can make sense of the rest.

Oh, and also: Do not select assumptions and conclusions when creating custom blocks. (I think they should be ignored, but I’m not sure if they actually are.)

[nomeata]

Not sure if there is anything actionable here; closing.

[alreadydone]

I can't create these two custom blocks, which seem simple enough:

[nomeata]

There are some limits. In the second picture, I see something in “New custom block” … does it not work?

With the first one, I think the problem might be the empty output in Block 10 … I vaguely remember that that causes problems, and I was wondering if we need a block that “eats inputs” without producing any.

[alreadydone]

When you select the last block, "New custom block" would disappear. Finally created a workaround custom block to solve this fun exercise ...

[alreadydone]

Another custom block (consisting of two sub-custom blocks) that I can't create:

[nomeata]

Hmm, does it work if you disconnect the two from the rest (so that no c14 constant shows up)?

[alreadydone]

Still doesn't work after disconnecting. (and the internal implementation detail doesn't matter, right? I think I read it somewhere.)

[nomeata]

Can you give me a screenshot of the two blocks, disconnected, with unconnected wires on all ends (to see what’s on there)

[alreadydone]

Hmm, there's a red line with question mark on it; I've seen such thing before and it only turns grey when connected properly to other blocks.

[nomeata]

Ah, the problem is higher-order unification. Notice the P4(y4) on the left? It does not know what predicate P4 is. You might be able to help the system with a annotation block (the one where you can write the formula), maybe on the left of block 4.

[alreadydone]

Thanks! When I include an annotation block, not only I can create both a custom block for the two blocks , but also for the whole proof. Things don't work if the annotation block is not included.

[nomeata]

Yay :-)