Highlight ancestors and descendants in transformation mode

[etiennecallies]

Implements #18

[etiennecallies]

Works rather fast. Can be tested on preprod @lionelvaux @olaure01

[lionelvaux]

Excellent job!

Two complaints:

• we want this in proof construction mode too,
• I think it would be visually more appealing if the formula under the pointer was highlighted too.

And one thing that should be discussed: currently, a formula (say A⊗B) is considered as ancestor of each of its subformulas (say A) above the corresponding rule (say the ⊗ rule). Maybe it would be better if we could highlight only the corresponding subformulas (say A inside A⊗B). This would allow to distinguish between the two cut free proofs of A⊗A⊸A⊗A for instance.

[etiennecallies]

Thanks @lionelvaux for your comments !

• we want this in proof construction mode too

Do we want a special option like "highlight ancestors" that would be available to toggle on/off both in construction and transformation mode? Or do we want the ancestors highlighting to be always on?

• I think it would be visually more appealing if the formula under the pointer was highlighted too.

I see one issue: we want the connectives to be clickable (for example reversible connectives to be applied first). So I would rather keep the highlighting for connectives, but we can underline ancestors instead. Let me try that and show you.

And one thing that should be discussed: currently, a formula (say A⊗B) is considered as ancestor of each of its subformulas (say A) above the corresponding rule (say the ⊗ rule). Maybe it would be better if we could highlight only the corresponding subformulas (say A inside A⊗B). This would allow to distinguish between the two cut free proofs of A⊗A⊸A⊗A for instance.

Would be painful to implement at subformula level... You can hover the subformula in the premisse of the tensor rule in your example, isn't it enough?

[etiennecallies]

Underline instead of hightlight can be tested on preprod @lionelvaux don't hesitate to propose other UI possibilities it is very easy to implement.

[lionelvaux]

Underline instead of hightlight can be tested on preprod @lionelvaux don't hesitate to propose other UI possibilities it is very easy to implement.

Very nice. This version is less distracting than the highlighted one and it is a good thing to distinguish visually between ancestry relations and clickable connectives.

The only other visual rendering of ancestry I can think of is actually drawing the tree over the proof (i.e. drawing a line from each formula to its predecessor), but I guess this would require more than CSS tricks.

[lionelvaux]

Thanks @lionelvaux for your comments !

• we want this in proof construction mode too

Do we want a special option like "highlight ancestors" that would be available to toggle on/off both in construction and transformation mode? Or do we want the ancestors highlighting to be always on?

A toggle would be nice, because moving the mouse over the proof makes information flash all over the place and it might distract the attention of the user.

And one thing that should be discussed: currently, a formula (say A⊗B) is considered as ancestor of each of its subformulas (say A) above the corresponding rule (say the ⊗ rule). Maybe it would be better if we could highlight only the corresponding subformulas (say A inside A⊗B). This would allow to distinguish between the two cut free proofs of A⊗A⊸A⊗A for instance.

Would be painful to implement at subformula level... You can hover the subformula in the premisse of the tensor rule in your example, isn't it enough?

It isn't. Here are two proofs, that should be distinct:

https://ccll.linear-logic.org/?s=A*A-oA*A&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJSCC8%2FPl15o2cdBQSb4YZcxhmXAc51ccjjCsG2aTjqo3uH20pPJTwn8eE9mJnAi9q3MUXBvMaCdWVe01YvCvbsjrT38%2Fl3KnhNVhSOQ3ORb5%2FArdA88n9cj8di%2BY66hknkG%2BDdM9Nk0iNXl8V%2BOU4Z4HelgFg6bapZ1GGMeCZOqMYoFKm%2BAmmeeVmMdaid5mIC37QiC3D1W2LnxKf54%2BypVYXmGcAk2U23XQRBMEQEk2MYgqPnirL%2FBGPfRkcj2CYGs1mIl%2F0BOKFDyVz9aUDaN8hBTFEGvxvUyliPOvWj9DzNu

https://ccll.linear-logic.org/?s=A*A-oA*A&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJSCC8%2FPl15o2cdBQSb4YZcxhmXAc51ccjjCsG2aTjqo3uH20pPJTwn8eE9mJnAi9q3MUXBvMaCdWVe01YvCvbsjrT38%2Fl3KnhNVhSOQ3ORb5%2FArdA88n9cj8di%2BY66hknkG%2BDdM9Nk0iNXl8V%2BOU4Z4HelgFg6bapZ1GGMeCZOqMYoFKm%2BAmmeeVmMdaid5mIC37QiC3D1W2LnxKf54%2BypVDheb4GEMFF4bWpUSFsyJknNpmy5fflkkHZkU3Hz0HgZeZAKfNnGAuKpIgb8JEZnu5yaEJaqNEip%2Bwc7Aqvvk%2F8PLlvo%3D

Currently there is no way to distinguish between them (i.e. there is no way to know which subformula of A^&A^ is involved, e.g., in the axiom on the left) other than exporting to Coq and looking at the permutation rule.

[olaure01]

There is apparently a bug in:
https://ccll.linear-logic.org/?s=A*A-oA*A&p=XQAAgAD%2F%2F%2F%2F%2F%2F%2F%2F%2F%2FwA9iIoHZADSvL4AO2WnajJ4cSZ3uOM1Jm1oajsTKyplYJSCC8%2FPl15o2cdBQSb4YZcxhmXAc51ccjjCsG2aTjqo3uH20pPJTwn8eE9mJnAi9q3MUXBvMaCdWVe01YvCvbsjrT38%2Fl3KnhNVhSOQ3ORb5%2FArdA88n9cj8di%2BY66hknkG%2BDdM9Nk0iNXl8V%2BOU4Z4HelgFg6bapZ1GGMeCZOqMYoFKm%2BAmmeeVmMdaid5mIC37QiC3D1W2LnxKf54%2BypVYXmGcAk2U23XQRBMEQEk2MYgqPnirL%2FBGPfRkcj2CYGs1mIl%2F0BOKFDyVz9aUDaN8hBTFEGvxvUyliPOvWj9DzNu&proofTransformation=1
Putting the mouse over a formula in the axioms leads to highlighting formulas of a different type just below.

[etiennecallies]

My fix doesn't work, I need to review the way we handle implicit permutation on javascript side.