Shorter proof of CHSH (377 lines instead of 514 lines)

chsh_v2.lean

import Mathlib
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Rat.Basic
import Mathlib.Data.Rat.Order

theorem le_pin (a b : Nat) (h1 : a <= b) (h2 : b <= a)
  : a = b
  := by
  apply Nat.eq_or_lt_of_le at h1
  cases h : (decide (a = b))
  simp at h
  simp [h] at h1
  absurd h1
  simp [h2]
  simp at h
  exact h

theorem offset_le (a b c : Nat) : (a <= b) <-> (a+c <= b+c)
  := by
  apply Iff.intro
  intro h
  simp
  exact h
  intro h
  simp at h
  exact h

theorem le_and_neq_gives_lt (a b : Nat) (h1 : a <= b) (h2 : not (a = b)) : a < b
  := by
  simp at h2
  apply Nat.eq_or_lt_of_le at h1
  simp [h2] at h1
  exact h1

theorem lt_succ_eq_le (a b : Nat) : (a < Nat.succ b) <-> (a <= b)
  := by
  apply Iff.intro
  intro h
  apply Nat.le_of_lt_succ
  exact h
  intro h1
  apply Nat.eq_or_lt_of_le at h1
  cases h3 : (decide (a = b))
  simp at h3
  simp [h3] at h1
  apply Nat.lt_of_succ_lt
  apply Nat.succ_lt_succ
  exact h1
  simp at h3
  simp [h3]

theorem add_preserves_le (a b c d : Nat) (hab : a <= b) (hcd : c <= d) : (a+c <= b+d)
  := by
  induction' b with b2 hb
  simp at hab
  simp [hab]
  exact hcd
  cases h : (decide (a < Nat.succ b2))
  {
    simp at h
    have h3 : a = Nat.succ b2
    apply le_pin _ _ hab h
    rw [h3]
    rw [Nat.add_comm, Nat.add_comm (Nat.succ b2)]
    rw [<- offset_le]
    exact hcd
  }
  {
    simp [lt_succ_eq_le] at h
    simp [h] at hb
    apply Nat.le_of_succ_le
    rw [Nat.succ_add, Nat.succ_le_succ_iff]
    exact hb
  }

theorem scale_le (a b c : Nat) (h : a != 0) : (b <= c) <-> (a*b <= a*c)
  := by
  apply Iff.intro
  intro habc
  induction' a
  simp
  simp
  exact habc
  intro habc
  induction' a
  absurd h
  simp
  simp at habc
  exact habc

theorem prod_preserves_le (a b c d : Nat) (hab : a <= b) (hcd : c <= d) : (a*c <= b*d)
  := by
  induction' b with b2 hb
  simp at hab
  simp [hab]
  cases h : (decide (a < Nat.succ b2))
  {
    have h1 : a = Nat.succ b2
    apply le_pin _ _ hab
    simp at h
    exact h
    rw [h1]
    rw [<- scale_le]
    exact hcd
    simp
  }
  {
    have h2 : a <= b2
    rw [<- lt_succ_eq_le]
    simp at h
    exact h
    rw [Nat.succ_mul, <- Nat.add_zero (a * c)]
    apply add_preserves_le
    simp [h2] at hb
    exact hb
    simp
  }

structure Odds where
  lose : Nat
  win : Nat
  valid : (lose != 0) ∨ (win != 0)

inductive
RandStrat where
  | always (value : Bool -> Bool)
  | rand (odds : Odds) (left : RandStrat) (right : RandStrat)

def Odds.le (a b : Odds) : Bool := a.win * b.lose <= b.win * a.lose
theorem Odds.le_def (a b : Odds)
  : (a.win * b.lose <= b.win * a.lose) <-> (Odds.le a b)
  := by
  apply Iff.intro
  intro h
  simp [Odds.le]
  exact h
  intro h
  simp [Odds.le] at h
  exact h
infixl:45 " ≤ " => Odds.le
infixl:45 " <= " => Odds.le

def Odds.max (a b : Odds) : Odds :=
  match Odds.le a b with
  | true => b
  | false => a

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

def Odds.merge (choose loser winner : Odds) : Odds :=
  Odds.mk
    (choose.lose * loser.lose + choose.win * winner.lose)
    (choose.lose * loser.win + choose.win * winner.win)
    (by
      induction' choose with cl _ cv
      induction' loser with ll _ lv
      induction' winner with _ _ wv
      simp at wv
      cases hcl : decide (cl = 0)
      {
        cases hll : decide (ll = 0)
        <;>
        {
          simp at hcl
          simp at hll
          simp [hll] at lv
          simp [lv, hcl, hll]
        }
      }
      {
        simp at hcl
        simp [hcl] at cv
        simp [hcl, cv]
        exact wv
      }
    )

def Odds.avg (left right : Odds) : Odds :=
  Odds.merge (Odds.mk 1 1 (by trivial)) left right

theorem odds_le_odds_max
  (a b : Odds)
  : a ≤ (Odds.max a b)
  := by
  cases h : Odds.le a b
  {
    unfold Odds.max
    rw [h]
    simp
    unfold Odds.le
    simp
  }
  {
    unfold Odds.max
    rw [h]
    simp
    exact h
  }

