The lecture notes accompanying the Induction chapter of Logical Foundations are now available.
View or download the source: InductionLecture.v
These notes cover proof by induction in Rocq — why simpl and destruct are not enough, the induction tactic, the replace tactic, and the contrast between formal and informal proofs. The notes conclude with a case study on binary numbers: defining incr and bin_to_nat, proving the nat→bin→nat round-trip, and normalizing binary representations to prove the bin→nat→bin direction. Load the file in VSCode with coq-lsp (or vsrocq) and step through it interactively.