Implicit exchange - Githubissues

ComputerAidedLL / click-and-collect

A web interactive tool for building proofs in the sequent calculus of Linear Logic, with its backend written in OCaml

GNU Lesser General Public License v2.1

17 stars 2 forks source link

Implicit exchange #99

Closed olaure01 closed 3 years ago

olaure01 commented 3 years ago

Extend the exchange rule with an additional permutation which can be used to encode the current state on screen and relied on for export with an implicit exchange rule. LaTeX export is extended with an implicit exchange version.

olaure01 commented 3 years ago

What should be looked at for this PR I think is:

should a second permutation be added on the json/rule-request side, and how?
how is the second permutation updated by the user doing drag&drops inside the ongoing proof?

etiennecallies commented 3 years ago

What should be looked at for this PR I think is:

should a second permutation be added on the json/rule-request side, and how?

how is the second permutation updated by the user doing drag&drops inside the ongoing proof?

I'm on it. A commit is coming soon.

etiennecallies commented 3 years ago

Implicit exchange should work on preprod except if proof starts with an exchange (cf. comment above). May I activate it (with Proof.to_latex (Some None))?

olaure01 commented 3 years ago

Once the code is correct, we could start testing things on pre-prod by using Proof.to_latex None for LaTeX export and Proof.to_latex (Some None) for png export (no opinion for pdf). In a second step this could become an option giving an uniform result for all three exports.

etiennecallies commented 3 years ago

Once the code is correct, we could start testing things on pre-prod by using Proof.to_latex None for LaTeX export and Proof.to_latex (Some None) for png export (no opinion for pdf). In a second step this could become an option giving an uniform result for all three exports.

On preprod:

PDF and Tex: explicit exchange
PNG: implicit exchange

olaure01 commented 3 years ago

There is something to decide regarding the concluding sequent when it has been permuted and thus is different from the original submitted one:

for explicit exchange, I would keep the original sequent as conclusion of the exported proof (as before)
for implicit exchange, should we do the same or have the displayed sequent as concluding sequent so that it could lead to a real snapshot? it is not clear in my mind: on the one side the idea of a snapshot is clear, on the other side the submitted sequent could be considered meaningful (and the user should submit the commuted version if this is what he wants to prove).

I would say, always keeping the original sequent is more general. @etiennecallies do you have a more definite opinion?

etiennecallies commented 3 years ago

I like the idea of snapshot. It is simple to understand.

Why would the user have changed the concluding sequent?

Because he wanted the LaTeX that way
Because he needed to permute (before a tensor) -> he can still permute the concluding sequent again.

olaure01 commented 3 years ago

OK for me. Should we then apply the same reasoning to explicit exchange export?

olaure01 commented 3 years ago

There is some exchange simplification to do (I did not really investigate the cause): A*A^,A|A^: auto-prove, then permute conclusions then pdf export: useless concluding identity exchange rule.

etiennecallies commented 3 years ago

I would say:

implicit permutation mode: we return a LaTeX-ed snapshot of the proof
explicit permutation mode (aka strict mode): we print an exchange rule only where needed (before tensor), and derivation rules are strictly respected through the proof (thus we ignore display_permutation).

It's what should be deployed on preprod. It seems natural to me. But I'm very opened to alternatives.

olaure01 commented 3 years ago

It looks good to me.

etiennecallies commented 3 years ago

I merge this, and will add the UI option (explicit/implicit) in another PR. Thanks