theorem odds_transitivity
  (a b c: Odds)
  (hab : a <= b)
  (hbc : b <= c)
  : (a <= c)
  := by
  induction' a with al aw av
  induction' b with bl bw bv
  induction' c with cl cw cv
  simp at av
  simp at bv
  simp at cv
  simp [Odds.le]
  simp [Odds.le] at hab
  simp [Odds.le] at hbc
  cases hbl : (decide (bl = 0))
  {
    simp at hbl
    cases hbw : (decide (bw = 0))
    {
      simp at hbw
      rw [scale_le (bl * bw) (aw * cl) (cw * al)]
      rw [<- Nat.mul_assoc]
      rw [<- Nat.mul_assoc]
      rw [Nat.mul_comm bl bw]
      rw [Nat.mul_assoc _ _ aw]
      rw [Nat.mul_comm bw]
      rw [Nat.mul_assoc _ _ cl]
      rw [Nat.mul_assoc bw]
      rw [Nat.mul_comm _ (bl * cw)]
      rw [Nat.mul_assoc _ _ al]
      rw [Nat.mul_comm _ (bw * al)]
      rw [Nat.mul_comm bl cw]
      rw [Nat.mul_comm bl aw]
      apply prod_preserves_le _ _ _ _ hab hbc
      simp [hbl, hbw]
    }
    {
      simp at hbw
      simp [hbw, hbl] at hab
      simp [hab]
    }
  }
  {
    simp at hbl
    cases hbw : (decide (bw = 0))
    {
      simp at hbw
      simp [hbl, hbw] at hbc
      simp [hbc]
    }
    {
      simp at hbw
      absurd bv
      simp [hbl, hbw]
    }
  }

theorem odds_merge_le_max(odds a b : Odds)
  : (Odds.merge odds a b) ≤ (Odds.max a b)
  := by
  cases h : a ≤ b
  unfold Odds.max
  simp [h]
  simp [Odds.le, Odds.merge]
  rw [Nat.add_mul, Nat.mul_add, <- Nat.mul_assoc, Nat.mul_comm a.win]
  apply Nat.add_le_add
  rfl
  rw [Nat.mul_comm (a.win), Nat.mul_assoc, Nat.mul_assoc]
  apply Nat.mul_le_mul
  rfl
  rw [Nat.mul_comm (b.lose)]
  simp [Odds.le] at h
  apply Nat.le_of_lt
  exact h
  simp [Odds.max, h]
  simp [Odds.le, Odds.merge]
  rw [Nat.add_mul, Nat.mul_add, <- Nat.mul_assoc]
  rw [Nat.add_comm, Nat.add_comm _ (b.win * (odds.win * b.lose))]
  rw [Nat.mul_comm b.win, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm b.win]
  apply Nat.add_le_add
  rfl
  rw [Nat.mul_comm (b.win), Nat.mul_assoc, Nat.mul_assoc]
  apply Nat.mul_le_mul
  rfl
  rw [Odds.le_def]
  exact h

theorem odds_max_bound_also_bounds_odds_merge(odds a b c : Odds)
  (h : (Odds.max a b) ≤ c)
  : (Odds.merge odds a b) ≤ c
  := by
  apply odds_transitivity (Odds.merge odds a b) (Odds.max a b) c
  apply odds_merge_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) : Odds := Odds.toBool (chsh_win_rule (a x) (b y) x y)
def chsh_win_rate_det (a b : Bool -> Bool) : Odds :=
  Odds.avg
    (Odds.avg
      (play_chsh_case a b false false)
      (play_chsh_case a b false true))
    (Odds.avg
      (play_chsh_case a b true false)
      (play_chsh_case a b true true))
def chsh_win_rate_semidet (a : Bool -> Bool) (br : RandStrat) : Odds :=
  match br with
  | RandStrat.always b => chsh_win_rate_det a b
  | RandStrat.rand oddsB leftB rightB => (Odds.merge oddsB (chsh_win_rate_semidet a leftB) (chsh_win_rate_semidet a rightB))
def chsh_win_rate (ar br : RandStrat) : Odds :=
  match ar with
  | RandStrat.always a => chsh_win_rate_semidet a br
  | RandStrat.rand odds left right => (Odds.merge odds (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) ≤ (Odds.mk 1 3 (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, Odds.toBool, Odds.avg, Odds.merge, Odds.le_def]
      repeat trivial
    }


theorem CHSH_inequality_for_semidet_strats
  (a : Bool -> Bool)
  (br : RandStrat)
  : chsh_win_rate_semidet a br ≤ Odds.mk 1 3 (by trivial)
  := by
    cases br with
    | always b =>
      simp [chsh_win_rate_semidet]
      apply CHSH_inequality_for_det_strats
    | rand b_odds b_left b_right =>
      simp [chsh_win_rate_semidet]
      apply odds_max_bound_also_bounds_odds_merge
      unfold Odds.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 ≤ Odds.mk 1 3 (by trivial)
  := by
    cases ar with
    | always a =>
      simp [chsh_win_rate]
      apply CHSH_inequality_for_semidet_strats
    | rand b_odds b_left b_right =>
      simp [chsh_win_rate]
      apply odds_max_bound_also_bounds_odds_merge
      unfold Odds.max
      cases cr : (chsh_win_rate b_left br ≤ chsh_win_rate b_right br) <;>
      {
        simp
        apply CHSH_inequality
      }