KKostya

verify ( (strategy) => Real.({
  valid_strategy(strategy) ==>
  ( expected_reward (
      make_scenario_pmf(pDoorsBiased,strategy)
  ) <= 2000000.0 / 3.0 ) 
}))

KKostya

expected_reward(
  make_scenario_pmf(pDoorsEqual, CX.strategy)
)

KKostya

type choice =
  | Stay
  | Swap
  
type scenario = 
  { prize       : door
  , first_guess : door
  , choice      : choice
  }

KKostya

let prize = 1000000.0

type door =
  | DoorA
  | DoorB
  | DoorC

KKostya

let pDoorsBiased = (door : door) => Real.(
  switch (door){
  | DoorA => 3.0 / 5.0
  | DoorB | DoorC => 1.0 / 5.0
  }
);

valid_door_pmf(pDoorsBiased)

KKostya

let random_then_stay_strategy : (door => choice => real) =
  (door) => (choice) => Real.(
    switch(door,choice){
    | ( _ ,Stay) => 1.0 / 3.0
    | ( _ ,Swap) => 0.0
    } 
  )

KKostya

expected_reward(
  make_scenario_pmf(pDoorsEqual, random_then_stay_strategy)
) 

KKostya

let make_scenario_pmf : (door => real) => (door => choice => real) => (scenario => real) = 
  (door_pmf) => (strategy) => (s) => Real.({
    door_pmf(s.prize) * strategy(s.first_guess, s.choice)
  })

KKostya

let expected_reward : (scenario => real) => real = 
  (scenario_pmf) => Real.({
    let pr = (s) => scenario_pmf(s) * reward(s);
      let avg = (choice) => {
        let avg = (first_guess) => {
          pr { prize: DoorA, first_guess, choice} +
          pr { prize: DoorB, first_guess, choice} +
          pr { prize: DoorC, first_guess, choice} 
        };
      avg(DoorA) + avg(DoorB) + avg(DoorC) 

KKostya

let valid_strategy : (door => choice => real) => bool = 
  (strategy) => Real.({  
    (strategy(DoorA,Stay) >= 0.0) && (strategy(DoorA,Swap) >= 0.0) &&
    (strategy(DoorB,Stay) >= 0.0) && (strategy(DoorB,Swap) >= 0.0) &&
    (strategy(DoorC,Stay) >= 0.0) && (strategy(DoorC,Swap) >= 0.0) &&
    ( strategy(DoorA,Stay) + strategy(DoorA,Swap) +
      strategy(DoorB,Stay) + strategy(DoorB,Swap) +
      strategy(DoorC,Stay) + strategy(DoorC,Swap) == 1.0) 
  });