Concept
Proof by simplification
Books
Journey Statuslearning
Tools: Rocq (formerly Coq)
INFO
(Proof/Reason technique, Logic) A proof technique that reduces expressions to simpler forms using definitional equalities, computation rules, or algebraic identities.
INFO
(Formal system, Proof/Reason technique, Language feature/design, Programming paradigm) [Rocq] A Proof technique in Rocq (via simpl or reflexivity) that reduces expressions using Computation rules (unfolding, beta reduction, pattern matching).