A lean proof of the CHSH inequality. More accurately: a terrible lean proof of the CHSH inequality, made by a complete beginner with no idea what they are doing. But the compiler accepts it!

chsh.lean

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

----------------- BASIC DATA TYPES AND COMBINATORS --------------------
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_bool (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 cw cv
      induction' loser with ll lw lv
      induction' winner with wl ww wv
      simp at wv
      cases hcl : decide (cl = 0)
      {
        simp at hcl
        cases hll : decide (ll = 0)
        {
          simp at hll
          simp [hcl, hll]
        }
        {
          simp at hll
          cases hlw : decide (lw = 0)
          {
            simp at hlw
            simp [hcl, hll, hlw]
          }
          {
            simp at hlw
            absurd lv
            simp [hll, hlw]
          }
        }
      }
      {
        simp at hcl
        simp [hcl] at cv
        simp [hcl, cv]
        exact wv
      }
    )
def average_odds (left right : Odds) : Odds :=
  odds_merge (Odds.mk 1 1 (by trivial)) left right


----------------- 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_bool (chsh_win_rule (a x) (b y) x y)
def chsh_win_rate_det (a b : Bool -> Bool) : Odds :=
  average_odds
    (average_odds
      (play_chsh_case a b false false)
      (play_chsh_case a b false true))
    (average_odds
      (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 --------------------

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

def odds_max (a b : Odds) : Odds :=
  match Odds.le_def a b with
  | true => b
  | false => a



theorem lt_to_le (a b : Nat) (h : a < b) : a <= b := by
  apply Nat.le_of_lt_succ
  apply Nat.lt_of_succ_lt
  apply Nat.succ_lt_succ
  exact h

theorem not_le_to_lt (a b : Nat) (h : !(b <= a)) : a < b := by
  apply Nat.gt_of_not_le
  simp at h
  simp
  exact h

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
    exact hab
    exact h
    rw [h3]
    rw [Nat.add_comm, Nat.add_comm (Nat.succ b2)]
    rw [<- offset_le]
    exact hcd
  }
  {
    simp at h
    rw [lt_succ_eq_le] at h
    simp [h] at hb
    apply Nat.le_of_succ_le
    rw [Nat.succ_add]
    apply Nat.succ_le_succ
    exact hb
  }

theorem scale_le (a b c : Nat) (h : a != 0) (habc : a*b <= a*c) : (b <= c)
  := by
  induction' a
  absurd h
  simp
  simp at habc
  exact habc

theorem scale_le2 (a b c : Nat) (h : a != 0) (habc : b <= c) : (a*b <= a*c)
  := by
  induction' a
  simp
  simp
  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))
  {
    simp at h
    have h2 : a = Nat.succ b2
    apply le_pin
    exact hab
    exact h
    rw [h2]
    apply scale_le2
    simp
    exact hcd
  }
  {
    simp at h
    have h4 : a <= b2
    rw [<- lt_succ_eq_le]
    exact h
    simp [h4] at hb
    rw [Nat.succ_mul, <- Nat.add_zero (a * c)]
    apply add_preserves_le
    exact hb
    simp
  }


theorem args_leq_odds_max
  (a b : Odds)
  :
  a ≤ (odds_max a b) := by
  cases h : Odds.le_def a b
  {
    unfold odds_max
    rw [h]
    simp
    unfold Odds.le_def
    simp
  }
  {
    unfold odds_max
    rw [h]
    simp
    exact h
  }

theorem zero_le_a_implies_not_a_eq_0 (a : Nat) (h : 0 < a) : !(a = 0)
  := by
  induction a
  trivial
  trivial

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_def]
  simp [Odds.le_def] at hab
  simp [Odds.le_def] at hbc
  cases hal : (decide (al > 0))
  {
    cases hcl : (decide (cl > 0))
    {
      simp at hcl
      simp [hcl]
    }
    {
      simp at hal
      simp [hal]
      left
      cases hbl : (decide (bl > 0))
      {
        simp at hcl
        apply zero_le_a_implies_not_a_eq_0 at hcl
        simp at hcl
        simp at hbl
        absurd hbc
        simp [hbl, hcl]
        simp [hbl] at bv
        exact bv
      }
      {
        simp at hbl
        simp [hal] at av
        simp [hal] at hab
        apply zero_le_a_implies_not_a_eq_0 at hbl
        simp at hbl
        simp [hbl] at hab
        exact hab
      }
    }
  }
  {
    cases hcl : (decide (cl > 0))
    {
      simp at hcl
      simp [hcl]
    }
    {
      cases hbl : (decide (bl > 0))
      {
        simp at hcl
        simp at hbl
        simp [hbl] at bv
        simp [hbl] at hbc
        apply zero_le_a_implies_not_a_eq_0 at hcl
        simp at hcl
        simp [hcl] at hbc
        absurd hbc
        exact bv
      }
      {
        cases hbw : (decide (bw > 0))
        {
          simp at hbw
          simp at hbl
          apply zero_le_a_implies_not_a_eq_0 at hbl
          simp at hbl
          simp [hbw, hbl] at hab
          simp [hab]
        }
        {
          have hh : (aw*bl)*(bw*cl) <= (bw*al)*(cw*bl)
          apply prod_preserves_le
          exact hab
          exact hbc
          rw [<- Nat.mul_assoc, Nat.mul_comm _ bw, Nat.mul_comm _ bl, <- Nat.mul_assoc] at hh
          rw [Nat.mul_assoc (bw * bl), Nat.mul_comm cw bl, <- Nat.mul_assoc (bw*al)] at hh
          rw [Nat.mul_assoc bw al, Nat.mul_comm al bl, <- Nat.mul_assoc bw, Nat.mul_assoc (bw * bl)] at hh
          apply scale_le at hh
          rw [Nat.mul_comm cw al]
          exact hh
          simp at hbl
          apply zero_le_a_implies_not_a_eq_0 at hbl
          simp at hbl
          simp at hbw
          apply zero_le_a_implies_not_a_eq_0 at hbw
          simp at hbw
          simp [hbl]
          exact hbw
        }
      }
    }
  }

