• Proof by Reflection (and why not to use it)

    Timothy Mou - Wed 27 March 2024 - lean, proof-assistants

    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 …

  • Type Safety using Logical Relations

    Timothy Mou - Wed 12 July 2023 -

    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: Sprague-Grundy Theorem

    Timothy Mou - Fri 17 March 2023 - game-theory

    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 …


  • Formalizing Theory of Impartial Games: Definitions

    Timothy Mou - Wed 08 March 2023 -

    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 …


  • Transitive Closure of a Well-Founded Relation

    Timothy Mou - Tue 07 March 2023 -

    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 …


  • Upper Bounds in Minimizing Constructions

    Timothy Mou - Wed 18 January 2023 -

    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)

    Timothy Mou - Sat 07 January 2023 -

    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 1n<240 1 \leq n < 2^{40}


  • Verifying Programming Contest Problems

    Timothy Mou - Mon 05 December 2022 -

    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 …