{"id":"e2f6ae2e-0c07-4525-9db1-9e5f7b7209fa","arxiv_id":"2505.13473","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"This paper presents an interactive Coq plugin, CommutativeDiagrams, that visualizes categorical proofs as commutative diagrams and lets users progress proofs through graph matching and pushout-based lemma application.","lead":"A Coq plugin now turns category theory proof states into interactive commutative diagrams, letting users advance proofs by dragging and matching graph elements. The tool targets students and proof engineers who want diagrammatic reasoning inside a general-purpose proof assistant.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The pushout-based lemma application in §4.3 lacks any soundness argument; if the graph operations do not exactly mirror Coq's refine, the plugin could silently accept an invalid proof.","rationale":"The reader's weakest assumption is exactly the point I find most load-bearing: soundness of the pushout-based lemma application. After reading the full text, including the operations in §3 and the lemma application in §4.3, I find no independent support for this soundness beyond the demo. The paper is honest about being a prototype and states limitations (scope to UniMath, no web version yet, cannot apply under a term), but those limitations do not address the core trust question: when the plugin advances the proof, does the new proof state exactly correspond to a valid Coq refinement? The absence of a formal account or at least a test suite is a real gap for a tool whose purpose is to 'progress the proof.' I considered other potential concerns—such as the replayability of the script language (§2.2) and the narrow library support—but these are less critical: replay failures would be visible and would not silently produce wrong proofs, and the UniMath restriction is stated up front. The pushout concern is dangerous precisely because it could fail silently. I therefore agree with the reader's CONDITIONAL verdict and do not propose any change. The proposed concrete test—comparing generated goals against `apply` on a battery of examples and typechecking the final proof term—would settle whether the concern is actual.","tokens_in":8890,"tokens_out":7194,"duration_ms":69615,"concrete_test":"Run the plugin on the Figure 1 example: apply `Hf` through the interface and compare the generated Coq goal with the goal produced by Coq's `apply Hf` (or `refine`) in the same normalized context. Repeat on a battery of at least 10 lemmas covering universal and existential quantifiers, partial matches, and forward and backward reasoning. If any generated obligation differs from the corresponding `apply` result, the pushout refinement is unsound. As a stronger test, complete one `diagram run` proof that concludes the goal, and independently typecheck the generated proof term using `Qed` in a fresh Coq run; if it fails the kernel, the operations are not trustable.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The most load-bearing step is the lemma-application operation described in §4.3. The paper states that after the user provides a partial match between the lemma graph and the goal graph, 'the pushout of the matching is computed and the result is the new proof state' (§4.3), and that at the end, 'the Coq state will be advanced such that any remaining proof obligation in the interface becomes a new Coq goal' (§2.1). For the central claim to hold, this pushout must produce exactly the proof obligation that Coq's `apply` or `refine` would produce from the same lemma and instantiation. The paper gives no formal statement of the correspondence between graph objects (nodes, edges, faces) and Coq terms, and no proof that the pushout preserves the logical content of the goal. Since the plugin's own restrictions (e.g., cannot apply a lemma under a term, §4.4) show that the graph representation is not a complete account of the Coq context, it is not self-evident that the pushout is sound beyond the cases shown. No machine-checked verification, test suite, or independent derivation of the pushout operation is provided. If the unification or merging of graph objects diverges from Coq's unification in some corner case (for example, when a lemma has existential quantifiers or when matching is partial), the plugin could accept a proof obligation that does not follow from the original goal, making the tool unsound in a silent way.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents a Coq plugin that renders a proof goal as a commutative diagram when the goal is an equality between morphisms in a category, using the UniMath library. The user can manipulate the diagram through operations such as splitting, merging, decomposing, composing, and normalizing edges, and can apply lemmas by matching a graph pattern extracted from the lemma statement, unifying terms via Coq, and then computing a pushout of the two graphs. The paper also describes a replayable textual script language for proof interactions and a split architecture in which a Rust interface communicates with a Coq plugin through a custom protocol, with a web version reported as in progress. The central claim is that interactive diagrammatic proof is feasible inside a generic proof assistant, with the graph operations producing valid Coq refinements.","tokens_in":9107,"tokens_out":6090,"duration_ms":60958,"significance":"If the implementation is correct, the tool is a useful educational artifact and a concrete step toward context-specific proof assistants layered over generic ones. The paper gives a worked example, explains the graph model and the main operations, and honestly discusses several limitations, including the restriction to a first-order fragment and the inability to apply lemmas under a term. The strengths are the concrete demonstration, the public repository, and the replayable script language. However, the paper does not supply a soundness theorem, a test suite, or a user study, so the significance is currently that of a feasibility demonstration rather than a verified or empirically evaluated system.","major_comments":[{"comment":"The central correctness claim of the paper is that the pushout-based lemma application produces a valid new proof state, but no soundness argument is given. The text states that 'the pushout of the matching is computed and the result is the new proof state,' yet it does not state a correspondence theorem between graph nodes, edges, and faces and Coq terms, nor does it prove that the pushout is logically equivalent to Coq's apply or refine. Since Section 4.4 explicitly restricts the supported fragment and admits that lemmas cannot be applied under a term, the graph representation is not a complete account of the Coq context, so soundness is not self-evident. A silent divergence from Coq's unification or refinement semantics in a corner case (for example, with existential quantifiers or partial matches) would make the tool unsound in a way that defeats its purpose. Please provide a precise statement of the correspondence, or at least a substantial automated test suite covering partial matches, existential lemmas, and nested terms; without this, the main claim that the user can progress proofs safely remains unverified.","section":"§4.3"},{"comment":"The proof-progressing operations described in Section 3, especially 'Merging' and 'Solving,' are specified only informally. For example, the solver 'attempts to construct an equality proof from the other equalities present, using the structure of the graph,' but the paper does not say what Coq term or tactic is generated when the solver succeeds. The same applies to 'Decomposition,' which 'refines the equality to reduce it to proof obligations for all the atomic planar regions.' Because these operations change the Coq proof state, the reader cannot judge whether they are guaranteed to produce well-typed refinements. Please specify the underlying proof-term construction or tactic for each operation that modifies the Coq state, or state which of them are intended only as heuristics whose outputs are checked by Coq before being accepted.","section":"§3"},{"comment":"The scope of the tool is narrower than the title and abstract suggest. The architecture description in Section 5.1, step ➋, says the plugin constructs the graph 'if it is an equality between morphisms,' and the concrete example in Section 2.1 is an equality goal. The abstract, however, announces 'a graphical interface for category theory proofs' without this qualification. This discrepancy should be corrected, either by narrowing the stated contribution to equality goals in the first-order fragment or by clearly stating the supported class of goals in the abstract and introduction; otherwise the central claim is broader than what is demonstrated.","section":"§5.1"}],"minor_comments":[{"comment":"There is a typo in the last paragraph of the introduction: 'We well begin' should be 'We will begin.'","section":"§1"},{"comment":"The scripting language example in Figure 4 contains the command 'succeed,' but the paper never explains its meaning or when it is generated. A brief description of each command in the script language would help readers understand the replay mechanism.","section":"§2.2"},{"comment":"The treatment of existential quantifiers in lemmas would benefit from a precise Coq term. The paper says 'an existential quantifier is a dependent pair' and that references can be substituted by 'the first projection of the lemma,' but the standard Coq ex type lives in Prop and does not have a first projection in the same sense as sigT. Please specify the exact Coq representation used (for example, sigT or a UniMath-specific dependent sum) so that this step can be checked.","section":"§4.2"},{"comment":"The web version is described as motivating a substantial asynchronous rewrite, but the paper states that it cannot yet provide a link and that the asynchronous version is still in progress. Marking this section more explicitly as future work would make the status of the web version clearer.","section":"§5.2"},{"comment":"The appendix lists the original screenshots but does not explicitly state which screenshots correspond to Figures 2 and 3. Adding a short mapping would make the appendix more useful to readers who want to compare the synthetic figures with the actual interface.","section":"Appendix A"}],"recommendation":"major_revision","confidential_remarks":null},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague,\n\nThis is a straightforward and honest tool paper. The new thing is that it lets you apply a categorical lemma to a goal by matching a diagram pattern and taking a pushout, then replay the interaction as a small text script. That combination, pushout-based lemma application plus a readable replay language, is not in Actema, the Lean widgets, or Lafont's editor. The demo in Section 2 is easy to follow, and the repository is public, so the existence claim is checkable.\n\nWhat I like: the paper separates graph manipulation from the Coq side, has a simple scripting language that is human-readable, and is candid about limitations (no web version yet, cannot apply under a term, hard-coded structures). The comparison with prior work is fair and not inflated.\n\nThe soft spot is the one the stress-test flags. Section 4.3 says the pushout of the matching is computed and becomes the new proof state, but nowhere does the paper give a formal correspondence between the graph and Coq terms, nor a proof that the pushout operation always produces exactly the obligation Coq's refine would produce. Since Coq's kernel will check the final proof term, a bug in the plugin could only make the user's life harder, not make an invalid proof accepted—unless the plugin itself constructs a wrong proof term from the graph. That risk is not addressed, and the paper does not provide tests or a safety argument. I would call it a moderate concern, not a fatal one: this is a workshop paper describing a working prototype, and the restriction to first-order categorical statements limits the blast radius.\n\nAlso, the educational motivation is plausible but unevaluated; there is no user study. That is a minor issue for a tool paper, not a reason to reject.\n\nBottom line: if the plugin works as described, it is a useful teaching aid and a good demonstration that graphical interaction can be layered on Coq. The paper deserves a serious referee; I would send it to review with a request for either a soundness sketch or a set of tests for the pushout operation, plus a pinned commit for reproducibility.","headline":"A coherent tool paper: the pushout-based lemma matching is genuinely new, but the soundness question is real and the paper would be stronger with one explicit statement of how Coq's kernel bounds the damage.","tokens_in":9668,"tokens_out":2881,"would_cite":false,"duration_ms":29058,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"A Coq plugin turns category-theory proof goals into interactive commutative diagrams and lets users advance proofs by manipulating those diagrams.","keywords":["category theory","proof assistant","commutative diagrams","Coq plugin","graphical proof","pushout","lemma application","diagrammatic reasoning"],"falsifier":"Record the full Coq proof term the plugin produces for a nontrivial category-theory proof and check it with Coq's kernel; a single accepted proof whose generated term fails type-checking, or a lemma application that creates a goal not derivable from the matched hypotheses, would refute the claim.","tokens_in":8625,"feed_emoji":"📐","tokens_out":3861,"duration_ms":40816,"temperature":0.7,"pith_summary":"The paper is trying to establish that categorical proofs can be read, edited, and advanced through a graphical interface living inside a general-purpose proof assistant, rather than in a separate diagram tool with its own logic. The plugin builds a commutative diagram directly from a Coq proof state, normalizes it, and exposes operations such as splitting, merging, decomposing, and lemma application that change both the diagram and the proof. Lemma application works by representing the lemma as a graph pattern, letting the user match its nodes and edges to the goal diagram, and gluing the two graphs along that match; the glued diagram becomes the new proof state. If this works as described, students could practice diagrammatic reasoning on concrete proofs, and the same proof scripts could be replayed or ported across proof assistants.","feed_headline":"Category-theory proofs become clickable diagrams inside Coq","feed_subtitle":"A plugin builds the diagram from the goal, then glues lemmas onto it so a proof can be finished by dragging and matching.","key_machinery":"The central object is the graph extracted from a Coq proof state, together with the pattern graph extracted from a first-order lemma about categories. The operation that carries lemma application is the pushout of a partial matching: the interface unifies the Coq terms on matched objects as the user selects them, then takes the union of the lemma graph and the goal graph and merges the matched objects, producing the new proof state by gluing the two diagrams together.","core_discovery":"The paper claims that a Coq plugin can read a proof goal whose conclusion is an equality between morphisms, extract a graph whose nodes are objects, whose edges are morphisms, and whose faces are equalities, and then let the user manipulate that graph, splitting and merging edges, decomposing faces, and applying lemmas, where each manipulation refines the underlying Coq proof state. In particular, applying a lemma is done by matching its extracted graph pattern against the goal graph and computing the pushout of the two graphs modulo the matching; the result becomes the new goal graph, and any remaining proof obligations are returned to Coq as new goals.","pith_inferences":["If the pushout operation is sound, the same mechanism could generalize from categories to any theory whose proof states admit a graph-like structure, turning lemma application into a generic diagrammatic rewriting step.","The plugin's soundness is ultimately a claim about the correspondence between graph unification and Coq's dependent type checker; a testable extension is to instrument every plugin step to emit the generated Coq refinement and verify it with the kernel.","For teaching, the web version suggests a further step: an exercise author could choose which lemmas are visible, turning the diagram editor into a puzzle environment where students build proofs by matching shapes."],"forward_implications":["A user can complete a categorical proof, including instantiating existential variables, without leaving the diagram, because merging matched objects unifies the underlying Coq terms.","The textual script language makes every graphical interaction replayable: the same file re-runs the proof without reopening the interface when it succeeds.","The uniform lemma-application mechanism covers backward reasoning, forward reasoning, exact application, and cut, all through the same pushout operation.","Because the plugin talks to the interface through a small protocol, the same interface could be reused by other proof assistants with a modest porting effort."],"supporting_citations":[{"why":"Provides the prior example of a proof-assistant widget that visualizes the proof state as a commutative diagram but is limited to visualization, marking the gap this paper fills.","marker":"[1]"},{"why":"Supplies an existing drag-and-drop proof tactic whose storage and interface decisions are compared against the present script-based approach.","marker":"[5]"},{"why":"Describes a parallel diagram editor integrated with Coq; this paper compares engineering decisions and expects the two tools to converge.","marker":"[6]"},{"why":"Establishes diagrammatic methods, specifically string diagrams, as an established way to manage abstraction in category theory.","marker":"[2]"},{"why":"Supplies the motivation that category theory bridges previously unconnected mathematical developments, motivating diagrammatic proof support.","marker":"[4]"}],"fun_headline_variants":["Drag category theory proofs into shape inside Coq","Coq plugin: prove by clicking and dragging diagrams","Graphical category theory: drag lemmas to finish Coq goals","Turn Coq proof goals into editable category theory graphs","Interactive graph manipulation for Coq category theory proofs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that gluing the lemma's diagram to the goal's diagram, after unifying the matched terms, yields exactly the proof obligations of a correct Coq refinement.","fun_headline_variants_meta":{"raw":{"variants":["Drag category theory proofs into shape inside Coq","Coq plugin: prove by clicking and dragging diagrams","Graphical category theory: drag lemmas to finish Coq goals","Turn Coq proof goals into editable category theory graphs","Interactive graph manipulation for Coq category theory proofs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000223,"raw_usage":{"total_tokens":1366,"prompt_tokens":763,"completion_tokens":603,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":379,"completion_tokens_details":{"reasoning_tokens":526}},"tokens_in":379,"tokens_out":603,"duration_ms":5867,"temperature":1.0,"reasoning_tokens":526,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T22:50:30.247535+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Record the full Coq proof term the plugin produces for a nontrivial category-theory proof and check it with Coq's kernel; a single accepted proof whose generated term fails type-checking, or a lemma application that creates a goal not derivable from the matched hypotheses, would refute the claim.","supporting_citations":[{"cited_title":"doi:10.17863/CAM.81869","cited_arxiv_id":null,"evidence_quote":"Provides the prior example of a proof-assistant widget that visualizes the proof state as a commutative diagram but is limited to visualization, marking the gap this paper fills."},{"cited_title":"In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs , ACM, Philadelphia PA USA, pp","cited_arxiv_id":null,"evidence_quote":"Supplies an existing drag-and-drop proof tactic whose storage and interface decisions are compared against the present script-based approach."},{"cited_title":"Available at https://hal","cited_arxiv_id":null,"evidence_quote":"Describes a parallel diagram editor integrated with Coq; this paper compares engineering decisions and expects the two tools to converge."},{"cited_title":"The unification of Mathematics via Topos Theory","cited_arxiv_id":"1006.3930","evidence_quote":"Supplies the motivation that category theory bridges previously unconnected mathematical developments, motivating diagrammatic proof support."}],"review_version":1}