TPPmark 2023

Author: Makoto Kanazawa, Faculty of Science and Engineering, Hosei University

Last updated: November 5, 2023

This is an Agda formalization of TPPmark 2023.

Tested with Agda 2.6.4 and the Agda standard library version 1.7.3.

module TPPmark where

open import Algebra.Definitions using (Associative; Commutative; Involutive)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Fin as F using (Fin; toℕ; fromℕ; fromℕ<)
open import Data.Fin.Properties using (toℕ-fromℕ<; fromℕ<-cong; all?; ¬∀⟶∃¬)
open import Data.Fin.Patterns
open import Data.Integer using (ℤ; +_; -[1+_]; 0ℤ; 1ℤ; -1ℤ; -_; _+_; _*_; ∣_∣)
open import Data.Integer.DivMod using (n%ℕd<d; a≡a%ℕn+[a/ℕn]*n)
  renaming (_divℕ_ to _/ℕ_; _modℕ_ to _%ℕ_)
open import Data.Integer.Properties using (+-assoc; +-identityˡ)
open import Data.List using (List; []; _∷_; _++_; map; foldr; applyUpTo)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Membership.Propositional.Properties 
  using (∈-++⁺ˡ; ∈-++⁺ʳ)
open import Data.List.Properties using (∷-injectiveˡ)
  renaming (≡-dec to List-≡-dec)
open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
open import Data.List.Relation.Binary.Subset.Propositional.Properties
  using (⊆-refl; ⊆-trans; xs⊆x∷xs; ∷⁺ʳ; ∈-∷⁺ʳ)
open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
import Data.List.Relation.Unary.All.Properties as Allₚ
open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
import Data.List.Relation.Unary.Any.Properties as Anyₚ
open import Data.Nat as ℕ using (ℕ; zero; suc; pred; _⊔_)
open import Data.Nat.DivMod using (_%_; _mod_)
open import Data.Nat.Properties
  using (suc[pred[n]]≡n; m≤m⊔n; m≤n⊔m; ⊔-idem; ≤-reflexive; ≤-trans; 1+n≰n)
-- This comment about m≤n⊔m in Data.Nat.Properties is wrong.
-- : ∀ m n → m ≤ n ⊔ m
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; ∃; ∃₂)
open import Data.Product.Properties using () renaming (≡-dec to ×-≡-dec)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Unit using (tt)
open import Function using (_∘_)
open import Relation.Binary as B using (DecidableEquality)
open import Relation.Binary.PropositionalEquality as Eq 
  using (_≡_; refl; _≢_; trans; sym; cong; cong₂; subst; _≗_)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Nullary.Decidable 
  using (True; False; toWitness; toWitnessFalse)
open import Relation.Nullary.Negation using (¬?)
open import Relation.Unary using (Decidable) renaming (_⊆_ to _⇒_)

open import Miscellaneous

Positional games

Let us define positional games (with infinitely many positions).

module PositionalGame 
  (Position : Set) 
  (_≟_ : DecidableEquality Position)
  (newPos : (xs : List Position) → Σ Position λ y → ¬ y ∈ xs)
  (WinningSet : List Position → Set)
  (¬ws[] : ¬ WinningSet [])
  where

  open import Data.List.Membership.DecPropositional _≟_ using (_∈?_) 

A state of the game is represented by a pair of lists of positions. The first list is the sequence of moves made by the player who is going to make the next move (the first player). The second list is the sequence of moves made by the other player (the second player). The game is won by the player who made the last move when the list of moves made by that player includes some winning set.

  IncludesWinningSet : List Position → Set
  IncludesWinningSet xs = Σ (List Position) λ ws → WinningSet ws × ws ⊆ xs

The first player can force a win if the second player has not already won and the first player can make a move that results in a state where the second (formerly first) player can force a win. The second player can force a win if the second player has already won or else no matter how the first player moves, it results in a state where the first (formerly second) player can force a win.

I choose not to use representations of players in the formalization. Information about the turn (which player is going to make the next move) is buried inside the predicates FirstCanForceWin and SecondCanForceWin. This makes everything much simpler. I give predicates and functions on states in curried form, so I never explicitly deal with objects of type List Position × List Position.

  FirstCanForceWin : List Position → List Position → Set
  data SecondCanForceWin : List Position → List Position → Set

  FirstCanForceWin xs ys = 
    ¬ IncludesWinningSet ys × 
    Σ Position λ x → ¬ x ∈ xs × ¬ x ∈ ys × SecondCanForceWin ys (x ∷ xs)

  data SecondCanForceWin where
    now   : ∀ {xs} ys → IncludesWinningSet ys → SecondCanForceWin xs ys
    later : {xs ys : List Position} → 
            ({x : Position} → ¬ x ∈ xs → ¬ x ∈ ys → 
              FirstCanForceWin ys (x ∷ xs)) → 
            SecondCanForceWin xs ys

Only one player can force a win from any given state.

  onlyOnePlayerCanForceWin : 
    (xs ys : List Position) → FirstCanForceWin xs ys → SecondCanForceWin xs ys →
    ⊥
  onlyOnePlayerCanForceWin xs ys (¬iws[ys] , h₁) (now .ys iws[ys])       = 
    ¬iws[ys] iws[ys]
  onlyOnePlayerCanForceWin xs ys (_ , x , ¬x∈xs , ¬x∈ys , h₁) (later h₂) = 
    onlyOnePlayerCanForceWin ys (x ∷ xs) (h₂ {x = x} ¬x∈xs ¬x∈ys) h₁

The first player can force a draw

We are going to prove that the second player has no winning strategy in any positional game.

Consider two states of the game. If the first component of the first state is included in the first component of the second state, and in addition the second components of the two states are the same, then whenever the first state is a winning state for the first player, so is the second state. Likewise, if the second component of the first state is included in the second component of the second state, and the first components of the two states are identical, then whenever the first state is a winning state for the second player, so is the second state. In other words, having secured additional positions is never a disadvantage for either player.

  monotonicityLemma₁ : (xs xs′ ys : List Position) →
    FirstCanForceWin xs ys → xs ⊆ xs′ → FirstCanForceWin xs′ ys

  monotonicityLemma₂ : (xs ys ys′ : List Position) →
    SecondCanForceWin xs ys → ys ⊆ ys′ → SecondCanForceWin xs ys′

  monotonicityLemma₁ xs xs′ ys (¬iws[ys] , x , ¬x∈xs , ¬x∈ys , h) xs⊆xs′ 
    with x ∈? xs′
  ... | no ¬x∈xs′ = ¬iws[ys] , x , ¬x∈xs′ , ¬x∈ys , 
                    monotonicityLemma₂ ys (x ∷ xs) (x ∷ xs′) h (∷⁺ʳ x xs⊆xs′)
  ... | yes x∈xs′ = ¬iws[ys] , y , ¬y∈xs′ , ¬y∈ys , 
                    monotonicityLemma₂ ys (x ∷ xs) (y ∷ xs′) h x∷xs⊆y∷xs′
    where
    y = proj₁ (newPos (xs′ ++ ys))
    ¬y∈xs′++ys : ¬ y ∈ xs′ ++ ys
    ¬y∈xs′++ys = proj₂ (newPos (xs′ ++ ys))
    ¬y∈xs′ : ¬ y ∈ xs′
    ¬y∈xs′ y∈xs′ = ¬y∈xs′++ys (∈-++⁺ˡ y∈xs′)
    ¬y∈ys : ¬ y ∈ ys
    ¬y∈ys y∈ys = ¬y∈xs′++ys (∈-++⁺ʳ xs′ y∈ys)
    x∷xs⊆xs′ : x ∷ xs ⊆ xs′
    x∷xs⊆xs′ = ∈-∷⁺ʳ x∈xs′ xs⊆xs′
    x∷xs⊆y∷xs′ : x ∷ xs ⊆ y ∷ xs′
    x∷xs⊆y∷xs′ = ⊆-trans x∷xs⊆xs′ (xs⊆x∷xs xs′ y)

  monotonicityLemma₂ xs ys ys′ (now .ys iws[ys]) ys⊆ys′ = 
    now ys′ (zs , ws[zs] , ⊆-trans zs⊆ys ys⊆ys′)
    where
    zs : List Position
    zs = proj₁ iws[ys]
    ws[zs] : WinningSet zs
    ws[zs] = proj₁ (proj₂ iws[ys])
    zs⊆ys : zs ⊆ ys
    zs⊆ys = proj₂ (proj₂ iws[ys])    
  monotonicityLemma₂ xs ys ys′ (later h) ys⊆ys′         = later h′
    where
    h′ : {x : Position} → ¬ x ∈ xs → ¬ x ∈ ys′ → FirstCanForceWin ys′ (x ∷ xs)
    h′ {x} ¬x∈xs ¬x∈ys′ = 
      monotonicityLemma₁ ys ys′ (x ∷ xs) (h ¬x∈xs ¬x∈ys) ys⊆ys′
      where
      ¬x∈ys : ¬ x ∈ ys
      ¬x∈ys x∈ys = ¬x∈ys′ (ys⊆ys′ x∈ys)

