# Library problem

# Puzzle: The King's Wine

How many barrels of wine do we have?

A tastingPlan describes which servants should drink which wine
(at one particular instance in time).

Definition tastingPlan (numServants : nat) : Set :=

Fin.t wineBarrels → Fin.t numServants → bool.

Fixpoint sumTrue {n : nat} (map : Fin.t n → bool) : Fin.t (S n)

:= (match n as n´ return n = n´ → Fin.t (S n´) with

| 0 ⇒ fun _ ⇒ Fin.F1

| S n´ ⇒ fun prf ⇒ let map´ := (eq_rect n (fun k ⇒ Fin.t k → bool) map (S n´) prf) in

let acc := sumTrue (fun x : Fin.t n´ ⇒ map´ (Fin.FS x)) in

if map´ Fin.F1

then Fin.FS acc

else Fin.L_R 1 acc

end) eq_refl.

Fin.t wineBarrels → Fin.t numServants → bool.

Fixpoint sumTrue {n : nat} (map : Fin.t n → bool) : Fin.t (S n)

:= (match n as n´ return n = n´ → Fin.t (S n´) with

| 0 ⇒ fun _ ⇒ Fin.F1

| S n´ ⇒ fun prf ⇒ let map´ := (eq_rect n (fun k ⇒ Fin.t k → bool) map (S n´) prf) in

let acc := sumTrue (fun x : Fin.t n´ ⇒ map´ (Fin.FS x)) in

if map´ Fin.F1

then Fin.FS acc

else Fin.L_R 1 acc

end) eq_refl.

A Strategy is an adaptive strategy of distributing wine to the tasters
to determine which barrel is poisoned. If there is no time remaining, then
we must pick a barrel we believe is poisoned. If there is at least one unit
of time remaining, we provide a tastingPlan to describe how to distribute
wine to the servants during this time unit, as well as a method of choosing
our strategy for the remaining time and surviving servants
after this time unit completes depending
on which which set of servants survive that tastingPlan.

Fixpoint Strategy

(servantsRemaining : nat) (timeRemaining : nat) : Set := match timeRemaining with

| 0 ⇒ Fin.t wineBarrels

| S timeRemaining´ ⇒ (tastingPlan servantsRemaining ×

(∀ (survival : Fin.t servantsRemaining → bool),

let servantsRemaining´ := projT1 (Fin.to_nat (sumTrue survival))

in Strategy servantsRemaining´ timeRemaining´))%type

end.

(servantsRemaining : nat) (timeRemaining : nat) : Set := match timeRemaining with

| 0 ⇒ Fin.t wineBarrels

| S timeRemaining´ ⇒ (tastingPlan servantsRemaining ×

(∀ (survival : Fin.t servantsRemaining → bool),

let servantsRemaining´ := projT1 (Fin.to_nat (sumTrue survival))

in Strategy servantsRemaining´ timeRemaining´))%type

end.

A servant survives a given tastingPlan if he doesn't drink the poisoned wine!

Definition tastingPlanSurvival {servantsRemaining : nat}

(plan : tastingPlan servantsRemaining) (poisonedBarrel : Fin.t wineBarrels)

(servant : Fin.t servantsRemaining) : bool := negb (plan poisonedBarrel servant).

(plan : tastingPlan servantsRemaining) (poisonedBarrel : Fin.t wineBarrels)

(servant : Fin.t servantsRemaining) : bool := negb (plan poisonedBarrel servant).

Supposing a particular wine barrel is poisoned, we run a Strategy to see
which wine barrel it will indicate is the poisoned one.

Fixpoint runStrategy {servantsRemaining timeRemaining : nat}

(strat : Strategy servantsRemaining timeRemaining)

(poisonedBarrel : Fin.t wineBarrels) : Fin.t wineBarrels :=

(match timeRemaining as timeRemaining´

return timeRemaining = timeRemaining´ → Fin.t wineBarrels with

| 0 ⇒ fun prf ⇒ eq_rect _ _ strat _ prf

| S time´ ⇒ fun prf ⇒ let (tastePlan, strats´) := eq_rect _ _ strat _ prf

in runStrategy (strats´ (tastingPlanSurvival tastePlan poisonedBarrel)) poisonedBarrel

end) eq_refl.

(strat : Strategy servantsRemaining timeRemaining)

(poisonedBarrel : Fin.t wineBarrels) : Fin.t wineBarrels :=

(match timeRemaining as timeRemaining´

return timeRemaining = timeRemaining´ → Fin.t wineBarrels with

| 0 ⇒ fun prf ⇒ eq_rect _ _ strat _ prf

| S time´ ⇒ fun prf ⇒ let (tastePlan, strats´) := eq_rect _ _ strat _ prf

in runStrategy (strats´ (tastingPlanSurvival tastePlan poisonedBarrel)) poisonedBarrel

end) eq_refl.

The initial number of servants and units of time which we begin with.

A strategy works if it will correctly indicate the poisoned barrel for
every possible poisoned barrel.

Definition strategyWorks (strategy : Strategy numServants time)

:= ∀ (poisonedBarrel : Fin.t wineBarrels),

runStrategy strategy poisonedBarrel = poisonedBarrel.

:= ∀ (poisonedBarrel : Fin.t wineBarrels),

runStrategy strategy poisonedBarrel = poisonedBarrel.

Is it possible to find a Strategy that is guaranteed to discover
the poisoned barrel in time for the party, or is accomplishing this
feat impossible?

Definition GeneralizedPuzzle := {∃ strategy, strategyWorks strategy}

+ {∀ strategy, ¬ strategyWorks strategy}.

End GeneralPuzzle.

+ {∀ strategy, ¬ strategyWorks strategy}.

End GeneralPuzzle.

Now we state the specific parameters of our puzzle. We have 240 wine
barrels, 5 servants, and 2 units of time before the party
(48 hours before the party / 24 hours for poisoning to take effect = 2).

Definition wineBarrels := 240.

Definition numServants := 5.

Definition time := 2.

Definition Puzzle := GeneralizedPuzzle wineBarrels numServants time.

Theorem Solution : Puzzle.

Proof.

Abort.

Definition numServants := 5.

Definition time := 2.

Definition Puzzle := GeneralizedPuzzle wineBarrels numServants time.

Theorem Solution : Puzzle.

Proof.

Abort.

Just a sanity check about the behavior of numTrue.

Proposition sumTrueAll : ∀ (n : nat),

projT1 (Fin.to_nat (@sumTrue n (fun _ ⇒ true))) = n.

Proof.

induction n.

- reflexivity.

- simpl. destruct (Fin.to_nat (sumTrue (fun _ : Fin.t n ⇒ true))) eqn:eqn.

simpl. simpl in IHn. rewrite IHn. reflexivity.

Qed.

projT1 (Fin.to_nat (@sumTrue n (fun _ ⇒ true))) = n.

Proof.

induction n.

- reflexivity.

- simpl. destruct (Fin.to_nat (sumTrue (fun _ : Fin.t n ⇒ true))) eqn:eqn.

simpl. simpl in IHn. rewrite IHn. reflexivity.

Qed.