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 :
type t = A | B | C
let sum = (f) => f(A) + f(B) + f(C)

Out:
type t = A | B | C
val sum : (t -> int) -> int = <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 :
instance( (f) => f(A) > 0 && f(B) > 0 && sum(f) == 42 )

Out:
- : (t -> int) -> bool = <fun>
module CX : sig val f : t -> int end

Instance (after 0 steps, 0.034s):
let f = function
| B -> 1
| C -> 0
| _ -> 41


Instance
proof attempt
ground_instances0
definitions0
inductions0
search_time
0.034s
details
Expand
smt_stats
 num checks 1 arith-make-feasible 2 arith-max-columns 9 rlimit count 356 mk clause 4 datatype occurs check 3 mk bool var 8 arith-lower 1 propagations 2 arith-max-rows 2 datatype accessor ax 3 num allocs 8.47751e+08 final checks 1 added eqs 3 del clause 4 arith eq adapter 1 arith-upper 3 memory 22.2 max memory 24.71
Expand
• start[0.034s]
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 = function | B -> 1 | C -> 0 | _ -> 41 )

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.

# 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 : verify ( (strategy) => Real.({ valid_strategy(strategy) ==> ( expected_reward ( make_scenario_pmf(pDoorsEqual,strategy) ) <= 1000000.0 / 3.0 ) }))  Out: - : (door -> choice -> real) -> bool = <fun> module CX : sig val strategy : door -> choice -> real end  Counterexample (after 0 steps, 0.021s): let strategy x_0 x_1 = match (x_0, x_1) with | (DoorB, Stay) -> (Real.mk_of_string "999997/1000000") | (DoorB, Swap) -> (Real.mk_of_string "3/1000000") | _ -> 0.0  Refuted proof attempt ground_instances0 definitions0 inductions0 search_time 0.021s details Expand smt_stats  num checks 1 arith-make-feasible 2 arith-max-columns 12 rlimit count 1820 mk clause 4 datatype occurs check 5 mk bool var 13 arith-lower 1 propagations 2 arith-max-rows 2 datatype accessor ax 5 num allocs 9.18133e+08 final checks 1 added eqs 3 del clause 4 arith eq adapter 1 arith-upper 8 memory 24.46 max memory 24.86 Expand • start[0.021s] 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 : real) = if Stay = Stay then 1000000 else 0 in let (_x_10 : bool) = DoorA = DoorA in let (_x_11 : bool) = DoorB = DoorA in let (_x_12 : bool) = DoorC = DoorA in let (_x_13 : real) = _x_6 *. _x_2 in let (_x_14 : bool) = DoorA = DoorB in let (_x_15 : bool) = DoorB = DoorB in let (_x_16 : bool) = DoorC = DoorB in let (_x_17 : real) = _x_6 *. _x_4 in let (_x_18 : bool) = DoorA = DoorC in let (_x_19 : bool) = DoorB = DoorC in let (_x_20 : bool) = DoorC = DoorC in let (_x_21 : real) = _x_6 *. _x_1 in let (_x_22 : real) = if Swap = Swap then 1000000 else 0 in let (_x_23 : real) = if Swap = Stay then 1000000 else 0 in let (_x_24 : real) = _x_6 *. _x_3 in let (_x_25 : 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 *. (if _x_10 then _x_9 else _x_8) +. _x_7 *. (if _x_11 then _x_9 else _x_8) +. _x_7 *. (if _x_12 then _x_9 else _x_8) +. (_x_13 *. (if _x_14 then _x_9 else _x_8) +. _x_13 *. (if _x_15 then _x_9 else _x_8) +. _x_13 *. (if _x_16 then _x_9 else _x_8)) +. (_x_17 *. (if _x_18 then _x_9 else _x_8) +. _x_17 *. (if _x_19 then _x_9 else _x_8) +. _x_17 *. (if _x_20 then _x_9 else _x_8)) +. (_x_21 *. (if _x_10 then _x_23 else _x_22) +. _x_21 *. (if _x_11 then _x_23 else _x_22) +. _x_21 *. (if _x_12 then _x_23 else _x_22) +. (_x_24 *. (if _x_14 then _x_23 else _x_22) +. _x_24 *. (if _x_15 then _x_23 else _x_22) +. _x_24 *. (if _x_16 then _x_23 else _x_22)) +. (_x_25 *. (if _x_18 then _x_23 else _x_22) +. _x_25 *. (if _x_19 then _x_23 else _x_22) +. _x_25 *. (if _x_20 then _x_23 else _x_22)))) <=. (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 x_0 x_1 = match (x_0, x_1) with | (DoorB, Stay) -> (Real.mk_of_string "999997/1000000") | (DoorB, Swap) -> (Real.mk_of_string "3/1000000") | _ -> 0.0 ) 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 : expected_reward( make_scenario_pmf(pDoorsEqual, CX.strategy) )  Out: - : 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 :
let random_then_swap_strategy = (door : door,choice) =>
switch(door,choice){ | (_,Swap) => Real.(1.0 / 3.0) | _ => 0.0 };
expected_reward(
make_scenario_pmf(pDoorsEqual,random_then_swap_strategy)
)