If the second player can force a win starting from a state xs, ys, then the first player can force a win starting from a state ys, xs by mimicking the second player’s strategy. This is called strategy stealing.

  strategyStealing : (xs ys : List Position) → ¬ IncludesWinningSet xs →
    SecondCanForceWin xs ys → FirstCanForceWin ys xs
  strategyStealing xs ys ¬iws[xs] h = ¬iws[xs] , x , ¬x∈ys , ¬x∈xs , [1]
    where
    x = proj₁ (newPos (xs ++ ys))
    ¬x∈xs++ys : ¬ x ∈ xs ++ ys
    ¬x∈xs++ys = proj₂ (newPos (xs ++ ys))
    ¬x∈xs : ¬ x ∈ xs
    ¬x∈xs x∈xs = ¬x∈xs++ys (∈-++⁺ˡ x∈xs)
    ¬x∈ys : ¬ x ∈ ys
    ¬x∈ys x∈ys = ¬x∈xs++ys (∈-++⁺ʳ xs x∈ys)
    [1] : SecondCanForceWin xs (x ∷ ys)
    [1] = monotonicityLemma₂ xs ys (x ∷ ys) h (xs⊆x∷xs ys x)

This proves that the second player has no winning strategy starting from the empty board.

  secondHasNoWinningStrategy : ¬ SecondCanForceWin [] []
  secondHasNoWinningStrategy h = onlyOnePlayerCanForceWin [] [] [2] h
    where
    [1] : ¬ IncludesWinningSet []
    [1] ([] , ws[zs] , zs⊆[])         = ¬ws[] ws[zs]
    [1] (x ∷ zs , ws[x∷zs] , x∷zs⊆[]) = x∷xs⊈[] x∷zs⊆[]
    [2] : FirstCanForceWin [] []
    [2] = strategyStealing [] [] [1] h

Pairing strategies

Now we are going to show that the existence of a pairing implies that the first player has no winning strategy. A function from the set of positions to the set of positions is a pairing if it is a permutation entirely consisting of 2-cycles. Note that a pairing must be injective.

The notion of a pairing only depends on the set of positions, so it is defined outside of the current module PositionalGame, which has a whole bunch of other parameters.

  open PairingDef Position

This declaration makes available the record type Pairing, defined as follows (Involutive _≡_ func means (x : Position) → func (func x) ≡ x)):

  record Pairing : Set where
    field
      func       : Position → Position
      noFix      : (x : Position) → func x ≢ x
      involutive : Involutive _≡_ func

    injective : {x y : Position} → func x ≡ func y → x ≡ y
    injective {x} {y} h = 
      trans (trans (sym (involutive x)) (cong func h)) (involutive y)

A pairing p blocks a list of positions xs by a position x if both x and func p x are in xs. We say that p blocks xs if p blocks xs by some position. This latter predicate has a slightly different formulation, which shows that it is decidable.

  open Pairing
  
  BlocksBy : Pairing → Position → List Position → Set
  BlocksBy p x xs = x ∈ xs × func p x ∈ xs

  Blocks : Pairing → List Position → Set
  Blocks p xs = Σ Position λ x → BlocksBy p x xs

  Blocks′ : Pairing → List Position → Set
  Blocks′ p xs = Any (λ x → func p x ∈ xs) xs

  blocks′? : B.Decidable Blocks′
  blocks′? p xs = Any.any? (λ x → func p x ∈? xs) xs

  blocks-equiv : (p : Pairing) (xs : List Position) → 
    Blocks p xs ↔ Blocks′ p xs
  blocks-equiv p xs = [1] xs xs , [2] xs xs
    where
    [1] : (ys xs : List Position) → (Σ Position λ x → x ∈ xs × func p x ∈ ys) → 
          Any (λ x → func p x ∈ ys) xs
    [1] ys (x ∷ xs) (x , here refl , h₂) = here h₂
    [1] ys (x ∷ xs) (x₁ , there h₁ , h₂) = there ([1] ys xs (x₁ , h₁ , h₂))
    [2] : (ys xs : List Position) → Any (λ x → func p x ∈ ys) xs → 
          Σ Position λ x → x ∈ xs × func p x ∈ ys
    [2] ys (x ∷ xs) (here px) = x , here refl , px
    [2] ys (x ∷ xs) (there h) with [2] ys xs h
    ... | y , h₁ , h₂ = y , there h₁ , h₂

  blocks? : B.Decidable Blocks
  blocks? p xs with blocks′? p xs
  ... | no ¬blocks′ = no (λ h → ¬blocks′ (proj₁ (blocks-equiv p xs) h))
  ... | yes blocks′ = yes (proj₂ (blocks-equiv p xs) blocks′)

A pairing is good if it blocks all winning sets.

  Good : Pairing → Set
  Good p = {xs : List Position} → WinningSet xs → Blocks p xs

The existence of a good pairing implies that the second player can force a draw, i.e., the first player cannot force a win. We first prove that a certain invariant that is incompatible with the first player’s win can be maintained throughout the game.

  module _ (p : Pairing) (good : Good p) where

    private
      f = func p

    blockingPos : {xs : List Position} (ws[xs] : WinningSet xs) → Position
    blockingPos ws[xs] = proj₁ (good ws[xs])

    blocksByBlockingPos : {xs : List Position} (ws[xs] : WinningSet xs) → 
      BlocksBy p (blockingPos ws[xs]) xs
    blocksByBlockingPos ws[xs] = proj₂ (good ws[xs])

    record Invariant (xs ys : List Position) : Set
    record Invariant xs ys where
      field
        disjoint : ¬ Σ Position λ x → x ∈ xs × x ∈ ys
        pair     : (x : Position) → x ∈ xs ↔ f x ∈ ys


    open Invariant

