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.