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
• 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)
• 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)
• 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) ⊸ ℕ?

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)