An Equations Tutorial
summary
Equations lets you write Coq functions by equations with rich pattern matching and recursion that elaborate to pure Gallina and generate a rewrite database of all clauses for automation. Each definition also produces an inductive graph (a recursion/evaluation principle) and a synthetic elimination principle for proofs. It supports notations, nested matching via with-abstraction, accumulator-style defs, indexed types like vectors, built-in no-confusion reasoning, tactic support, and a transparency switch for reduction vs. logical simplification.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 0:50Writing Equations
- 1:40Reasoning Principles
- 2:57Evolution Principle
- 5:00Recursive Functions
- 21:40Summary
- 25:10Simplifying
related talks
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
01h 34mFormal Logic Undressed
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
11mLocal algebraic effect theories
29mMechanized monadic equational reasoning for ML references
20mPractical and sound equality tests, automatically
22mAutomated Proof Generation for Associative and Distributive Rewriting with E-Graphs
16mUntangling Mechanized Proofs