Out:
val random_then_swap_strategy : door -> choice -> real = <fun>
- : 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 :
verify ( (strategy) => Real.({
valid_strategy(strategy) ==>
( expected_reward (
make_scenario_pmf(pDoorsEqual,strategy)
) <= 2000000.0 / 3.0 )
}))

Out:
- : (door -> choice -> real) -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.022s
details
Expand
smt_stats
 num checks 1 arith-make-feasible 1 arith-max-columns 12 rlimit count 1776 mk clause 6 mk bool var 13 arith-max-rows 2 conflicts 1 datatype accessor ax 5 arith-bound-propagations-lp 2 num allocs 9.51434e+08 added eqs 2 arith eq adapter 1 arith-upper 7 memory 27.17 max memory 27.57
Expand
• start[0.022s]
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 : real) = if Stay = Stay then 1000000 else 0 in
let (_x_10 : bool) = DoorA = DoorA in
let (_x_11 : bool) = DoorB = DoorA in
let (_x_12 : bool) = DoorC = DoorA in
let (_x_13 : real) = _x_6 *. _x_2 in
let (_x_14 : bool) = DoorA = DoorB in
let (_x_15 : bool) = DoorB = DoorB in
let (_x_16 : bool) = DoorC = DoorB in
let (_x_17 : real) = _x_6 *. _x_4 in
let (_x_18 : bool) = DoorA = DoorC in
let (_x_19 : bool) = DoorB = DoorC in
let (_x_20 : bool) = DoorC = DoorC in
let (_x_21 : real) = _x_6 *. _x_1 in
let (_x_22 : real) = if Swap = Swap then 1000000 else 0 in
let (_x_23 : real) = if Swap = Stay then 1000000 else 0 in
let (_x_24 : real) = _x_6 *. _x_3 in
let (_x_25 : 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 *. (if _x_10 then _x_9 else _x_8)
+. _x_7 *. (if _x_11 then _x_9 else _x_8)
+. _x_7 *. (if _x_12 then _x_9 else _x_8)
+. (_x_13 *. (if _x_14 then _x_9 else _x_8)
+. _x_13 *. (if _x_15 then _x_9 else _x_8)
+. _x_13 *. (if _x_16 then _x_9 else _x_8))
+. (_x_17 *. (if _x_18 then _x_9 else _x_8)
+. _x_17 *. (if _x_19 then _x_9 else _x_8)
+. _x_17 *. (if _x_20 then _x_9 else _x_8))
+. (_x_21 *. (if _x_10 then _x_23 else _x_22)
+. _x_21 *. (if _x_11 then _x_23 else _x_22)
+. _x_21 *. (if _x_12 then _x_23 else _x_22)
+. (_x_24 *. (if _x_14 then _x_23 else _x_22)
+. _x_24 *. (if _x_15 then _x_23 else _x_22)
+. _x_24 *. (if _x_16 then _x_23 else _x_22))
+. (_x_25 *. (if _x_18 then _x_23 else _x_22)
+. _x_25 *. (if _x_19 then _x_23 else _x_22)
+. _x_25 *. (if _x_20 then _x_23 else _x_22))))
<=. (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 :
instance ( (strategy) => Real.({
valid_strategy(strategy) &&
( expected_reward (
make_scenario_pmf(pDoorsEqual,strategy)
) == 2000000.0 / 3.0 )
}))

Out:
- : (door -> choice -> real) -> bool = <fun>
module CX : sig val strategy : door -> choice -> real end

Instance (after 0 steps, 0.027s):
let strategy x_0 x_1 =
match (x_0, x_1) with
| (DoorB, Swap) -> 1.0
| _ -> 0.0


Instance
proof attempt
ground_instances0
definitions0
inductions0
search_time
0.027s
details
Expand
smt_stats
 num checks 1 arith-make-feasible 2 arith-max-columns 13 rlimit count 1794 mk clause 8 datatype occurs check 5 mk bool var 15 arith-lower 2 propagations 3 arith-max-rows 3 datatype accessor ax 5 arith-bound-propagations-lp 1 num allocs 1.03606e+09 final checks 1 added eqs 4 del clause 8 arith eq adapter 2 arith-upper 8 memory 24.74 max memory 27.57
Expand
• start[0.027s]
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 : real) = if Stay = Stay then 1000000 else 0 in
let (_x_10 : bool) = DoorA = DoorA in
let (_x_11 : bool) = DoorB = DoorA in
let (_x_12 : bool) = DoorC = DoorA in
let (_x_13 : real) = _x_6 *. _x_2 in
let (_x_14 : bool) = DoorA = DoorB in
let (_x_15 : bool) = DoorB = DoorB in
let (_x_16 : bool) = DoorC = DoorB in
let (_x_17 : real) = _x_6 *. _x_4 in
let (_x_18 : bool) = DoorA = DoorC in
let (_x_19 : bool) = DoorB = DoorC in
let (_x_20 : bool) = DoorC = DoorC in
let (_x_21 : real) = _x_6 *. _x_1 in
let (_x_22 : real) = if Swap = Swap then 1000000 else 0 in
let (_x_23 : real) = if Swap = Stay then 1000000 else 0 in
let (_x_24 : real) = _x_6 *. _x_3 in
let (_x_25 : 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 *. (if _x_10 then _x_9 else _x_8)
+. _x_7 *. (if _x_11 then _x_9 else _x_8)
+. _x_7 *. (if _x_12 then _x_9 else _x_8)
+. (_x_13 *. (if _x_14 then _x_9 else _x_8)
+. _x_13 *. (if _x_15 then _x_9 else _x_8)
+. _x_13 *. (if _x_16 then _x_9 else _x_8))
+. (_x_17 *. (if _x_18 then _x_9 else _x_8)
+. _x_17 *. (if _x_19 then _x_9 else _x_8)
+. _x_17 *. (if _x_20 then _x_9 else _x_8))
+. (_x_21 *. (if _x_10 then _x_23 else _x_22)
+. _x_21 *. (if _x_11 then _x_23 else _x_22)
+. _x_21 *. (if _x_12 then _x_23 else _x_22)
+. (_x_24 *. (if _x_14 then _x_23 else _x_22)
+. _x_24 *. (if _x_15 then _x_23 else _x_22)
+. _x_24 *. (if _x_16 then _x_23 else _x_22))
+. (_x_25 *. (if _x_18 then _x_23 else _x_22)
+. _x_25 *. (if _x_19 then _x_23 else _x_22)
+. _x_25 *. (if _x_20 then _x_23 else _x_22)))
= 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 x_0 x_1 = match (x_0, x_1) with | (DoorB, Swap) -> 1.0 | _ -> 0.0 )

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 :
let pDoorsBiased = (door : door) => Real.(
switch (door){
| DoorA => 3.0 / 5.0
| DoorB | DoorC => 1.0 / 5.0
}
);

