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 ⊢ Γσ₁

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)