Basic Bignum Lemmas

Fundamental theorems about bignum operations, ported from s2n-bignum/common/bignum.ml

Main Theorems

• high_low_digits - Decomposition: n = 2^(64*i) * highdigits n i + lowdigits n i
• highdigits_clauses - Recursive characterization of highdigits
• lowdigits_clauses - Recursive characterization of lowdigits
• bigdigitsum_works - Sum of digits equals the number (when bounded)

References

Source: s2n-bignum/common/bignum.ml (lines 79-150)

theorem Bignum.high_low_digits (n i : ℕ) : 2 ^ (64 * i) * highdigits n i + lowdigits n i = n

Fundamental decomposition theorem: any number can be split into high and low parts.

Corresponds to HOL Light theorem:

let HIGH_LOW_DIGITS = prove
 (`(!n i. 2 EXP (64 * i) * highdigits n i + lowdigits n i = n) /\
   (!n i. lowdigits n i + 2 EXP (64 * i) * highdigits n i = n) /\
   (!n i. highdigits n i * 2 EXP (64 * i) + lowdigits n i = n) /\
   (!n i. lowdigits n i + highdigits n i * 2 EXP (64 * i) = n)`, ...);;

Source: s2n-bignum/common/bignum.ml:79-85

theorem Bignum.highdigits_succ (n i : ℕ) : highdigits n (i + 1) = highdigits n i / 2 ^ 64

Recursive characterization of highdigits. This is the second clause of HOL Light's HIGHDIGITS_CLAUSES. The first clause (highdigits n 0 = n) is in Defs.lean as highdigits_zero.

Corresponds to HOL Light theorem:

let HIGHDIGITS_CLAUSES = prove
 (`(!n. highdigits n 0 = n) /\  -- clause 1
   (!n i. highdigits n (i + 1) = highdigits n i DIV 2 EXP 64)`, ...);; -- clause 2

Source: s2n-bignum/common/bignum.ml:87-91 (HIGHDIGITS_CLAUSES, clause 2)

theorem Bignum.highdigits_step (n i : ℕ) : highdigits n i = 2 ^ 64 * highdigits n (i + 1) + bigdigit n i

Step theorem: relating highdigits at position i with i+1 and the digit at i.

This is a key decomposition theorem: highdigits at position i equals the highdigits at i+1 (shifted left by 64 bits) plus the digit at position i.

Corresponds to HOL Light theorem:

let HIGHDIGITS_STEP = prove
 (`!n i. highdigits n i = 2 EXP 64 * highdigits n (i + 1) + bigdigit n i`,
  REWRITE_TAC[highdigits; bigdigit; LEFT_ADD_DISTRIB; MULT_CLAUSES] THEN
  REWRITE_TAC[EXP_ADD; GSYM DIV_DIV] THEN ARITH_TAC);;

Source: s2n-bignum/common/bignum.ml:93-96

theorem Bignum.lowdigits_succ (n i : ℕ) : lowdigits n (i + 1) = 2 ^ (64 * i) * bigdigit n i + lowdigits n i

Recursive characterization of lowdigits. This is the second clause of HOL Light's LOWDIGITS_CLAUSES. Corresponds to HOL Light theorem:

let LOWDIGITS_CLAUSES = prove
 (`(!n. lowdigits n 0 = 0) /\
   (!n i. lowdigits n (i + 1) =
          2 EXP (64 * i) * bigdigit n i + lowdigits n i)`, ...);;

Source: s2n-bignum/common/bignum.ml:98-103

theorem Bignum.highdigits_eq_zero (n i : ℕ) : highdigits n i = 0 ↔ n < 2 ^ (64 * i)

highdigits equals 0 iff n is bounded.

Corresponds to HOL Light theorem:

let HIGHDIGITS_EQ_0 = prove
 (`!n i. highdigits n i = 0 <=> n < 2 EXP (64 * i)`, ...);;

Source: s2n-bignum/common/bignum.ml:105-107

theorem Bignum.highdigits_of_lt (n i : ℕ) (h : n < 2 ^ (64 * i)) : highdigits n i = 0

If n is bounded, then highdigits n i = 0.

Corresponds to HOL Light theorem:

let HIGHDIGITS_ZERO = prove
 (`!n i. n < 2 EXP (64 * i) ==> highdigits n i = 0`, ...);;

Source: s2n-bignum/common/bignum.ml:113-115

theorem Bignum.highdigits_top (n k : ℕ) (h : n < 2 ^ (64 * k)) : highdigits n (k - 1) = bigdigit n (k - 1)

If n is bounded, the top digit equals highdigits at position k-1.

Corresponds to HOL Light theorem:

let HIGHDIGITS_TOP = prove
 (`!n k. n < 2 EXP (64 * k) ==> highdigits n (k - 1) = bigdigit n (k - 1)`,
  REPEAT STRIP_TAC THEN REWRITE_TAC[highdigits; bigdigit] THEN
  CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_LT THEN
  SIMP_TAC[RDIV_LT_EQ; EXP_EQ_0; ARITH_EQ; GSYM EXP_ADD] THEN
  TRANS_TAC LTE_TRANS `2 EXP (64 * k)` THEN
  ASM_REWRITE_TAC[LE_EXP] THEN ARITH_TAC);;

Source: s2n-bignum/common/bignum.ml:131-137

theorem Bignum.highdigits_trivial (n : ℕ) : highdigits 0 n = 0

highdigits of 0 is always 0.

Corresponds to HOL Light theorem:

let HIGHDIGITS_TRIVIAL = prove
 (`!n. highdigits 0 n = 0`,
  REWRITE_TAC[highdigits; DIV_0]);;

Source: s2n-bignum/common/bignum.ml:117-119

theorem Bignum.highdigits_highdigits (n i j : ℕ) : highdigits (highdigits n i) j = highdigits n (i + j)

Compositionality of highdigits: taking highdigits twice is equivalent to adding indices.

Corresponds to HOL Light theorem:

let HIGHDIGITS_HIGHDIGITS = prove
 (`!n i j. highdigits (highdigits n i) j = highdigits n (i + j)`,
  REPEAT GEN_TAC THEN REWRITE_TAC[highdigits] THEN
  REWRITE_TAC[LEFT_ADD_DISTRIB; EXP_ADD; DIV_DIV]);;

Source: s2n-bignum/common/bignum.ml:169-172

theorem Bignum.lowdigits_of_lt (n i : ℕ) (h : n < 2 ^ (64 * i)) : lowdigits n i = n

If n is bounded, then lowdigits n i = n.

Corresponds to HOL Light theorem:

let LOWDIGITS_SELF = prove
 (`!n i. n < 2 EXP (64 * i) ==> lowdigits n i = n`, ...);;

Source: s2n-bignum/common/bignum.ml:147-149

theorem Bignum.lowdigits_one (n : ℕ) : lowdigits n 1 = bigdigit n 0

The first lowdigit equals the 0-th bigdigit.

Corresponds to HOL Light theorem:

let LOWDIGITS_1 = prove
 (`!n. lowdigits n 1 = bigdigit n 0`,
  SUBST1_TAC(ARITH_RULE `1 = 0 + 1`) THEN
  REWRITE_TAC[LOWDIGITS_CLAUSES; LOWDIGITS_0] THEN
  REWRITE_TAC[MULT_CLAUSES; EXP; ADD_CLAUSES]);;

Source: s2n-bignum/common/bignum.ml:125-129

theorem Bignum.lowdigits_trivial (n : ℕ) : lowdigits 0 n = 0

lowdigits of 0 is always 0.

Corresponds to HOL Light theorem:

let LOWDIGITS_TRIVIAL = prove
 (`!n. lowdigits 0 n = 0`,
  REWRITE_TAC[lowdigits; MOD_0]);;

Source: s2n-bignum/common/bignum.ml:151-153

theorem Bignum.lowdigits_eq_self (n i : ℕ) : lowdigits n i = n ↔ n < 2 ^ (64 * i)

lowdigits equals n iff n is bounded.

This is the bidirectional version of lowdigits_of_lt.

Corresponds to HOL Light theorem:

let LOWDIGITS_EQ_SELF = prove
 (`!n i. lowdigits n i = n <=> n < 2 EXP (64 * i)`,
  SIMP_TAC[lowdigits; MOD_EQ_SELF; EXP_EQ_0; ARITH_EQ]);;

Source: s2n-bignum/common/bignum.ml:143-145

theorem Bignum.lowdigits_le (n i : ℕ) : lowdigits n i ≤ n

lowdigits is always less than or equal to the original number.

Corresponds to HOL Light theorem:

let LOWDIGITS_LE = prove
 (`!n i. lowdigits n i <= n`,
  REWRITE_TAC[lowdigits; MOD_LE]);;

Source: s2n-bignum/common/bignum.ml:155-157

theorem Bignum.lowdigits_lowdigits (n i j : ℕ) : lowdigits (lowdigits n i) j = lowdigits n (min i j)

Compositionality of lowdigits: taking lowdigits twice equals taking the minimum.

Corresponds to HOL Light theorem:

let LOWDIGITS_LOWDIGITS = prove
 (`!n i j. lowdigits (lowdigits n i) j = lowdigits n (MIN i j)`,
  REPEAT GEN_TAC THEN REWRITE_TAC[lowdigits; MOD_MOD_EXP_MIN] THEN
  AP_TERM_TAC THEN AP_TERM_TAC THEN ARITH_TAC);;

Source: s2n-bignum/common/bignum.ml:159-162

theorem Bignum.bigdigitsum_works (n k : ℕ) (h : n < 2 ^ (64 * k)) : List.foldl (fun (i : ℕ) => 2 ^ (64 * i) * ↑(bigdigit n i)) 0 (Finset.range k).toList = n

If n is bounded by 2^(64*k), then the sum of its digits equals n.

Corresponds to HOL Light theorem:

let BIGDIGITSUM_WORKS = prove
 (`!n k. n < 2 EXP (64 * k)
         ==> nsum {i | i < k} (\i. 2 EXP (64 * i) * bigdigit n i) = n`, ...);;

Source: s2n-bignum/common/bignum.ml:19-22

Note: We use Finset.sum instead of HOL Light's nsum.

theorem Bignum.bigdigit_of_lt (n i : ℕ) (h : n < 2 ^ (64 * i)) : bigdigit n i = 0

If a number is less than 2^(64*i), then its i-th bigdigit is 0.

Corresponds to HOL Light theorem:

let BIGDIGIT_ZERO = prove
 (`!n i. n < 2 EXP (64 * i) ==> bigdigit n i = 0`, ...);;

Source: s2n-bignum/common/bignum.ml:37-39

theorem Bignum.bigdigit_add_left (a n b i : ℕ) (h : i < n) : bigdigit (a + 2 ^ (64 * n) * b) i = bigdigit a i

bigdigit is unaffected by adding a high-order term.

If we add a term 2^(64*n) * b to a, the digits below position n remain unchanged.

Corresponds to HOL Light theorem:

let BIGDIGIT_ADD_LEFT =
  prove(`forall a n b i.
  i < n ==> bigdigit (a + 2 EXP (64 * n) * b) i = bigdigit a i`,
  REPEAT STRIP_TAC THEN
  REWRITE_TAC[bigdigit] THEN
  SUBGOAL_THEN `2 EXP (64 * n) = 2 EXP (64 * i) * (2 EXP (64 * (n-i)))` SUBST_ALL_TAC THENL [
    REWRITE_TAC[GSYM EXP_ADD] THEN
    REWRITE_TAC[GSYM LEFT_ADD_DISTRIB] THEN
    AP_TERM_TAC THEN AP_TERM_TAC THEN ASM_ARITH_TAC;

    REWRITE_TAC[GSYM MULT_ASSOC] THEN
    IMP_REWRITE_TAC[DIV_MULT_ADD; EXP_2_NE_0] THEN
    SUBGOAL_THEN
      `2 EXP (64*(n-i)) = 2 EXP 64 * (2 EXP (64*(n-i-1)))`
      SUBST_ALL_TAC THENL [
      REWRITE_TAC[GSYM EXP_ADD] THEN
      AP_TERM_TAC THEN ASM_ARITH_TAC;

      ALL_TAC
    ] THEN
    REWRITE_TAC[GSYM MULT_ASSOC] THEN
    IMP_REWRITE_TAC[MOD_MULT_ADD; EXP_2_NE_0]]);;