valid_door_pmf(pDoorsBiased)

Out:
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 :
verify ( (strategy) => Real.({
valid_strategy(strategy) ==>
( expected_reward (
make_scenario_pmf(pDoorsBiased,strategy)
) <= 2000000.0 / 3.0 )
}))

Out:
- : (door -> choice -> real) -> bool = <fun>
module CX : sig val strategy : door -> choice -> real end

Counterexample (after 0 steps, 0.037s):
let strategy x_0 x_1 =
match (x_0, x_1) with
| (DoorA, Swap) -> (Real.mk_of_string "399997/1200000")
| (DoorB, Swap) -> (Real.mk_of_string "800003/1200000")
| _ -> 0.0


Refuted
proof attempt
ground_instances0
definitions0
inductions0
search_time
0.037s
details
Expand
smt_stats
 num checks 1 arith-make-feasible 2 arith-max-columns 12 rlimit count 2074 mk clause 4 datatype occurs check 5 mk bool var 13 arith-lower 1 propagations 2 arith-max-rows 2 datatype accessor ax 5 num allocs 1.07426e+09 final checks 1 added eqs 3 del clause 4 arith eq adapter 1 arith-upper 8 memory 27.62 max memory 28.02
Expand
• start[0.037s]
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 /. 5 in
let (_x_7 : real) = 3 /. 5 in
let (_x_8 : bool) = DoorA = DoorA in
let (_x_9 : real) = if _x_8 then _x_7 else _x_6 in
let (_x_10 : real) = if Stay = Swap then 1000000 else 0 in
let (_x_11 : real) = if Stay = Stay then 1000000 else 0 in
let (_x_12 : bool) = DoorB = DoorA in
let (_x_13 : real) = if _x_12 then _x_7 else _x_6 in
let (_x_14 : bool) = DoorC = DoorA in
let (_x_15 : real) = if _x_14 then _x_7 else _x_6 in
let (_x_16 : bool) = DoorA = DoorB in
let (_x_17 : bool) = DoorB = DoorB in
let (_x_18 : bool) = DoorC = DoorB in
let (_x_19 : bool) = DoorA = DoorC in
let (_x_20 : bool) = DoorB = DoorC in
let (_x_21 : bool) = DoorC = DoorC in
let (_x_22 : real) = if Swap = Swap then 1000000 else 0 in
let (_x_23 : real) = if Swap = Stay then 1000000 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_9 *. _x_0 *. (if _x_8 then _x_11 else _x_10)
+. _x_13 *. _x_0 *. (if _x_12 then _x_11 else _x_10)
+. _x_15 *. _x_0 *. (if _x_14 then _x_11 else _x_10)
+. (_x_9 *. _x_2 *. (if _x_16 then _x_11 else _x_10)
+. _x_13 *. _x_2 *. (if _x_17 then _x_11 else _x_10)
+. _x_15 *. _x_2 *. (if _x_18 then _x_11 else _x_10))
+. (_x_9 *. _x_4 *. (if _x_19 then _x_11 else _x_10)
+. _x_13 *. _x_4 *. (if _x_20 then _x_11 else _x_10)
+. _x_15 *. _x_4 *. (if _x_21 then _x_11 else _x_10))
+. (_x_9 *. _x_1 *. (if _x_8 then _x_23 else _x_22)
+. _x_13 *. _x_1 *. (if _x_12 then _x_23 else _x_22)
+. _x_15 *. _x_1 *. (if _x_14 then _x_23 else _x_22)
+. (_x_9 *. _x_3 *. (if _x_16 then _x_23 else _x_22)
+. _x_13 *. _x_3 *. (if _x_17 then _x_23 else _x_22)
+. _x_15 *. _x_3 *. (if _x_18 then _x_23 else _x_22))
+. (_x_9 *. _x_5 *. (if _x_19 then _x_23 else _x_22)
+. _x_13 *. _x_5 *. (if _x_20 then _x_23 else _x_22)
+. _x_15 *. _x_5 *. (if _x_21 then _x_23 else _x_22))))
<=. (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 x_0 x_1 = match (x_0, x_1) with | (DoorA, Swap) -> (Real.mk_of_string "399997/1200000") | (DoorB, Swap) -> (Real.mk_of_string "800003/1200000") | _ -> 0.0 )

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 :
let aStayStrategy = (door,choice) =>
switch(door,choice){ | (DoorA,Stay) => 1.0 | _ => 0.0 };
expected_reward(
make_scenario_pmf(pDoorsBiased,aStayStrategy)
);
let cSwapStrategy = (door,choice) =>
switch(door,choice){ | (DoorC,Swap) => 1.0 | _ => 0.0 };
expected_reward(
make_scenario_pmf(pDoorsBiased,cSwapStrategy)
);

