Puzzle: The King's Wine

The king is throwing a party in 48 hours and is ready to celebrate with 240 barrels of wine. Unfortunately, he has learned that exactly one of these barrels has been poisoned and does not know which. But the king has 5 wine-tasting servants prepared to die in the king's service to determine which barrel is poisoned. If a servant drinks poisoned wine, he will die anywhere between 0 and 24 hours afterwards.
Is it possible to arrange a plan for the servants to discover which barrel of wine has been poisoned in time for the king's party?
(A warning: the formulation of this problem in Coq is slightly less general and so may provide a small hint in comparison to the presentation above.)

Require Fin.

Section GeneralPuzzle.

How many barrels of wine do we have?
Variable wineBarrels : nat.

A tastingPlan describes which servants should drink which wine (at one particular instance in time).
Definition tastingPlan (numServants : nat) : Set :=
Fin.t wineBarrelsFin.t numServantsbool.

Fixpoint sumTrue {n : nat} (map : Fin.t nbool) : Fin.t (S n)
:= (match n as return n = Fin.t (S ) with
| 0 ⇒ fun _Fin.F1
| S fun prflet map´ := (eq_rect n (fun kFin.t kbool) map (S ) prf) in
let acc := sumTrue (fun x : Fin.t 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 servantsRemainingbool),
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).

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 prfeq_rect _ _ strat _ prf
| S time´fun prflet (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.
Variable numServants : nat.
Variable time : nat.

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.

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.

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.

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 ntrue))) eqn:eqn.
simpl. simpl in IHn. rewrite IHn. reflexivity.
Qed.