Source: s2n-bignum/common/bignum.ml:41-62

theorem Bignum.bigdigit_succ (n i t : ℕ) (h : t < 2 ^ 64) : bigdigit (t + 2 ^ 64 * n) (i + 1) = bigdigit n i

Successor digit extraction: extracting digit (i+1) from a 2-word number.

When a number is written as t + 2^64 * n where t < 2^64, the digit at position (i+1) equals the digit at position i of n.

Corresponds to HOL Light theorem:

let BIGDIGIT_SUC = prove(`forall n i t.
  t < 2 EXP 64 ==> bigdigit (t + 2 EXP 64 * n) (SUC i) = bigdigit n i`,

  REPEAT STRIP_TAC THEN
  REWRITE_TAC[bigdigit;ARITH_RULE`SUC i = 1 + i`;LEFT_ADD_DISTRIB;EXP_ADD;GSYM DIV_DIV;
              ARITH_RULE`64 * 1 = 64`] THEN
  IMP_REWRITE_TAC[DIV_MULT_ADD;EXP_2_NE_0;SPECL [`t:num`;`2 EXP 64`] DIV_LT] THEN
  REWRITE_TAC[ADD]);;

Source: s2n-bignum/common/bignum.ml:64-71

theorem Bignum.bigdigit_highdigits (n i j : ℕ) : bigdigit (highdigits n i) j = bigdigit n (i + j)

Compositionality: bigdigit of highdigits shifts indices.

Extracting digit j from highdigits at position i is the same as extracting digit (i+j) from the original number.

Corresponds to HOL Light theorem:

let BIGDIGIT_HIGHDIGITS = prove
 (`!n i j. bigdigit (highdigits n i) j = bigdigit n (i + j)`,
  REPEAT GEN_TAC THEN REWRITE_TAC[bigdigit; highdigits] THEN
  REWRITE_TAC[LEFT_ADD_DISTRIB; EXP_ADD; DIV_DIV]);;

Source: s2n-bignum/common/bignum.ml:164-167

theorem Bignum.bigdigit_lowdigits (n i j : ℕ) : bigdigit (lowdigits n i) j = if j < i then bigdigit n j else 0

Extracting digits from lowdigits: only digits below position i are preserved.

Corresponds to HOL Light theorem:

let BIGDIGIT_LOWDIGITS = prove
 (`!n i j. bigdigit (lowdigits n i) j = if j < i then bigdigit n j else 0`,
  REPEAT GEN_TAC THEN REWRITE_TAC[bigdigit; lowdigits] THEN
  COND_CASES_TAC THENL
   [REWRITE_TAC[DIV_MOD; GSYM EXP_ADD; MOD_MOD_EXP_MIN] THEN
    ASM_SIMP_TAC[ARITH_RULE
     `j < i ==> MIN (64 * i) (64 * j + 64) = 64 * j + 64`];
    MATCH_MP_TAC(MESON[MOD_0] `x = 0 ==> x MOD n = 0`) THEN
    SIMP_TAC[DIV_EQ_0; EXP_EQ_0; ARITH_EQ] THEN
    TRANS_TAC LTE_TRANS `2 EXP (64 * i)` THEN
    REWRITE_TAC[MOD_LT_EQ; EXP_EQ_0; ARITH_EQ; LE_EXP] THEN ASM_ARITH_TAC]);;

Source: s2n-bignum/common/bignum.ml:174-184