Invariant xs ys implies that neither xs nor ys can include a winning set.

    invariant⇒¬IWS : (xs ys : List Position) → Invariant xs ys → 
      ¬ IncludesWinningSet xs × ¬ IncludesWinningSet ys
    invariant⇒¬IWS xs ys h = [1] , [2]
      where
      [1] : ¬ IncludesWinningSet xs
      [1] (zs , ws[zs] , zs⊆xs) = disjoint h (f z , f[z]∈xs , f[z]∈ys)
        where
        z = blockingPos ws[zs]
        [1-1] : BlocksBy p z zs
        [1-1] = blocksByBlockingPos ws[zs]
        z∈zs : z ∈ zs
        z∈zs = proj₁ [1-1]
        f[z]∈zs : f z ∈ zs
        f[z]∈zs = proj₂ [1-1]
        z∈xs : z ∈ xs
        z∈xs = zs⊆xs z∈zs
        f[z]∈xs : f z ∈ xs
        f[z]∈xs = zs⊆xs f[z]∈zs
        f[z]∈ys : f z ∈ ys
        f[z]∈ys = proj₁ (pair h z) z∈xs
      [2] : ¬ IncludesWinningSet ys
      [2] (zs , ws[zs] , zs⊆ys) = disjoint h (z , z∈xs , z∈ys)
        where
        z = blockingPos ws[zs]
        [2-1] : BlocksBy p z zs
        [2-1] = blocksByBlockingPos ws[zs]
        z∈zs = proj₁ [2-1]
        f[z]∈zs : f z ∈ zs
        f[z]∈zs = proj₂ [2-1]
        z∈ys : z ∈ ys
        z∈ys = zs⊆ys z∈zs
        f[z]∈ys : f z ∈ ys
        f[z]∈ys = zs⊆ys f[z]∈zs
        z∈xs : z ∈ xs
        z∈xs = proj₂ (pair h z) f[z]∈ys

The invariant holds of the initial state.

    invariantInitial : Invariant [] []
    invariantInitial = record { disjoint = [1] ; pair = [2] }
      where
      [1] : ¬ Σ Position λ x → x ∈ [] × x ∈ []
      [1] ()
      [2] : (x : Position) → (x ∈ [] → f x ∈ []) × (f x ∈ [] → x ∈ [])
      [2] x = (λ ()) , λ ()

The invariant can be maintained throughout the game, which is inconsistent with the existence of a winning strategy for the first player.

    invariant⇒¬FirstCanForceWin : (xs ys : List Position) → Invariant xs ys → 
      ¬ FirstCanForceWin xs ys

Suppose Invariant xs ys and FirstCanForceWin xs ys. Then the first player can make a move x that results in a state where the now second (i.e., formerly first) player can force a win.

Case 1. The second (formerly first) player has already won, i.e., x ∷ xs now includes a winning set zs. Let z₁, z₂ = f z₁ be the blocking pair for zs. Then both z₁ and z₂ are in x ∷ xs.

    invariant⇒¬FirstCanForceWin xs ys h₁ 
      (¬iws[ys] , x , ¬x∈xs , ¬x∈ys , now .(x ∷ xs) iws[x∷xs]) = contra
      where
      ¬iws[xs] : ¬ IncludesWinningSet xs
      ¬iws[xs] = proj₁ (invariant⇒¬IWS xs ys h₁)
      zs = proj₁ iws[x∷xs]
      ws[zs] : WinningSet zs
      ws[zs] = proj₁ (proj₂ iws[x∷xs])
      zs⊆x∷xs : zs ⊆ x ∷ xs
      zs⊆x∷xs = proj₂ (proj₂ iws[x∷xs])
      z₁ = blockingPos ws[zs]
      z₁∈zs : z₁ ∈ zs
      z₁∈zs = proj₁ (blocksByBlockingPos ws[zs])
      z₁∈x∷xs : z₁ ∈ x ∷ xs
      z₁∈x∷xs = zs⊆x∷xs z₁∈zs
      z₂ = f z₁
      z₂∈zs : z₂ ∈ zs
      z₂∈zs = proj₂ (blocksByBlockingPos ws[zs])
      z₂∈x∷xs : z₂ ∈ x ∷ xs
      z₂∈x∷xs = zs⊆x∷xs z₂∈zs

There are four cases to consider, depending on whether z₁ ≡ x or z₁ ∈ xs and on whether z₂ ≡ x or z₂ ∈ xs. All cases will result in a contradiction.

      [1] : z₁ ∈ xs → z₂ ∈ ys
      [1] = proj₁ (pair h₁ z₁)
      [2] : z₂ ∈ xs → z₁ ∈ ys
      [2] = subst (λ z → z₂ ∈ xs → z ∈ ys) (involutive p z₁) (proj₁ (pair h₁ z₂))
      contra : ⊥
      contra with z₁∈x∷xs | z₂∈x∷xs
      ... | here z₁≡x | here z₂≡x     = noFix p z₁ z₂≡z₁
        where
        z₂≡z₁ : z₂ ≡ z₁
        z₂≡z₁ rewrite z₁≡x | z₂≡x = refl
      ... | here z₁≡x | there z₂∈xs   = ¬z₁∈ys z₁∈ys
        where
        z₁∈ys : z₁ ∈ ys
        z₁∈ys = [2] z₂∈xs
        ¬z₁∈ys : ¬ z₁ ∈ ys
        ¬z₁∈ys rewrite z₁≡x = ¬x∈ys
      ... | there z₁∈xs | here z₂≡x   = ¬z₂∈ys z₂∈ys
        where
        z₂∈ys : z₂ ∈ ys
        z₂∈ys = [1] z₁∈xs
        ¬z₂∈ys : ¬ z₂ ∈ ys
        ¬z₂∈ys rewrite z₂≡x = ¬x∈ys
      ... | there z₁∈xs | there z₂∈xs = disjoint h₁ (z₂ , z₂∈xs , z₂∈ys)
        where
        z₂∈ys : z₂ ∈ ys
        z₂∈ys = [1] z₁∈xs

Case 2. The first (formerly second) player responds with an arbitrary move. Suppose the move is f x. It must result in a state where the original first player has a winning strategy. It suffices to show that the invariant still holds in that state.

    invariant⇒¬FirstCanForceWin xs ys h₁ 
      (¬iws[ys] , x , ¬x∈xs , ¬x∈ys , later h₂) = 
      invariant⇒¬FirstCanForceWin (x ∷ xs) (f x ∷ ys) [5]
      (h₂ ¬f[x]∈ys ¬f[x]∈x∷xs)  -- Writing [*] here makes termination checking fail.
      where
      [1] : f x ∈ ys → x ∈ xs
      [1] = proj₂ (pair h₁ x)
      [2] : f x ∈ xs → x ∈ ys
      [2] = subst (λ z → f x ∈ xs → z ∈ ys) (involutive p x) 
            (proj₁ (pair h₁ (f x)))
      ¬f[x]∈ys : ¬ f x ∈ ys
      ¬f[x]∈ys fx∈ys = ¬x∈xs ([1] fx∈ys)
      ¬f[x]∈xs : ¬ f x ∈ xs
      ¬f[x]∈xs fx∈xs = ¬x∈ys ([2] fx∈xs)
      ¬f[x]∈x∷xs : ¬ f x ∈ x ∷ xs
      ¬f[x]∈x∷xs (here f[x]≡x)   = noFix p x f[x]≡x
      ¬f[x]∈x∷xs (there f[x]∈xs) = ¬f[x]∈xs f[x]∈xs
      [3] : ¬ Σ Position λ z → z ∈ x ∷ xs × z ∈ f x ∷ ys
      [3] (z , here refl , here z≡f[x]) = noFix p x (sym z≡f[x])
      [3] (z , here refl , there z∈ys) = ¬x∈ys z∈ys
      [3] (z , there f[x]∈xs , here refl) = ¬f[x]∈xs f[x]∈xs
      [3] (z , there z∈xs , there z∈ys) = disjoint h₁ (z , z∈xs , z∈ys)
      [4] : (z : Position) → 
            (z ∈ x ∷ xs → f z ∈ f x ∷ ys) × (f z ∈ f x ∷ ys → z ∈ x ∷ xs)
      [4] z = [4-3] , [4-4]
        where
        [4-1] : z ∈ xs → f z ∈ ys
        [4-1] = proj₁ (pair h₁ z)
        [4-2] : f z ∈ ys → z ∈ xs
        [4-2] = proj₂ (pair h₁ z)
        [4-3] : z ∈ x ∷ xs → f z ∈ f x ∷ ys
        [4-3] (here refl) = here refl
        [4-3] (there z∈xs) = there ([4-1] z∈xs)
        [4-4] : f z ∈ f x ∷ ys → z ∈ x ∷ xs
        [4-4] (here f[z]≡f[x])     = here (injective p f[z]≡f[x])
        [4-4] (there f[z]∈ys) = there ([4-2] f[z]∈ys)
      [5] : Invariant (x ∷ xs) (f x ∷ ys)
      [5] = record { disjoint = [3] ; pair = [4] }
      -- [*] : FirstCanForceWin (x ∷ xs) (f x ∷ ys)
      -- [*] = h₂ ¬f[x]∈ys ¬f[x]∈x∷xs

