Exchange management inside proofs

[olaure01]

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]

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]

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]

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.