Out:
val aStayStrategy : door -> choice -> real = <fun>
- : real = 600000
val cSwapStrategy : door -> choice -> real = <fun>
- : 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 :
verify ( (strategy) => Real.({
valid_strategy(strategy) ==>
( expected_reward (
make_scenario_pmf(pDoorsBiased,strategy)
) <= 800000.0 )
}))

Out:
- : (door -> choice -> real) -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.043s
details
Expand
smt_stats
 num checks 1 arith-make-feasible 1 arith-max-columns 12 rlimit count 2028 mk clause 6 mk bool var 13 arith-max-rows 2 conflicts 1 datatype accessor ax 5 arith-bound-propagations-lp 2 num allocs 1.19771e+09 added eqs 2 arith eq adapter 1 arith-upper 7 memory 22.39 max memory 28.02
Expand
• start[0.043s]
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 /. 5 in
let (_x_7 : real) = 3 /. 5 in
let (_x_8 : bool) = DoorA = DoorA in
let (_x_9 : real) = if _x_8 then _x_7 else _x_6 in
let (_x_10 : real) = if Stay = Swap then 1000000 else 0 in
let (_x_11 : real) = if Stay = Stay then 1000000 else 0 in
let (_x_12 : bool) = DoorB = DoorA in
let (_x_13 : real) = if _x_12 then _x_7 else _x_6 in
let (_x_14 : bool) = DoorC = DoorA in
let (_x_15 : real) = if _x_14 then _x_7 else _x_6 in
let (_x_16 : bool) = DoorA = DoorB in
let (_x_17 : bool) = DoorB = DoorB in
let (_x_18 : bool) = DoorC = DoorB in
let (_x_19 : bool) = DoorA = DoorC in
let (_x_20 : bool) = DoorB = DoorC in
let (_x_21 : bool) = DoorC = DoorC in
let (_x_22 : real) = if Swap = Swap then 1000000 else 0 in
let (_x_23 : real) = if Swap = Stay then 1000000 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_9 *. _x_0 *. (if _x_8 then _x_11 else _x_10)
+. _x_13 *. _x_0 *. (if _x_12 then _x_11 else _x_10)
+. _x_15 *. _x_0 *. (if _x_14 then _x_11 else _x_10)
+. (_x_9 *. _x_2 *. (if _x_16 then _x_11 else _x_10)
+. _x_13 *. _x_2 *. (if _x_17 then _x_11 else _x_10)
+. _x_15 *. _x_2 *. (if _x_18 then _x_11 else _x_10))
+. (_x_9 *. _x_4 *. (if _x_19 then _x_11 else _x_10)
+. _x_13 *. _x_4 *. (if _x_20 then _x_11 else _x_10)
+. _x_15 *. _x_4 *. (if _x_21 then _x_11 else _x_10))
+. (_x_9 *. _x_1 *. (if _x_8 then _x_23 else _x_22)
+. _x_13 *. _x_1 *. (if _x_12 then _x_23 else _x_22)
+. _x_15 *. _x_1 *. (if _x_14 then _x_23 else _x_22)
+. (_x_9 *. _x_3 *. (if _x_16 then _x_23 else _x_22)
+. _x_13 *. _x_3 *. (if _x_17 then _x_23 else _x_22)
+. _x_15 *. _x_3 *. (if _x_18 then _x_23 else _x_22))
+. (_x_9 *. _x_5 *. (if _x_19 then _x_23 else _x_22)
+. _x_13 *. _x_5 *. (if _x_20 then _x_23 else _x_22)
+. _x_15 *. _x_5 *. (if _x_21 then _x_23 else _x_22))))
<=. 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 :
let pDoorsComplex = (door : door) => Real.(
switch (door){
| DoorA => 5.0 / 10.0
| DoorB => 3.0 / 10.0
| DoorC => 2.0 / 10.0
}
);

