CycleQ: an efficient basis for cyclic equational reasoning
summary
CycleQ presents a cyclic proof system that folds equational reasoning into cycle formation via a synthesized subst rule, implemented as a Haskell GHC plugin that rewrites goals using existing graph nodes as lemmas. It proves examples with mutually inductive datatypes without upfront induction schemas, checks global validity with sized‑change graphs, subsumes rewriting‑induction techniques, and solves over half the benchmarks in under 0.1s while notably lacking automated lemma discovery and conditional‑equation support.
AI-written summary · about
chapters (6)
- 0:00Start
- 2:03Cyclic Proofs
- 2:29Proof of the Commutativity of Addition
- 2:48Case Analysis
- 5:47Matching Function
- 8:47Example of the the Proof of Commutativity of Addition
related talks
27mAn Equations Tutorial
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
29mMechanized monadic equational reasoning for ML references
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
21mChecking Equivalence in a Non-strict Language
15mAssertion-Based Optimization of Quantum Programs
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
22mAutomated Proof Generation for Associative and Distributive Rewriting with E-Graphs