From 63b1a4e96afd6f1570a74da05dcea6267abfcc6b Mon Sep 17 00:00:00 2001 From: Willem Vanhulle Date: Fri, 25 Jul 2025 23:13:11 +0200 Subject: [PATCH 1/2] Fix errors --- RiddleProofs/MontyHall.lean | 5 +- RiddleProofs/MontyHall/Basic.lean | 307 ++++++++++++++++++++++++ RiddleProofs/MontyHall/Enumeration.lean | 53 ---- RiddleProofs/MontyHall/Measure.lean | 49 ---- RiddleProofs/MontyHall/Solution.lean | 156 ------------ RiddleProofs/MontyHall/Statement.lean | 57 ----- 6 files changed, 308 insertions(+), 319 deletions(-) create mode 100644 RiddleProofs/MontyHall/Basic.lean delete mode 100644 RiddleProofs/MontyHall/Enumeration.lean delete mode 100644 RiddleProofs/MontyHall/Measure.lean delete mode 100644 RiddleProofs/MontyHall/Solution.lean delete mode 100644 RiddleProofs/MontyHall/Statement.lean 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..60133df --- /dev/null +++ b/RiddleProofs/MontyHall/Basic.lean @@ -0,0 +1,307 @@ +import Mathlib.Probability.Notation +import Mathlib.MeasureTheory.MeasurableSpace.Basic +import Mathlib.Probability.Distributions.Uniform +import ENNRealArith +open PMF +/-! +# 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 -- Door 1 +| middle -- Door 2 +| right -- Door 3 +deriving DecidableEq, Repr, Fintype + +instance : Nonempty Door := ⟨Door.left⟩ + +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) + host_not_pick: host ≠ pick + host_not_car: host ≠ car + deriving DecidableEq, Repr, Fintype + +open Door ProbabilityTheory MeasureTheory + + +instance measurableSpace : MeasurableSpace Game := ⊤ + + + +/-- The set of games where the host opens door d -/ +def host_opens (d : Door) : Set Game := {ω | ω.host = d} + +/-- The set of games where the car is behind door d -/ +def car_at (d : Door) : Set Game := {ω | ω.car = d} + +/-- The set of games where the player picks door d -/ +def pick_door (d : Door) : Set Game := {ω | ω.pick = d} + + + + +@[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 + +def game_triples := ({0, 1, 2} ×ˢ {0, 1, 2} ×ˢ {0, 1, 2} : Finset (Fin 3 × Fin 3 × Fin 3) ) + +def game_enumeration : Finset Game := + (Finset.univ : Finset Game) + +theorem equivalence_game_repr : (Finset.univ : Finset Game) = game_enumeration := by + rfl + + + +def door_tuples := ({0, 1, 2} ×ˢ {0, 1, 2} : Finset (Fin 3 × Fin 3) ) + +def door_enumeration: Finset (Door × Door) := + door_tuples.map ⟨ (fun x => match x with + | (door_1, door_2) => (fin_to_door door_1, fin_to_door door_2)), by + unfold Function.Injective + intros a b h + simp at h + refine Prod.ext_iff.mpr ?_ + constructor + . exact fin_to_door_injective h.1 + . exact fin_to_door_injective h.2 ⟩ + +lemma equivalence_door_repr: (Finset.univ : Finset (Door × Door)) = door_enumeration := by rfl + +instance: Nonempty Game := + ⟨ {pick := left, host := right, car := middle, host_not_car := (by simp), host_not_pick := (by simp)} ⟩ + +noncomputable def p := + PMF.uniformOfFintype Game + +notation:max "ℙ[" A "]" => p.toMeasure A + +noncomputable def Prob := p.toMeasure + +instance : IsProbabilityMeasure Prob := by + unfold Prob + infer_instance + + +/-- Apply a permutation of doors to a game -/ +def permute_game (σ : Equiv.Perm Door) (g : Game) : Game where + car := σ g.car + pick := σ g.pick + host := σ g.host + host_not_pick := σ.injective.ne g.host_not_pick + host_not_car := σ.injective.ne g.host_not_car + +/-- Two games are equivalent if one can be obtained from the other by a door permutation -/ +def GameEquiv : Game → Game → Prop := + fun g₁ g₂ => ∃ σ : Equiv.Perm Door, permute_game σ g₁ = g₂ + + +open Equiv + +instance: Equivalence GameEquiv where + refl g := ⟨1, by ext <;> simp [permute_game]⟩ + symm {g₁ g₂} := fun ⟨σ, h⟩ => ⟨σ⁻¹, by + rw [← h] + ext <;> simp [permute_game]⟩ + trans {g₁ g₂ g₃} := fun ⟨σ₁, h₁⟩ ⟨σ₂, h₂⟩ => ⟨σ₂ * σ₁, by + rw [← h₂, ← h₁] + ext <;> simp [permute_game, Perm.mul_apply]⟩ + + + +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 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 + +-- Count games where host opens a specific door AND car is at a specific position +lemma host_car_finset_card { host car: Door} (hnc: host ≠ car) : + (Finset.univ.filter (fun (ω : Game) => ω.host = host ∧ ω.car = car)).card = 2 := by + fin_cases host <;> fin_cases car <;> simp at hnc <;> decide + +-- General conversion lemma for sets to finsets +lemma set_to_finset_conv {P : Game → Prop} [DecidablePred P] : + {(ω : Game) | P ω} = ↑(Finset.univ.filter P) := by + ext ω + simp [Finset.mem_univ] + +lemma car_set_to_finset { car: Door} : {(ω : Game) | ω.car = car} = ↑(Finset.univ.filter (fun (ω : Game) => ω.car = car)) := by + exact set_to_finset_conv + +lemma host_car_set_to_finset { host car: Door} : + {(ω : Game) | ω.host = host ∧ ω.car = car} = ↑(Finset.univ.filter (fun (ω : Game) => ω.host = host ∧ ω.car = car)) := by + exact set_to_finset_conv + + +lemma car_host_set_to_finset { car host: Door} : + {(ω : Game) | ω.car = car ∧ ω.host = host} = ↑(Finset.univ.filter (fun (ω : Game) => ω.car = car ∧ ω.host = host)) := by + exact set_to_finset_conv + +-- Conversion lemma for pick, host and car triple +lemma pick_host_car_set_to_finset { pick host car: Door} : + {(ω : Game) | ω.car = car ∧ ω.host = host ∧ ω.pick = pick} = ↑(Finset.univ.filter (fun (ω : Game) => ω.car = car ∧ ω.host = host ∧ ω.pick = pick)) := by + exact set_to_finset_conv + + + +lemma car_behind_door { car: Door}: Prob (car_at car) = 1 / 3 := by + unfold Prob p car_at + rw [car_set_to_finset] + rw [PMF.toMeasure_apply_finset] + simp only [PMF.uniformOfFintype_apply] + rw [Finset.sum_const, nsmul_eq_mul] + rw [car_finset_card] + rw [total_games] + norm_num + eq_as_reals + +lemma host_car_card { host car: Door} (hnc: host ≠ car) : (Finset.univ.filter (fun (ω : Game) => ω.host = host ∧ ω.car = car)).card = 2 := by + fin_cases host <;> fin_cases car <;> simp at hnc <;> decide + +-- Same lemma but with reversed conjunction order +lemma car_host_card { car host: Door} (hnc: host ≠ car) : (Finset.univ.filter (fun (ω : Game) => ω.car = car ∧ ω.host = host)).card = 2 := by + have h : (Finset.univ.filter (fun (ω : Game) => ω.car = car ∧ ω.host = host)) = + (Finset.univ.filter (fun (ω : Game) => ω.host = host ∧ ω.car = car)) := by + ext ω + simp [and_comm] + rw [h] + exact host_car_card hnc + + +-- When car = pick, the host cannot open that door, so this probability is 0 +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 p + rw [cond_apply] + simp only [host_opens, car_at] + -- Convert intersection to conjunction + have h_inter : {(ω : Game) | ω.car = pick} ∩ {(ω : Game) | ω.host = host} = + {(ω : Game) | ω.car = pick ∧ ω.host = host} := by + ext ω + simp [Set.mem_inter_iff] + rw [h_inter] + -- Convert to finsets + have h_conv1 : {(ω : Game) | ω.car = pick} = ↑(Finset.univ.filter (fun (ω : Game) => ω.car = pick)) := by + exact set_to_finset_conv + have h_conv2 : {(ω : Game) | ω.car = pick ∧ ω.host = host} = + ↑(Finset.univ.filter (fun (ω : Game) => ω.car = pick ∧ ω.host = host)) := by + exact set_to_finset_conv + rw [h_conv1, h_conv2] + rw [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] + -- Count cardinalities + have h_pick_card : (Finset.univ.filter (fun (ω : Game) => ω.car = pick)).card = 4 := by + exact car_finset_card + have h_pick_host_card : (Finset.univ.filter (fun (ω : Game) => ω.car = pick ∧ ω.host = host)).card = 2 := by + -- When car = pick, host ≠ pick, there are 2 games (one for each possible player pick) + exact car_host_card hnp + rw [h_pick_card, h_pick_host_card, total_games] + -- Now we have: (4 * 12⁻¹)⁻¹ * (2 * 12⁻¹) = 1/2 + 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 + unfold Prob p + rw [cond_apply] + · simp only [host_opens] + sorry + · trivial + +lemma car_not_behind_door {car: Door} : Prob ((car_at car)ᶜ) = 2/3 := by + -- Use that Prob(car_at car) = 1/3 and Prob(Aᶜ) = 1 - Prob(A) + have h_car : Prob (car_at car) = 1/3 := car_behind_door + rw [measure_compl (by trivial) (by exact measure_ne_top Prob _)] + rw [measure_univ, h_car] + rw [ENNReal.sub_eq_of_eq_add_rev] + norm_num + rw [ENNReal.div_add_div_same] + eq_as_reals + +theorem monty_hall_stay_probability (pick host : Door) (hnp: host ≠ pick) : Prob[car_at pick | host_opens host] = 1/3 := by + rw [ProbabilityTheory.cond_eq_inv_mul_cond_mul (by exact trivial) (by exact trivial)] + nth_rewrite 1 [law_of_total_probability Prob (host_opens host) (car_at pick)] + · rw [@door_opened_by_host_when_car_equals_pick pick host hnp, car_behind_door, + @door_opened_by_host_when_car_not_equals_pick pick host hnp, car_not_behind_door] + have: ((1/2) * (1/3) + (1/2) * (2/3))⁻¹ * (1/2) * (1/3) = 1/(3: ENNReal) := by + ring_nf + norm_num + eq_as_reals + rw [this] + . 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 From f1e612fe6c1bdea8cf30d43d97d7172a99092227 Mon Sep 17 00:00:00 2001 From: Willem Vanhulle Date: Fri, 25 Jul 2025 23:21:48 +0200 Subject: [PATCH 2/2] Make more compact --- RiddleProofs/MontyHall/Basic.lean | 279 +++++++----------------------- 1 file changed, 65 insertions(+), 214 deletions(-) diff --git a/RiddleProofs/MontyHall/Basic.lean b/RiddleProofs/MontyHall/Basic.lean index 60133df..9d199b0 100644 --- a/RiddleProofs/MontyHall/Basic.lean +++ b/RiddleProofs/MontyHall/Basic.lean @@ -2,11 +2,13 @@ import Mathlib.Probability.Notation import Mathlib.MeasureTheory.MeasurableSpace.Basic import Mathlib.Probability.Distributions.Uniform import ENNRealArith -open PMF + +open PMF ProbabilityTheory MeasureTheory + /-! # The Monty Hall Problem -## Statement** +## 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. @@ -29,124 +31,43 @@ Is it to your advantage to switch doors? -/ inductive Door : Type -| left -- Door 1 -| middle -- Door 2 -| right -- Door 3 +| left +| middle +| right deriving DecidableEq, Repr, Fintype instance : Nonempty Door := ⟨Door.left⟩ -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) - host_not_pick: host ≠ pick - host_not_car: host ≠ car - deriving DecidableEq, Repr, Fintype - -open Door ProbabilityTheory MeasureTheory +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 measurableSpace : MeasurableSpace Game := ⊤ - +instance : Nonempty Game := ⟨{ + pick := left, host := right, car := middle, + host_not_car := by simp, host_not_pick := by simp +}⟩ +instance : MeasurableSpace Game := ⊤ -/-- The set of games where the host opens door d -/ def host_opens (d : Door) : Set Game := {ω | ω.host = d} - -/-- The set of games where the car is behind door d -/ def car_at (d : Door) : Set Game := {ω | ω.car = d} -/-- The set of games where the player picks door d -/ -def pick_door (d : Door) : Set Game := {ω | ω.pick = d} - - - - @[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 - -def game_triples := ({0, 1, 2} ×ˢ {0, 1, 2} ×ˢ {0, 1, 2} : Finset (Fin 3 × Fin 3 × Fin 3) ) - -def game_enumeration : Finset Game := - (Finset.univ : Finset Game) - -theorem equivalence_game_repr : (Finset.univ : Finset Game) = game_enumeration := by - rfl - - - -def door_tuples := ({0, 1, 2} ×ˢ {0, 1, 2} : Finset (Fin 3 × Fin 3) ) - -def door_enumeration: Finset (Door × Door) := - door_tuples.map ⟨ (fun x => match x with - | (door_1, door_2) => (fin_to_door door_1, fin_to_door door_2)), by - unfold Function.Injective - intros a b h - simp at h - refine Prod.ext_iff.mpr ?_ - constructor - . exact fin_to_door_injective h.1 - . exact fin_to_door_injective h.2 ⟩ - -lemma equivalence_door_repr: (Finset.univ : Finset (Door × Door)) = door_enumeration := by rfl - -instance: Nonempty Game := - ⟨ {pick := left, host := right, car := middle, host_not_car := (by simp), host_not_pick := (by simp)} ⟩ - -noncomputable def p := - PMF.uniformOfFintype Game - -notation:max "ℙ[" A "]" => p.toMeasure A - -noncomputable def Prob := p.toMeasure +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₃] -instance : IsProbabilityMeasure Prob := by - unfold Prob - infer_instance - - -/-- Apply a permutation of doors to a game -/ -def permute_game (σ : Equiv.Perm Door) (g : Game) : Game where - car := σ g.car - pick := σ g.pick - host := σ g.host - host_not_pick := σ.injective.ne g.host_not_pick - host_not_car := σ.injective.ne g.host_not_car - -/-- Two games are equivalent if one can be obtained from the other by a door permutation -/ -def GameEquiv : Game → Game → Prop := - fun g₁ g₂ => ∃ σ : Equiv.Perm Door, permute_game σ g₁ = g₂ +noncomputable def Prob : Measure Game := (uniformOfFintype Game).toMeasure +instance : IsProbabilityMeasure Prob := by unfold Prob; infer_instance -open Equiv - -instance: Equivalence GameEquiv where - refl g := ⟨1, by ext <;> simp [permute_game]⟩ - symm {g₁ g₂} := fun ⟨σ, h⟩ => ⟨σ⁻¹, by - rw [← h] - ext <;> simp [permute_game]⟩ - trans {g₁ g₂ g₃} := fun ⟨σ₁, h₁⟩ ⟨σ₂, h₂⟩ => ⟨σ₂ * σ₁, by - rw [← h₂, ← h₁] - ext <;> simp [permute_game, Perm.mul_apply]⟩ - +notation:max "ℙ[" A "]" => Prob A theorem law_of_total_probability {Ω : Type*} [MeasurableSpace Ω] @@ -182,126 +103,56 @@ theorem law_of_total_probability {Ω : Type*} [MeasurableSpace Ω] rw [← ProbabilityTheory.cond_mul_eq_inter (by exact MeasurableSet.compl_iff.mpr hB) A μ] -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 - --- Count games where host opens a specific door AND car is at a specific position -lemma host_car_finset_card { host car: Door} (hnc: host ≠ car) : - (Finset.univ.filter (fun (ω : Game) => ω.host = host ∧ ω.car = car)).card = 2 := by - fin_cases host <;> fin_cases car <;> simp at hnc <;> decide - --- General conversion lemma for sets to finsets lemma set_to_finset_conv {P : Game → Prop} [DecidablePred P] : - {(ω : Game) | P ω} = ↑(Finset.univ.filter P) := by - ext ω - simp [Finset.mem_univ] - -lemma car_set_to_finset { car: Door} : {(ω : Game) | ω.car = car} = ↑(Finset.univ.filter (fun (ω : Game) => ω.car = car)) := by - exact set_to_finset_conv - -lemma host_car_set_to_finset { host car: Door} : - {(ω : Game) | ω.host = host ∧ ω.car = car} = ↑(Finset.univ.filter (fun (ω : Game) => ω.host = host ∧ ω.car = car)) := by - exact set_to_finset_conv + {ω : Game | P ω} = ↑(Finset.univ.filter P) := by + ext ω; simp +lemma total_games : Fintype.card Game = 12 := by decide -lemma car_host_set_to_finset { car host: Door} : - {(ω : Game) | ω.car = car ∧ ω.host = host} = ↑(Finset.univ.filter (fun (ω : Game) => ω.car = car ∧ ω.host = host)) := by - exact set_to_finset_conv - --- Conversion lemma for pick, host and car triple -lemma pick_host_car_set_to_finset { pick host car: Door} : - {(ω : Game) | ω.car = car ∧ ω.host = host ∧ ω.pick = pick} = ↑(Finset.univ.filter (fun (ω : Game) => ω.car = car ∧ ω.host = host ∧ ω.pick = pick)) := by - exact set_to_finset_conv - - - -lemma car_behind_door { car: Door}: Prob (car_at car) = 1 / 3 := by - unfold Prob p car_at - rw [car_set_to_finset] - rw [PMF.toMeasure_apply_finset] - simp only [PMF.uniformOfFintype_apply] - rw [Finset.sum_const, nsmul_eq_mul] - rw [car_finset_card] - rw [total_games] - norm_num - eq_as_reals +lemma car_finset_card {car : Door} : + (Finset.univ.filter (fun ω : Game => ω.car = car)).card = 4 := by + fin_cases car <;> decide -lemma host_car_card { host car: Door} (hnc: host ≠ car) : (Finset.univ.filter (fun (ω : Game) => ω.host = host ∧ ω.car = car)).card = 2 := by +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 --- Same lemma but with reversed conjunction order -lemma car_host_card { car host: Door} (hnc: host ≠ car) : (Finset.univ.filter (fun (ω : Game) => ω.car = car ∧ ω.host = host)).card = 2 := by - have h : (Finset.univ.filter (fun (ω : Game) => ω.car = car ∧ ω.host = host)) = - (Finset.univ.filter (fun (ω : Game) => ω.host = host ∧ ω.car = car)) := by - ext ω - simp [and_comm] - rw [h] - exact host_car_card hnc +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 --- When car = pick, the host cannot open that door, so this probability is 0 -lemma door_opened_by_host_when_car_equals_pick { pick host : Door} {hnp: host ≠ pick} : +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 p + unfold Prob rw [cond_apply] simp only [host_opens, car_at] - -- Convert intersection to conjunction - have h_inter : {(ω : Game) | ω.car = pick} ∩ {(ω : Game) | ω.host = host} = - {(ω : Game) | ω.car = pick ∧ ω.host = host} := by - ext ω - simp [Set.mem_inter_iff] - rw [h_inter] - -- Convert to finsets - have h_conv1 : {(ω : Game) | ω.car = pick} = ↑(Finset.univ.filter (fun (ω : Game) => ω.car = pick)) := by - exact set_to_finset_conv - have h_conv2 : {(ω : Game) | ω.car = pick ∧ ω.host = host} = - ↑(Finset.univ.filter (fun (ω : Game) => ω.car = pick ∧ ω.host = host)) := by - exact set_to_finset_conv - rw [h_conv1, h_conv2] - rw [PMF.toMeasure_apply_finset, PMF.toMeasure_apply_finset] + 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] - -- Count cardinalities - have h_pick_card : (Finset.univ.filter (fun (ω : Game) => ω.car = pick)).card = 4 := by - exact car_finset_card - have h_pick_host_card : (Finset.univ.filter (fun (ω : Game) => ω.car = pick ∧ ω.host = host)).card = 2 := by - -- When car = pick, host ≠ pick, there are 2 games (one for each possible player pick) - exact car_host_card hnp - rw [h_pick_card, h_pick_host_card, total_games] - -- Now we have: (4 * 12⁻¹)⁻¹ * (2 * 12⁻¹) = 1/2 - norm_num - eq_as_reals - -lemma door_opened_by_host_when_car_not_equals_pick { pick host : Door} {hnp: host ≠ pick} : + 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 - unfold Prob p - rw [cond_apply] - · simp only [host_opens] - sorry + 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 - -lemma car_not_behind_door {car: Door} : Prob ((car_at car)ᶜ) = 2/3 := by - -- Use that Prob(car_at car) = 1/3 and Prob(Aᶜ) = 1 - Prob(A) - have h_car : Prob (car_at car) = 1/3 := car_behind_door - rw [measure_compl (by trivial) (by exact measure_ne_top Prob _)] - rw [measure_univ, h_car] - rw [ENNReal.sub_eq_of_eq_add_rev] - norm_num - rw [ENNReal.div_add_div_same] - eq_as_reals - -theorem monty_hall_stay_probability (pick host : Door) (hnp: host ≠ pick) : Prob[car_at pick | host_opens host] = 1/3 := by - rw [ProbabilityTheory.cond_eq_inv_mul_cond_mul (by exact trivial) (by exact trivial)] - nth_rewrite 1 [law_of_total_probability Prob (host_opens host) (car_at pick)] - · rw [@door_opened_by_host_when_car_equals_pick pick host hnp, car_behind_door, - @door_opened_by_host_when_car_not_equals_pick pick host hnp, car_not_behind_door] - have: ((1/2) * (1/3) + (1/2) * (2/3))⁻¹ * (1/2) * (1/3) = 1/(3: ENNReal) := by - ring_nf - norm_num - eq_as_reals - rw [this] - . trivial - . trivial