Another iteration on shortening the CHSH proof.

chsh_v3.lean

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Linarith

----------------- DEFINE PROBABILITY --------------------
structure Chance where
  p : Rat
  v : (p >= 0) ∧ (p <= 1)

def Chance.le (a b : Chance) : Bool := a.p <= b.p
infixl:45 " ≤ " => Chance.le
infixl:45 " <= " => Chance.le

theorem Chance.le_def (a b : Chance)
  : a.p <= b.p <-> (Chance.le a b)
  := by
  apply Iff.intro
  intro h
  simp [Chance.le]
  exact h
  intro h
  simp [Chance.le] at h
  exact h

def Chance.max (a b : Chance) : Chance :=
  match a <= b with
  | true => b
  | false => a

def Chance.ofBool (b : Bool) : Chance :=
  match b with
  | true => Chance.mk 1 (by trivial)
  | false => Chance.mk 0 (by trivial)

def Rat.lerp (t a b : Rat) : Rat := a + t * (b - a)
def Chance.lerp (t a b : Chance) : Chance :=
  Chance.mk
    (Rat.lerp t.p a.p b.p)
    (by
      induction t
      induction a
      induction b
      simp [Rat.lerp]
      apply And.intro
      nlinarith
      nlinarith
    )

theorem Chance.le_trans
  (a b c: Chance)
  (hab : a <= b)
  (hbc : b <= c)
  : (a <= c)
  := by
  simp [Chance.le] at hab
  simp [Chance.le] at hbc
  simp [Chance.le]
  apply Rat.le_trans hab hbc

def Chance.avg (a b : Chance) : Chance :=
  Chance.lerp (Chance.mk 0.5 (by trivial)) a b
def Chance.avg4 (a b c d : Chance) : Chance :=
  Chance.avg (Chance.avg a b) (Chance.avg c d)

theorem Chance.lerp_le_max(t a b : Chance)
  : (Chance.lerp t a b) ≤ (Chance.max a b)
  := by
  induction' t with cp cv
  cases h : a ≤ b
  <;>
  {
    unfold Chance.max
    simp [h]
    simp [Chance.le] at h
    simp [Chance.le, Chance.lerp, Rat.lerp]
    nlinarith
  }

theorem Chance.le_max_from_le_lerp(t a b c : Chance)
  (h : (Chance.max a b) ≤ c)
  : (Chance.lerp t a b) ≤ c
  := by
  apply Chance.le_trans (Chance.lerp t a b) (Chance.max a b) c
  apply Chance.lerp_le_max
  exact h


----------------- DEFINE CHSH GAME --------------------

def chsh_win_rule
  (a b x y : Bool)
  : Bool
  := (xor a b) = (x && y)
def play_chsh_case
  (a b : Bool -> Bool)
  (x y : Bool)
  : Chance
  := Chance.ofBool (chsh_win_rule (a x) (b y) x y)

inductive RandStrat where
  | always (value : Bool -> Bool)
  | rand (chance : Chance) (left : RandStrat) (right : RandStrat)

def chsh_win_rate_det (a b : Bool -> Bool) : Chance :=
  Chance.avg4
    (play_chsh_case a b false false)
    (play_chsh_case a b false true)
    (play_chsh_case a b true false)
    (play_chsh_case a b true true)

def chsh_win_rate_semidet
  (a : Bool -> Bool)
  (br : RandStrat)
  : Chance
  :=
  match br with
  | RandStrat.always b => chsh_win_rate_det a b
  | RandStrat.rand p left right => Chance.lerp
    p
    (chsh_win_rate_semidet a left)
    (chsh_win_rate_semidet a right)

def chsh_win_rate
  (ar br : RandStrat)
  : Chance
  :=
  match ar with
  | RandStrat.always a => chsh_win_rate_semidet a br
  | RandStrat.rand p left right =>
    Chance.lerp
      p
      (chsh_win_rate left br)
      (chsh_win_rate right br)

----------------- LEMMAS --------------------
theorem CHSH_inequality_for_det_strats
  (alice_strategy bob_strategy : Bool → Bool)
  : (chsh_win_rate_det alice_strategy bob_strategy) ≤ (Chance.mk 0.75 (by trivial))
  := by
  unfold chsh_win_rate_det
  unfold play_chsh_case
  unfold chsh_win_rule
  cases (alice_strategy false) <;>
  cases (alice_strategy true) <;>
  cases (bob_strategy false) <;>
  cases (bob_strategy true) <;>
  {
    simp [xor, Chance.ofBool, Chance.avg, Chance.lerp, Chance.le_def]
    repeat trivial
  }

theorem CHSH_inequality_for_semidet_strats
  (a : Bool -> Bool)
  (br : RandStrat)
  : chsh_win_rate_semidet a br ≤ Chance.mk 0.75 (by trivial)
  := by
  cases br with
  | always b =>
    simp [chsh_win_rate_semidet]
    apply CHSH_inequality_for_det_strats
  | rand b_chance b_left b_right =>
    simp [chsh_win_rate_semidet]
    apply Chance.le_max_from_le_lerp
    unfold Chance.max
    cases cr : (chsh_win_rate_semidet a b_left ≤ chsh_win_rate_semidet a b_right) <;>
    {
      simp
      apply CHSH_inequality_for_semidet_strats
    }

----------------- PROVE CHSH INEQUALITY --------------------
theorem CHSH_inequality
  (ar : RandStrat)
  (br : RandStrat)
  : chsh_win_rate ar br ≤ Chance.mk 0.75 (by trivial)
  := by
  cases ar with
  | always a =>
    simp [chsh_win_rate]
    apply CHSH_inequality_for_semidet_strats
  | rand b_chance b_left b_right =>
    simp [chsh_win_rate]
    apply Chance.le_max_from_le_lerp
    unfold Chance.max
    cases cr : (chsh_win_rate b_left br ≤ chsh_win_rate b_right br) <;>
    {
      simp
      apply CHSH_inequality
    }