Enhancement Proposals

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)
  • define an unfolding function on sequents to call provability checks and automated prover
    • no unfolding of definitions
    • eliminate cycles in definitions (by erasure) and unfold the obtained restricted definition set
  • generalize context of promotion rules to formulas defined as a ? formula (this may require to do a finite unfolding of a possibly cyclic set of definitions)
  • 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) ⊸ ℕ?

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
    • 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 to be transformed
• 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
    • focused expansion
  • cut elimination: 3 buttons on cut rules (active or not, depending on premises)
    • ←: commutative left (including ax/*, ⊤/*, as well as ?c/*, ?w/* and ?p/* if * has ?-context)
    • ↑: key case (only !/?d for exponentials, none for ⊤)
    • →: commutative right (cf commutative left)
  • 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)
  • focusing