An amazing feature of Imandra is the ability to reason about functional inputs and generate functional instances and counterexamples. For example we can introduce a variant type and a second-order function that evaluates its argument on each variant and computes the sum of the results.

In [1]:
type t = A | B | C
let sum f = f(A) + f(B) + f(C)
Out[1]:
type t = A | B | C
val sum : (t -> Z.t) -> Z.t = <fun>

Now, let's ask Imandra to come up with an instance of a function f that returns positive values and that produces 42 when calling sum(f):

In [2]:
instance( fun (f) -> f(A) > 0 && f(B) > 0 && sum(f) = 42 )
Out[2]:
- : (t -> Z.t) -> bool = <fun>
module CX : sig val f : t -> Z.t end
Instance (after 0 steps, 0.018s):
let f : t -> int = fun (x_0 : t) -> if x_0 = C then 40 else 1
Instance
proof attempt
ground_instances:0
definitions:0
inductions:0
search_time:
0.018s
details:
Expand
smt_stats:
num checks:1
arith assert lower:3
arith tableau max rows:1
arith tableau max columns:4
arith pivots:1
rlimit count:350
mk clause:3
datatype occurs check:3
mk bool var:5
arith assert upper:1
propagations:2
datatype accessor ax:3
arith num rows:1
num allocs:6238629
final checks:1
added eqs:1
del clause:3
arith eq adapter:1
time:0.008000
memory:15.410000
max memory:15.840000
Expand
  • start[0.018s]
      let (_x_0 : int) = sko_f_0 A in
      let (_x_1 : int) = sko_f_0 B in
      (_x_0 > 0) && ((_x_1 > 0) && (_x_0 + _x_1 + sko_f_0 C = 42))
  • simplify

    into:
    let (_x_0 : int) = sko_f_0 A in
    let (_x_1 : int) = sko_f_0 B in
    not (_x_0 <= 0) && not (_x_1 <= 0) && (_x_0 + _x_1 + sko_f_0 C = 42)
    expansions:
    []
    rewrite_steps:
      forward_chaining:
      • Sat (Some let f : t -> int = fun (x_0 : t) -> if x_0 = C then (Z.of_nativeint (40n)) else (Z.of_nativeint (1n)) )

      A natural application of this ability is to apply it to formal reasoning about random variables and probability distributions over them. In the following, we'll consider an application of this kind of reasoning to analyse the famous Monty Hall problem.

      Monty Hall problem

      In the Monty Hall problem, you are participating in a game where you are given three doors to choose from. One of the doors randomly contains a $1,000,000 prize. Let’s encode that in OCaml — we’ll introduce the value of the prize and the variant type for the doors.

      In [3]:
      let prize = 1000000.0
      
      type door =
        | DoorA
        | DoorB
        | DoorC
      
      Out[3]:
      val prize : real = 1000000
      type door = DoorA | DoorB | DoorC
      

      The game then proceeds as follows: first, you guess one of the doors, then the host opens another door — a door that, the host knows, doesn’t contain the prize. The host then offers you to change your initial guess or stay with it.

      To encode that, we’ll introduce another variant type for the player choice and gather all the values that describe a single Monty Hall trial into a scenario record.

      In [4]:
      type choice =
        | Stay
        | Swap
      
      type scenario = 
        { prize       : door
        ; first_guess : door
        ; choice      : choice
        }
      
      Out[4]:
      type choice = Stay | Swap
      type scenario = { prize : door; first_guess : door; choice : choice; }
      

      Probability mass functions 

      We want to treat scenarios described by the "scenario" record as random. This means that we would like to deal with probability mass functions (PMFs) over the variables of the declared types. As a first example, let's make a PMF for the doors that distributes over the three doors with equal probabilities:

      In [5]:
      let pDoorsEqual : (door -> real) = fun (door) -> Real.(1.0 / 3.0)
      
      Out[5]:
      val pDoorsEqual : door -> real = <fun>
      

      Notice that we are using the real type for numeric values in our examples. Internally, Imandra represents reals in an arbitrary-precision manner. The real-valued arithmetic operators are gathered in the Real module. Further, we’ll be explicitly opening the Real module to stress that we are dealing with real arithmetic.

      Not just any function can be a probability mass function — PMFs must satisfy the so-called “measure axioms”: all the returned values must be non-negative and the total probability over the whole function domain must sum to one. Let’s make a predicate that checks whether a function is a valid PMF over doors.

      In [6]:
      let valid_door_pmf : (door -> real) -> bool =  
        fun (pmf) -> Real.(
          (pmf(DoorA) + pmf(DoorB) + pmf(DoorC) = 1.0) &&
          (pmf(DoorA) >= 0.0) &&
          (pmf(DoorB) >= 0.0) &&
          (pmf(DoorC) >= 0.0)  
        )
      
      Out[6]:
      val valid_door_pmf : (door -> real) -> bool = <fun>
      

      To check that this predicate works we use it on our pDoorsEqual function.

      In [7]:
      valid_door_pmf(pDoorsEqual)
      
      Out[7]:
      - : bool = true
      

      The player controls the first_guess and the choice fields of the scenario record. In general, the player can also choose his actions randomly. Following the game theory nomenclature, we’ll call the probability distribution over the player choices a “strategy”. For example, here is a strategy that chooses the first guess door randomly and then stays with that choice:

      In [8]:
      let random_then_stay_strategy : (door -> choice -> real) =
        fun door choice -> Real.(
          match door,choice with
          | ( _ ,Stay) -> 1.0 / 3.0
          | ( _ ,Swap) -> 0.0 
        )
      
      Out[8]:
      val random_then_stay_strategy : door -> choice -> real = <fun>
      

      A strategy’s type is door -> choice -> real: it takes in which door the player chooses and which choice he makes and returns the probability with which that happens. To check that such a function is a valid probability mass function we introduce and apply a predicate for it:

      In [9]:
      let valid_strategy : (door -> choice -> real) -> bool = 
        fun 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) 
        )
      
      Out[9]:
      val valid_strategy : (door -> choice -> real) -> bool = <fun>
      
      In [10]:
      valid_strategy(random_then_stay_strategy)
      
      Out[10]:
      - : bool = true
      

      Finally, we’ll need one last function that constructs a PMF over the whole scenario record. It shall take a door -> real prize PMF, a door -> choice -> real player strategy and return a scenario -> real PMF over the scenarios. Since we consider the host and the player choices to be independent, the total probability of the full scenario must be the product of the probabilities of the host and player choices:

      In [11]:
      let make_scenario_pmf : (door -> real) -> (door -> choice -> real) -> (scenario -> real) = 
        fun door_pmf strategy s -> Real.(
          door_pmf s.prize * strategy s.first_guess s.choice
        )
      
      Out[11]:
      val make_scenario_pmf :
        (door -> real) -> (door -> choice -> real) -> scenario -> real = <fun>
      

      Expected rewards

      Given a scenario variable, we can calculate the player's "reward." When the first guess is equal to the prize location, then we return the prize value if the player decided to stay. Alternatively, when the first guess is not equal to the prize location, then we return the prize value if the player decided to swap.

      In [12]:
      let reward scenario =
        if scenario.prize = scenario.first_guess then (
            if scenario.choice = Stay then prize else 0.0
        ) else (
            if scenario.choice = Swap then prize else 0.0
        )
      
      Out[12]:
      val reward : scenario -> real = <fun>
      

      Given a probability distribution over scenarios, we want to calculate the expected value of the reward - the probability-weighted average of possible values of the reward for each outcome.

      $$ E[reward] = \sum_s P(s)\,reward(s) $$

      We create a function that performs this averaging: it takes in a scenario PMF of type scenario => real and returns a real for the expected value:

      In [13]:
      let expected_reward : (scenario -> real) -> real = 
        let open Real in
        fun scenario_pmf -> 
          let pr s = scenario_pmf(s) * reward(s) in
            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} 
              in
            avg(DoorA) + avg(DoorB) + avg(DoorC) 
            in
          avg(Stay) + avg(Swap)
      
      Out[13]:
      val expected_reward : (scenario -> real) -> real = <fun>
      

      As a final example, let’s use what we’ve built so far to calculate the expected reward for the scenario when the host hides the prize equally randomly and the player uses the random_then_stay_strategy:

      In [14]:
      random_then_stay_strategy
      |> make_scenario_pmf pDoorsEqual 
      |> expected_reward
      
      Out[14]:
      - : real = 1000000/3
      

      We get an obvious result that if we choose a random door and stay with it, then the expected reward is 1/3 of a $1,000,000. That seems reasonable and it is not very obvious that one can increase his chances of winning.

      Reasoning about Monty Hall probabilities

      Let’s ask Imandra if 1/3 of a 1,000,000$ is the best outcome for any strategy the player can employ. To do this we’ll use Imandra verify directive to verify that, for any valid strategy, the scenario with equally probable prize placement gives an expected reward less or equal than 1000000/3.

      In [15]:
      verify ( fun strategy -> Real.(
        valid_strategy(strategy) ==>
        ( expected_reward (make_scenario_pmf pDoorsEqual strategy)
        ) <= 1000000.0 / 3.0 ) 
      )
      
      Out[15]:
      - : (door -> choice -> real) -> bool = <fun>
      module CX : sig val strategy : door -> choice -> real end
      
      Counterexample (after 0 steps, 0.018s):
      let strategy : door -> choice -> real =
        fun (x_0 : door) ->
         fun (x_1 : choice) ->
          if (x_0 = DoorA) && (x_1 = Swap) then 3/1000000
          else if (x_0 = DoorB) && (x_1 = Stay) then 999997/1000000 else 0
      
      Refuted
      proof attempt
      ground_instances:0
      definitions:0
      inductions:0
      search_time:
      0.018s
      details:
      Expand
      smt_stats:
      num checks:1
      arith assert lower:8
      arith tableau max rows:2
      arith tableau max columns:11
      arith pivots:2
      rlimit count:1971
      mk clause:3
      datatype occurs check:5
      mk bool var:10
      arith assert upper:1
      arith row summations:2
      propagations:2
      datatype accessor ax:5
      arith num rows:2
      num allocs:14706061
      final checks:1
      added eqs:1
      del clause:3
      arith eq adapter:1
      time:0.008000
      memory:17.700000
      max memory:18.100000
      Expand
      • start[0.018s]
          let (_x_0 : real) = sko_strategy_0 DoorA Stay in
          let (_x_1 : real) = sko_strategy_0 DoorA Swap in
          let (_x_2 : real) = sko_strategy_0 DoorB Stay in
          let (_x_3 : real) = sko_strategy_0 DoorB Swap in
          let (_x_4 : real) = sko_strategy_0 DoorC Stay in
          let (_x_5 : real) = sko_strategy_0 DoorC Swap in
          let (_x_6 : real) = 1 / 3 in
          let (_x_7 : real) = _x_6 * _x_0 in
          let (_x_8 : real) = if Stay = Swap then 1000000 else 0 in
          let (_x_9 : bool) = DoorB = DoorA in
          let (_x_10 : bool) = DoorC = DoorA in
          let (_x_11 : real) = _x_6 * _x_2 in
          let (_x_12 : bool) = DoorA = DoorB in
          let (_x_13 : bool) = DoorC = DoorB in
          let (_x_14 : real) = _x_6 * _x_4 in
          let (_x_15 : bool) = DoorA = DoorC in
          let (_x_16 : bool) = DoorB = DoorC in
          let (_x_17 : real) = _x_6 * _x_1 in
          let (_x_18 : real) = if Swap = Stay then 1000000 else 0 in
          let (_x_19 : real) = _x_6 * _x_3 in
          let (_x_20 : real) = _x_6 * _x_5 in
          (_x_0 >= 0)
          && ((_x_1 >= 0)
              && ((_x_2 >= 0)
                  && ((_x_3 >= 0)
                      && ((_x_4 >= 0)
                          && ((_x_5 >= 0)
                              && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1))))))
          ==> _x_7 * 1000000 +. _x_7 * (if _x_9 then 1000000 else _x_8)
              +. _x_7 * (if _x_10 then 1000000 else _x_8)
              +. (_x_11 * (if _x_12 then 1000000 else _x_8) +. _x_11 * 1000000
                  +. _x_11 * (if _x_13 then 1000000 else _x_8))
              +. (_x_14 * (if _x_15 then 1000000 else _x_8)
                  +. _x_14 * (if _x_16 then 1000000 else _x_8) +. _x_14 * 1000000)
              +. (_x_17 * _x_18 +. _x_17 * (if _x_9 then _x_18 else 1000000)
                  +. _x_17 * (if _x_10 then _x_18 else 1000000)
                  +. (_x_19 * (if _x_12 then _x_18 else 1000000) +. _x_19 * _x_18
                      +. _x_19 * (if _x_13 then _x_18 else 1000000))
                  +. (_x_20 * (if _x_15 then _x_18 else 1000000)
                      +. _x_20 * (if _x_16 then _x_18 else 1000000) +. _x_20 * _x_18))
              <= 1000000 / 3
      • simplify

        into:
        let (_x_0 : real) = sko_strategy_0 DoorA Stay in
        let (_x_1 : real) = sko_strategy_0 DoorA Swap in
        let (_x_2 : real) = sko_strategy_0 DoorB Stay in
        let (_x_3 : real) = sko_strategy_0 DoorB Swap in
        let (_x_4 : real) = sko_strategy_0 DoorC Stay in
        let (_x_5 : real) = sko_strategy_0 DoorC Swap in
        not
        ((_x_0 >= 0) && (_x_1 >= 0) && (_x_2 >= 0) && (_x_3 >= 0) && (_x_4 >= 0)
         && (_x_5 >= 0) && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1))
        || (1000000/3 * _x_0 +. 1000000/3 * _x_2 +. 1000000/3 * _x_4
            +. 2000000/3 * _x_1 +. 2000000/3 * _x_3 +. 2000000/3 * _x_5 <= 1000000/3)
        expansions:
        []
        rewrite_steps:
          forward_chaining:
          • Sat (Some let strategy : door -> choice -> real = fun (x_0 : door) -> fun (x_1 : choice) -> if (x_0 = DoorA) && (x_1 = Swap) then (Q.of_string "3/1000000") else if (x_0 = DoorB) && (x_1 = Stay) then (Q.of_string "999997/1000000") else (Q.of_nativeint (0n)) )

          Imandra refuted our statement and provided us with a counterexample strategy. Imandra suggests that the expected reward will be greater than 1000000/3 if the player chooses DoorA and then Swaps his choice in 0.0003% of the cases. The counterexample strategy is defined in the CX module, so let's see what is the expected reward with this strategy:

          In [16]:
          CX.strategy
          |> make_scenario_pmf pDoorsEqual 
          |> expected_reward
          
          Out[16]:
          - : real = 1000003/3
          

          The counterexample strategy that Imandra produced increased our expected winnings by 1$. This counterexample strategy employs swapping instead of staying. What would be our expected reward if we always swap?

          In [17]:
          let random_then_swap_strategy door choice = 
            match (door,choice) with | _,Swap -> Real.(1.0 / 3.0) | _ -> 0.0 in
          random_then_swap_strategy
          |> make_scenario_pmf pDoorsEqual
          |> expected_reward
          
          Out[17]:
          - : real = 2000000/3
          

          By always swapping we’ve increased our chances of winning up to 2/3. Is this the best possible expected reward one might get in this game?

          In [18]:
          verify ( fun strategy -> Real.(
            valid_strategy(strategy) ==>
            ( expected_reward (make_scenario_pmf pDoorsEqual strategy)
            ) <= 2000000.0 / 3.0 ) 
          )
          
          Out[18]:
          - : (door -> choice -> real) -> bool = <fun>
          
          Proved
          proof
          ground_instances:0
          definitions:0
          inductions:0
          search_time:
          0.018s
          details:
          Expand
          smt_stats:
          num checks:1
          arith assert lower:8
          arith tableau max rows:2
          arith tableau max columns:11
          arith pivots:2
          rlimit count:1953
          mk clause:3
          mk bool var:10
          arith assert upper:1
          arith row summations:2
          propagations:2
          conflicts:1
          datatype accessor ax:5
          arith conflicts:1
          arith num rows:2
          num allocs:23779088
          added eqs:1
          arith eq adapter:1
          time:0.008000
          memory:18.050000
          max memory:18.460000
          Expand
          • start[0.018s]
              let (_x_0 : real) = sko_strategy_0 DoorA Stay in
              let (_x_1 : real) = sko_strategy_0 DoorA Swap in
              let (_x_2 : real) = sko_strategy_0 DoorB Stay in
              let (_x_3 : real) = sko_strategy_0 DoorB Swap in
              let (_x_4 : real) = sko_strategy_0 DoorC Stay in
              let (_x_5 : real) = sko_strategy_0 DoorC Swap in
              let (_x_6 : real) = 1 / 3 in
              let (_x_7 : real) = _x_6 * _x_0 in
              let (_x_8 : real) = if Stay = Swap then 1000000 else 0 in
              let (_x_9 : bool) = DoorB = DoorA in
              let (_x_10 : bool) = DoorC = DoorA in
              let (_x_11 : real) = _x_6 * _x_2 in
              let (_x_12 : bool) = DoorA = DoorB in
              let (_x_13 : bool) = DoorC = DoorB in
              let (_x_14 : real) = _x_6 * _x_4 in
              let (_x_15 : bool) = DoorA = DoorC in
              let (_x_16 : bool) = DoorB = DoorC in
              let (_x_17 : real) = _x_6 * _x_1 in
              let (_x_18 : real) = if Swap = Stay then 1000000 else 0 in
              let (_x_19 : real) = _x_6 * _x_3 in
              let (_x_20 : real) = _x_6 * _x_5 in
              (_x_0 >= 0)
              && ((_x_1 >= 0)
                  && ((_x_2 >= 0)
                      && ((_x_3 >= 0)
                          && ((_x_4 >= 0)
                              && ((_x_5 >= 0)
                                  && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1))))))
              ==> _x_7 * 1000000 +. _x_7 * (if _x_9 then 1000000 else _x_8)
                  +. _x_7 * (if _x_10 then 1000000 else _x_8)
                  +. (_x_11 * (if _x_12 then 1000000 else _x_8) +. _x_11 * 1000000
                      +. _x_11 * (if _x_13 then 1000000 else _x_8))
                  +. (_x_14 * (if _x_15 then 1000000 else _x_8)
                      +. _x_14 * (if _x_16 then 1000000 else _x_8) +. _x_14 * 1000000)
                  +. (_x_17 * _x_18 +. _x_17 * (if _x_9 then _x_18 else 1000000)
                      +. _x_17 * (if _x_10 then _x_18 else 1000000)
                      +. (_x_19 * (if _x_12 then _x_18 else 1000000) +. _x_19 * _x_18
                          +. _x_19 * (if _x_13 then _x_18 else 1000000))
                      +. (_x_20 * (if _x_15 then _x_18 else 1000000)
                          +. _x_20 * (if _x_16 then _x_18 else 1000000) +. _x_20 * _x_18))
                  <= 2000000 / 3
          • simplify

            into:
            let (_x_0 : real) = sko_strategy_0 DoorA Stay in
            let (_x_1 : real) = sko_strategy_0 DoorA Swap in
            let (_x_2 : real) = sko_strategy_0 DoorB Stay in
            let (_x_3 : real) = sko_strategy_0 DoorB Swap in
            let (_x_4 : real) = sko_strategy_0 DoorC Stay in
            let (_x_5 : real) = sko_strategy_0 DoorC Swap in
            not
            ((_x_0 >= 0) && (_x_1 >= 0) && (_x_2 >= 0) && (_x_3 >= 0) && (_x_4 >= 0)
             && (_x_5 >= 0) && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1))
            || (1000000/3 * _x_0 +. 1000000/3 * _x_2 +. 1000000/3 * _x_4
                +. 2000000/3 * _x_1 +. 2000000/3 * _x_3 +. 2000000/3 * _x_5 <= 2000000/3)
            expansions:
            []
            rewrite_steps:
              forward_chaining:
              • Unsat

              We’ve proven that the best possible expected reward in the Monty Hall game is 2/3 of a $1,000,000 in an (arguably, rather counterintuitive) result that one has to always swap his first choice to double his chances of winning.

              Suppose now that we don’t know the winning strategy, but we do know that it is possible to win in 2/3 of the cases. Can we ask Imandra to synthesise the optimal strategy? For this purpose we can use the instance directive:

              In [19]:
              instance ( fun strategy -> Real.(
                valid_strategy(strategy) &&
                ( expected_reward (make_scenario_pmf pDoorsEqual strategy)
                ) = 2000000.0 / 3.0 ) 
              )
              
              Out[19]:
              - : (door -> choice -> real) -> bool = <fun>
              module CX : sig val strategy : door -> choice -> real end
              
              Instance (after 0 steps, 0.020s):
              let strategy : door -> choice -> real =
                fun (x_0 : door) ->
                 fun (x_1 : choice) -> if (x_0 = DoorA) && (x_1 = Swap) then 1 else 0
              
              Instance
              proof attempt
              ground_instances:0
              definitions:0
              inductions:0
              search_time:
              0.020s
              details:
              Expand
              smt_stats:
              num checks:1
              arith assert lower:8
              arith tableau max rows:2
              arith tableau max columns:11
              arith pivots:2
              rlimit count:1935
              mk clause:6
              datatype occurs check:5
              mk bool var:12
              arith assert upper:2
              arith row summations:2
              propagations:4
              datatype accessor ax:5
              arith num rows:2
              num allocs:35268144
              final checks:1
              added eqs:2
              del clause:6
              arith eq adapter:2
              time:0.011000
              memory:18.440000
              max memory:18.830000
              Expand
              • start[0.020s]
                  let (_x_0 : real) = sko_strategy_0 DoorA Stay in
                  let (_x_1 : real) = sko_strategy_0 DoorA Swap in
                  let (_x_2 : real) = sko_strategy_0 DoorB Stay in
                  let (_x_3 : real) = sko_strategy_0 DoorB Swap in
                  let (_x_4 : real) = sko_strategy_0 DoorC Stay in
                  let (_x_5 : real) = sko_strategy_0 DoorC Swap in
                  let (_x_6 : real) = 1 / 3 in
                  let (_x_7 : real) = _x_6 * _x_0 in
                  let (_x_8 : real) = if Stay = Swap then 1000000 else 0 in
                  let (_x_9 : bool) = DoorB = DoorA in
                  let (_x_10 : bool) = DoorC = DoorA in
                  let (_x_11 : real) = _x_6 * _x_2 in
                  let (_x_12 : bool) = DoorA = DoorB in
                  let (_x_13 : bool) = DoorC = DoorB in
                  let (_x_14 : real) = _x_6 * _x_4 in
                  let (_x_15 : bool) = DoorA = DoorC in
                  let (_x_16 : bool) = DoorB = DoorC in
                  let (_x_17 : real) = _x_6 * _x_1 in
                  let (_x_18 : real) = if Swap = Stay then 1000000 else 0 in
                  let (_x_19 : real) = _x_6 * _x_3 in
                  let (_x_20 : real) = _x_6 * _x_5 in
                  (_x_0 >= 0)
                  && ((_x_1 >= 0)
                      && ((_x_2 >= 0)
                          && ((_x_3 >= 0)
                              && ((_x_4 >= 0)
                                  && ((_x_5 >= 0)
                                      && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1))))))
                  && (_x_7 * 1000000 +. _x_7 * (if _x_9 then 1000000 else _x_8)
                      +. _x_7 * (if _x_10 then 1000000 else _x_8)
                      +. (_x_11 * (if _x_12 then 1000000 else _x_8) +. _x_11 * 1000000
                          +. _x_11 * (if _x_13 then 1000000 else _x_8))
                      +. (_x_14 * (if _x_15 then 1000000 else _x_8)
                          +. _x_14 * (if _x_16 then 1000000 else _x_8) +. _x_14 * 1000000)
                      +. (_x_17 * _x_18 +. _x_17 * (if _x_9 then _x_18 else 1000000)
                          +. _x_17 * (if _x_10 then _x_18 else 1000000)
                          +. (_x_19 * (if _x_12 then _x_18 else 1000000) +. _x_19 * _x_18
                              +. _x_19 * (if _x_13 then _x_18 else 1000000))
                          +. (_x_20 * (if _x_15 then _x_18 else 1000000)
                              +. _x_20 * (if _x_16 then _x_18 else 1000000) +. _x_20 * _x_18))
                      = 2000000 / 3)
              • simplify

                into:
                let (_x_0 : real) = sko_strategy_0 DoorA Stay in
                let (_x_1 : real) = sko_strategy_0 DoorA Swap in
                let (_x_2 : real) = sko_strategy_0 DoorB Stay in
                let (_x_3 : real) = sko_strategy_0 DoorB Swap in
                let (_x_4 : real) = sko_strategy_0 DoorC Stay in
                let (_x_5 : real) = sko_strategy_0 DoorC Swap in
                (_x_0 >= 0) && (_x_1 >= 0) && (_x_2 >= 0) && (_x_3 >= 0) && (_x_4 >= 0)
                && (_x_5 >= 0) && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1)
                && (1000000/3 * _x_0 +. 1000000/3 * _x_2 +. 1000000/3 * _x_4
                    +. 2000000/3 * _x_1 +. 2000000/3 * _x_3 +. 2000000/3 * _x_5 = 2000000/3)
                expansions:
                []
                rewrite_steps:
                  forward_chaining:
                  • Sat (Some let strategy : door -> choice -> real = fun (x_0 : door) -> fun (x_1 : choice) -> if (x_0 = DoorA) && (x_1 = Swap) then (Q.of_nativeint (1n)) else (Q.of_nativeint (0n)) )

                  We've got an example of an optimal strategy - this one doesn't randomize over doors, but suggests to always choose the DoorA and then swap.

                  Biased Monty Hall

                  Now let's apply what we've learned about the "standard" Monty Hall paradox to a more complicated game setup - suppose that we somehow know that the host is biased towards the DoorA -- the probability that the host will hide the prize behind the first door is 3 times higher than the individual probabilities for two other doors. Should one still always swap? Or, maybe, it makes more sense to always choose the more likely DoorA and stay?

                  We encode our biased host in the biased PMF over doors (also doing a sanity check that it is a valid probability distribution):

                  In [20]:
                  let pDoorsBiased door = Real.(
                    match door with
                    | DoorA -> 3.0 / 5.0
                    | DoorB | DoorC -> 1.0 / 5.0
                  );;
                  
                  valid_door_pmf(pDoorsBiased)
                  
                  Out[20]:
                  val pDoorsBiased : door -> real = <fun>
                  - : bool = true
                  

                  In the previous section, we've proven that the maximal possible expected reward in the "standard" Monty Hall problem is 2/3 of a million. Again, we ask Imandra whether we can improve on this in the biased case:

                  In [21]:
                  verify ( fun (strategy) -> Real.(
                    valid_strategy(strategy) ==>
                    ( expected_reward (make_scenario_pmf pDoorsBiased strategy)
                    ) <= 2000000.0 / 3.0 ) 
                  )
                  
                  Out[21]:
                  - : (door -> choice -> real) -> bool = <fun>
                  module CX : sig val strategy : door -> choice -> real end
                  
                  Counterexample (after 0 steps, 0.019s):
                  let strategy : door -> choice -> real =
                    fun (x_0 : door) ->
                     fun (x_1 : choice) ->
                      if (x_0 = DoorA) && (x_1 = Stay) then 399997/600000
                      else if (x_0 = DoorC) && (x_1 = Swap) then 200003/600000 else 0
                  
                  Refuted
                  proof attempt
                  ground_instances:0
                  definitions:0
                  inductions:0
                  search_time:
                  0.019s
                  details:
                  Expand
                  smt_stats:
                  num checks:1
                  arith assert lower:8
                  arith tableau max rows:2
                  arith tableau max columns:13
                  arith pivots:3
                  rlimit count:2307
                  mk clause:3
                  datatype occurs check:5
                  mk bool var:10
                  arith assert upper:1
                  arith row summations:3
                  propagations:2
                  datatype accessor ax:5
                  arith num rows:2
                  num allocs:49689857
                  final checks:1
                  added eqs:1
                  del clause:3
                  arith eq adapter:1
                  time:0.009000
                  memory:19.010000
                  max memory:19.410000
                  Expand
                  • start[0.019s]
                      let (_x_0 : real) = sko_strategy_0 DoorA Stay in
                      let (_x_1 : real) = sko_strategy_0 DoorA Swap in
                      let (_x_2 : real) = sko_strategy_0 DoorB Stay in
                      let (_x_3 : real) = sko_strategy_0 DoorB Swap in
                      let (_x_4 : real) = sko_strategy_0 DoorC Stay in
                      let (_x_5 : real) = sko_strategy_0 DoorC Swap in
                      let (_x_6 : real) = 3 / 5 in
                      let (_x_7 : real) = 1 / 5 in
                      let (_x_8 : real) = _x_7 * _x_0 in
                      let (_x_9 : real) = if Stay = Swap then 1000000 else 0 in
                      let (_x_10 : bool) = DoorB = DoorA in
                      let (_x_11 : bool) = DoorC = DoorA in
                      let (_x_12 : bool) = DoorA = DoorB in
                      let (_x_13 : real) = _x_7 * _x_2 in
                      let (_x_14 : bool) = DoorC = DoorB in
                      let (_x_15 : bool) = DoorA = DoorC in
                      let (_x_16 : real) = _x_7 * _x_4 in
                      let (_x_17 : bool) = DoorB = DoorC in
                      let (_x_18 : real) = if Swap = Stay then 1000000 else 0 in
                      let (_x_19 : real) = _x_7 * _x_1 in
                      let (_x_20 : real) = _x_7 * _x_3 in
                      let (_x_21 : real) = _x_7 * _x_5 in
                      (_x_0 >= 0)
                      && ((_x_1 >= 0)
                          && ((_x_2 >= 0)
                              && ((_x_3 >= 0)
                                  && ((_x_4 >= 0)
                                      && ((_x_5 >= 0)
                                          && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1))))))
                      ==> _x_6 * _x_0 * 1000000 +. _x_8 * (if _x_10 then 1000000 else _x_9)
                          +. _x_8 * (if _x_11 then 1000000 else _x_9)
                          +. (_x_6 * _x_2 * (if _x_12 then 1000000 else _x_9) +. _x_13 * 1000000
                              +. _x_13 * (if _x_14 then 1000000 else _x_9))
                          +. (_x_6 * _x_4 * (if _x_15 then 1000000 else _x_9)
                              +. _x_16 * (if _x_17 then 1000000 else _x_9) +. _x_16 * 1000000)
                          +. (_x_6 * _x_1 * _x_18 +. _x_19 * (if _x_10 then _x_18 else 1000000)
                              +. _x_19 * (if _x_11 then _x_18 else 1000000)
                              +. (_x_6 * _x_3 * (if _x_12 then _x_18 else 1000000)
                                  +. _x_20 * _x_18 +. _x_20 * (if _x_14 then _x_18 else 1000000))
                              +. (_x_6 * _x_5 * (if _x_15 then _x_18 else 1000000)
                                  +. _x_21 * (if _x_17 then _x_18 else 1000000) +. _x_21 * _x_18))
                          <= 2000000 / 3
                  • simplify

                    into:
                    let (_x_0 : real) = sko_strategy_0 DoorA Stay in
                    let (_x_1 : real) = sko_strategy_0 DoorA Swap in
                    let (_x_2 : real) = sko_strategy_0 DoorB Stay in
                    let (_x_3 : real) = sko_strategy_0 DoorB Swap in
                    let (_x_4 : real) = sko_strategy_0 DoorC Stay in
                    let (_x_5 : real) = sko_strategy_0 DoorC Swap in
                    not
                    ((_x_0 >= 0) && (_x_1 >= 0) && (_x_2 >= 0) && (_x_3 >= 0) && (_x_4 >= 0)
                     && (_x_5 >= 0) && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1))
                    || (600000 * _x_0 +. 200000 * _x_2 +. 200000 * _x_4 +. 400000 * _x_1
                        +. 800000 * _x_3 +. 800000 * _x_5 <= 2000000/3)
                    expansions:
                    []
                    rewrite_steps:
                      forward_chaining:
                      • Sat (Some let strategy : door -> choice -> real = fun (x_0 : door) -> fun (x_1 : choice) -> if (x_0 = DoorA) && (x_1 = Stay) then (Q.of_string "399997/600000") else if (x_0 = DoorC) && (x_1 = Swap) then (Q.of_string "200003/600000") else (Q.of_nativeint (0n)) )

                      Imandra suggests that we can do better than 2/3 if we use a mixed strategy of either choosing the DoorA and staying or choosing the DoorC and swapping. Let's test both of these pure strategies and see what would be the expected rewards for each:

                      In [22]:
                      let aStayStrategy door choice = 
                        match door,choice with | DoorA,Stay -> 1.0 | _ -> 0.0 in
                      aStayStrategy
                      |> make_scenario_pmf pDoorsBiased
                      |> expected_reward 
                      ;;
                      let cSwapStrategy door choice = 
                        match door,choice with | DoorC,Swap -> 1.0 | _ -> 0.0 in
                      cSwapStrategy
                      |> make_scenario_pmf pDoorsBiased
                      |> expected_reward 
                      ;;
                      
                      Out[22]:
                      - : real = 600000
                      - : real = 800000
                      

                      Choosing the DoorC and then swapping increases the chances of winning up to 80%! Again, is this the best outcome one can get?

                      In [23]:
                      verify ( fun strategy -> Real.(
                        valid_strategy(strategy) ==>
                        ( expected_reward (make_scenario_pmf pDoorsBiased strategy)
                        ) <= 800000.0 ) 
                      )
                      
                      Out[23]:
                      - : (door -> choice -> real) -> bool = <fun>
                      
                      Proved
                      proof
                      ground_instances:0
                      definitions:0
                      inductions:0
                      search_time:
                      0.019s
                      details:
                      Expand
                      smt_stats:
                      num checks:1
                      arith assert lower:8
                      arith tableau max rows:2
                      arith tableau max columns:13
                      arith pivots:3
                      rlimit count:2287
                      mk clause:3
                      mk bool var:10
                      arith assert upper:1
                      arith row summations:3
                      propagations:2
                      conflicts:1
                      datatype accessor ax:5
                      arith conflicts:1
                      arith num rows:2
                      num allocs:66141752
                      added eqs:1
                      arith eq adapter:1
                      time:0.009000
                      memory:19.390000
                      max memory:19.790000
                      Expand
                      • start[0.019s]
                          let (_x_0 : real) = sko_strategy_0 DoorA Stay in
                          let (_x_1 : real) = sko_strategy_0 DoorA Swap in
                          let (_x_2 : real) = sko_strategy_0 DoorB Stay in
                          let (_x_3 : real) = sko_strategy_0 DoorB Swap in
                          let (_x_4 : real) = sko_strategy_0 DoorC Stay in
                          let (_x_5 : real) = sko_strategy_0 DoorC Swap in
                          let (_x_6 : real) = 3 / 5 in
                          let (_x_7 : real) = 1 / 5 in
                          let (_x_8 : real) = _x_7 * _x_0 in
                          let (_x_9 : real) = if Stay = Swap then 1000000 else 0 in
                          let (_x_10 : bool) = DoorB = DoorA in
                          let (_x_11 : bool) = DoorC = DoorA in
                          let (_x_12 : bool) = DoorA = DoorB in
                          let (_x_13 : real) = _x_7 * _x_2 in
                          let (_x_14 : bool) = DoorC = DoorB in
                          let (_x_15 : bool) = DoorA = DoorC in
                          let (_x_16 : real) = _x_7 * _x_4 in
                          let (_x_17 : bool) = DoorB = DoorC in
                          let (_x_18 : real) = if Swap = Stay then 1000000 else 0 in
                          let (_x_19 : real) = _x_7 * _x_1 in
                          let (_x_20 : real) = _x_7 * _x_3 in
                          let (_x_21 : real) = _x_7 * _x_5 in
                          (_x_0 >= 0)
                          && ((_x_1 >= 0)
                              && ((_x_2 >= 0)
                                  && ((_x_3 >= 0)
                                      && ((_x_4 >= 0)
                                          && ((_x_5 >= 0)
                                              && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1))))))
                          ==> _x_6 * _x_0 * 1000000 +. _x_8 * (if _x_10 then 1000000 else _x_9)
                              +. _x_8 * (if _x_11 then 1000000 else _x_9)
                              +. (_x_6 * _x_2 * (if _x_12 then 1000000 else _x_9) +. _x_13 * 1000000
                                  +. _x_13 * (if _x_14 then 1000000 else _x_9))
                              +. (_x_6 * _x_4 * (if _x_15 then 1000000 else _x_9)
                                  +. _x_16 * (if _x_17 then 1000000 else _x_9) +. _x_16 * 1000000)
                              +. (_x_6 * _x_1 * _x_18 +. _x_19 * (if _x_10 then _x_18 else 1000000)
                                  +. _x_19 * (if _x_11 then _x_18 else 1000000)
                                  +. (_x_6 * _x_3 * (if _x_12 then _x_18 else 1000000)
                                      +. _x_20 * _x_18 +. _x_20 * (if _x_14 then _x_18 else 1000000))
                                  +. (_x_6 * _x_5 * (if _x_15 then _x_18 else 1000000)
                                      +. _x_21 * (if _x_17 then _x_18 else 1000000) +. _x_21 * _x_18))
                              <= 800000
                      • simplify

                        into:
                        let (_x_0 : real) = sko_strategy_0 DoorA Stay in
                        let (_x_1 : real) = sko_strategy_0 DoorA Swap in
                        let (_x_2 : real) = sko_strategy_0 DoorB Stay in
                        let (_x_3 : real) = sko_strategy_0 DoorB Swap in
                        let (_x_4 : real) = sko_strategy_0 DoorC Stay in
                        let (_x_5 : real) = sko_strategy_0 DoorC Swap in
                        not
                        ((_x_0 >= 0) && (_x_1 >= 0) && (_x_2 >= 0) && (_x_3 >= 0) && (_x_4 >= 0)
                         && (_x_5 >= 0) && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1))
                        || (600000 * _x_0 +. 200000 * _x_2 +. 200000 * _x_4 +. 400000 * _x_1
                            +. 800000 * _x_3 +. 800000 * _x_5 <= 800000)
                        expansions:
                        []
                        rewrite_steps:
                          forward_chaining:
                          • Unsat

                          And we've proven that the DoorC-Swap is the best strategy the player can employ in this setup. Intuitively the reason for that is that it is better to choose the least likely door, forcing the host to reveal more information about the prize location in the more likely doors.

                          Even more complex example

                          Using this approach one can go further and analyse even more complicated Monty-Hall-like games (for example, the prize value might depend on the door and/or player actions).

                          In [24]:
                          let pDoorsComplex door = Real.(
                            match door with
                            | DoorA -> 5.0 / 10.0
                            | DoorB -> 3.0 / 10.0 
                            | DoorC -> 2.0 / 10.0
                          );;
                          
                          let reward_complex scenario = 
                            let prize = match scenario.prize with
                              | DoorA -> 1000000.
                              | DoorB -> 2000000.
                              | DoorC -> 4000000.      
                            in 
                            if scenario.prize = scenario.first_guess then (
                                if scenario.choice = Stay then prize else 0.0
                            ) else (
                                if scenario.choice = Swap then prize else 0.0
                            )
                          ;;
                          
                          let expected_reward_complex : (scenario -> real) -> real = 
                            let open Real in
                            fun scenario_pmf -> 
                              let pr s = scenario_pmf(s) * reward_complex(s) in
                                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} 
                                  in
                                avg(DoorA) + avg(DoorB) + avg(DoorC) 
                                in
                              avg(Stay) + avg(Swap)
                          ;;
                          
                          Out[24]:
                          val pDoorsComplex : door -> real = <fun>
                          val reward_complex : scenario -> real = <fun>
                          val expected_reward_complex : (scenario -> real) -> real = <fun>
                          
                          In [25]:
                          verify ( fun strategy -> Real.(
                            valid_strategy(strategy) ==>
                            ( expected_reward_complex ( make_scenario_pmf pDoorsComplex strategy)
                            ) <= 1400000.0 ) 
                          )
                          
                          Out[25]:
                          - : (door -> choice -> real) -> bool = <fun>
                          
                          Proved
                          proof
                          ground_instances:0
                          definitions:0
                          inductions:0
                          search_time:
                          0.018s
                          details:
                          Expand
                          smt_stats:
                          num checks:1
                          arith assert lower:8
                          arith tableau max rows:2
                          arith tableau max columns:15
                          arith pivots:2
                          rlimit count:2473
                          mk clause:3
                          mk bool var:10
                          arith assert upper:1
                          arith row summations:2
                          propagations:2
                          conflicts:1
                          datatype accessor ax:5
                          arith conflicts:1
                          arith num rows:2
                          num allocs:87009617
                          added eqs:1
                          arith eq adapter:1
                          time:0.009000
                          memory:20.310000
                          max memory:20.700000
                          Expand
                          • start[0.018s]
                              let (_x_0 : real) = sko_strategy_0 DoorA Stay in
                              let (_x_1 : real) = sko_strategy_0 DoorA Swap in
                              let (_x_2 : real) = sko_strategy_0 DoorB Stay in
                              let (_x_3 : real) = sko_strategy_0 DoorB Swap in
                              let (_x_4 : real) = sko_strategy_0 DoorC Stay in
                              let (_x_5 : real) = sko_strategy_0 DoorC Swap in
                              let (_x_6 : real) = 5 / 10 in
                              let (_x_7 : real) = 3 / 10 in
                              let (_x_8 : bool) = DoorB = DoorA in
                              let (_x_9 : real) = if _x_8 then _x_6 else _x_7 in
                              let (_x_10 : real) = if _x_8 then 1000000 else 2000000 in
                              let (_x_11 : bool) = Stay = Swap in
                              let (_x_12 : real) = if _x_11 then _x_10 else 0 in
                              let (_x_13 : bool) = DoorC = DoorB in
                              let (_x_14 : bool) = DoorC = DoorA in
                              let (_x_15 : real) = if _x_14 then _x_6 else if _x_13 then _x_7 else 2 / 10
                              in
                              let (_x_16 : real)
                                  = if _x_14 then 1000000 else if _x_13 then 2000000 else 4000000
                              in
                              let (_x_17 : real) = if _x_11 then _x_16 else 0 in
                              let (_x_18 : real) = if _x_11 then 1000000 else 0 in
                              let (_x_19 : bool) = DoorA = DoorB in
                              let (_x_20 : bool) = DoorA = DoorC in
                              let (_x_21 : bool) = DoorB = DoorC in
                              let (_x_22 : bool) = Swap = Stay in
                              let (_x_23 : real) = if _x_22 then 1000000 else 0 in
                              let (_x_24 : real) = if _x_22 then _x_10 else 0 in
                              let (_x_25 : real) = if _x_22 then _x_16 else 0 in
                              (_x_0 >= 0)
                              && ((_x_1 >= 0)
                                  && ((_x_2 >= 0)
                                      && ((_x_3 >= 0)
                                          && ((_x_4 >= 0)
                                              && ((_x_5 >= 0)
                                                  && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1))))))
                              ==> _x_6 * _x_0 * 1000000 +. _x_9 * _x_0 * (if _x_8 then _x_10 else _x_12)
                                  +. _x_15 * _x_0 * (if _x_14 then _x_16 else _x_17)
                                  +. (_x_6 * _x_2 * (if _x_19 then 1000000 else _x_18)
                                      +. _x_9 * _x_2 * _x_10
                                      +. _x_15 * _x_2 * (if _x_13 then _x_16 else _x_17))
                                  +. (_x_6 * _x_4 * (if _x_20 then 1000000 else _x_18)
                                      +. _x_9 * _x_4 * (if _x_21 then _x_10 else _x_12)
                                      +. _x_15 * _x_4 * _x_16)
                                  +. (_x_6 * _x_1 * _x_23
                                      +. _x_9 * _x_1 * (if _x_8 then _x_24 else _x_10)
                                      +. _x_15 * _x_1 * (if _x_14 then _x_25 else _x_16)
                                      +. (_x_6 * _x_3 * (if _x_19 then _x_23 else 1000000)
                                          +. _x_9 * _x_3 * _x_24
                                          +. _x_15 * _x_3 * (if _x_13 then _x_25 else _x_16))
                                      +. (_x_6 * _x_5 * (if _x_20 then _x_23 else 1000000)
                                          +. _x_9 * _x_5 * (if _x_21 then _x_24 else _x_10)
                                          +. _x_15 * _x_5 * _x_25))
                                  <= 1400000
                          • simplify

                            into:
                            let (_x_0 : real) = sko_strategy_0 DoorA Stay in
                            let (_x_1 : real) = sko_strategy_0 DoorA Swap in
                            let (_x_2 : real) = sko_strategy_0 DoorB Stay in
                            let (_x_3 : real) = sko_strategy_0 DoorB Swap in
                            let (_x_4 : real) = sko_strategy_0 DoorC Stay in
                            let (_x_5 : real) = sko_strategy_0 DoorC Swap in
                            not
                            ((_x_0 >= 0) && (_x_1 >= 0) && (_x_2 >= 0) && (_x_3 >= 0) && (_x_4 >= 0)
                             && (_x_5 >= 0) && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1))
                            || (500000 * _x_0 +. 600000 * _x_2 +. 800000 * _x_4 +. 1400000 * _x_1
                                +. 1300000 * _x_3 +. 1100000 * _x_5 <= 1400000)
                            expansions:
                            []
                            rewrite_steps:
                              forward_chaining:
                              • Unsat
                              In [26]:
                              instance ( fun strategy -> Real.(
                                valid_strategy(strategy) &&
                                ( expected_reward_complex ( make_scenario_pmf pDoorsComplex strategy)
                                ) = 1400000.0 ) 
                              )
                              
                              Out[26]:
                              - : (door -> choice -> real) -> bool = <fun>
                              module CX : sig val strategy : door -> choice -> real end
                              
                              Instance (after 0 steps, 0.018s):
                              let strategy : door -> choice -> real =
                                fun (x_0 : door) ->
                                 fun (x_1 : choice) -> if (x_0 = DoorA) && (x_1 = Swap) then 1 else 0
                              
                              Instance
                              proof attempt
                              ground_instances:0
                              definitions:0
                              inductions:0
                              search_time:
                              0.018s
                              details:
                              Expand
                              smt_stats:
                              num checks:1
                              arith assert lower:8
                              arith tableau max rows:2
                              arith tableau max columns:15
                              arith pivots:2
                              rlimit count:2455
                              mk clause:6
                              datatype occurs check:5
                              mk bool var:12
                              arith assert upper:2
                              arith row summations:2
                              propagations:4
                              datatype accessor ax:5
                              arith num rows:2
                              num allocs:108492837
                              final checks:1
                              added eqs:2
                              del clause:6
                              arith eq adapter:2
                              time:0.008000
                              memory:20.720000
                              max memory:21.120000
                              Expand
                              • start[0.018s]
                                  let (_x_0 : real) = sko_strategy_0 DoorA Stay in
                                  let (_x_1 : real) = sko_strategy_0 DoorA Swap in
                                  let (_x_2 : real) = sko_strategy_0 DoorB Stay in
                                  let (_x_3 : real) = sko_strategy_0 DoorB Swap in
                                  let (_x_4 : real) = sko_strategy_0 DoorC Stay in
                                  let (_x_5 : real) = sko_strategy_0 DoorC Swap in
                                  let (_x_6 : real) = 5 / 10 in
                                  let (_x_7 : real) = 3 / 10 in
                                  let (_x_8 : bool) = DoorB = DoorA in
                                  let (_x_9 : real) = if _x_8 then _x_6 else _x_7 in
                                  let (_x_10 : real) = if _x_8 then 1000000 else 2000000 in
                                  let (_x_11 : bool) = Stay = Swap in
                                  let (_x_12 : real) = if _x_11 then _x_10 else 0 in
                                  let (_x_13 : bool) = DoorC = DoorB in
                                  let (_x_14 : bool) = DoorC = DoorA in
                                  let (_x_15 : real) = if _x_14 then _x_6 else if _x_13 then _x_7 else 2 / 10
                                  in
                                  let (_x_16 : real)
                                      = if _x_14 then 1000000 else if _x_13 then 2000000 else 4000000
                                  in
                                  let (_x_17 : real) = if _x_11 then _x_16 else 0 in
                                  let (_x_18 : real) = if _x_11 then 1000000 else 0 in
                                  let (_x_19 : bool) = DoorA = DoorB in
                                  let (_x_20 : bool) = DoorA = DoorC in
                                  let (_x_21 : bool) = DoorB = DoorC in
                                  let (_x_22 : bool) = Swap = Stay in
                                  let (_x_23 : real) = if _x_22 then 1000000 else 0 in
                                  let (_x_24 : real) = if _x_22 then _x_10 else 0 in
                                  let (_x_25 : real) = if _x_22 then _x_16 else 0 in
                                  (_x_0 >= 0)
                                  && ((_x_1 >= 0)
                                      && ((_x_2 >= 0)
                                          && ((_x_3 >= 0)
                                              && ((_x_4 >= 0)
                                                  && ((_x_5 >= 0)
                                                      && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1))))))
                                  && (_x_6 * _x_0 * 1000000 +. _x_9 * _x_0 * (if _x_8 then _x_10 else _x_12)
                                      +. _x_15 * _x_0 * (if _x_14 then _x_16 else _x_17)
                                      +. (_x_6 * _x_2 * (if _x_19 then 1000000 else _x_18)
                                          +. _x_9 * _x_2 * _x_10
                                          +. _x_15 * _x_2 * (if _x_13 then _x_16 else _x_17))
                                      +. (_x_6 * _x_4 * (if _x_20 then 1000000 else _x_18)
                                          +. _x_9 * _x_4 * (if _x_21 then _x_10 else _x_12)
                                          +. _x_15 * _x_4 * _x_16)
                                      +. (_x_6 * _x_1 * _x_23
                                          +. _x_9 * _x_1 * (if _x_8 then _x_24 else _x_10)
                                          +. _x_15 * _x_1 * (if _x_14 then _x_25 else _x_16)
                                          +. (_x_6 * _x_3 * (if _x_19 then _x_23 else 1000000)
                                              +. _x_9 * _x_3 * _x_24
                                              +. _x_15 * _x_3 * (if _x_13 then _x_25 else _x_16))
                                          +. (_x_6 * _x_5 * (if _x_20 then _x_23 else 1000000)
                                              +. _x_9 * _x_5 * (if _x_21 then _x_24 else _x_10)
                                              +. _x_15 * _x_5 * _x_25))
                                      = 1400000)
                              • simplify

                                into:
                                let (_x_0 : real) = sko_strategy_0 DoorA Stay in
                                let (_x_1 : real) = sko_strategy_0 DoorA Swap in
                                let (_x_2 : real) = sko_strategy_0 DoorB Stay in
                                let (_x_3 : real) = sko_strategy_0 DoorB Swap in
                                let (_x_4 : real) = sko_strategy_0 DoorC Stay in
                                let (_x_5 : real) = sko_strategy_0 DoorC Swap in
                                (_x_0 >= 0) && (_x_1 >= 0) && (_x_2 >= 0) && (_x_3 >= 0) && (_x_4 >= 0)
                                && (_x_5 >= 0) && (_x_0 +. _x_1 +. _x_2 +. _x_3 +. _x_4 +. _x_5 = 1)
                                && (500000 * _x_0 +. 600000 * _x_2 +. 800000 * _x_4 +. 1400000 * _x_1
                                    +. 1300000 * _x_3 +. 1100000 * _x_5 = 1400000)
                                expansions:
                                []
                                rewrite_steps:
                                  forward_chaining:
                                  • Sat (Some let strategy : door -> choice -> real = fun (x_0 : door) -> fun (x_1 : choice) -> if (x_0 = DoorA) && (x_1 = Swap) then (Q.of_nativeint (1n)) else (Q.of_nativeint (0n)) )

                                  More generally, this illustrates how we can use Imandra’s ability to reason about functional values and real arithmetic to formally prove and refute statements about probability distributions. These abilities allow us to formally analyse many kinds of scenarios requiring the ability to reason about random variables.