Enhancement Proposals

Implicit Exchange

• Goal: provide export of proofs matching what the user sees on the screen
• Code:
  • extend Exchange_proof with type sequent * int list * int list * proof (let us call σ₁ the first permutation and σ₂ the second one)
  • if ⊢ Γ is the conclusion of the premise, ⊢ Γσ₁ is what is on the screen (generated by a posteriori drag and drop by user) and ⊢ Γσ₂ is the conclusion of the proof
  • when a rule is generated, σ₁ is the identity
  • when the user modifies the order in an existing sequent, σ₂ is unchanged and σ₁ is updated
  • for Coq export, only σ₂ matters, the conclusion of the proof is ⊢ Γσ₂, as well as for exports with explicit exchange rules
  • for export with implicit exchange rule, the displayed conclusion of the proof is ⊢ Γσ₁

Formula Definitions

• Goal: provide short names for compound formulas, and rely on the same mechanism to manipulate infinite formulas described through recursive equations

  𝔹 ::= (A ⊗ A) ⊸ (A ⊗ A)
  ℕ ::= !(A ⊸ A) ⊸ !(A ⊸ A)
  o ::= !o ⊸ o
  

• Interface:
  • provide a list of fields to input expressions of the shape name ::= formula
  • name can be "defined" only once
  • clicking on an atom name (or dual name^⊥) which is a defined name unfolds the definition once (or its dual)
  • possibilities for unfold rule display:
    • implicit: in place unfold as for implicit exchange
    • explicit: this unfold rule might be displayed differently from others with dashed line for example
• Code:
  • register an association table (name, formula) according to input definitions by the user
  • add unfold rule with premise ⊢ Γ, A, Δ and conclusion ⊢ Γ, X, Δ, and with premise ⊢ Γ, A^⊥, Δ and conclusion ⊢ Γ, X^⊥, Δ if (X, A) is a registered definition
  • unfold has priority over axiom: clicking on X in ⊢ X, X^⊥ unfolds X if X is defined rather than applying an axiom rule (axiom rule is reachable through clicking on the turnstile)
  • Coq export
    • non-recursive definitions using Notation: allows implicit use of definitions, entails some automatic folding
    • non-recursive definitions using Definition: explicit unfold matches use of unfold rule
    • recursive definitions: to be investigated, maybe using a co-inductive definition of formulas
• Possible Extensions:
  • automatic folding a formula A into X if a definition X ::= A is detected
    • what if two definitions X ::= A and Y ::= A?
    • if we have both ℕ ::= !(A ⊸ A) ⊸ !(A ⊸ A) and 𝕃 ::= !(A ⊸ A) ⊸ !(A ⊸ A) ⊸ !(A ⊸ A), do we want unfolding of 𝕃 to give !(A ⊸ A) ⊸ ℕ?

Cut Rule

• Discussion: issue #12
• Goal: integrate cut rule in proof construction
• Interface:
  • activate cut rule through option
  • in cut mode, sequents are displayed as ⊢ . E , F , G , H . where both , and . are clickable
  • click on active , or . opens a pop-up asking for a cut formula A
  • the cut rule is applied in the following shape with context split at clicking point

    ⊢ . Γ , A .      ⊢ . A^ , Δ .
    _____________________________
            ⊢ . Γ , Δ .
    

• Code:
  • add a constructor to proof: Cut_proof of formula list * formula * formula list * proof * proof
  • Coq export

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)