# Shortening a 4-levels-of-match lean4 proof of the CHSH inequality

In the CHSH game, Alice (Bob) is given the value $$x$$ ($$y$$) and needs to pick a value $$a$$ ($$b$$) such that $$a \oplus b = xy$$. The CHSH inequality proves they can win at most 75% of the time with classical strategies if $$x$$ and $$y$$ are being chosen at random andthe players can't communicate during the game. (Whereas quantum strategies can win 85% of the time.)

Currently I've just proven the inequality for deterministic strategies, but the proof strikes me as repetitive in a way that can probably be fixed. All I do is just brute force evaluate all 16 possible deterministic strategies. The result is this big tree of "cases" blocks with every leaf just being "trivial" since at that point it's just a basic arithmetic evaluation. Is there a way to say, like, "for each assignment of these four expressions, it will be trivial"?

Here's the current proof:

def xor (a b : Bool) : Bool :=
match a with
| false => b
| true => !b

infixl:65 " ⊕ " => xor

def strat_wins_case
(a b : Bool → Bool)
(x y : Bool)
: Bool
:= ((a x) ⊕ (b y)) = (x && y)

def bool_2_nat (b : Bool) : Nat :=
match b with
| false => 0
| true => 1

def win_count (a b : Bool → Bool) : Nat
:= ((bool_2_nat (strat_wins_case a b false false))
+ (bool_2_nat (strat_wins_case a b false true))
+ (bool_2_nat (strat_wins_case a b true false))
+ (bool_2_nat (strat_wins_case a b true true)))

theorem CHSH_inequality(a b : Bool → Bool) : win_count a b ≤ 3 := by
unfold win_count
unfold strat_wins_case
cases (a false) with
| false =>
cases (a true) with
| false =>
cases (b false) with
| false =>
cases (b true) with
| false =>
trivial
| true =>
trivial
| true =>
cases (b true) with
| false =>
trivial
| true =>
trivial
| true =>
cases (b false) with
| false =>
cases (b true) with
| false =>
trivial
| true =>
trivial
| true =>
cases (b true) with
| false =>
trivial
| true =>
trivial
| true =>
cases (a true) with
| false =>
cases (b false) with
| false =>
cases (b true) with
| false =>
trivial
| true =>
trivial
| true =>
cases (b true) with
| false =>
trivial
| true =>
trivial
| true =>
cases (b false) with
| false =>
cases (b true) with
| false =>
trivial
| true =>
trivial
| true =>
cases (b true) with
| false =>
trivial
| true =>
trivial


The combinator tactic <;> is useful here since you are doing the same steps in each branch.

theorem CHSH_inequality(a b : Bool → Bool) : win_count a b ≤ 3 := by
unfold win_count
unfold strat_wins_case
cases (a false) <;> cases (a true) <;> cases (b false) <;> cases (b true) <;> trivial

• Could you link to the documentation on <;>? It's not very searchable. Dec 4, 2023 at 1:35
• @CraigGidney Done (sort of). Dec 4, 2023 at 3:04

Everything here is finite, so you can invoke the decidability checker, decide:

import Mathlib.Data.Fintype.Pi

infixl:65 " ⊕ " => xor

def strat_wins_case
(a b : Bool → Bool)
(x y : Bool) :
Bool :=
((a x) ⊕ (b y)) = (x && y)

def bool_2_nat : Bool → Nat
| false => 0
| true => 1

def win_count (a b : Bool → Bool) : Nat :=
((bool_2_nat (strat_wins_case a b false false))
+ (bool_2_nat (strat_wins_case a b false true))
+ (bool_2_nat (strat_wins_case a b true false))
+ (bool_2_nat (strat_wins_case a b true true)))

theorem CHSH_inequality (a b : Bool → Bool) : win_count a b ≤ 3 := by
revert a b
decide


I deleted xor since it was already defined in a prerequisite to the imports I am using, but you can reintroduce it under a different name if you need your own definition.

• By the way, you can also define win_count more quickly as the size of the "winning set": def win_count (a b : Bool → Bool) := (Finset.univ.filter (fun p : Bool × Bool => strat_wins_case a b p.1 p.2)).card. You don't need bool_2_nat for that. (You do need a few imports, I'll let you figure out which.) Dec 6, 2023 at 4:50