Let's say you frequently need to solve equalities on monoids, and you find yourself proving lots of goals like the following:

example [Monoid α]: ∀ (a b c d : α), 
  a * b * c * d * 1 = a * (b * c) * (1 * 1 * d) := by
  intros a b c d
  rw [mul_one]
  rw [mul_one …

This is a continuation of this previous post covering a formalization of impartial games. In this post, I will define the game of Nim, and use it to state and prove the Sprague-Grundy theorem.

Defining Nim

I chose to define Nim in terms of the BinNat.N type rather than …

I've been working on a formalization of combinatorial game theory, focusing on solving the game of Nim and the Sprague-Grundy theorem. Initially, I wanted to make this post a literate Coq document, but as I started writing, I realized there was not much to gain from cluttering the posts with …

I recently encountered this issue when working with a well-founded relation R. I wanted to use well-founded induction to prove a proposition P, but I needed to use the fact that P holds for not just any y where R y x, but also any z where R z y …

I will describe a type of constructive problem that comes up fairly regularly on programming contests, especially Codeforces. We are given what I will call a "minimizing construction" problem, one where we are asked to construct a least such object that satisfies certain properties. One common prototype is that we …

I encountered this Codeforces problem with some really interesting and remarkable ideas, so I decided to write a short note about it. This solution is partly based off an explanation by CF user aryanc403.

We are given integers $1 \leq n < 2^{40}$