StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>I'll try to answer some of your questions, but I don't think you're apporaching this from the right angle. While you certainly can work with bounded numbers using explicit proofs, you'll most likely be more successful with data type instead.</p> <p>For your <code>makeMove</code> (I've renamed it to <code>move</code> in the rest of the answer), you need a number bounded by the available free squares. That is, when you have 4 free squares, you want to be able to call <code>move</code> only with 0, 1, 2 and 3. There's one very nice way to achieve that.</p> <p>Looking at <a href="http://vituscze.github.io/agda-stdlib-html/Data.Fin.html#775" rel="nofollow"><code>Data.Fin</code></a>, we find this interesting data type:</p> <pre><code>data Fin : ℕ → Set where zero : {n : ℕ} → Fin (suc n) suc : {n : ℕ} (i : Fin n) → Fin (suc n) </code></pre> <p><code>Fin 0</code> is empty (both <code>zero</code> and <code>suc</code> construct <code>Fin n</code> for <code>n</code> greater or equal than 1). <code>Fin 1</code> only has <code>zero</code>, <code>Fin 2</code> has <code>zero</code> and <code>suc zero</code>, and so on. This represents exactly what we need: a number bounded by <code>n</code>. You might have seen this used in the implementation of safe vector lookup:</p> <pre><code>lookup : ∀ {a n} {A : Set a} → Fin n → Vec A n → A lookup zero (x ∷ xs) = x lookup (suc i) (x ∷ xs) = lookup i xs </code></pre> <p>The <code>lookup _ []</code> case is impossible, because <code>Fin 0</code> has no elements!</p> <p>How to apply this nicely to your problem? Firstly, we'll have to track how many empty squares we have. This allows us to prove that <code>gameMaster</code> is indeed a terminating function (the number of empty squares is always decreasing). Let's write a variant of <code>Vec</code> which tracks not only length, but also the empty squares:</p> <pre><code>data Player : Set where x o : Player data SquareVec : (len : ℕ) (empty : ℕ) → Set where [] : SquareVec 0 0 -∷_ : ∀ {l e} → SquareVec l e → SquareVec (suc l) (suc e) _∷_ : ∀ {l e} (p : Player) → SquareVec l e → SquareVec (suc l) e </code></pre> <p>Notice that I got rid of the <code>Square</code> data type; instead, the empty square is baked directly into the <code>-∷_</code> constructor. Instead of <code>- ∷ rest</code> we have <code>-∷ rest</code>.</p> <p>We can now write the <code>move</code> function. What should its type be? Well, it'll take a <code>SquareVec</code> with at least one empty square, a <code>Fin e</code> (where <code>e</code> is the number of empty squares) and a <code>Player</code>. The <code>Fin e</code> guarantees us that this function can always find the appropriate empty square:</p> <pre><code>move : ∀ {l e} → Player → SquareVec l (suc e) → Fin (suc e) → SquareVec l e 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 </code></pre> <p>Notice that this function gives us a <code>SquareVec</code> with exactly one empty square filled. This function couldn't have filled more than one or no empty squares at all!</p> <p>We walk down the vector looking for an empty square; once we find it, the <code>Fin</code> argument tells us whether it's the square we want to fill in. If it's <code>zero</code>, we fill in the player; if it isn't, we continue searching the rest of the vector but with a smaller number.</p> <p>Now, the game representation. Thanks to the extra work we did earlier, we can simplify the <code>Game</code> data type. The <code>move-p</code> constructor just tells us where the move happened and that's it! I got rid of the <code>Player</code> index for simplicity; but it would work just fine with it.</p> <pre><code>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) </code></pre> <p>Oh, what's <code>empty</code>? It's shortcut for your <code>- ∷ - ∷ ...</code>:</p> <pre><code>empty : ∀ {n} → SquareVec n n empty {zero} = [] empty {suc _} = -∷ empty </code></pre> <p>Now, the states. I separated the states into a state of a possibly running game and a state of an ended game. Again, you can use your original <code>GameCondition</code>:</p> <pre><code>data State : Set where win : Player → State draw : State going : State data FinalState : Set where win : Player → FinalState draw : FinalState </code></pre> <p>For the following code, we'll need these imports:</p> <pre><code>open import <a href="http://vituscze.github.io/agda-stdlib-html/Data.Empty.html" rel="nofollow">Data.Empty</a> open import <a href="http://vituscze.github.io/agda-stdlib-html/Data.Product.html" rel="nofollow">Data.Product</a> open import <a href="http://vituscze.github.io/agda-stdlib-html/Relation.Binary.PropositionalEquality.html" rel="nofollow">Relation.Binary.PropositionalEquality</a> </code></pre> <p>And a function to determine the game state. Fill in with your actual implementation; this one just lets players play until the board is completly full.</p> <pre><code>-- Dummy implementation. state : ∀ {e} {gs : SquareVec 9 e} → Game gs → State state {zero} gs = draw state {suc _} gs = going </code></pre> <p>Next, we need to prove that the <code>State</code> cannot be <code>going</code> when there are no empty squares:</p> <pre><code>zero-no-going : ∀ {gs : SquareVec 9 0} (g : Game gs) → state g ≢ going zero-no-going g () </code></pre> <p>Again, this is the proof for the dummy <code>state</code>, the proof for your actual implementation will be very different.</p> <p>Now, we have all the tools we need to implement <code>gameMaster</code>. Firstly, we'll have to decide what its type is. Much like your version, we'll take two functions that represent the <em>AI</em>, one for <code>o</code> and other for <code>x</code>. Then we'll take the game state and produce <code>FinalState</code>. In this version, I'm actually returning the final board so we can see how the game progressed.</p> <p>Now, the AI functions will return just the turn they want to make instead of returning whole new game state. This is easier to work with.</p> <p>Brace yourself, here's the type signature I conjured up:</p> <pre><code>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′) </code></pre> <p>Notice that the AI functions take a game state with at least one empty square and return a move. Now for the implementation.</p> <pre><code>gameMaster sp xm om g with state g ... | win p = win p , _ , _ , g ... | draw = draw , _ , _ , g ... | going = ? </code></pre> <p>So, if the current state is <code>win</code> or <code>draw</code>, we'll return the corresponding <code>FinalState</code> and the current board. Now, we have to deal with the <code>going</code> case. We'll pattern match on <code>e</code> (the number of empty squares) to figure out whether the game is at the end or not:</p> <pre><code>gameMaster {zero} sp xm om g | going = ? gameMaster {suc e} x xm om g | going = ? gameMaster {suc e} o xm om g | going = ? </code></pre> <p>The <code>zero</code> case cannot happen, we proved earlier that <code>state</code> cannot return <code>going</code> when the number of empty squares is zero. How to apply that proof here?</p> <p>We have pattern matched on <code>state g</code> and we now know that <code>state g ≡ going</code>; but sadly Agda already forgot this information. This is what Dominique Devriese was hinting at: the <code>inspect</code> machinery allows us to retain the proof!</p> <p>Instead of pattern matching on just <code>state g</code>, we'll also pattern matching on <code>inspect state g</code>:</p> <pre><code>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 | _ = ? </code></pre> <p><code>pf</code> is now the proof that <code>state g ≡ going</code>, which we can feed to <code>zero-no-going</code>:</p> <pre><code>gameMaster {zero} sp xm om g | going | [ pf ] = ⊥-elim (zero-no-going g pf) </code></pre> <p>The other two cases are easy: we just apply the AI function and recursively apply <code>gameMaster</code> to the result:</p> <pre><code>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) </code></pre> <hr> <p>I wrote some dumb AIs, the first one fills the first available empty square; the second one fills the last one.</p> <pre><code>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 </code></pre> <p>Now, let's match <code>player-lowest</code> against <code>player-lowest</code>! In the Emacs, type <code>C-c C-n gameMaster x player-lowest player-lowest start <RET></code>:</p> <pre><code>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)))))))) </code></pre> <p>We can see that all squares are filled and they alternate between <code>x</code> and <code>o</code>. Matching <code>player-lowest</code> with <code>player-highest</code> gives us:</p> <pre><code>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)))))))) </code></pre> <hr> <p>If you really want to work with the proofs, then I suggest the following representation of <code>Fin</code>:</p> <pre><code>Fin₂ : ℕ → Set Fin₂ n = ∃ λ m → m < n fin⟶fin₂ : ∀ {n} → Fin n → Fin₂ n fin⟶fin₂ zero = zero , s≤s z≤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≤s p) = suc (fin₂⟶fin (_ , p)) </code></pre> <hr> <p>Not strictly related to the question, but <code>inspect</code> uses rather interesting trick which might be worth mentioning. To understand this trick, we'll have to take a look at how <code>with</code> works.</p> <p>When you use <code>with</code> on an expression <code>expr</code>, Agda goes through the types of all arguments and replaces any occurence of <code>expr</code> with a fresh variable, let's call it <code>w</code>. For example:</p> <pre><code>test : (n : ℕ) → Vec ℕ (n + 0) → ℕ test n v = ? </code></pre> <p>Here, the type of <code>v</code> is <code>Vec ℕ (n + 0)</code>, as you would expect.</p> <pre><code>test : (n : ℕ) → Vec ℕ (n + 0) → ℕ test n v with n + 0 ... | w = ? </code></pre> <p>However, once we abstract over <code>n + 0</code>, the type of <code>v</code> suddenly changes to <code>Vec ℕ w</code>. If you later want to use something which contains <code>n + 0</code> in its type, the substitution won't take place again - it's a one time deal.</p> <p>In the <code>gameMaster</code> function, we applied <code>with</code> to <code>state g</code> and pattern matched to find out it's <code>going</code>. By the time we use <code>zero-no-going</code>, <code>state g</code> and <code>going</code> are two separate things which have no relation as far as Agda is concerned.</p> <p>How do we preserve this information? We somehow need to get <code>state g ≡ state g</code> and have the <code>with</code> replace only <code>state g</code> on either side - this would give us the needed <code>state g ≡ going</code>.</p> <p>What the <code>inspect</code> does is that it hides the function application <code>state g</code>. We have to write a function <code>hide</code> in a way that Agda cannot see <code>hide state g</code> and <code>state g</code> are in fact the same thing.</p> <p>One possible way to hide something is to use the fact that for any type <code>A</code>, <code>A</code> and <code>⊤ → A</code> are isomorphic - that is, we can freely go from one representation to the other without losing any information.</p> <p>However, we cannot use the <code>⊤</code> as defined in the standard library. In a moment I'll show why, but for now, we'll define a new type:</p> <pre><code>data Unit : Set where unit : Unit </code></pre> <p>And what it means for a value to be hidden:</p> <pre><code>Hidden : Set → Set Hidden A = Unit → A </code></pre> <p>We can easily <code>reveal</code> the hidden value by applying <code>unit</code> to it:</p> <pre><code>reveal : {A : Set} → Hidden A → A reveal f = f unit </code></pre> <p>The last step we need to take is the <code>hide</code> function:</p> <pre><code>hide : {A : Set} {B : A → Set} → ((x : A) → B x) → ((x : A) → Hidden (B x)) hide f x unit = f x </code></pre> <p>Why wouldn't this work with <code>⊤</code>? If you declare <code>⊤</code> as record, Agda can figure out on its own that <code>tt</code> is the only value. So, when faced with <code>hide f x</code>, Agda won't stop at the third argument (because it already knows how it must look like) and automatically reduce it to <code>λ _ → f x</code>. Data types defined with the <code>data</code> keyword don't have these special rules, so <code>hide f x</code> remains that way until someone <code>reveal</code>s it and the type checker cannot see that there's a <code>f x</code> subexpression inside <code>hide f x</code>.</p> <p>The rest is just arranging stuff so we can get the proof later:</p> <pre><code>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 f x) is (f x) inspect f x = [ refl ] </code></pre> <p>So, there you have it:</p> <pre><code>inspect state g : Reveal (hide state g) is (state g) -- pattern match on (state g) inspect state g : Reveal (hide state g) is going </code></pre> <p>When you then <code>reveal</code> <code>hide state g</code>, you'll get <code>state g</code> and finally the proof that <code>state g ≡ going</code>.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload