Documentation

PrimeCert.Interval

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.

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

source
theorem forall_start {P : ℕ → Prop} {hi : ℕ} (ih : ∀ (n : ℕ), 0 ≤ n → n < hi → P n) (n : ℕ) :
n < hi → P n
source
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
source
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
source
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
source
theorem forall_last {P : ℕ → Prop} {hi : ℕ} (n : ℕ) :
hi ≤ n → n < hi → P n
source
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 #

source
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
source
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
source
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
source
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
source
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
source
@[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.
Instances For
    source
    def makeForallBisectHi (P : Lean.Expr) (hi : ℕ) (pf : ℕ → Lean.Expr) :
    Lean.Expr

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

    Equations
    Instances For
      source
      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.

      source
      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
      Instances For
        source
        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
        Instances For