Using Lean to Prove 1080 Sets

All of my friends know that I play Set at a level so beyond obsessive it almost integer overflows to mundane -- the simplicity and symmetry of the game makes for an easy way to reset the marbles in my brain, and it's a quick way to idly pass by a minute or two between subway stops. Because of the elegant (one could even say algebraic) nature of the game, it's also fun to use for combinatorics questions. Since I've been trying to get more used to Lean anyway, I decided to try proving some Set combinatorics in Lean.

Let's first look at how many distinct sets there should be from the deck of 81 cards. The Fundamental Theorem of Set says that given two cards, we can uniquely determine the third card in the set (try it!). So there are $\binom{81}{2} \cdot \frac{1}{3} = 1080$ unique sets we can create (remember we divide by 3 to correctly account for the 3 different ways to choose the first 2 cards from the 3 cards in a set).

I won't go into the rules of Set or how I chose the specific representation of cards (plenty has been written about this), but since Set cards have 4 attributes with 3 choices each, one elegant way to represent a card is as a 4-dimensional vector space over the set of integers mod 3, or $\mathbb{Z}_3^4$.

def Card := Fin 3 × Fin 3 × Fin 3 × Fin 3

Then the really elegant thing is that we can test three cards form a set by seeing what the elementwise sum of the 3 vectors is. We get a set if and only if the resulting sum is the 0 vector, because three cards are a set if and only if for each of the attributes, the cards are either all the same or all different. This elegant set condition is pretty unique to the number of options per attribute and number of cards defined as making up a set (try it!).

Remember that by our definition, Lean reads Card as looking like something like this: Fin 3 × (Fin 3 × (Fin 3 × Fin 3)), so we have to do some funny indexing to do elementwise addition. We also denote this as just a statement of truth by using Prop:

def isSet (c1 c2 c3 : Card) : Prop :=
  c1.1 + c2.1 + c3.1 = 0 ∧
  c1.2.1 + c2.2.1 + c3.2.1 = 0 ∧
  c1.2.2.1 + c2.2.2.1 + c3.2.2.1 = 0 ∧
  c1.2.2.2 + c2.2.2.2 + c3.2.2.2 = 0

Then we need to do some setup before we can tell Lean to prove there's 1080 sets in a deck. First, let's tell it what to do with a group of 3 cards. We use Decidable to tell Lean that it will use our isSet Prop to make an executable boolean program that takes as input an instance of 3 cards. Lean automatically does this via infer_instance, but we need to tell it to unfold isSet because our Card is defined via raw nested products.

instance (c1 c2 c3 : Card) : Decidable (isSet c1 c2 c3) :=
  by unfold isSet; infer_instance

Actually, we also need to tell Lean how to decidably check for equality and how to perform addition, so we have to explicitly add in our previous definition that Card derives from Fintype and DecidableEq.

def Card := Fin 3 × Fin 3 × Fin 3 × Fin 3
  deriving Fintype, DecidableEq

From here, the basic sketch of this method is that we will tell Lean how to construct all sets from the deck, and since the Set deck is relatively small and there aren't too many sets, Lean can bash out how many sets there are and check that it's equal to what we know combinatorially.

To make our lives easier, let's define an ordering of set cards so that we can cleanly keep track of which sets we've seen before. To accomplish this, for readability (and perhaps teachability, because this is certainly not the easiest way) we can "overload" the < operator to do some lexicographical ordering for us:

def cardLessThanBool (c1 c2 : Card) : Bool :=
  (c1.1 < c2.1) ||
  (c1.1 == c2.1 && c1.2.1 < c2.2.1) ||
  (c1.1 == c2.1 && c1.2.1 == c2.2.1 && c1.2.2.1 < c2.2.2.1) ||
  (c1.1 == c2.1 && c1.2.1 == c2.2.1 && c1.2.2.1 == c2.2.2.1 && c1.2.2.2 < c2.2.2.2)

instance : LT Card where
  lt c1 c2 := cardLessThanBool c1 c2 = true

I say overload in quotes because it feels like overloading a method, but actually Lean implements this using a typeclass system. LT is a global typeclass defined in Lean's core library: "Any type implementing LT must provide a function called lt that takes two items and determines a proposition." So we have to make sure to return a Prop, not a Bool, which is why we return cardLessThanBool c1 c2 = true.

Similar to before, we also have to make sure Lean knows how to compute whether a card is less than another card. Again, Decidable tells Lean that we are providing an explicit algorithm to check our claim and provide a true/false. change here tells Lean that because we've overloaded < previously, we can rewrite the target goal using cardLessThanBool to explicitly show the boolean equality equation. Then infer_instance searches Lean's typeclass database, finds the core library built-in rule that says "Checking if a known boolean function outputs true is always decidable (you just run it)", and uses that to automatically construct the runtime validation block.

instance (c1 c2 : Card) : Decidable (c1 < c2) :=
  by change Decidable (cardLessThanBool c1 c2 = true); infer_instance

Here I had to stop and think about why Lean was seemingly so smart in some areas (it knows how to infer if boolean functions are decidable!) but not in other areas (we have to use by change as a macro hint to... tell Lean that the overloaded lt boolean function... is... decidable??). It turns out that when Lean sees something like (c1 < c2), it looks for an algorithm to compute Decidable (c1 < c2) by looking for Decidable (LT.lt c1 c2). It doesn't automatically open up the definition of LT.lt to realize that the custom logic is just a simple Bool function. So we have to tell Lean to look under the abstract wrapper using the by change tactic.

That all said, we're now pretty close to being able to finish our bashy count proof. We'll use two nested loops to represent our first two cards, then use our lt operator to cleanly search for the third card using our previously-defined isSet. We use biUnion as a flat map for the first two cards, and filter for the third card's conditions. WLOG, we only have to look for a c3 if c1 < c2, and we only count the set if c2 < c3, otherwise we just use the null set ∅. This helps with recursion depth issues. map packages up the three cards so we take c1, c2, c3 as a set.

def allSetsProduct : Finset (Card × Card × Card) :=
  (Finset.univ : Finset Card).biUnion fun c1 =>
    (Finset.univ : Finset Card).biUnion fun c2 =>
      if c1 < c2 then
        ((Finset.univ : Finset Card).filter fun c3 => c2 < c3 ∧ isSet c1 c2 c3).map
          ⟨fun c3 => (c1, c2, c3), fun _ _ h => by injection h; rename_i h2; injection h2⟩
      else ∅

What's that second to last line? Well, a Finset contains unique items by definition. So before using map, we have to prove that we aren't counting duplicate entries. We use by injection h to prove that if two c3 cards are identical, their output triples must be identical too. Similar to the change tactic above, that injection tactic peels back the nested layers to satisfy the safety checker.

Then we can check that Lean does indeed find 1080 sets by the following:

theorem card_sets_product : (allSetsProduct).card = 1080 := by decide

Actually, we also need to add something like this:

set_option maxRecDepth 1000000
set_option maxHeartbeats 1000000

maxRecDepth sets the max recursion depth, and maxHeartbeats sets an allowed amount of computation effort. A heartbeat roughly corresponds to 1,000 small memory allocations.

Whew! We did it! Okay, admittedly that was pretty bashy. We basically told Lean how to check set conditions for a given trio, and made it look at all the (ordered) trios to match that number to what we calculated combinatorially before. Along the way, we had to do some "casting" and some "overloading". We could optimize on this approach by modeling cards as Fin 4 → Fin 3 and using Pi.Lex for ordering. This also makes addition in our isSet definition more elegant. But I think there's still a more combinatorial (not sure if this is more elegant code-wise though) way to prove this, which I'll explore in a follow-up post.