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 …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 …
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.
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
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 …