We can now conlude that the first player has no winning strategy. This conclusion was derived under the assumption of the existence of a good pairing.

    firstHasNoWinningStrategy : ¬ FirstCanForceWin [] []
    firstHasNoWinningStrategy = 
      invariant⇒¬FirstCanForceWin [] [] invariantInitial

N-in-a-row

We define the N-in-a-row game as a concrete example of a positional game. A position is a pair of integers.

Position : Set
Position = ℤ × ℤ

Clearly, there are infinitely many positions.

maxAbs : List Position → ℕ
maxAbs = foldr (λ { (k , l) m → ∣ k ∣ ⊔ ∣ l ∣ ⊔ m }) 

maxAbs-head : (k l : ℤ) (xs : List Position) → 
              ∣ k ∣ ⊔ ∣ l ∣ ℕ.≤ maxAbs ((k , l) ∷ xs)
maxAbs-head k l xs = m≤m⊔n (∣ k ∣ ⊔ ∣ l ∣) (maxAbs xs)  

maxAbs-tail : (m n : ℤ) (xs : List Position) → 
              maxAbs xs ℕ.≤ maxAbs ((m , n) ∷ xs)
maxAbs-tail m n xs = m≤n⊔m (∣ m ∣ ⊔ ∣ n ∣) (maxAbs xs)

maxAbs-≤ : (xs : List Position) → 
           All (λ { (k , l) → ∣ k ∣ ⊔ ∣ l ∣ ℕ.≤ maxAbs xs }) xs
maxAbs-≤ []             = []
maxAbs-≤ ((m , n) ∷ xs) = maxAbs-head m n xs ∷ [1] 
  where
  P : Position → Set
  P = λ{ (k , l) → ∣ k ∣ ⊔ ∣ l ∣ ℕ.≤ maxAbs xs }
  Q : Position → Position → Set
  Q (x , y) = λ{ (k , l) → ∣ k ∣ ⊔ ∣ l ∣ ℕ.≤ maxAbs ((x , y) ∷ xs) }
  [1] : All (λ { (k , l) → ∣ k ∣ ⊔ ∣ l ∣ ℕ.≤ maxAbs ((m , n) ∷ xs) }) xs
  [1] = all-⇒ {A = Position} {P = P} {Q = Q (m , n)} 
        (λ h → ≤-trans h (maxAbs-tail m n xs)) (maxAbs-≤ xs)

newPos : (xs : List Position) → Σ Position λ y → ¬ y ∈ xs
newPos xs = ( + suc (maxAbs xs) , + suc (maxAbs xs) ) , [1]
  where
  [1] : ¬ (+ suc (maxAbs xs) , + suc (maxAbs xs)) ∈ xs
  [1] h = 1+n≰n [1-1]
    where
    [1-1] : suc (maxAbs xs) ℕ.≤ maxAbs xs
    [1-1] = ≤-trans (≤-reflexive (sym (⊔-idem (suc (maxAbs xs))))) 
            (all-∈ (maxAbs-≤ xs) h)

Each winning set is represented by a list of positions determined by one of its end position and a direction, which is also a pair of integers.

directions : List (ℤ × ℤ)
directions = (1ℤ , 0ℤ) ∷ (0ℤ , 1ℤ) ∷ (1ℤ , 1ℤ) ∷ (-1ℤ , 1ℤ) ∷ []

N-in-a-row is parameterized by a positive number n, which determines the length of each winning set.

module _ (n : ℕ) {n≢0 : False (n ℕ.≟ )} where

  ¬n≡0 : ¬ n ≡ 
  ¬n≡0 = toWitnessFalse n≢0

  suc-pred : suc (pred n) ≡ n
  suc-pred = suc[pred[n]]≡n ¬n≡0

  winningSet : Position → ℤ × ℤ → List Position
  winningSet z d = applyUpTo (λ k → (k · d) +₂ z) n

  WinningSet : List Position → Set
  WinningSet xs = Σ Position λ z → Any (λ d → xs ≡ winningSet z d) directions

It is clear that WinningSet is decidable.

  winningSet-cons : ∀ x xs → WinningSet (x ∷ xs) → 
    Any (λ d → x ∷ xs ≡ winningSet x d) directions
  winningSet-cons x xs (z , h) = 
    subst (λ w → Any (λ d → x ∷ xs ≡ winningSet w d) directions)
    (sym ([1] directions h)) h
    where
    [1] : ∀ ys → 
      Any (λ d → x ∷ xs ≡ winningSet z d) ys → x ≡ z
    [1] (y ∷ ys) (here px)  rewrite sym suc-pred = 
      trans (∷-injectiveˡ px) 
      (cong₂ _,_ (+-identityˡ (proj₁ z)) (+-identityˡ (proj₂ z)))
    [1] (y ∷ ys) (there h₁) = [1] ys h₁

  ¬WinningSet[] : ¬ WinningSet []
  ¬WinningSet[] (z , h) rewrite sym suc-pred = ∀¬-¬any [1] directions h
    where
    P = λ d → [] ≡ ( · d) +₂ z ∷ applyUpTo (λ k → (suc k · d) +₂ z) (pred n)
    [1] : ∀ d → ¬ P d
    [1] d ()

  winningSet-equiv : 
    ∀ x xs → (WinningSet (x ∷ xs) ↔ 
    Any (λ d → x ∷ xs ≡ winningSet x d) directions)
  winningSet-equiv x xs = winningSet-cons x xs , λ h → (x , h)

  winningSet? : Decidable WinningSet
  winningSet? [] = no ¬WinningSet[]
  winningSet? (x ∷ xs) 
    with Any.any? (λ d → List-≡-dec ℤ×ℤ._≟_ (x ∷ xs) 
        (winningSet x d)) directions
  ... | no ¬p = no (λ v → ¬p (proj₁ (winningSet-equiv x xs) v))
  ... | yes p = yes (proj₂ (winningSet-equiv x xs) p)

Doubly periodic predicates and functions

A predicate P : ℤ × ℤ → Set or a function g : ℤ × ℤ → A is doubly d-periodic if it is periodic with period d with respect to both coordinates. The universal closure of a doubly d-periodic predicate is true whenever the predicate holds throughout the d×d square whose lower left corner is the origin.

module _ (d : ℕ) {d≢0 : False (d ℕ.≟ )} where

  Periodic₂ : (ℤ × ℤ → Set) → Set
  Periodic₂ P = (k l : ℤ) → P (k , l) ↔ P (+ (k %ℕ d) {d≢0} , + (l %ℕ d) {d≢0})

  periodic₂-⇔ : {P Q : ℤ × ℤ → Set} → ((z : ℤ × ℤ) → P z ↔ Q z) → 
                Periodic₂ P → Periodic₂ Q
  periodic₂-⇔ P⇔Q h k l = 
    ↔-trans (↔-trans (↔-sym (P⇔Q (k , l))) (h k l)) 
    (P⇔Q (+ (k %ℕ d) , + (l %ℕ d)))

  PeriodicF₂ : {A : Set} → (ℤ × ℤ → A) → Set
  PeriodicF₂ g = (k l : ℤ) → g (k , l) ≡ g (+ (k %ℕ d) {d≢0} , + (l %ℕ d) {d≢0})

  periodicF₂-periodic₂ : {A : Set} (g : ℤ × ℤ → A) → PeriodicF₂ g ↔ 
                        ((x : A) → Periodic₂ (λ z → g z ≡ x))
  periodicF₂-periodic₂ {A} g = [1] , [2]
    where
    [1] : PeriodicF₂ g → (x : A) → Periodic₂ (λ z → g z ≡ x)
    [1] h x k l rewrite sym (h k l) = ↔-refl
    [2] : ((x : A) → Periodic₂ (λ z → g z ≡ x)) → PeriodicF₂ g
    [2] h k l = sym (proj₁ (h (g (k , l)) k l) refl)