let reward_complex = (scenario) => {
let prize = switch(scenario.prize) {
| DoorA => 1000000.
| DoorB => 2000000.
| DoorC => 4000000.
};
if( scenario.prize == scenario.first_guess ) {
if(scenario.choice == Stay) prize else 0.0;
} else {
if(scenario.choice == Swap) prize else 0.0;
}
};

let expected_reward_complex : (scenario => real) => real =
(scenario_pmf) => Real.({
let pr = (s) => scenario_pmf(s) * reward_complex(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)
};
avg(Stay) + avg(Swap)
})

Out:
val pDoorsComplex : door -> real = <fun>
val reward_complex : scenario -> real = <fun>
val expected_reward_complex : (scenario -> real) -> real = <fun>

In :
verify ( (strategy) => Real.({
valid_strategy(strategy) ==>
( expected_reward_complex (
make_scenario_pmf(pDoorsComplex,strategy)
) <= 1400000.0 )
}))

Out:
- : (door -> choice -> real) -> bool = <fun>

Proved
proof
ground_instances0
definitions0
inductions0
search_time
0.026s
details
Expand
smt_stats
 num checks 1 arith-make-feasible 2 arith-max-columns 12 arith-conflicts 1 rlimit count 2473 mk clause 4 mk bool var 13 arith-lower 1 propagations 2 arith-max-rows 2 conflicts 1 datatype accessor ax 5 num allocs 1.26878e+09 added eqs 3 arith eq adapter 1 arith-upper 8 memory 23.08 max memory 28.02
