3
$\begingroup$

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
$\endgroup$

2 Answers 2

3
$\begingroup$

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
$\endgroup$
2
  • $\begingroup$ Could you link to the documentation on <;>? It's not very searchable. $\endgroup$ Dec 4, 2023 at 1:35
  • $\begingroup$ @CraigGidney Done (sort of). $\endgroup$
    – Jason Rute
    Dec 4, 2023 at 3:04
3
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ 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.) $\endgroup$
    – macbeth
    Dec 6, 2023 at 4:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.