Integrating graphical proofs in Coq
summary
A prototype called Actema implements gesture-driven proof construction and integrates with Coq via a coq-actema plugin using a client–server protocol: goals are rendered in the interface, drag‑and‑drop and click gestures compile to tactic sequences, and graphical proofs are stored separately and recompiled on script execution so they can be replayed visually. The compilation uses a deep embedding and about 3,000 lines of Ltac plus a proved soundness theorem; demos show targeted rewrites, existential instantiation, induction and usable proof terms, though lemma search in the GUI is not yet implemented.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 2:00Demonstration
- 4:15Forward mode
- 9:07Conflict quantifier
- 10:07Conditional rewrites
- 12:05Induction
- 13:27Summary
- 14:15Architecture
- 15:00Protocol
- 16:47Actions
- 17:52Conclusion
- 18:30Infrastructure challenges
- 20:10Questions
related talks
24mActema: Integrating Graphical Proofs into ITPs via Plugin-Driven Gestural Interaction
22mA diagram editor to mechanize categorical proofs
13mA Drag-and-Drop Proof Tactic
21mLive Verification in an Interactive Proof Assistant
22mInducTeX: A MetaCoq plugin for typesetting inductive definitions
01h 10mMedium-scale automation for proof assistants
21mIntegrating Dependency Building with Document Checking in Coq
24mTowards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by(…)