In Agda, Fin d is the type of natural numbers less than d. The function toℕ converts elements of Fin d to elements of ℕ, and the function fromℕ< converts proofs of i ℕ.< d into elements of Fin d. Then toℕ-fromℕ< takes a proof i<d of i ℕ.< d and returns a proof of i ≡ toℕ (fromℕ< i<d).

  UnivFin : (ℤ × ℤ → Set) → Set
  UnivFin P = (i j : Fin d) → P (+ (toℕ i) , + (toℕ j))

  periodic₂-univ : {P : ℤ × ℤ → Set} → Periodic₂ P → 
    UnivFin P → (z : ℤ × ℤ) → P z
  periodic₂-univ {P} h h₁ (m , n) = proj₂ (h m n) [1]
    where
    [1] : P (+ (m %ℕ d) {d≢0} , + (n %ℕ d) {d≢0})
    [1] rewrite sym (toℕ-fromℕ< (n%ℕd<d m d {d≢0})) | 
                sym (toℕ-fromℕ< (n%ℕd<d n d {d≢0}))
      = h₁ (fromℕ< (n%ℕd<d m d {d≢0})) (fromℕ< (n%ℕd<d n d {d≢0}))

Whenever Q is a decidable binary relation on Fin d, then we can decide if Q holds universally. It follows that if a doubly periodic predicate P : ℤ × ℤ → Set is decidable, we can decide whether it holds universally.

  univFin? : {P : ℤ × ℤ → Set} → Decidable P → Dec (UnivFin P)
  univFin? P? = all? (λ i → all? λ j → P? (+ toℕ i , + toℕ j))

  univ? : {P : ℤ × ℤ → Set} → Decidable P → Periodic₂ P → 
          Dec ((z : ℤ × ℤ) → P z)
  univ? {P} P? h with univFin? P?
  ... | no ¬p = no (λ q → ¬Pij (q (+ toℕ i , + toℕ j)))
    where
    [1] : ∃₂ λ i j → ¬ P (+ toℕ i , + toℕ j)
    [1] = ¬∀₂⟶∃₂¬ d (λ i j → P (+ toℕ i , + toℕ j)) 
      (λ i j → P? (+ toℕ i , + toℕ j)) ¬p
    i = proj₁ [1]
    j = proj₁ (proj₂ [1])
    ¬Pij : ¬ P (+ toℕ i , + toℕ j)
    ¬Pij = proj₂ (proj₂ [1])
  ... | yes p = yes [1]
    where
    [1] : (z : ℤ × ℤ) → P z
    [1] (k , l) = proj₂ (h k l) [3]
      where
      [2] : P (+ toℕ (fromℕ< (n%ℕd<d k d)) , + toℕ (fromℕ< (n%ℕd<d k d))) 
      [2] = p (fromℕ< (n%ℕd<d k d {d≢0})) (fromℕ< (n%ℕd<d k d {d≢0}))
      [3] : P (+ (k %ℕ d) {d≢0} , + (l %ℕ d) {d≢0})
      [3] rewrite sym (toℕ-fromℕ< (n%ℕd<d k d {d≢0})) | 
                  sym (toℕ-fromℕ< (n%ℕd<d l d {d≢0}))
          = p (fromℕ< (n%ℕd<d k d {d≢0})) (fromℕ< (n%ℕd<d l d {d≢0}))

It will be useful to give an alternative formulation of double periodicity.

  Periodic₂-+-* : (ℤ × ℤ → Set) → Set
  Periodic₂-+-* P = (q₁ q₂ k l : ℤ) → P (k , l) ↔ P (k + q₁ * + d , l + q₂ * + d)

  periodic₂-periodic₂-+-* : {P : ℤ × ℤ → Set} → Periodic₂ P ↔ Periodic₂-+-* P
  periodic₂-periodic₂-+-* {P} = [1] , [2]
    where
    [1] : Periodic₂ P → Periodic₂-+-* P
    [1] h q₁ q₂ k l = ↔-trans (↔-trans (h k l) [1-1]) 
          (↔-sym (h (k + q₁ * + d) (l + q₂ * + d)))
      where
      [1-1] : P (+ (k %ℕ d) {d≢0} , + (l %ℕ d) {d≢0}) ↔ 
              P (+ ((k + q₁ * + d) %ℕ d) {d≢0} , + ((l + q₂ * + d) %ℕ d) {d≢0})
      [1-1] rewrite [m+kn]%ℕn≡[m]%ℕn k q₁ d {d≢0}
                  | [m+kn]%ℕn≡[m]%ℕn l q₂ d {d≢0} = ↔-refl
    [2] : Periodic₂-+-* P → Periodic₂ P
    [2] h k l = ↔-trans [2-1] (↔-sym (h ((k /ℕ d) {d≢0}) 
      ((l /ℕ d) {d≢0}) k′ l′))
      where
      k′ = + (k %ℕ d) {d≢0}
      l′ = + (l %ℕ d) {d≢0}
      k′′ = k′ + (k /ℕ d) {d≢0} * + d
      l′′ = l′ + (l /ℕ d) {d≢0} * + d
      [2-1] : P (k , l) ↔ P (k′′ , l′′)
      [2-1] rewrite sym (a≡a%ℕn+[a/ℕn]*n k d {d≢0})
                  | sym (a≡a%ℕn+[a/ℕn]*n l d {d≢0}) = ↔-refl

  PeriodicF₂-+-* : {A : Set} → (ℤ × ℤ → A) → Set
  PeriodicF₂-+-* g = 
    (q₁ q₂ k l : ℤ) → g (k , l) ≡ g (k + q₁ * + d , l + q₂ * + d)

  periodicF₂-+-*-periodic₂-+-* : {A : Set} (g : ℤ × ℤ → A) → PeriodicF₂-+-* g ↔ 
                        ((x : A) → Periodic₂-+-* (λ z → g z ≡ x))
  periodicF₂-+-*-periodic₂-+-* {A} g = [1] , [2]
    where
    [1] : PeriodicF₂-+-* g → (x : A) → Periodic₂-+-* (λ z → g z ≡ x)
    [1] h x q₁ q₂ k l rewrite sym (h q₁ q₂ k l) = ↔-refl
    [2] : ((x : A) → Periodic₂-+-* (λ z → g z ≡ x)) → PeriodicF₂-+-* g
    [2] h q₁ q₂ k l = sym (proj₁ (h (g (k , l)) q₁ q₂ k l) refl)

  periodicF₂-periodicF₂-+-* : {A : Set} (g : ℤ × ℤ → A) →
                              PeriodicF₂ g ↔ PeriodicF₂-+-* g
  periodicF₂-periodicF₂-+-* {A} g = 
    ↔-trans (↔-trans (periodicF₂-periodic₂ g) [3]) 
    (↔-sym (periodicF₂-+-*-periodic₂-+-* g)) 
    where
    [1] : ((x : A) → Periodic₂ (λ z → g z ≡ x)) → 
          ((x : A) → Periodic₂-+-* (λ z → g z ≡ x))
    [1] h x = proj₁ periodic₂-periodic₂-+-* (h x)
    [2] : ((x : A) → Periodic₂-+-* (λ z → g z ≡ x)) →
          ((x : A) → Periodic₂ (λ z → g z ≡ x))
    [2] h x = proj₂ periodic₂-periodic₂-+-* (h x)
    [3] : ((x : A) → Periodic₂ (λ z → g z ≡ x)) ↔ 
          ((x : A) → Periodic₂-+-* (λ z → g z ≡ x))
    [3] = [1] , [2]

