Quelle  Monty.thy

(*
 * Copyright (C) 2014 NICTA
 * All rights reserved.
 *)

(* Author: David Cock - David.Cock@nicta.com.au *)

section "The Monty Hall Problem"

theory Monty imports "../pGCL" begin

text ‹
  now tackle a more substantial example, allowing us to demonstrate
  tools for compositional reasoning and the use of invariants in
 -recursive programs. Our example is the well-known Monty Hall puzzle
  statistical inference 🍋‹"Selvin_75"›.

  setting is a game show: There is a prize hidden behind one
  three doors, and the contestant is invited to choose one. Once
  guess is made, the host than opens one of the remaining two
 , revealing a goat and showing that the prize is elsewhere. The
  is then given the choice of switching their guess to the
  unopened door, or sticking to their first guess.

  puzzle is whether the contestant is better off switching or
  put; or indeed whether it makes a difference at all. Most people's
  suggests that it make no difference, whereas in fact,
  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,
  the clue (the door the host opens). These are not constrained a
  to the range @{term "{1::real,2,3}"}, but are simply natural numbers:
  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
  ― ‹Note that this is getting slow›
  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
  calculational reasoning to get our result.›
lemma wp_monty_switch_modular:
  "(λs. 2/3) ⊨!!! wp (monty True) «player_wins¬"
proof(rule wp_validD)  ― ‹Work in probabilistic Hoare triples›
  note wp_validI[OF wp_scale, OF wp_hide_prize, simplified]
    ― ‹Here we apply scaling to match our pre-expectation›
  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