I will try to answer some of your questions, but I do not think that you are doing this from the right angle. Although you can certainly work with limited numbers with explicit evidence, you are more likely to be more successful with the data type.
For your makeMove (I renamed it move in the rest of the answer), you need a number limited by the available free squares. That is, when you have 4 free squares, you want to be able to call move only from 0, 1, 2 and 3. There is one very good way to achieve this.
Looking at Data.Fin , we find this interesting data type:
data Fin : β β Set where zero : {n : β} β Fin (suc n) suc : {n : β} (i : Fin n) β Fin (suc n)
Fin 0 empty (both zero and suc the Fin n construct for n greater than or equal to 1). Fin 1 has only zero , Fin 2 has zero and suc zero , etc. This is exactly what we need: a number bounded by n . You may have seen this in the implementation of safe vector searches:
lookup : β {an} {A : Set a} β Fin n β Vec A n β A lookup zero (x β· xs) = x lookup (suc i) (x β· xs) = lookup i xs
The case lookup _ [] not possible because Fin 0 has no elements!
How to apply this to your problem? First, we have to keep track of how many empty squares we have. This allows us to prove that gameMaster indeed the final function (the number of empty squares always decreases). Letβs write a variant of Vec that tracks not only length, but also empty squares:
data Player : Set where xo : Player data SquareVec : (len : β) (empty : β) β Set where [] : SquareVec 0 0 -β·_ : β {le} β SquareVec le β SquareVec (suc l) (suc e) _β·_ : β {le} (p : Player) β SquareVec le β SquareVec (suc l) e
Note that I got rid of the Square data type; instead, an empty square is baked directly in the -β·_ constructor. Instead of - β· rest we have -β· rest .
Now we can write the move function. What should be its type? Well, it will take SquareVec with at least one empty square, a Fin e (where e is the number of empty squares) and a Player . Fin e ensures that this function can always find the desired empty square:
move : β {le} β Player β SquareVec l (suc e) β Fin (suc e) β SquareVec le move p ( -β· sqs) zero = p β· sqs move {e = zero} p ( -β· sqs) (suc ()) move {e = suc e} p ( -β· sqs) (suc fe) = -β· move p sqs fe move p (pβ² β· sqs) fe = pβ² β· move p sqs fe
Note that this function gives us SquareVec with exactly one empty square filled. This function could not fill more than one or even empty squares!
We walk along the vector, looking for an empty square; as soon as we find it, the Fin argument tells us whether it is the square we want to fill. If it is zero , we fill the player; if this is not the case, we continue to search for the rest of the vector, but with a smaller number.
Now a presentation of the game. Thanks to the extra work we did earlier, we can simplify the Game data type. The move-p constructor simply tells us where this move happened and what it is! I just got rid of the Player index for simplicity; but everything will be fine with him.
data Game : β {e} β SquareVec 9 e β Set where start : Game empty move-p : β {e} {gs} p (fe : Fin (suc e)) β Game gs β Game (move p gs fe)
Oh, what is empty ? This is a shortcut for your - β· - β· ... :
empty : β {n} β SquareVec nn empty {zero} = [] empty {suc _} = -β· empty
Now the state. I divided the states into the state of a possible running game and the state of the finished game. Again, you can use your original GameCondition :
data State : Set where win : Player β State draw : State going : State data FinalState : Set where win : Player β FinalState draw : FinalState
For the following code we will need the following imports:
open import Data.Empty open import Data.Product open import Relation.Binary.PropositionalEquality
And the function of determining the state of the game. Fill in your actual implementation; this only allows players to play until the board is completely full.
-- Dummy implementation. state : β {e} {gs : SquareVec 9 e} β Game gs β State state {zero} gs = draw state {suc _} gs = going
Next, we need to prove that State cannot be going when there are no empty squares:
zero-no-going : β {gs : SquareVec 9 0} (g : Game gs) β state g β’ going zero-no-going g ()
Again, this is evidence for the State mannequin, the evidence for your actual implementation will be very different.
Now we have all the tools necessary to implement gameMaster . First, we have to decide what its type is. Like your version, we will take two functions representing the AI, one for o and the other for x . Then we take the state of the game and produce FinalState . In this version, I actually bring the final board back so we can see how the game has progressed.
Now the AI ββfunctions will return only to the turn that they want to make, instead of returning an all new state of the game. Itβs easier to work with.
Pick yourself up, here is the type signature I called:
AI : Set AI = β {e} {sqv : SquareVec 9 (suc e)} β Game sqv β Fin (suc e) gameMaster : β {e} {sqv : SquareVec 9 e} (sp : Player) (x-move o-move : AI) β Game sqv β FinalState Γ (Ξ£[ eβ² β β ] Ξ£[ sqvβ² β SquareVec 9 eβ² ] Game sqvβ²)
Please note that AI functions accept the state of the game with at least one empty square and return movement. Now for the implementation.
gameMaster sp xm om g with state g ... | win p = win p , _ , _ , g ... | draw = draw , _ , _ , g ... | going = ?
So, if the current state is win or draw , we will return the corresponding FinalState and current board. Now we have to deal with the going case. We will match the match on e (the number of empty squares) to find out if the game is at the end or not:
gameMaster {zero} sp xm om g | going = ? gameMaster {suc e} x xm om g | going = ? gameMaster {suc e} o xm om g | going = ?
The case of zero cannot happen, we previously proved that State cannot return going when the number of empty squares is zero. How to apply this proof here?
We have a pattern matching state g , and now we know that state g β‘ going ; but, unfortunately, Agda has already forgotten this information. This is what Dominic Devries hinted at: the inspect mechanism allows us to keep the evidence!
Instead of matching patterns to only state g we will also match patterns to inspect state g :
gameMaster sp xm om g with state g | inspect state g ... | win p | _ = win p , _ , _ , g ... | draw | _ = draw , _ , _ , g gameMaster {zero} sp xm om g | going | [ pf ] = ? gameMaster {suc e} x xm om g | going | _ = ? gameMaster {suc e} o xm om g | going | _ = ?
pf now proof that state g β‘ going , which we can pass up to zero-no-going :
gameMaster {zero} sp xm om g | going | [ pf ] = β₯-elim (zero-no-going g pf)
The other two cases are simple: we just apply the AI ββfunction and recursively apply gameMaster to the result:
gameMaster {suc e} x xm om g | going | _ = gameMaster o xm om (move-p x (xm g) g) gameMaster {suc e} o xm om g | going | _ = gameMaster x xm om (move-p o (om g) g)
I wrote some dumb AIs, the first fills the first available empty square; the second fills the last.
player-lowest : AI player-lowest _ = zero max : β {e} β Fin (suc e) max {zero} = zero max {suc e} = suc max player-highest : AI player-highest _ = max
Now match player-lowest with player-lowest ! In Emacs, enter Cc Cn gameMaster x player-lowest player-lowest start <RET> :
draw , 0 , x β· (o β· (x β· (o β· (x β· (o β· (x β· (o β· (x β· [])))))))) , move-p x zero (move-p o zero (move-p x zero (move-p o zero (move-p x zero (move-p o zero (move-p x zero (move-p o zero (move-p x zero start))))))))
We see that all the squares are filled, and they alternate between x and o . Matching player-lowest with player-highest gives us:
draw , 0 , x β· (x β· (x β· (x β· (x β· (o β· (o β· (o β· (o β· [])))))))) , move-p x zero (move-p o (suc zero) (move-p x zero (move-p o (suc (suc (suc zero))) (move-p x zero (move-p o (suc (suc (suc (suc (suc zero))))) (move-p x zero (move-p o (suc (suc (suc (suc (suc (suc (suc zero))))))) (move-p x zero start))))))))
If you really want to work with evidence, I suggest the following Fin view:
Finβ : β β Set Finβ n = β Ξ» m β m < n finβΆfinβ : β {n} β Fin n β Finβ n finβΆfinβ zero = zero , sβ€szβ€n finβΆfinβ (suc n) = map suc sβ€s (finβΆfinβ n) finββΆfin : β {n} β Finβ n β Fin n finββΆfin {zero} (_ , ()) finββΆfin {suc _} (zero , _) = zero finββΆfin {suc _} (suc _ , sβ€sp) = suc (finββΆfin (_ , p))
Not strictly related to the question, but inspect uses a rather interesting trick worth mentioning. To understand this trick, we need to see how with works.
When you use with in an expr expression, Agda looks at the types of all arguments and replaces any appearance of expr fresh variable, let it call it w . For instance:
test : (n : β) β Vec β (n + 0) β β test nv = ?
Here the type v is equal to Vec β (n + 0) , as one would expect.
test : (n : β) β Vec β (n + 0) β β test nv with n + 0 ... | w = ?
However, as soon as we abstract over n + 0 , the type v suddenly changes to Vec β w . If you later want to use something that contains n + 0 in its type, the replacement will not be performed again - this is a one-time deal.
In the gameMaster function gameMaster we applied with to state g and matched the template to see if it was going . By the time we use zero-no-going , state g and going are two separate things that are not related to Agda.
How to save this information? We somehow need to get state g β‘ state g and replace with only state g on both sides - this will give us the necessary state g β‘ going .
What inspect does is that it hides the state g application application. We must write the hide function in such a way that Agda cannot see hide state g and state g is actually the same thing.
One of the possible ways to hide something is to use the fact that for any type A , A and β€ β A are isomorphic, that is, we can freely move from one representation to another without losing any information.
However, we cannot use β€ as defined in the standard library. At some point I will show why, but for now we will define a new type:
data Unit : Set where unit : Unit
And what this means is that the value will be hidden:
Hidden : Set β Set Hidden A = Unit β A
We can easily hide the reveal value by applying unit to it:
reveal : {A : Set} β Hidden A β A reveal f = f unit
The last step we need to complete is the hide function:
hide : {A : Set} {B : A β Set} β ((x : A) β B x) β ((x : A) β Hidden (B x)) hide fx unit = fx
Why does this not work with β€ ? If you declare β€ as a record, Agda can independently determine that tt is the only value. Therefore, faced with hide fx , Agda will not stop at the third argument (because he already knows how it should look) and will automatically reduce it to Ξ» _ β fx . Data types defined using the data keyword do not have these special rules, so hide fx stays that way until someone reveal and can see that there is a subexpression fx inside hide fx fx .
The rest simply organizes the material so that we can get the proof later:
data Reveal_is_ {A : Set} (x : Hidden A) (y : A) : Set where [_] : (eq : reveal x β‘ y) β Reveal x is y inspect : {A : Set} {B : A β Set} (f : (x : A) β B x) (x : A) β Reveal (hide fx) is (fx) inspect fx = [ refl ]
So you have this:
inspect state g : Reveal (hide state g) is (state g) -- pattern match on (state g) inspect state g : Reveal (hide state g) is going
When you then reveal hide state g , you get state g and, finally, proof that state g β‘ going .