We state a couple of useful facts for later use.

  periodicF₂-comp : 
    {A B C : Set} {g₁ : ℤ × ℤ → A} {g₂ : ℤ × ℤ → B} (g : A → B → C) →
    PeriodicF₂ g₁ → PeriodicF₂ g₂ → PeriodicF₂ (λ z → g (g₁ z) (g₂ z))
  periodicF₂-comp g h₁ h₂ k l = cong₂ g (h₁ k l) (h₂ k l)

  periodic₂-all : {A : Set} {R : A → ℤ × ℤ → Set} → ((x : A) → 
                  Periodic₂ (R x)) → (xs : List A) → 
                  Periodic₂ (λ z → All (λ x → R x z) xs)
  periodic₂-all {R = R} h xs k l = [1] , [2]
    where
    [1] : All (λ x → R x (k , l)) xs → 
          All (λ x → R x (+ (k %ℕ d) {d≢0} , + (l %ℕ d) {d≢0})) xs
    [1] = all-⇒ {P = λ x → R x (k , l)} 
      {Q = (λ x → R x (+ (k %ℕ d) , + (l %ℕ d)))} (λ {x} → proj₁ (h x k l)) {xs}
    [2] : All (λ x → R x (+ (k %ℕ d) {d≢0}, + (l %ℕ d) {d≢0})) xs → 
          All (λ x → R x (k , l)) xs
    [2] = all-⇒ {P = (λ x → R x (+ (k %ℕ d) , + (l %ℕ d)))} 
      {Q = λ x → R x (k , l)} (λ {x} → proj₂ (h x k l)) {xs}

Hales-Jewett pairing

We define the Hales-Jewett pairing. This is one of several pairings for the N-in-a-row game that are known to be good for N ≥ 9. It is defined in terms of the following 8 × 8 table.

table : Fin  → Fin  → ℤ × ℤ
table 0F 0F = (0ℤ , 1ℤ)
table 0F 1F = -₂ (0ℤ , 1ℤ)
table 0F 2F = (1ℤ , 1ℤ)
table 0F 3F = -₂ (-1ℤ , 1ℤ)
table 0F 4F = -₂ (1ℤ , 0ℤ)
table 0F 5F = -₂ (1ℤ , 0ℤ)
table 0F 6F = (1ℤ , 1ℤ)
table 0F 7F = -₂ (-1ℤ , 1ℤ)
table 1F 0F = (1ℤ , 0ℤ)
table 1F 1F = (1ℤ , 0ℤ)
table 1F 2F = (-1ℤ , 1ℤ)
table 1F 3F = -₂ (1ℤ , 1ℤ)
table 1F 4F = (0ℤ , 1ℤ)
table 1F 5F = -₂ (0ℤ , 1ℤ)
table 1F 6F = (-1ℤ , 1ℤ)
table 1F 7F = -₂ (1ℤ , 1ℤ)
table 2F 0F = -₂ (1ℤ , 0ℤ)
table 2F 1F = -₂ (1ℤ , 0ℤ)
table 2F 2F = -₂ (-1ℤ , 1ℤ)
table 2F 3F = (1ℤ , 1ℤ)
table 2F 4F = (0ℤ , 1ℤ)
table 2F 5F = -₂ (0ℤ , 1ℤ)
table 2F 6F = -₂ (-1ℤ , 1ℤ)
table 2F 7F = (1ℤ , 1ℤ)
table 3F 0F = -₂ (1ℤ , 1ℤ)
table 3F 1F = (-1ℤ , 1ℤ)
table 3F 2F = (0ℤ , 1ℤ)
table 3F 3F = -₂ (0ℤ , 1ℤ)
table 3F 4F = -₂ (1ℤ , 1ℤ)
table 3F 5F = (-1ℤ , 1ℤ)
table 3F 6F = (1ℤ , 0ℤ)
table 3F 7F = (1ℤ , 0ℤ)
table 4F 0F = (1ℤ , 1ℤ)
table 4F 1F = -₂ (-1ℤ , 1ℤ)
table 4F 2F = (0ℤ , 1ℤ)
table 4F 3F = -₂ (0ℤ , 1ℤ)
table 4F 4F = (1ℤ , 1ℤ)
table 4F 5F = -₂ (-1ℤ , 1ℤ)
table 4F 6F = -₂ (1ℤ , 0ℤ)
table 4F 7F = -₂ (1ℤ , 0ℤ)
table 5F 0F = (-1ℤ , 1ℤ)
table 5F 1F = -₂ (1ℤ , 1ℤ)
table 5F 2F = (1ℤ , 0ℤ)
table 5F 3F = (1ℤ , 0ℤ)
table 5F 4F = (-1ℤ , 1ℤ)
table 5F 5F = -₂ (1ℤ , 1ℤ)
table 5F 6F = (0ℤ , 1ℤ)
table 5F 7F = -₂ (0ℤ , 1ℤ)
table 6F 0F = -₂ (-1ℤ , 1ℤ)
table 6F 1F = (1ℤ , 1ℤ)
table 6F 2F = -₂ (1ℤ , 0ℤ)
table 6F 3F = -₂ (1ℤ , 0ℤ)
table 6F 4F = -₂ (-1ℤ , 1ℤ)
table 6F 5F = (1ℤ , 1ℤ)
table 6F 6F = (0ℤ , 1ℤ)
table 6F 7F = -₂ (0ℤ , 1ℤ)
table 7F 0F = (0ℤ , 1ℤ)
table 7F 1F = -₂ (0ℤ , 1ℤ)
table 7F 2F = -₂ (1ℤ , 1ℤ)
table 7F 3F = (-1ℤ , 1ℤ)
table 7F 4F = (1ℤ , 0ℤ)
table 7F 5F = (1ℤ , 0ℤ)
table 7F 6F = -₂ (1ℤ , 1ℤ)
table 7F 7F = (-1ℤ , 1ℤ)

This table has no entry equal to (0ℤ , 0ℤ). We can let Agda automatically generate the proof of this assertion simply by showing that it is decidable.

TableNonZero : Set
TableNonZero = (i j : Fin ) → table i j ≢ (0ℤ , 0ℤ)

tableNonZero? : Dec (TableNonZero)
tableNonZero? = all? (λ i → all? λ j → ¬? (ℤ×ℤ._≟_ (table i j) ((0ℤ , 0ℤ))))

tableNonZero : TableNonZero
tableNonZero = toWitness {Q = tableNonZero?} tt

Of course, it is also easy (though tedious) to prove TableNonZero manually; it would require case split into 64 cases.

tableNonZero : TableNonZero
tableNonZero 0F 0F ()
tableNonZero 0F 1F ()
tableNonZero 0F 2F ()
tableNonZero 0F 3F ()
tableNonZero 0F 4F ()
tableNonZero 0F 5F ()
tableNonZero 0F 6F ()
tableNonZero 0F 7F ()
tableNonZero 1F 0F ()
...
...
tableNonZero 7F 7F ()

The Hales-Jewett pairing is defined in terms of the extension of this table to the whole plane. We call this pairing f.

extendToℤ×ℤ : {d : ℕ} {d≢0 : False (d ℕ.≟ )} {A : Set} → (Fin d → Fin d → A) → 
              ℤ × ℤ → A