theorem odds_merge_leq_odds_max(odds a b : Odds)
  : (odds_merge odds a b) ≤ (odds_max a b)
  := by
  cases h : a ≤ b
  unfold odds_max
  rw [h]
  simp
  unfold Odds.le_def
  unfold odds_merge
  simp
  rw [Nat.add_mul, Nat.mul_add, <- Nat.mul_assoc, Nat.mul_comm a.win]
  apply Nat.add_le_add
  simp
  rw [Nat.mul_comm (a.win), Nat.mul_assoc, Nat.mul_assoc]
  apply Nat.mul_le_mul
  simp
  rw [Nat.mul_comm (b.lose)]
  simp [Odds.le_def] at h
  apply lt_to_le
  apply not_le_to_lt
  simp
  exact h
  unfold odds_max
  rw [h]
  simp
  unfold Odds.le_def
  unfold odds_merge
  simp
  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
  simp
  rw [Nat.mul_comm (b.win), Nat.mul_assoc, Nat.mul_assoc]
  apply Nat.mul_le_mul
  simp
  unfold Odds.le_def at h
  simp at h
  exact h

theorem odds_max_bounded_by_c_implies_odds_merge_bounded_also(odds a b c : Odds)
  (h : (odds_max a b) ≤ c)
  : (odds_merge odds a b) ≤ c := by
  simp [odds_max] at h
  cases h2 : a ≤ b with
  | false =>
    simp [h2] at h
    simp [Odds.le_def] at h
    simp [Odds.le_def] at h2
    simp [odds_merge]
    simp [Odds.le_def]
    rw [Nat.add_mul, Nat.mul_add, Nat.mul_assoc, Nat.mul_assoc]
    rw [Nat.mul_comm odds.win, Nat.add_comm]
    rw [Nat.mul_comm odds.win, <- Nat.mul_assoc c.win, <- Nat.mul_assoc c.win]
    rw [Nat.add_comm _ (c.win * b.lose * odds.win)]
    apply Nat.add_le_add
    apply Nat.mul_le_mul
    rw [Odds.le_def_un]
    rw [Odds.le_def_un] at h
    apply Nat.le_of_lt at h2
    rw [Odds.le_def_un b a] at h2
    apply odds_transitivity b a c
    exact h2
    exact h
    simp
    rw [Nat.mul_comm c.win, Nat.mul_assoc]
    apply Nat.mul_le_mul
    simp
    exact h
  | true =>
    simp [h2] at h
    simp [Odds.le_def] at h
    simp [Odds.le_def] at h2
    simp [odds_merge]
    simp [Odds.le_def]
    rw [Nat.add_mul, Nat.mul_add, Nat.mul_assoc, Nat.mul_assoc]
    rw [Nat.mul_comm odds.win, Nat.add_comm]
    rw [Nat.mul_comm odds.win, <- Nat.mul_assoc c.win, <- Nat.mul_assoc c.win]
    rw [Nat.add_comm _ (c.win * b.lose * odds.win)]
    apply Nat.add_le_add
    apply Nat.mul_le_mul
    exact h
    simp
    rw [Nat.mul_comm c.win, Nat.mul_assoc]
    apply Nat.mul_le_mul
    simp
    rw [Odds.le_def_un]
    rw [Odds.le_def_un] at h
    rw [Odds.le_def_un] at h2
    apply odds_transitivity a b c
    exact h2
    exact h

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_bool, average_odds, 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_bounded_by_c_implies_odds_merge_bounded_also
      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_bounded_by_c_implies_odds_merge_bounded_also
      unfold odds_max
      cases cr : (chsh_win_rate b_left br ≤ chsh_win_rate b_right br) <;>
      {
        simp
        apply CHSH_inequality
      }