Expand
• start[0.026s]
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) = 2 /. 10 in
let (_x_7 : real) = 3 /. 10 in
let (_x_8 : bool) = DoorA = DoorB in
let (_x_9 : real) = 5 /. 10 in
let (_x_10 : bool) = DoorA = DoorA in
let (_x_11 : real) = if _x_10 then _x_9 else if _x_8 then _x_7 else _x_6 in
let (_x_12 : real)
= if _x_10 then 1000000 else if _x_8 then 2000000 else 4000000
in
let (_x_13 : bool) = Stay = Swap in
let (_x_14 : real) = if _x_13 then _x_12 else 0 in
let (_x_15 : bool) = Stay = Stay in
let (_x_16 : real) = if _x_15 then _x_12 else 0 in
let (_x_17 : bool) = DoorB = DoorB in
let (_x_18 : bool) = DoorB = DoorA in
let (_x_19 : real) = if _x_18 then _x_9 else if _x_17 then _x_7 else _x_6
in
let (_x_20 : real)
= if _x_18 then 1000000 else if _x_17 then 2000000 else 4000000
in
let (_x_21 : real) = if _x_13 then _x_20 else 0 in
let (_x_22 : real) = if _x_15 then _x_20 else 0 in
let (_x_23 : bool) = DoorC = DoorB in
let (_x_24 : bool) = DoorC = DoorA in
let (_x_25 : real) = if _x_24 then _x_9 else if _x_23 then _x_7 else _x_6
in
let (_x_26 : real)
= if _x_24 then 1000000 else if _x_23 then 2000000 else 4000000
in
let (_x_27 : real) = if _x_13 then _x_26 else 0 in
let (_x_28 : real) = if _x_15 then _x_26 else 0 in
let (_x_29 : bool) = DoorA = DoorC in
let (_x_30 : bool) = DoorB = DoorC in
let (_x_31 : bool) = DoorC = DoorC in
let (_x_32 : bool) = Swap = Swap in
let (_x_33 : real) = if _x_32 then _x_12 else 0 in
let (_x_34 : bool) = Swap = Stay in
let (_x_35 : real) = if _x_34 then _x_12 else 0 in
let (_x_36 : real) = if _x_32 then _x_20 else 0 in
let (_x_37 : real) = if _x_34 then _x_20 else 0 in
let (_x_38 : real) = if _x_32 then _x_26 else 0 in
let (_x_39 : real) = if _x_34 then _x_26 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_11 *. _x_0 *. (if _x_10 then _x_16 else _x_14)
+. _x_19 *. _x_0 *. (if _x_18 then _x_22 else _x_21)
+. _x_25 *. _x_0 *. (if _x_24 then _x_28 else _x_27)
+. (_x_11 *. _x_2 *. (if _x_8 then _x_16 else _x_14)
+. _x_19 *. _x_2 *. (if _x_17 then _x_22 else _x_21)
+. _x_25 *. _x_2 *. (if _x_23 then _x_28 else _x_27))
+. (_x_11 *. _x_4 *. (if _x_29 then _x_16 else _x_14)
+. _x_19 *. _x_4 *. (if _x_30 then _x_22 else _x_21)
+. _x_25 *. _x_4 *. (if _x_31 then _x_28 else _x_27))
+. (_x_11 *. _x_1 *. (if _x_10 then _x_35 else _x_33)
+. _x_19 *. _x_1 *. (if _x_18 then _x_37 else _x_36)
+. _x_25 *. _x_1 *. (if _x_24 then _x_39 else _x_38)
+. (_x_11 *. _x_3 *. (if _x_8 then _x_35 else _x_33)
+. _x_19 *. _x_3 *. (if _x_17 then _x_37 else _x_36)
+. _x_25 *. _x_3 *. (if _x_23 then _x_39 else _x_38))
+. (_x_11 *. _x_5 *. (if _x_29 then _x_35 else _x_33)
+. _x_19 *. _x_5 *. (if _x_30 then _x_37 else _x_36)
+. _x_25 *. _x_5 *. (if _x_31 then _x_39 else _x_38))))
<=. 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 :
instance ( (strategy) => Real.({
valid_strategy(strategy) &&
( expected_reward_complex (
make_scenario_pmf(pDoorsComplex,strategy)
) == 1400000.0 )
}))