extendToℤ×ℤ {d} {d≢0} g (k , l) = 
  g (fromℕ< ((n%ℕd<d k d) {d≢0})) (fromℕ< ((n%ℕd<d l d) {d≢0}))

tableℤ×ℤ : (ℤ × ℤ) → (ℤ × ℤ)
tableℤ×ℤ = extendToℤ×ℤ table

tableℤ×ℤ-periodicF₂ : PeriodicF₂  tableℤ×ℤ
tableℤ×ℤ-periodicF₂ k l = sym (cong₂ table [3] [4])
  where
  [1] : + (k %ℕ ) %ℕ  ≡ k %ℕ 
  [1] = [[m]%ℕn]%ℕn≡[m]%ℕn k 
  [2] : + (l %ℕ ) %ℕ  ≡ l %ℕ 
  [2] = [[m]%ℕn]%ℕn≡[m]%ℕn l 
  [3] : fromℕ< (n%ℕd<d (+ (k %ℕ )) ) ≡ fromℕ< (n%ℕd<d k )
  [3] = fromℕ<-cong (+ (k %ℕ ) %ℕ ) (k %ℕ ) [1] 
        (n%ℕd<d (+ (k %ℕ )) ) (n%ℕd<d k )
  [4] : fromℕ< (n%ℕd<d (+ (l %ℕ )) ) ≡ fromℕ< (n%ℕd<d l )
  [4] = fromℕ<-cong (+ (l %ℕ ) %ℕ ) (l %ℕ ) [2] 
        (n%ℕd<d (+ (l %ℕ )) ) (n%ℕd<d l )

tableℤ×ℤ-periodicF₂-+-* : PeriodicF₂-+-*  tableℤ×ℤ
tableℤ×ℤ-periodicF₂-+-* = 
  proj₁ (periodicF₂-periodicF₂-+-*  tableℤ×ℤ) tableℤ×ℤ-periodicF₂

f : Position → Position
f z = tableℤ×ℤ z +₂ z

We can already prove that f has no fixed point.

noFix : ∀ z → f z ≢ z
noFix (k , l) h = tableNonZero (fromℕ< (n%ℕd<d k )) (fromℕ< (n%ℕd<d l )) [1]
  where
  [1] : tableℤ×ℤ (k , l) ≡ (0ℤ , 0ℤ)
  [1] = z+w≡w⇒z≡0 h

To show that f is involutive, we use the fact that f (f z) ≡ z is a doubly periodic predicate. (We could have used the double periodicity of the predicate f z ≡ z to show that f has no fixed point, but we took a more direct approach.)

The following property of f will be useful.

f-+q*8 : (k l q₁ q₂ : ℤ) → 
  f (k + q₁ * +  , l + q₂ * + ) ≡ f (k , l) +₂ (q₁ * +  , q₂ * + )
f-+q*8 k l q₁ q₂ = begin 
  f (k + q₁ * +  , l + q₂ * + ) 
    ≡⟨⟩ 
  tableℤ×ℤ (k + q₁ * +  , l + q₂ * + ) +₂ (k + q₁ * +  , l + q₂ * + ) 
    ≡˘⟨ cong (_+₂ (k + q₁ * +  , l + q₂ * + )) 
        (tableℤ×ℤ-periodicF₂-+-* q₁ q₂ k l) ⟩ 
  tableℤ×ℤ (k , l) +₂ (k + q₁ * +  , l + q₂ * + ) 
    ≡˘⟨ +₂-assoc (tableℤ×ℤ (k , l)) (k , l) (q₁ * +  , q₂ * + ) ⟩ 
  tableℤ×ℤ (k , l) +₂ (k , l) +₂ (q₁ * +  , q₂ * + ) 
    ≡⟨⟩ 
  f (k , l) +₂ (q₁ * +  , q₂ * + ) 
    ∎ where open Eq.≡-Reasoning

f∘f-+q*8 : (k l q₁ q₂ : ℤ) → 
  f (f (k + q₁ * +  , l + q₂ * + )) ≡ f (f (k , l)) +₂ (q₁ * +  , q₂ * + )
f∘f-+q*8 k l q₁ q₂ = begin 
  f (f (k + q₁ * +  , l + q₂ * + ))    ≡⟨ cong f (f-+q*8 k l q₁ q₂) ⟩
  f (f (k , l) +₂ (q₁ * +  , q₂ * + )) ≡⟨ f-+q*8 k₁ l₁ q₁ q₂ ⟩ 
  f (f (k , l)) +₂ (q₁ * +  , q₂ * + ) ∎
  where
  open Eq.≡-Reasoning
  k₁ = proj₁ (f (k , l))
  l₁ = proj₂ (f (k , l))

We are now ready to prove that the predicate f (f z) ≡ z is doubly periodic.

Invol : Position → Set
Invol z = f (f z) ≡ z

invol-periodic₂-+-* : Periodic₂-+-*  Invol
invol-periodic₂-+-* q₁ q₂ k l = ↔-trans [1] [2]
  where
  [1] : f (f (k , l)) ≡ (k , l) ↔ 
    f (f (k , l)) +₂ (q₁ * +  , q₂ * + ) ≡ (k , l) +₂ (q₁ * +  , q₂ * + )
  [1] = z≡w⇔z+v≡w+v (f (f (k , l))) (k , l) (q₁ * +  , q₂ * + )
  [2] : f (f (k , l)) +₂ (q₁ * +  , q₂ * + ) ≡ (k , l) +₂ (q₁ * +  , q₂ * + )
    ↔ f (f ((k , l) +₂ (q₁ * +  , q₂ * + ))) ≡ (k , l) +₂ (q₁ * +  , q₂ * + )
  [2] rewrite f∘f-+q*8 k l q₁ q₂ = ↔-refl

invol-periodic₂ : Periodic₂  Invol
invol-periodic₂ = proj₂ (periodic₂-periodic₂-+-* ) invol-periodic₂-+-*

We have shown that the predicate f (f z) ≡ z is doubly periodic. Since it is easy to see that it is decidable, our earlier argument shows that Agda can decide whether its universal closure is a true statement. (Note that the double periodicity of f (f z) ≡ z only depends on the fact that f is defined by f (k , l) = extendToℤ×ℤ g (k , l) +₂ (k , l) for some g : Fin d → Fin d → ℤ × ℤ.)

invol? : Decidable Invol
invol? z = f (f z) ℤ×ℤ.≟ z

involutive? : Dec (Involutive _≡_ f)
involutive? = univ?  invol? invol-periodic₂

involutive : Involutive _≡_ f
involutive = toWitness {Q = involutive?} tt

We have shown that the function f is a pairing of ℤ × ℤ.

open PairingDef Position

pairing : Pairing
pairing = record 
  { func       = f
  ; noFix      = noFix
  ; involutive = involutive
  }

We are now going to show that this pairing is good when n ≡ 9. For this, we will express Good pairing in terms of the universal closure of a predicate BlocksWinningSetsAt. This predicate is doubly periodic with period 8, so we can decide whether its universal closure holds.

