Explicit Exchange

• Discussion: issue #11
• Goal: display explicit exchange rules in the interface
• Code: provided as an option
• Interface:
  • drag and drop is restricted to hypotheses of proofs (if applied inside a proof, reset proof to this point)
  • a drag and drop operation on a sequent which is not premise of an explicit exchange rule generates an exchange rule
  • a drag and drop operation on a sequent which is premise of an explicit exchange rule does not generate a new rule and updates the permutation
• Options / Choices:
  • mention the permutation in the rule name
  • use explicit exchange rules of the shape ⊢ Γ, A, Δ, Σ ⟷ ⊢ Γ, Δ, A, Σ (thus matching each drag and drop operation)
  • add colors to follow occurrences

Cyclic Proofs

• Goal: dealing with infinite proofs through back edges connecting a proof leaf to an identical sequent met previously during proof construction
• Interface: drag and drop a turnstile symbol to another sequent which is equal (not up to permutation since permutation is meaningful) and lower in the proof (this has to be checked)

Proof Transformations

• Discussion: issue #119
• Goal: define a special mode for proof transformations
• Interface:
  • activate proof-transformation mode (which deactivates other options, keeps export, possible to come back to proof-editing mode)
    • completely changes the impact of clicking on proofs: current proof is frozen
    • no drag-and-drop at all
    • introduces buttons (on the left?) of rules for transformations
    • changes Help
• Code:
  • implement each proof-transformation action defined in the interface
  • check 'availability' of each proof transformation to decide if buttons should be active or not
• Transformations
  • axiom expansion: 3 buttons on ax rules (active or not, depending on the shape of the formulas)
    • one-step expansion (for pairs of non atomic formulas): applies reversible rule, then non-reversible one
    • full alternating expansion: iteratively applies one-step expansion (possibly a double click on one-step expansion button rather than a dedicated one)
    • focused expansion
  • cut elimination: 3 buttons on cut rules (active or not, depending on premises)
    • due to the implicit exchange rules, the pattern to take into consideration is:

            rule             rule
          exchange         exchange
                     cut
      

    • ←: commutative left

      ax (left formula) / *, ax (right formula) / *, ⊤ (context) / *, ⊥ (context) / *, ⊗ (left context) / *, ⊗ (right context) / *, ⅋ (context) / *, & (context) / *, ⊕1 (context) / *, ⊕2 (context) / *, ! (context) / * (with ?-context), ?d (context) / *, ?w (context) / *, ?w (main) / * (with ?-context), ?c (context) / *, ?c (main) / * (with ?-context), cut (left context) / *, cut (right context) / *, def (context) / *
      

    • ↑: key case

      1 / ⊥, ⊗ / ⅋, & / ⊕1, & / ⊕2, ! / ?d, def / def
      

    • →: commutative right (cf commutative left)
    • double-click on ↑: eliminates the considered cut as well as all its residuals
    • full cut elimination: remove all cuts from the proof
  • reversing
    • click on a reversible connective (including ! in ?-context): applies the corresponding rule and do the corresponding reversing in the above proof (may require some axiom expansion steps, and modifying hypotheses as well)
    • double click on a reversible connective: applies recursively reversing on sub-formulas
  • focusing
    • local focusing: click on a positive connective attracts as many positive rules as possible to it push it up as much as possible
    • global focusing: for complete proofs, generates a cut-free focused proof by rule commutations (this is atomic weapon applying almost all the other transformations)
  • substitution
    • click on an atomic formula: opens a pop-up asking for a formula and applies substitution everywhere in the proof
  • rule commutations: 2 buttons on (non-cut, non-ax) rules (active or not) to move the considered rule up or down