What is logical relations? That is a question we won't try to answer here in full generality. For our purposes, we can think of logical relations as a technique for proving properties about a language that can require stronger inductive hypotheses than those that are …

Formalizing Theory of Impartial Games: SpragueGrundy Theorem
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 SpragueGrundy theorem.
Defining Nim
I chose to define Nim in terms of the
BinNat.N
type rather than … 
Formalizing Theory of Impartial Games: Definitions
I've been working on a formalization of combinatorial game theory, focusing on solving the game of Nim and the SpragueGrundy 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 …

Transitive Closure of a WellFounded Relation
I recently encountered this issue when working with a wellfounded relation
R
. I wanted to use wellfounded induction to prove a propositionP
, but I needed to use the fact thatP
holds for not just anyy
whereR y x
, but also anyz
whereR z y …

Upper Bounds in Minimizing Constructions
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 …

Koxia and Sequence (CF 1770F)
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}$

Verifying Programming Contest Problems
In programming contests, one of the most frustrating (and common!) verdicts to receive is Wrong Answer (WA). One of the reasons behind this is that there are often many potential sources of WA that a programmer has to hunt down. A WA could come from …