## 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.

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