Logic Puzzles in Agda

This post assumes basic knowledge of Agda.

A few days ago, Paul Snively published a post which set me thinking on how Agda (which is the closest thing to Coq I have some knowledge of) fares in similar scenarios. Pretty well, it turns out.

I’ll start by solving the problem Paul solves in his post, which is also the first problem in the book Logical Labyrinths by Raymond M. Smullyan:

Context: Abercrombie is in a weird island where all knaves lie and all knights are truthful

On the day of his arrival, Abercrombie came across three inhabitants, whom we will call A, B and C. He asked A: “Are you a knight or a knave?” A answered, but so indistinctly that Abercrombie could not understand what he said. He then asked B: “What did he say?” B replied: “He said that he is a knave.” At this point, C piped up and said: “Don’t believe that; it’s a lie!”. Was C a knight or a knave?

We begin by defining (equality) and (a type with no values):

data _≡_ {A : Set} (a : A) : A → Set where
  refl : a ≡ a

data ⊥ : Set where

Now a Person can either be a knight or knave. We model that

data Person : Set where
  knight : Person
  knave : Person

and the fact that a knight always speaks the truth and that a knave always lies

says : Person → Set → Set
says knight p = p
says knave p = p → ⊥

The intuition behind says is that says p predicate always gives us a a predicate that is true. This is actually enough to represent and solve the first problem — we represent the problem as a type such that a value of that type is the solution we need:

data Solution₀ : Set where
  soln₀ : (a : Person) → (b : Person) → (c : Person) →
          (says b (says a (a ≡ knave))) → (says c (b ≡ knave)) →
          Solution₀

We encode the constraints in the problem here in a very straightforward way; it is possible to construct a value of type Solution₀ if and only if we have proofs for (says b (says a (a ≡ knave))) and (says c (b ≡ knave)). We now ask Agda to search for a solution:

solution₀ : Solution₀
solution₀ = ?

and Agda fills up the ?:

solution₀ = soln₀ knight knave knight (λ ()) refl

As cool as this undoubtedly is, for this particular problem the solution is the proof of the solution and that isn’t as involved as I’d like to be. Let’s look at something deeper (problem 1.11 from the same book).

Suppose that you visit the Island of Knights and Knaves because you have heard a rumor that there is gold buried there. You meet a native and you wish to find out from him whether there really is gold there, but you don’t know whether he is a knight or a knave. You are allowed to ask him only one question answerable by yes or no. What question would you ask?

The answer, of course, is to ask “if I were to ask you whether there is gold buried somewhere here, what would you say?”. The knights answer truthfully and the knaves end up answering truthfully since they lie about a lie and hence negate a negation. Is Agda smart enough to figure this out?

A question to which only two answers are possible is basically a predicate and can be represented by a Set. However, since we’d like to be able to ask questions containing the phrase “you” or even questions like “if you are a knight then is the sky red else are you a knave?”, we represent questions as

Prp : Set₁
Prp = Person → Set

We also declare some standard ammo

record _∧_ (A : Set) (B : Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B

prj₁ : {A : Set} {B : Set} → A ∧ B → A
prj₁ = _∧_.proj₁
prj₂ : {A : Set} {B : Set} → A ∧ B → B
prj₂ = _∧_.proj₂


_⇔_ : Set → Set → Set
_⇔_ a b = (a → b) ∧ (b → a)

to represent logical conjunctions, and if and only if. With these, we are ready to represent our problem. We represent a slightly more general version of the problem — “is gold buried in your island” is really an arbitrary predicate and we model it as such

data PredicateTransform : Set₁ where
  predicateTrans : (f : Prp → Prp) →
                   ((OldP : Prp) → (p : Person) →
                    (OldP p) ⇔ (says p ((f OldP) p))) →
                   PredicateTransform

The way to construct a PredicateTransform value is by providing a function that maps a predicate to a new one, and proving that the old predicate is equivalent to an arbitrary Person asserting the new one. So, in the specific case of the question, the predicate would hopefully transform “is gold buried in your island” to a knight/knave-hood agnostic one and provide a proof for the same. We try our old trick again

soln : PredicateTransform
soln = ?

which unfortunately doesn’t work this time. The reason why it doesn’t is fundamental — remember how, for knaves, our solution would work by eliminating double negation? You can’t do that in constructive logic (and hence Agda). But all is not lost, we have the mighty ? to the rescue:

elim-double-neg : {A : Set} → ((A → ⊥) → ⊥) → A
elim-double-neg = ?

We can’t provide a body for elim-double-neg but that doesn’t stop us from keeping it around and using it to prove things. We just won’t get a complete proof, since such a proof lies outside the realm of constructive logic.

The “solution” we came up with basically transforms predicate “P” to “Would you assert the truth of predicate P”? Succinctly,

soln₁ : PredicateTransform
soln₁ = predicateTrans f ?
  where f : Prp → Prp
        f q p = says p (q p)

where ? is something we have to (interactively) fill in. We proceed the usual, high-school, way — proving both the implications separately and put them together to prove the iff:

soln₁ : PredicateTransform
soln₁ = predicateTrans f proof
  where f : Prp → Prp
        f q p = says p (q p)
        proof₀ : (A : Prp) → (p : Person) → (A p) → (says p ((f A) p))
        proof₀ = ?
        proof₁ : (A : Prp) → (p : Person) → (says p ((f A) p)) → (A p)
        proof₁ = ?
        proof : (A : Prp) → (p : Person) → (A p) ⇔ (says p ((f A) p))
        proof A p = proof₀ A p , proof₁ A p

Note that a person can either be a knight or a knave. We tell Agda this and ask it to search for the individual proof terms:

proof₀ : (A : Prp) → (p : Person) → (A p) → (says p ((f A) p))
proof₀ A knight prf = prf
proof₀ A knave prf = λ z → z prf
proof₁ : (A : Prp) → (p : Person) → (says p ((f A) p)) → (A p)
proof₁ A knight prf = prf
proof₁ A knave prf = ?

The only place Agda gets stuck is the place where it would have to use elim-double-neg. The type of prf here is (A knave → ⊥) → ⊥ (in emacs hit C-c C-d) and the type of the hole is A knave. We can use double-neg-elim here

proof₁ A knave prf = elim-double-neg prf

and we’re done!

Another interesting solution to the problem is transforming the predicate “P” to “Is P true iff you are a knight?”:

soln₂ : PredicateTransform
soln₂ = predicateTrans f ?
  where f : Prp → Prp
        f q p = (p ≡ knight) ⇔ (q p)

I leave this as an exercise. 🙂

The full source (and the solution to the “exercise”) is here. If you’ve made it this far please do leave a comment, especially if you think I’m mistaken somewhere.

Advertisements
This entry was posted in Computers and tagged , , , . Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s