diff --git a/RiddleProofs/MontyHall.lean b/RiddleProofs/MontyHall.lean index 11d766f..23e3244 100644 --- a/RiddleProofs/MontyHall.lean +++ b/RiddleProofs/MontyHall.lean @@ -1,4 +1 @@ -import RiddleProofs.MontyHall.Statement -import RiddleProofs.MontyHall.Enumeration -import RiddleProofs.MontyHall.Measure -import RiddleProofs.MontyHall.Solution +import RiddleProofs.MontyHall.Basic diff --git a/RiddleProofs/MontyHall/Basic.lean b/RiddleProofs/MontyHall/Basic.lean new file mode 100644 index 0000000..9d199b0 --- /dev/null +++ b/RiddleProofs/MontyHall/Basic.lean @@ -0,0 +1,158 @@ +import Mathlib.Probability.Notation +import Mathlib.MeasureTheory.MeasurableSpace.Basic +import Mathlib.Probability.Distributions.Uniform +import ENNRealArith + +open PMF ProbabilityTheory MeasureTheory + +/-! +# The Monty Hall Problem + +## Statement + +You are a contestant on a game show. You are presented with three closed doors. Behind one door is a car (the prize), and behind the other two are goats. + + ┌───────┐ ┌───────┐ ┌───────┐ + │ Door 1│ │ Door 2│ │ Door 3│ + │ ??? │ │ ??? │ │ ??? │ + └───────┘ └───────┘ └───────┘ + ^ ^ ^ + [Goat/Car] [Goat/Car] [Goat/Car] + +You complete the following steps: +1. You choose one door. +2. The host, who knows where the car is, opens one of the other two doors to reveal a goat. +3. The host asks if you want to switch your choice to the remaining closed door. + +## Question + +Is it to your advantage to switch doors? + +-/ + +inductive Door : Type +| left +| middle +| right +deriving DecidableEq, Repr, Fintype + +instance : Nonempty Door := ⟨Door.left⟩ + +open Door + +structure Game where + car : Door + pick : Door + host : Door + host_not_pick : host ≠ pick + host_not_car : host ≠ car +deriving DecidableEq, Repr, Fintype + +instance : Nonempty Game := ⟨{ + pick := left, host := right, car := middle, + host_not_car := by simp, host_not_pick := by simp +}⟩ + +instance : MeasurableSpace Game := ⊤ + +def host_opens (d : Door) : Set Game := {ω | ω.host = d} +def car_at (d : Door) : Set Game := {ω | ω.car = d} + +@[ext] +theorem Game.ext {g₁ g₂ : Game} (h₁ : g₁.car = g₂.car) (h₂ : g₁.pick = g₂.pick) + (h₃ : g₁.host = g₂.host) : g₁ = g₂ := by + cases g₁; cases g₂; simp at h₁ h₂ h₃; simp [h₁, h₂, h₃] + +noncomputable def Prob : Measure Game := (uniformOfFintype Game).toMeasure + +instance : IsProbabilityMeasure Prob := by unfold Prob; infer_instance + +notation:max "ℙ[" A "]" => Prob A + + +theorem law_of_total_probability {Ω : Type*} [MeasurableSpace Ω] + (μ : Measure Ω) [IsProbabilityMeasure μ] (A B : Set Ω) + {hA : MeasurableSet A} {hB : MeasurableSet B} : + μ A = μ[A | B] * μ B + μ[A | Bᶜ] * μ Bᶜ := by + have h_partition : A = (A ∩ B) ∪ (A ∩ Bᶜ) := by + ext ω + simp only [Set.mem_union, Set.mem_inter_iff, Set.mem_compl_iff] + tauto + have h_disjoint : Disjoint (A ∩ B) (A ∩ Bᶜ) := by + simp only [Set.disjoint_iff_inter_eq_empty] + ext ω + simp only [Set.mem_inter_iff, Set.mem_compl_iff, Set.mem_empty_iff_false] + constructor + · intro ⟨⟨_, hωB⟩, ⟨_, hωBc⟩⟩ + exact hωBc hωB + · intro h + exfalso + exact h + calc μ A + _ = μ (A ∩ B ∪ A ∩ Bᶜ) := by + exact congrArg (⇑μ) h_partition + _ = μ (A ∩ B) + μ (A ∩ Bᶜ) := by + rw [measure_union h_disjoint (MeasurableSet.inter hA hB.compl)] + _ = μ[A | B] * μ B + μ (A ∩ Bᶜ) := by + congr 1 + rw [Set.inter_comm] + rw [← ProbabilityTheory.cond_mul_eq_inter hB A μ] + _ = μ[A | B] * μ B + μ[A | Bᶜ] * μ Bᶜ := by + congr 2 + rw [Set.inter_comm] + rw [← ProbabilityTheory.cond_mul_eq_inter (by exact MeasurableSet.compl_iff.mpr hB) A μ] + + +lemma set_to_finset_conv {P : Game → Prop} [DecidablePred P] : + {ω : Game | P ω} = ↑(Finset.univ.filter P) := by + ext ω; simp + +lemma total_games : Fintype.card Game = 12 := by decide + +lemma car_finset_card {car : Door} : + (Finset.univ.filter (fun ω : Game => ω.car = car)).card = 4 := by + fin_cases car <;> decide + +lemma car_host_card {car host : Door} (hnc : host ≠ car) : + (Finset.univ.filter (fun ω : Game => ω.car = car ∧ ω.host = host)).card = 2 := by + fin_cases host <;> fin_cases car <;> simp at hnc <;> decide + +lemma car_behind_door {car : Door} : Prob (car_at car) = 1/3 := by + unfold Prob car_at + rw [set_to_finset_conv, PMF.toMeasure_apply_finset] + simp only [PMF.uniformOfFintype_apply] + rw [Finset.sum_const, nsmul_eq_mul, car_finset_card, total_games] + norm_num; eq_as_reals + +lemma car_not_behind_door {car : Door} : Prob ((car_at car)ᶜ) = 2/3 := by + rw [measure_compl (by trivial) (measure_ne_top _ _), measure_univ, car_behind_door] + rw [ENNReal.sub_eq_of_eq_add_rev]; norm_num + rw [ENNReal.div_add_div_same]; eq_as_reals + +lemma door_opened_by_host_when_car_equals_pick {pick host : Door} (hnp : host ≠ pick) : + Prob[host_opens host | car_at pick] = 1/2 := by + unfold Prob + rw [cond_apply] + simp only [host_opens, car_at] + have h_inter : {ω : Game | ω.car = pick} ∩ {ω : Game | ω.host = host} = {ω : Game | ω.car = pick ∧ ω.host = host} := by + ext ω; simp + rw [h_inter, set_to_finset_conv, set_to_finset_conv, + PMF.toMeasure_apply_finset, PMF.toMeasure_apply_finset] + simp only [PMF.uniformOfFintype_apply] + rw [Finset.sum_const, Finset.sum_const, + nsmul_eq_mul, nsmul_eq_mul, car_finset_card, car_host_card hnp, total_games] + norm_num; eq_as_reals + +lemma door_opened_by_host_when_car_not_equals_pick {pick host : Door} (hnp : host ≠ pick) : + Prob[host_opens host | (car_at pick)ᶜ] = 1/2 := by + sorry + +theorem monty_hall_stay_probability (pick host : Door) (hnp : host ≠ pick) : + Prob[car_at pick | host_opens host] = 1/3 := by + rw [cond_eq_inv_mul_cond_mul (by trivial) (by trivial)] + nth_rewrite 1 [law_of_total_probability Prob (host_opens host) (car_at pick)] + · rw [door_opened_by_host_when_car_equals_pick hnp, car_behind_door, + door_opened_by_host_when_car_not_equals_pick hnp, car_not_behind_door] + ring_nf; norm_num; eq_as_reals + · trivial + · trivial diff --git a/RiddleProofs/MontyHall/Enumeration.lean b/RiddleProofs/MontyHall/Enumeration.lean deleted file mode 100644 index e528653..0000000 --- a/RiddleProofs/MontyHall/Enumeration.lean +++ /dev/null @@ -1,53 +0,0 @@ -/- -This file takes a computational approach to the Monty Hall problem by enumerating -all possible game scenarios and counting outcomes. --/ - -import RiddleProofs.MontyHall.Statement - - - -open Door - -@[ext] -theorem Game.ext {g₁ g₂ : Game} : g₁.car = g₂.car → g₁.pick = g₂.pick → - g₁.host = g₂.host → g₁ = g₂ := by - intro h₁ h₂ h₃ - cases g₁ with | mk c₁ p₁ h₁ => - cases g₂ with | mk c₂ p₂ h₂ => - simp at h₁ h₂ h₃ - simp [h₁, h₂, h₃] - --- Convert numbers 0,1,2 to doors (left, middle, right) -def fin_to_door (f : Fin 3) : Door := - match f with - | 0 => left - | 1 => middle - | 2 => right - -lemma fin_to_door_injective : Function.Injective fin_to_door := by - intro a b h - fin_cases a <;> fin_cases b <;> simp [fin_to_door] at h <;> rfl - --- All possible triples (car_location, initial_pick, host_choice) --- This gives us 3 × 3 × 3 = 27 different scenarios -def pairs := ({0, 1, 2} ×ˢ {0, 1, 2} ×ˢ {0, 1, 2} : Finset (Fin 3 × Fin 3 × Fin 3) ) - --- Alternative enumeration of Game using pairs. `deriving Fintype` already provides something similar. -def game_enumeration : Finset Game := - pairs.map ⟨(fun x => match x with - | (car_idx, pick_idx, host_idx) => - {car := fin_to_door car_idx, pick := fin_to_door pick_idx, host := fin_to_door host_idx}), - by - intro ⟨a1, a2, a3⟩ ⟨b1, b2, b3⟩ h - simp at h - have h1 : a1 = b1 := fin_to_door_injective h.1 - have h2 : a2 = b2 := fin_to_door_injective h.2.1 - have h3 : a3 = b3 := fin_to_door_injective h.2.2 - simp [h1, h2, h3]⟩ - -theorem equivalence_game_repr : (Finset.univ : Finset Game) = game_enumeration := by - rfl -- Both sides are definitionally equal by construction. - -instance fin_outcome : Finset Game := - Finset.univ diff --git a/RiddleProofs/MontyHall/Measure.lean b/RiddleProofs/MontyHall/Measure.lean deleted file mode 100644 index b7f4d72..0000000 --- a/RiddleProofs/MontyHall/Measure.lean +++ /dev/null @@ -1,49 +0,0 @@ -/- This file constructs the proper probability measure for the Monty Hall problem. -The key insight is that not all 27 possible games are equally likely - we need -to account for the host's strategy and the rules of the game. --/ - -import RiddleProofs.MontyHall.Enumeration -import Mathlib.Probability.ProbabilityMassFunction.Constructions -import ENNRealArith - - - -open MeasureTheory Door ENNRealArith - -instance measurableSpace : MeasurableSpace Game := ⊤ - -instance : DiscreteMeasurableSpace Game := ⟨fun _ => trivial⟩ - --- **The probability density function for games** --- This encodes the rules and probabilities of the Monty Hall problem -noncomputable def game_density (ω : Game) : ENNReal := - if ω.host = ω.pick then 0 -- Invalid: host can't open contestant's door - else if ω.host = ω.car then 0 -- Invalid: host can't reveal the car - else - if ω.car = ω.pick then 1/18 -- Contestant guessed correctly: host has 2 valid choices - else 2/18 -- Contestant guessed wrong: host has 1 valid choice - -theorem density_sum_one : ∑ ω : Game, game_density ω = 1 := by - simp [game_density] - simp [equivalence_game_repr, game_enumeration, pairs] - simp [Finset.sum_product] - simp [fin_to_door] - eq_as_reals - - -lemma prob_density_zero_outside : ∀ a ∉ (Finset.univ : Finset Game), game_density a = 0 := by - intro a ha - exfalso - exact ha (Finset.mem_univ a) - -noncomputable def p : PMF Game := - PMF.ofFinset game_density (Finset.univ : Finset Game) density_sum_one prob_density_zero_outside - -notation:max "ℙ[" A "]" => p.toMeasure A - -noncomputable def Prob := p.toMeasure - -instance : IsProbabilityMeasure Prob := by - unfold Prob - infer_instance diff --git a/RiddleProofs/MontyHall/Solution.lean b/RiddleProofs/MontyHall/Solution.lean deleted file mode 100644 index 7d9d7da..0000000 --- a/RiddleProofs/MontyHall/Solution.lean +++ /dev/null @@ -1,156 +0,0 @@ -import RiddleProofs.MontyHall.Measure -import RiddleProofs.MontyHall.Enumeration -import RiddleProofs.MontyHall.Statement -import ENNRealArith -import Mathlib.Probability.Notation - -open ProbabilityTheory ENNReal Door ENNRealArith - - -def host_opens (d : Door) : Set Game := {ω | ω.host = d} -def car_at (d : Door) : Set Game := {ω | ω.car = d} -def pick_door (d : Door) : Set Game := {ω | ω.pick = d} - - -lemma unique_game_set (car pick host : Door) : - {ω : Game | ω.pick = pick ∧ ω.host = host ∧ ω.car = car} = - {({car := car, pick := pick, host := host} : Game)} := by - ext ω - simp only [Set.mem_setOf_eq, Set.mem_singleton_iff] - constructor - · intro ⟨h1, h2, h3⟩ - exact Game.ext h3 h1 h2 - · intro h - rw [h]; simp - -lemma prob_density_car_eq_pick (car pick host : Door) (h_eq : car = pick) (h_valid : host ≠ pick ∧ host ≠ car) : - game_density {car := car, pick := pick, host := host} = (1 : ENNReal) / 18 := by - simp only [game_density, h_eq, h_valid.1, if_true, if_false] - -lemma prob_density_car_ne_pick (car pick host : Door) (h_ne : car ≠ pick) (h_valid : host ≠ pick ∧ host ≠ car) : - game_density {car := car, pick := pick, host := host} = (1 : ENNReal) / 9 := by - simp only [game_density, h_ne, h_valid.1, h_valid.2, if_false] - eq_as_reals - -lemma prob_density_left_left_right : - game_density {car := left, pick := left, host := right} = 1/18 := by - simp [prob_density_car_eq_pick] - -lemma prob_density_middle_left_right : - game_density {car := middle, pick := left, host := right} = 1/9 := by - simp [prob_density_car_ne_pick] - -lemma prob_density_right_left_right : - game_density {car := right, pick := left, host := right} = 0 := by - simp only [game_density] - -- host = right = car, so the second condition triggers, returning 0 - simp only [if_pos]; rfl - -lemma prob_pick_left_host_right : - ℙ[{ω | ω.pick = left} ∩ {ω | ω.host = right}] = 1/6 := by - have h_inter_eq : ({ω : Game | ω.pick = left} ∩ {ω : Game | ω.host = right}) = - {ω : Game | ω.pick = left ∧ ω.host = right} := by - ext ω; simp [Set.mem_inter_iff] - - calc ℙ[{ω | ω.pick = left} ∩ {ω | ω.host = right}] - = ℙ[{ω : Game | ω.pick = left ∧ ω.host = right}] := by - rw [h_inter_eq] - _ = ℙ[↑(game_enumeration.filter (fun ω => ω.pick = left ∧ ω.host = right))] := by - congr 1; rw [← equivalence_game_repr]; ext ω; simp - _ = ∑ ω ∈ game_enumeration.filter (fun ω => ω.pick = left ∧ ω.host = right), p ω := by - rw [PMF.toMeasure_apply_finset] - _ = ∑ ω ∈ {({car := left, pick := left, host := right} : Game), - ({car := middle, pick := left, host := right} : Game), - ({car := right, pick := left, host := right} : Game)}, p ω := by - apply Finset.sum_congr - · simp [game_enumeration]; decide - · intros; rfl - _ = p {car := left, pick := left, host := right} + - p {car := middle, pick := left, host := right} + - p {car := right, pick := left, host := right} := by - rw [Finset.sum_insert, Finset.sum_insert, Finset.sum_singleton] - · simp [add_assoc] - · simp - · simp - _ = 1/18 + 1/9 + 0 := by - simp only [p, PMF.ofFinset_apply, - prob_density_left_left_right, - prob_density_middle_left_right, - prob_density_right_left_right] - _ = 1/6 := by eq_as_reals - -lemma prob_car_at_given_pick_host (car : Door) : - ℙ[{ω | ω.pick = left} ∩ {ω | ω.host = right} ∩ {ω | ω.car = car}] = - game_density {car := car, pick := left, host := right} := by - calc ℙ[{ω | ω.pick = left} ∩ {ω | ω.host = right} ∩ {ω | ω.car = car}] - = ℙ[{ω : Game | ω.pick = left ∧ ω.host = right ∧ ω.car = car}] := by - congr 1 - ext ω; simp only [Set.mem_inter_iff, Set.mem_setOf_eq] - constructor - · intro ⟨⟨h1, h2⟩, h3⟩; exact ⟨h1, h2, h3⟩ - · intro ⟨h1, h2, h3⟩; exact ⟨⟨h1, h2⟩, h3⟩ - _ = ℙ[{({car := car, pick := left, host := right} : Game)}] := by - congr 1 - exact unique_game_set car left right - _ = p ({car := car, pick := left, host := right} : Game) := by - rw [PMF.toMeasure_apply_singleton] - exact MeasurableSet.singleton _ - _ = game_density {car := car, pick := left, host := right} := by - rfl - -lemma prob_car_left_pick_left_host_right : - ℙ[{ω | ω.pick = left} ∩ {ω | ω.host = right} ∩ {ω | ω.car = left}] = 1/18 := by - rw [prob_car_at_given_pick_host, prob_density_left_left_right] - -lemma prob_car_middle_pick_left_host_right : - ℙ[{ω | ω.pick = left} ∩ {ω | ω.host = right} ∩ {ω | ω.car = middle}] = 1/9 := by - rw [prob_car_at_given_pick_host, prob_density_middle_left_right] - -/- Probability of winning if you stay with your original choice -P(car at left | picked left, host opened right) = 1/3 --/ -theorem monty_hall_stay_probability : - Prob[car_at left | pick_door left ∩ host_opens right] = 1/3 := by - have h_meas : MeasurableSet (pick_door left ∩ host_opens right) := by - apply MeasurableSet.inter <;> exact MeasurableSet.of_discrete - unfold Prob - rw [ProbabilityTheory.cond_apply h_meas] - calc (ℙ[pick_door left ∩ host_opens right])⁻¹ * - ℙ[(pick_door left ∩ host_opens right) ∩ car_at left] - = (ℙ[{ω | ω.pick = left} ∩ {ω | ω.host = right}])⁻¹ * - ℙ[{ω | ω.pick = left} ∩ {ω | ω.host = right} ∩ {ω | ω.car = left}] := by - simp only [car_at, pick_door, host_opens] - _ = (1/6)⁻¹ * (1/18) := by - rw [prob_pick_left_host_right, prob_car_left_pick_left_host_right] - _ = 1/3 := by eq_as_reals - -/-- Probability of winning if you switch to the other door - P(car at middle | picked left, host opened right) = 2/3 -This proves that switching is the better strategy! --/ -theorem monty_hall_switch_probability : - Prob[car_at middle | pick_door left ∩ host_opens right] = 2/3 := by - have h_meas : MeasurableSet (pick_door left ∩ host_opens right) := by - apply MeasurableSet.inter <;> exact MeasurableSet.of_discrete - unfold Prob - rw [ProbabilityTheory.cond_apply h_meas] - calc (ℙ[pick_door left ∩ host_opens right])⁻¹ * - ℙ[(pick_door left ∩ host_opens right) ∩ car_at middle] - = (ℙ[{ω | ω.pick = left} ∩ {ω | ω.host = right}])⁻¹ * - ℙ[{ω | ω.pick = left} ∩ {ω | ω.host = right} ∩ {ω | ω.car = middle}] := by - simp only [car_at, pick_door, host_opens] - _ = (1/6)⁻¹ * (1/9) := by - rw [prob_pick_left_host_right, prob_car_middle_pick_left_host_right] - _ = 2/3 := by eq_as_reals - - -/- - -## Challenges - - -- Derive a statement for the "total probability" law -- Proof the total probability law as a theorem / lemma. -- Replace boilerplate proof code in `Dilemma.lean` by the total probability law. - --/ diff --git a/RiddleProofs/MontyHall/Statement.lean b/RiddleProofs/MontyHall/Statement.lean deleted file mode 100644 index c00d368..0000000 --- a/RiddleProofs/MontyHall/Statement.lean +++ /dev/null @@ -1,57 +0,0 @@ -import Mathlib.Probability.Notation - -/-! -# The Monty Hall Problem - -This file formalizes the Monty Hall problem, a classic probability puzzle. - -## Statement** - -You are a contestant on a game show. You are presented with three closed doors. Behind one door is a car (the prize), and behind the other two are goats. - - ┌───────┐ ┌───────┐ ┌───────┐ - │ Door 1│ │ Door 2│ │ Door 3│ - │ ??? │ │ ??? │ │ ??? │ - └───────┘ └───────┘ └───────┘ - ^ ^ ^ - [Goat/Car] [Goat/Car] [Goat/Car] - -You complete the following steps: -1. You choose one door. -2. The host, who knows where the car is, opens one of the other two doors to reveal a goat. -3. The host asks if you want to switch your choice to the remaining closed door. - -## Question - -Is it to your advantage to switch doors? - --/ - -inductive Door : Type -| left -- Door 1 -| middle -- Door 2 -| right -- Door 3 -deriving DecidableEq, Repr, Fintype - -open Door - -structure Game where - car : Door -- which door has the car behind it - pick : Door -- which door the contestant initially picks - host : Door -- which door the host opens (must have a goat) - deriving DecidableEq, Repr, Fintype - -instance : Nonempty Door := ⟨Door.left⟩ - --- Get the third door (the one that's neither door1 nor door2) -def other_door (door1 door2 : Door) : Door := - if door1 = left ∧ door2 = middle then right - else if door1 = left ∧ door2 = right then middle - else if door1 = middle ∧ door2 = left then right - else if door1 = middle ∧ door2 = right then left - else if door1 = right ∧ door2 = left then middle - else if door1 = right ∧ door2 = middle then left - else left -- fallback case (shouldn't happen in valid games) - -example : other_door left middle = right := by rfl -example : other_door left right = middle := by rfl