Exchange management inside proofs

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

Exchange management inside proofs #165

Open olaure01 opened 3 years ago

olaure01 commented 3 years ago

Permuting formulas inside a proof has some strange consequences. Consider the proof and permute a⊗a and 1 in the middle sequent. Then:

PNG export with implicit exchange gives what is on the screen
PNG export with explicit exchange gives the original proof (no exchange rule)
going back and forth to "proof transformation" mode gives back the original proof

etiennecallies commented 3 years ago

REMARK #1: Explicit exchange ignores "display permutations". Would you prefer to display two exchanges rules ?

REMARK #2: proof transformation mode ignores "display permutations" as well. I think this can be improved, I'm on it.

My own remark: we did the choice to display only the conclusion of an exchange rule (and not its premise) when we display a proof. Yet, in construction mode we display conclusion, that's why anytime you reload a proof (when you switch to "transformation mode", when you reload a shared proof...) what is displayed changes.

olaure01 commented 3 years ago

REMARK 1: Explicit exchange ignores "display permutations". Would you prefer to display two exchanges rules ?

not clear to me, what is new is that we have a simplification function now so if export gives too many exchanges, the user can first simplify and then export again (but possibly this should be documented)

REMARK #2: proof transformation mode ignores "display permutations" as well. I think this can be improved, I'm on it.

this would be nice, I find strange in practice that going back and forth to proof-transformation-mode modifies the proof

etiennecallies commented 3 years ago

REMARK 1: Explicit exchange ignores "display permutations". Would you prefer to display two exchanges rules ?

not clear to me, what is new is that we have a simplification function now so if export gives too many exchanges, the user can first simplify and then export again (but possibly this should be documented)

I wonder if the two exchanges are worth it to be implemented... I think it's only ocaml side if you decide to code it.

REMARK #2: proof transformation mode ignores "display permutations" as well. I think this can be improved, I'm on it.

this would be nice, I find strange in practice that going back and forth to proof-transformation-mode modifies the proof

Fixes deployed on preprod.