Theory Monty
section "The Monty Hall Problem"
theory Monty imports "../pGCL" begin
text ‹
We now tackle a more substantial example, allowing us to demonstrate
the tools for compositional reasoning and the use of invariants in
non-recursive programs. Our example is the well-known Monty Hall puzzle
in statistical inference \<^citep>‹"Selvin_75"›.
The setting is a game show: There is a prize hidden behind one
of three doors, and the contestant is invited to choose one. Once
the guess is made, the host than opens one of the remaining two
doors, revealing a goat and showing that the prize is elsewhere. The
contestent is then given the choice of switching their guess to the
other unopened door, or sticking to their first guess.
The puzzle is whether the contestant is better off switching or
staying put; or indeed whether it makes a difference at all. Most people's
intuition suggests that it make no difference, whereas in fact,
switching raises the chance of success from 1/3 to 2/3.
›
subsection ‹The State Space›
text ‹The game state consists of the prize location, the guess,
and the clue (the door the host opens). These are not constrained a
priori to the range @{term "{1::real,2,3}"}, but are simply natural numbers:
We instead show that this is in fact an invariant.
›
record game =
prize :: nat
"guess" :: nat
clue :: nat
text ‹The victory condition: The player wins if they have guessed the
correct door, when the game ends.›
definition player_wins :: "game ⇒ bool"
where "player_wins g ≡ guess g = prize g"
subsubsection ‹Invariants›
text ‹We prove explicitly that only valid doors are ever chosen.›
definition inv_prize :: "game ⇒ bool"
where "inv_prize g ≡ prize g ∈ {1,2,3}"
definition inv_clue :: "game ⇒ bool"
where "inv_clue g ≡ clue g ∈ {1,2,3}"
definition inv_guess :: "game ⇒ bool"
where "inv_guess g ≡ guess g ∈ {1,2,3}"
subsection ‹The Game›
text ‹Hide the prize behind door @{term D}.›
definition hide_behind :: "nat ⇒ game prog"
where "hide_behind D ≡ Apply (prize_update (λx. D))"
text ‹Choose door @{term D}.›
definition guess_behind :: "nat ⇒ game prog"
where "guess_behind D ≡ Apply (guess_update (λx. D))"
text ‹Open door @{term D} and reveal what's behind.›
definition open_door :: "nat ⇒ game prog"
where "open_door D ≡ Apply (clue_update (λx. D))"
text ‹Hide the prize behind door 1, 2 or 3, demonically i.e.~according
to any probability distribution (or none).›
definition hide_prize :: "game prog"
where "hide_prize ≡ hide_behind 1 ⨅ hide_behind 2 ⨅ hide_behind 3"
text ‹Guess uniformly at random.›
definition make_guess :: "game prog"
where "make_guess ≡ guess_behind 1 ⇘(λs. 1/3)⇙⊕
guess_behind 2 ⇘(λs. 1/2)⇙⊕ guess_behind 3"
text ‹Open one of the two doors that \emph{doesn't} hide the prize.›
definition reveal :: "game prog"
where "reveal ≡ ⨅d∈(λs. {1,2,3} - {prize s, guess s}). open_door d"
text ‹Switch your guess to the other unopened door.›
definition switch_guess :: "game prog"
where "switch_guess ≡ ⨅d∈(λs. {1,2,3} - {clue s, guess s}). guess_behind d"
text ‹The complete game, either with or without switching guesses.›
definition monty :: "bool ⇒ game prog"
where
"monty switch ≡ hide_prize ;;
make_guess ;;
reveal ;;
(if switch then switch_guess else Skip)"
subsection ‹A Brute Force Solution›
text ‹For sufficiently simple programs, we can calculate the exact weakest
pre-expectation by unfolding.›
lemma eval_win[simp]:
"p = g ⟹ «player_wins» (s⦇ prize := p, guess := g, clue := c ⦈) = 1"
by(simp add:embed_bool_def player_wins_def)
lemma eval_loss[simp]:
"p ≠ g ⟹ «player_wins» (s⦇ prize := p, guess := g, clue := c ⦈) = 0"
by(simp add:embed_bool_def player_wins_def)
text ‹If they stick to their guns, the player wins with $p=1/3$.›
lemma wp_monty_noswitch:
"(λs. 1/3) = wp (monty False) «player_wins»"
unfolding monty_def hide_prize_def make_guess_def reveal_def
hide_behind_def guess_behind_def open_door_def
switch_guess_def
by(simp add:wp_eval insert_Diff_if o_def)
lemma swap_upd:
"s⦇ prize := p, clue := c, guess := g ⦈ =
s⦇ prize := p, guess := g, clue := c ⦈"
by(simp)
text ‹If they switch, they win with $p=2/3$. Brute force here
takes longer, but is still feasible. On larger programs,
this will rapidly become impossible, as the size of the terms
(generally) grows exponentially with the length of the program.›
lemma wp_monty_switch_bruteforce:
"(λs. 2/3) = wp (monty True) «player_wins»"
unfolding monty_def hide_prize_def make_guess_def reveal_def
hide_behind_def guess_behind_def open_door_def
switch_guess_def
by (simp add: wp_eval insert_Diff_if swap_upd o_def cong del: INF_cong_simp)
subsection ‹A Modular Approach›
text ‹We can solve the problem more efficiently, at the cost of
a little more user effort, by breaking up the problem and annotating
each step of the game separately. While this is not strictly necessary
for this program, it will scale to larger examples, as the work in
annotation only increases linearly with the length of the program.›
subsubsection ‹Healthiness›
text ‹We first establish healthiness for each step. This follows
straightforwardly by applying the supplied rulesets.›
lemma wd_hide_prize:
"well_def hide_prize"
unfolding hide_prize_def hide_behind_def
by(simp add:wd_intros)
lemma wd_make_guess:
"well_def make_guess"
unfolding make_guess_def guess_behind_def
by(simp add:wd_intros)
lemma wd_reveal:
"well_def reveal"
proof -
txt ‹Here, we do need a subsidiary lemma: that there is always
a `fresh' door available. The rest of the healthiness proof follows
as usual.›
have "⋀s. {1, 2, 3} - {prize s, guess s} ≠ {}"
by(auto simp:insert_Diff_if)
thus ?thesis
unfolding reveal_def open_door_def
by(intro wd_intros, auto)
qed
lemma wd_switch_guess:
"well_def switch_guess"
proof -
have "⋀s. {1, 2, 3} - {clue s, guess s} ≠ {}"
by(auto simp:insert_Diff_if)
thus ?thesis
unfolding switch_guess_def guess_behind_def
by(intro wd_intros, auto)
qed
lemmas monty_healthy =
wd_switch_guess wd_reveal wd_make_guess wd_hide_prize
subsubsection ‹Annotations›
text ‹We now annotate each step individually, and then combine them to
produce an annotation for the entire program.›
text ‹@{term hide_prize} chooses a valid door.›
lemma wp_hide_prize:
"(λs. 1) ⊩ wp hide_prize «inv_prize»"
unfolding hide_prize_def hide_behind_def wp_eval o_def
by(simp add:embed_bool_def inv_prize_def)
text ‹Given the prize invariant, @{term make_guess} chooses a valid
door, and guesses incorrectly with probability at least 2/3.›
lemma wp_make_guess:
"(λs. 2/3 * «λg. inv_prize g» s) ⊩
wp make_guess «λg. guess g ≠ prize g ∧ inv_prize g ∧ inv_guess g»"
unfolding make_guess_def guess_behind_def wp_eval o_def
by(auto simp:embed_bool_def inv_prize_def inv_guess_def)
lemma last_one:
assumes "a ≠ b" and "a ∈ {1::nat,2,3}" and "b ∈ {1,2,3}"
shows "∃!c. {1,2,3} - {b,a} = {c}"
apply(simp add:insert_Diff_if)
using assms by(auto intro:assms)
text ‹Given the composed invariants, and an incorrect guess, @{term reveal}
will give a clue that is neither the prize, nor the guess.›
lemma wp_reveal:
"«λg. guess g ≠ prize g ∧ inv_prize g ∧ inv_guess g» ⊩
wp reveal «λg. guess g ≠ prize g ∧
clue g ≠ prize g ∧
clue g ≠ guess g ∧
inv_prize g ∧ inv_guess g ∧ inv_clue g»"
(is "?X ⊩ wp reveal ?Y")
proof(rule use_premise, rule well_def_wp_healthy[OF wd_reveal], clarify)
fix s
assume "guess s ≠ prize s"
and "inv_prize s"
and "inv_guess s"
moreover then obtain c
where singleton: "{Suc 0,2,3} - {prize s, guess s} = {c}"
and "c ≠ prize s"
and "c ≠ guess s"
and "c ∈ {Suc 0,2,3}"
unfolding inv_prize_def inv_guess_def
by(force dest:last_one elim!:ex1E)
ultimately show "1 ≤ wp reveal ?Y s"
by(simp add:reveal_def open_door_def wp_eval singleton o_def
embed_bool_def inv_prize_def inv_guess_def inv_clue_def)
qed
text ‹Showing that the three doors are all district is a largeish
first-order problem, for which sledgehammer gives us a reasonable
script.›
lemma distinct_game:
"⟦ guess g ≠ prize g; clue g ≠ prize g; clue g ≠ guess g;
inv_prize g; inv_guess g; inv_clue g ⟧ ⟹
{1, 2, 3} = {guess g, prize g, clue g}"
unfolding inv_prize_def inv_guess_def inv_clue_def
apply(rule set_eqI)
apply(rule iffI)
apply(clarify)
apply(metis (full_types) empty_iff insert_iff)
apply(metis insert_iff)
done
text ‹Given the invariants, switching from the wrong guess gives
the right one.›
lemma wp_switch_guess:
"«λg. guess g ≠ prize g ∧ clue g ≠ prize g ∧ clue g ≠ guess g ∧
inv_prize g ∧ inv_guess g ∧ inv_clue g» ⊩
wp switch_guess «player_wins»"
proof(rule use_premise, safe)
from wd_switch_guess show "healthy (wp switch_guess)" by(auto)
fix s
assume "guess s ≠ prize s" and "clue s ≠ prize s"
and "clue s ≠ guess s" and "inv_prize s"
and "inv_guess s" and "inv_clue s"
note state = this
hence "1 ≤ Inf ((λa. « player_wins » (s⦇guess := a⦈)) `
({guess s, prize s, clue s} - {clue s, guess s}))"
by(auto simp:insert_Diff_if player_wins_def)
also from state
have "... = Inf ((λa. « player_wins » (s⦇guess := a⦈)) `
({1, 2, 3} - {clue s, guess s}))"
by(simp add:distinct_game[symmetric])
also have "... = wp switch_guess «player_wins» s"
by(simp add:switch_guess_def guess_behind_def wp_eval o_def)
finally show "1 ≤ wp switch_guess « player_wins » s" .
qed
text ‹Given componentwise specifications, we can glue them together
with calculational reasoning to get our result.›
lemma wp_monty_switch_modular:
"(λs. 2/3) ⊩ wp (monty True) «player_wins»"
proof(rule wp_validD)
note wp_validI[OF wp_scale, OF wp_hide_prize, simplified]
also note wp_validI[OF wp_make_guess]
also note wp_validI[OF wp_reveal]
also note wp_validI[OF wp_switch_guess]
finally show "⦃λs. 2/3⦄ monty True ⦃«player_wins»⦄p"
unfolding monty_def
by(simp add:wd_intros sound_intros monty_healthy)
qed
subsubsection ‹Using the VCG›
lemmas scaled_hide = wp_scale[OF wp_hide_prize, simplified]
declare scaled_hide[pwp] wp_make_guess[pwp] wp_reveal[pwp] wp_switch_guess[pwp]
declare wd_hide_prize[wd] wd_make_guess[wd] wd_reveal[wd] wd_switch_guess[wd]
text ‹Alternatively, the VCG will get this using the same annotations.›
lemma wp_monty_switch_vcg:
"(λs. 2/3) ⊩ wp (monty True) «player_wins»"
unfolding monty_def
by(simp, pvcg)
end