Out:
- : (door -> choice -> real) -> bool = <fun>
module CX : sig val strategy : door -> choice -> real end

Instance (after 0 steps, 0.019s):
let strategy x_0 x_1 =
match (x_0, x_1) with
| (DoorA, Swap) -> 1.0
| _ -> 0.0


Instance
proof attempt
ground_instances0
definitions0
inductions0
search_time
0.020s
details
Expand
smt_stats
 num checks 1 arith-make-feasible 2 arith-max-columns 13 rlimit count 2484 mk clause 8 datatype occurs check 5 mk bool var 16 arith-lower 2 propagations 4 arith-max-rows 3 datatype accessor ax 5 num allocs 1.30811e+09 final checks 1 added eqs 6 del clause 8 arith eq adapter 2 arith-upper 8 memory 25.84 max memory 28.02
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) = 2 /. 10 in
let (_x_7 : real) = 3 /. 10 in
let (_x_8 : bool) = DoorA = DoorB in
let (_x_9 : real) = 5 /. 10 in
let (_x_10 : bool) = DoorA = DoorA in
let (_x_11 : real) = if _x_10 then _x_9 else if _x_8 then _x_7 else _x_6 in
let (_x_12 : real)
= if _x_10 then 1000000 else if _x_8 then 2000000 else 4000000
in
let (_x_13 : bool) = Stay = Swap in
let (_x_14 : real) = if _x_13 then _x_12 else 0 in
let (_x_15 : bool) = Stay = Stay in
let (_x_16 : real) = if _x_15 then _x_12 else 0 in
let (_x_17 : bool) = DoorB = DoorB in
let (_x_18 : bool) = DoorB = DoorA in
let (_x_19 : real) = if _x_18 then _x_9 else if _x_17 then _x_7 else _x_6
in
let (_x_20 : real)
= if _x_18 then 1000000 else if _x_17 then 2000000 else 4000000
in
let (_x_21 : real) = if _x_13 then _x_20 else 0 in
let (_x_22 : real) = if _x_15 then _x_20 else 0 in
let (_x_23 : bool) = DoorC = DoorB in
let (_x_24 : bool) = DoorC = DoorA in
let (_x_25 : real) = if _x_24 then _x_9 else if _x_23 then _x_7 else _x_6
in
let (_x_26 : real)
= if _x_24 then 1000000 else if _x_23 then 2000000 else 4000000
in
let (_x_27 : real) = if _x_13 then _x_26 else 0 in
let (_x_28 : real) = if _x_15 then _x_26 else 0 in
let (_x_29 : bool) = DoorA = DoorC in
let (_x_30 : bool) = DoorB = DoorC in
let (_x_31 : bool) = DoorC = DoorC in
let (_x_32 : bool) = Swap = Swap in
let (_x_33 : real) = if _x_32 then _x_12 else 0 in
let (_x_34 : bool) = Swap = Stay in
let (_x_35 : real) = if _x_34 then _x_12 else 0 in
let (_x_36 : real) = if _x_32 then _x_20 else 0 in
let (_x_37 : real) = if _x_34 then _x_20 else 0 in
let (_x_38 : real) = if _x_32 then _x_26 else 0 in
let (_x_39 : real) = if _x_34 then _x_26 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_11 *. _x_0 *. (if _x_10 then _x_16 else _x_14)
+. _x_19 *. _x_0 *. (if _x_18 then _x_22 else _x_21)
+. _x_25 *. _x_0 *. (if _x_24 then _x_28 else _x_27)
+. (_x_11 *. _x_2 *. (if _x_8 then _x_16 else _x_14)
+. _x_19 *. _x_2 *. (if _x_17 then _x_22 else _x_21)
+. _x_25 *. _x_2 *. (if _x_23 then _x_28 else _x_27))
+. (_x_11 *. _x_4 *. (if _x_29 then _x_16 else _x_14)
+. _x_19 *. _x_4 *. (if _x_30 then _x_22 else _x_21)
+. _x_25 *. _x_4 *. (if _x_31 then _x_28 else _x_27))
+. (_x_11 *. _x_1 *. (if _x_10 then _x_35 else _x_33)
+. _x_19 *. _x_1 *. (if _x_18 then _x_37 else _x_36)
+. _x_25 *. _x_1 *. (if _x_24 then _x_39 else _x_38)
+. (_x_11 *. _x_3 *. (if _x_8 then _x_35 else _x_33)
+. _x_19 *. _x_3 *. (if _x_17 then _x_37 else _x_36)
+. _x_25 *. _x_3 *. (if _x_23 then _x_39 else _x_38))
+. (_x_11 *. _x_5 *. (if _x_29 then _x_35 else _x_33)
+. _x_19 *. _x_5 *. (if _x_30 then _x_37 else _x_36)
+. _x_25 *. _x_5 *. (if _x_31 then _x_39 else _x_38)))
= 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 x_0 x_1 = match (x_0, x_1) with | (DoorA, Swap) -> 1.0 | _ -> 0.0 )

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 us to formally analyse many kinds of scenarios requiring the ability to reason about random variables.