module N-in-a-row (n : ℕ) {n≢0 : False (n ℕ.≟ )} where
  open PositionalGame Position ℤ×ℤ._≟_ newPos (WinningSet n {n≢0}) 
    (¬WinningSet[] n {n≢0}) public

  BlocksWinningSetsAt : Pairing → Position → Set
  BlocksWinningSetsAt p z = 
    All (λ d → Blocks p (winningSet n {n≢0} z d)) directions

  blocksAllWinningSets-equiv : (p : Pairing) → 
    ((z : Position) → BlocksWinningSetsAt p z) ↔ Good p
  blocksAllWinningSets-equiv p = [1] , [2]
    where
    [1] : ((z : Position) → BlocksWinningSetsAt p z) → Good p
    [1] h {xs} (z , h₁) = [1-3]
      where
      [1-1] : xs ∈ map (λ d → winningSet n {n≢0} z d) directions
      [1-1] = Anyₚ.map⁺ {f = λ d → winningSet n {n≢0} z d} {P = xs ≡_} 
              h₁
      [1-2] : All (Blocks p) 
              (map (λ d → winningSet n {n≢0} z d) directions)
      [1-2] = Allₚ.map⁺ {P = Blocks p} 
              {f = λ d → winningSet n {n≢0} z d} (h z)
      [1-3] : Blocks p xs
      [1-3] = all-∈ {P = Blocks p} [1-2] [1-1]

    [2] : Good p → (z : Position) → BlocksWinningSetsAt p z
    [2] h z = Allₚ.map⁻ {P = Blocks p} 
              {f = (λ d → winningSet n {n≢0} z d)} [2-2]
      where
      [2-1] : (xs : List Position) → 
              xs ∈ map (λ d → winningSet n {n≢0} z d) directions → 
              Blocks p xs
      [2-1] xs h₁ = h [2-1-1]
        where
        [2-1-1] : WinningSet n {n≢0} xs
        [2-1-1] = z , Anyₚ.map⁻ {f = λ d → winningSet n {n≢0} z d} h₁
      [2-2] : All (Blocks p) 
              (map (λ d → winningSet n {n≢0} z d) directions)
      [2-2] = ∈-All (map (λ d → winningSet n {n≢0} z d) directions) 
              [2-1]

  blocksWinningSetsAt? : B.Decidable BlocksWinningSetsAt
  blocksWinningSetsAt? p z = 
    All.all? (λ d → blocks? p (winningSet n {n≢0} z d)) directions

BlocksWinningSetsAt p z holds if p blocks four specific winning sets of the form winningSet n z d. Each of thsese winning sets is a list that has z as its head, and its other elements are determined by z and the direction d.

  BlocksWinningSet : Pairing → ℤ × ℤ → Position → Set
  BlocksWinningSet p d z = Blocks p (winningSet n {n≢0} z d)

Note that BlocksWinningSetsAt p z = All (λ d → BlocksWinningSet p d z) directions. We show that BlocksWinningSet pairing d is doubly periodic for all d. This suffices to show that BlocksWinningSetsAt pairing is doubly periodic.

  member-winningSet-+-* : 
    (z v : Position) (d : ℤ × ℤ) (q₁ q₂ : ℤ) →
    v ∈ winningSet n {n≢0} z d ↔
    v +₂ (q₁ * +  , q₂ * + ) ∈ 
    winningSet n {n≢0} (z +₂ (q₁ * +  , q₂ * + )) d
  member-winningSet-+-* z v d q₁ q₂ = ↔-trans (↔-trans [1] [3]) (↔-sym [2])
    where
    z₁ = z +₂ (q₁ * +  , q₂ * + )
    v₁ = v +₂ (q₁ * +  , q₂ * + )
    [1] : v ∈ winningSet n {n≢0} z d ↔ ∃ λ i → i ℕ.< n × v ≡ (i · d) +₂ z
    [1] = ∈-applyUpTo (λ k → (k · d) +₂ z)
    [2] : v₁ ∈ winningSet n {n≢0} z₁ d ↔ ∃ λ i → i ℕ.< n × v₁ ≡ (i · d) +₂ z₁
    [2] = ∈-applyUpTo (λ k → (k · d) +₂ z₁)
    [3] : (∃ λ i → i ℕ.< n × v ≡ (i · d) +₂ z) ↔ 
          ∃ λ i → i ℕ.< n × v₁ ≡ (i · d) +₂ z₁
    [3] = ↔-∃ [3-1]
      where
      [3-1] : (i : ℕ) → 
              (i ℕ.< n × v ≡ (i · d) +₂ z) ↔ (i ℕ.< n × v₁ ≡ (i · d) +₂ z₁)
      [3-1] i = ↔-× ↔-refl [3-1-1]
        where
        [3-1-1] : v ≡ (i · d) +₂ z ↔ v₁ ≡ (i · d) +₂ z₁
        [3-1-1] rewrite sym (+₂-assoc (i · d) z (q₁ * +  , q₂ * + )) = 
          z≡w⇔z+v≡w+v v ((i · d) +₂ z) (q₁ * +  , q₂ * + )

  blocksWinningSet-periodic₂-+-* : (d : ℤ × ℤ) → 
    Periodic₂-+-*  (BlocksWinningSet pairing d)
  blocksWinningSet-periodic₂-+-* d q₁ q₂ k l = [1] , [2]
    where
    [1] : BlocksWinningSet pairing d (k , l) →
      BlocksWinningSet pairing d (k + q₁ * +  , l + q₂ * + )
    [1] (x , x∈ , f[x]∈) = x₁ , x₁∈ , f[x₁]∈
      where
      x₁ = x +₂ (q₁ * +  , q₂ * + )
      x₁∈ : x₁ ∈ winningSet n {n≢0} (k + q₁ * +  , l + q₂ * + ) d
      x₁∈ = proj₁ (member-winningSet-+-* (k , l) x d q₁ q₂) x∈
      [1-1] : f x₁ ≡ f x +₂ (q₁ * +  , q₂ * + )
      [1-1] = f-+q*8 (proj₁ x) (proj₂ x) q₁ q₂
      f[x₁]∈ : f x₁ ∈ winningSet n {n≢0} (k + q₁ * +  , l + q₂ * + ) d
      f[x₁]∈ rewrite [1-1] = 
        proj₁ (member-winningSet-+-* (k , l) (f x) d q₁ q₂) f[x]∈
    [2] : BlocksWinningSet pairing d (k + q₁ * +  , l + q₂ * + ) →
      BlocksWinningSet pairing d (k , l)
    [2] (x₁ , x₁∈ , f[x₁]∈) = x , x∈ , f[x]∈
      where
      x = x₁ +₂ (-₂ (q₁ * +  , q₂ * + ))
      [2-1] : x₁ ≡ x +₂ (q₁ * +  , q₂ * + )
      [2-1] = sym (z-v+v≡z x₁ (q₁ * +  , q₂ * + ))
      [2-2] : x +₂ (q₁ * +  , q₂ * + ) ∈ 
              winningSet n {n≢0} (k + q₁ * +  , l + q₂ * + ) d
      [2-2] rewrite sym [2-1] = x₁∈
      x∈ : x ∈ winningSet n {n≢0} (k , l) d
      x∈ = proj₂ (member-winningSet-+-* (k , l) x d q₁ q₂) [2-2]
      [2-3] : f x₁ ≡ f x +₂ (q₁ * +  , q₂ * + )
      [2-3] = subst (λ w → f w ≡ f x +₂ (q₁ * +  , q₂ * + )) 
        (sym [2-1]) (f-+q*8 (proj₁ x) (proj₂ x) q₁ q₂)
      [2-4] : f x +₂ (q₁ * +  , q₂ * + ) ∈ 
              winningSet n {n≢0} (k + q₁ * +  , l + q₂ * + ) d
      [2-4] rewrite sym [2-3] = f[x₁]∈
      f[x]∈ : f x ∈ winningSet n {n≢0} (k , l) d
      f[x]∈ = proj₂ (member-winningSet-+-* (k , l) (f x) d q₁ q₂) [2-4]

  blocksWinningSet-periodic₂ : (d : ℤ × ℤ) → 
    Periodic₂  (BlocksWinningSet pairing d)
  blocksWinningSet-periodic₂ d = 
    proj₂ (periodic₂-periodic₂-+-* ) (blocksWinningSet-periodic₂-+-* d)

  blocksWinningSetsAt-periodic₂ : Periodic₂  (BlocksWinningSetsAt pairing)
  blocksWinningSetsAt-periodic₂ = 
    periodic₂-all  blocksWinningSet-periodic₂ directions