Interval checking by binary search

The check_interval tactic proves goals of the form ∀ n, lo ≤ n → n < hi → P n or ∀ n, lo ≤ n → n < hi → n % b = r → P n by building a balanced binary tree of eagerReduce proof terms, one per value in the range.

noncomputable def forallB (f : ℕ → Bool) (start len : ℕ) (step : ℕ := 1) : Bool

Equations

• forallB f start len step = (Nat.rec (start, true) (fun (x : ℕ) (ih : ℕ × Bool) => Prod.rec (fun (i : ℕ) (b : Bool) => (i.add step, (f i).and' b)) ih) len).snd

theorem forallB_iff_range' (f : ℕ → Bool) (start len step : ℕ) : forallB f start len step = true ↔ ∀ (n : ℕ), n ∈ List.range' start len step → f n = true

theorem forallB_iff (f : ℕ → Bool) (start len step : ℕ) : forallB f start len step = true ↔ ∀ (n : ℕ), n < len → f (n * step + start) = true

theorem forallB_iff' (f : ℕ → Bool) (start r len step : ℕ) : forallB f (start * step + r) len step = true ↔ ∀ (n : ℕ), start ≤ n → n < start + len → f (n * step + r) = true

theorem forallB_one_iff (f : ℕ → Bool) (start len : ℕ) : forallB f start len = true ↔ ∀ (n : ℕ), start ≤ n → n < start + len → f n = true

Tools for automation of ∀ n, lo ≤ n → n < hi → P n

theorem forall_start {P : ℕ → Prop} {hi : ℕ} (ih : ∀ (n : ℕ), 0 ≤ n → n < hi → P n) (n : ℕ) : n < hi → P n

theorem forall_step {P : ℕ → Prop} {curr hi : ℕ} (next : ℕ) (now : P curr) (h : curr.succ = next) (ih : ∀ (n : ℕ), next ≤ n → n < hi → P n) (n : ℕ) : curr ≤ n → n < hi → P n

theorem forall_bisect {P : ℕ → Prop} {lo hi : ℕ} (mi : ℕ) (h₁ : ∀ (n : ℕ), lo ≤ n → n < mi → P n) (h₂ : ∀ (n : ℕ), mi ≤ n → n < hi → P n) (n : ℕ) : lo ≤ n → n < hi → P n

theorem forall_succ {P : ℕ → Prop} {lo hi : ℕ} (h : P lo) (spec : hi.ble lo.succ = true := by rfl) (n : ℕ) : lo ≤ n → n < hi → P n

theorem forall_last {P : ℕ → Prop} {hi : ℕ} (n : ℕ) : hi ≤ n → n < hi → P n

theorem forall_exceed {P : ℕ → Prop} {lo hi : ℕ} (h : hi.ble lo = true) (n : ℕ) : lo ≤ n → n < hi → P n

Tools for automation of ∀ n, lo ≤ n → n < hi → n % b = r → P n

theorem forall_mod_start {P : ℕ → Prop} {hi b r : ℕ} (ih : ∀ (n : ℕ), r ≤ n → n < hi → n % b = r → P n) (n : ℕ) : n < hi → n % b = r → P n

theorem forall_mod_step {P : ℕ → Prop} {lo hi b r : ℕ} (next : ℕ) (now : P lo) (ih : ∀ (n : ℕ), next ≤ n → n < hi → n % b = r → P n) (spec₁ : lo + b = next := by rfl) (spec₂ : lo % b = r := by rfl) (n : ℕ) : lo ≤ n → n < hi → n % b = r → P n

theorem forall_mod_succ {P : ℕ → Prop} {lo hi b r : ℕ} (now : P lo) (spec₁ : lo % b = r := by rfl) (spec₂ : hi.ble (lo.add b) = true := by rfl) (n : ℕ) : lo ≤ n → n < hi → n % b = r → P n

theorem forall_mod_bisect {P : ℕ → Prop} {lo hi b r : ℕ} (mi : ℕ) (ih₁ : ∀ (n : ℕ), lo ≤ n → n < mi → n % b = r → P n) (ih₂ : ∀ (n : ℕ), mi ≤ n → n < hi → n % b = r → P n) (n : ℕ) : lo ≤ n → n < hi → n % b = r → P n

theorem forall_mod_exceed {P : ℕ → Prop} {lo hi b r : ℕ} (h : hi.ble lo = true) (n : ℕ) : lo ≤ n → n < hi → n % b = r → P n

@[irreducible]

def makeForallBisectLoHi (P : Lean.Expr) (lo hi : ℕ) (pf : ℕ → Lean.Expr) : Lean.Expr

An expression to prove statement of the form ∀ n, lo ≤ n → n < hi → P n

Equations

• One or more equations did not get rendered due to their size.

def makeForallBisectHi (P : Lean.Expr) (hi : ℕ) (pf : ℕ → Lean.Expr) : Lean.Expr

An expression to prove statement of the form ∀ n < hi → P n

Equations

• makeForallBisectHi P hi pf = Lean.mkApp3 (Lean.mkConst `forall_start) P (Lean.mkRawNatLit hi) (makeForallBisectLoHi P 0 hi pf)

partial def makeForallModBisectLoHi (P : Lean.Expr) (lo hi b r : ℕ) (bE rE : Lean.Expr) (pf : ℕ → Lean.Expr) : Lean.Expr

An expression to prove statement of the form ∀ n, lo ≤ n → n < hi → n % b = r → P n. This always assumes lo % b = r.

def makeForallModBisectHi (P : Lean.Expr) (hi b r : ℕ) (bE rE : Lean.Expr) (pf : ℕ → Lean.Expr) : Lean.Expr

An expression to prove statement of the form ∀ n < hi → n % b = r → P n.

Equations

• makeForallModBisectHi P hi b r bE rE pf = Lean.mkApp5 (Lean.mkConst `forall_mod_start) P (Lean.mkRawNatLit hi) bE rE (makeForallModBisectLoHi P r hi b r bE rE pf)

def tacticCheck_interval : Lean.ParserDescr

Tactic to prove bounded universal statements by exhaustive kernel checking. Accepts four goal shapes:

• ∀ n < hi, P n
• ∀ n, lo ≤ n → n < hi → P n
• ∀ n < hi, n % b = r → P n
• ∀ n, lo ≤ n → n < hi → n % b = r → P n

The predicate P n must reduce to true (via eagerReduce) for every n in range. The tactic builds a balanced binary tree of proof terms, so the elaboration depth is logarithmic in the range size.

-- Check that wieferichKR is false or mirimanoffKR is false for all n ≡ 1 (mod 6), n < 6000:
theorem wieferich_mirimanoff₁ : ∀ n < 6000, n % 6 = 1 →
    (wieferichKR n).not'.or' (mirimanoffKR n).not' := by
  check_interval

Equations

• tacticCheck_interval = Lean.ParserDescr.node `tacticCheck_interval 1024 (Lean.ParserDescr.nonReservedSymbol "check_interval" false)