A Formalisation of Addition Chains
Laurent Théry · HAL (Le Centre pour la Communication Scientifique Directe) · 2025
This note explains how some basic facts about addition chains have been formalised and proved correct in the Coq proof assistant using the SSReflect extension. Addition Chain An addition chain is a sequence of additions that, starting from 1, allows to reach a given number n. We are particularly interested here in a specific type of chains : the Euclidean addition chains. They are controlled by a pair (m, n) of natural numbers and there are only two possible steps: In our formalisation, this is represented by the next function 1 . Definition next (b : bool ) (p : bool * bool ) := let (m, n) := p in if b then (m, m + n) else (n, m + n).