Examples/gcdrecurrence.ml

   1 (* ========================================================================= *)
   2 (* Some divisibility properties of certain linear integer recurrences.       *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/prime.ml";;
   6 needs "Library/integer.ml";;
   7
   8 prioritize_int();;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* A customized induction principle.                                         *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let INDUCT_SPECIAL = prove
  15  (`!P. (!n. P 0 n) /\
  16        (!m n. P m n <=> P n m) /\
  17        (!m n. P m n ==> P n (m + n))
  18        ==> !m n. P m n`,
  19   GEN_TAC THEN STRIP_TAC THEN
  20   REPEAT GEN_TAC THEN WF_INDUCT_TAC `m + n:num` THEN
  21   ASM_CASES_TAC `m = 0` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
  22   ASM_CASES_TAC `n = 0` THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
  23   DISJ_CASES_THEN MP_TAC (ARITH_RULE `m <= n:num \/ n <= m`) THEN
  24   REWRITE_TAC[LE_EXISTS] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
  25   DISCH_THEN(X_CHOOSE_THEN `p:num` SUBST_ALL_TAC) THENL
  26    [ALL_TAC; ASM (GEN_REWRITE_TAC I) []] THEN
  27   MATCH_MP_TAC(ASSUME `!m n:num. P m n ==> P n (m + n)`) THEN
  28   FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_ARITH_TAC);;
  29
  30 (* ------------------------------------------------------------------------- *)
  31 (* The main results; to literally apply integer gcd we need nonnegativity.   *)
  32 (* ------------------------------------------------------------------------- *)
  33
  34 let INT_DIVISORS_RECURRENCE = prove
  35  (`!G a b. G(0) = &0 /\ G(1) = &1 /\
  36            coprime(a,b) /\ (!n. G(n + 2) = a * G(n + 1) + b * G(n))
  37            ==> !d m n. d divides (G m) /\ d divides (G n) <=>
  38                        d divides G(gcd(m,n))`,
  39   REPEAT GEN_TAC THEN STRIP_TAC THEN
  40   SUBGOAL_THEN `!n. coprime(G(n + 1),b)` ASSUME_TAC THENL
  41    [INDUCT_TAC THEN ASM_REWRITE_TAC[ARITH; ARITH_RULE `SUC n + 1 = n + 2`] THEN
  42     REPEAT(POP_ASSUM MP_TAC) THEN NUMBER_TAC;
  43     ALL_TAC] THEN
  44   SUBGOAL_THEN `!n. coprime(G(n + 1),G n)` ASSUME_TAC THENL
  45    [INDUCT_TAC THENL [ASM_REWRITE_TAC[ARITH] THEN NUMBER_TAC; ALL_TAC] THEN
  46     REPEAT(FIRST_X_ASSUM(ASSUME_TAC o SPEC `n:num`)) THEN
  47     ASM_REWRITE_TAC[ADD1; ARITH_RULE `(n + 1) + 1 = n + 2`] THEN
  48     REPEAT(POP_ASSUM MP_TAC) THEN INTEGER_TAC;
  49     ALL_TAC] THEN
  50   SUBGOAL_THEN `!m p. G(m + 1 + p) = G(m + 1) * G(p + 1) + b * G(m) * G(p)`
  51   ASSUME_TAC THENL
  52    [INDUCT_TAC THENL
  53      [ASM_REWRITE_TAC[ADD_CLAUSES; ADD_AC] THEN INTEGER_TAC; ALL_TAC] THEN
  54     ASM_REWRITE_TAC[ARITH_RULE `SUC m + 1 + p = (m + p) + 2`] THEN
  55     ASM_REWRITE_TAC[ARITH_RULE `SUC m + 1 = m + 2`] THEN
  56     ASM_REWRITE_TAC[ARITH_RULE `(m + p) + 1 = m + 1 + p`] THEN
  57     INDUCT_TAC THEN ASM_REWRITE_TAC[ARITH; ADD_CLAUSES] THEN
  58     ASM_REWRITE_TAC[ARITH_RULE `SUC(m + p) = m + 1 + p`] THEN
  59     ASM_REWRITE_TAC[ARITH_RULE `SUC(m + 1) = m + 2`; ARITH] THEN
  60     REWRITE_TAC[ADD1] THEN ARITH_TAC;
  61     ALL_TAC] THEN
  62   SUBGOAL_THEN `!m p:num. gcd(G(m + p),G m) = gcd(G m,G p)` ASSUME_TAC THENL
  63    [INDUCT_TAC THEN
  64     REWRITE_TAC[ADD_CLAUSES; EQT_INTRO(SPEC_ALL INT_GCD_SYM)] THEN
  65     ASM_REWRITE_TAC[ADD1; ARITH_RULE `(m + p) + 1 = m + 1 + p`] THEN
  66     GEN_TAC THEN SIMP_TAC[INT_GCD_POS; GSYM INT_DIVIDES_ANTISYM_POS] THEN
  67     MP_TAC(SPEC `m:num` (ASSUME `!n. coprime(G(n + 1),b)`)) THEN
  68     MP_TAC(SPEC `m:num` (ASSUME `!n. coprime(G(n + 1),G n)`)) THEN
  69     INTEGER_TAC;
  70     ALL_TAC] THEN
  71   GEN_TAC THEN MATCH_MP_TAC INDUCT_SPECIAL THEN REPEAT CONJ_TAC THENL
  72    [ASM_REWRITE_TAC[GCD_0; INT_DIVIDES_0]; MESON_TAC[GCD_SYM]; ALL_TAC] THEN
  73   ASM_MESON_TAC[GCD_ADD; INT_DIVIDES_GCD; INT_GCD_SYM; ADD_SYM; GCD_SYM]);;
  74
  75 let INT_GCD_RECURRENCE = prove
  76  (`!G a b. G(0) = &0 /\ G(1) = &1 /\
  77            coprime(a,b) /\ (!n. G(n + 2) = a * G(n + 1) + b * G(n)) /\
  78            (!n. &0 <= G n)
  79            ==> !m n. gcd(G m,G n) = G(gcd(m,n))`,
  80   REPEAT GEN_TAC THEN DISCH_TAC THEN
  81   ASM_SIMP_TAC[GSYM INT_DIVIDES_ANTISYM_POS; INT_GCD_POS] THEN
  82   REWRITE_TAC[INT_DIVIDES_ANTISYM_DIVISORS; INT_DIVIDES_GCD] THEN
  83   ASM_MESON_TAC[INT_DIVISORS_RECURRENCE]);;
  84
  85 (* ------------------------------------------------------------------------- *)
  86 (* Natural number variants of the same results.                              *)
  87 (* ------------------------------------------------------------------------- *)
  88
  89 let GCD_RECURRENCE = prove
  90  (`!G a b. G(0) = 0 /\ G(1) = 1 /\
  91            coprime(a,b) /\ (!n. G(n + 2) = a * G(n + 1) + b * G(n))
  92            ==> !m n. gcd(G m,G n) = G(gcd(m,n))`,
  93   REPEAT STRIP_TAC THEN
  94   MP_TAC(SPECL [`& o (G:num->num)`; `&a:int`; `&b:int`]
  95         INT_GCD_RECURRENCE) THEN
  96   ASM_REWRITE_TAC[o_THM; GSYM INT_OF_NUM_ADD; GSYM INT_OF_NUM_MUL] THEN
  97   ASM_SIMP_TAC[GSYM num_coprime; INT_POS; GSYM NUM_GCD; INT_OF_NUM_EQ]);;
  98
  99 let DIVISORS_RECURRENCE = prove
 100  (`!G a b. G(0) = 0 /\ G(1) = 1 /\
 101            coprime(a,b) /\ (!n. G(n + 2) = a * G(n + 1) + b * G(n))
 102            ==> !d m n. d divides (G m) /\ d divides (G n) <=>
 103                        d divides G(gcd(m,n))`,
 104   REWRITE_TAC[GSYM DIVIDES_GCD] THEN MESON_TAC[DIVISORS_EQ; GCD_RECURRENCE]);;
 105
 106 (* ------------------------------------------------------------------------- *)
 107 (* Application 1: Mersenne numbers.                                          *)
 108 (* ------------------------------------------------------------------------- *)
 109
 110 let GCD_MERSENNE = prove
 111  (`!m n. gcd(2 EXP m - 1,2 EXP n - 1) = 2 EXP (gcd(m,n)) - 1`,
 112   SIMP_TAC[GSYM INT_OF_NUM_EQ; NUM_GCD; GSYM INT_OF_NUM_SUB;
 113            GSYM INT_OF_NUM_POW; EXP_LT_0; ARITH;
 114            ARITH_RULE `1 <= n <=> 0 < n`] THEN
 115   MATCH_MP_TAC INT_GCD_RECURRENCE THEN
 116   MAP_EVERY EXISTS_TAC [`&3`; `-- &2`] THEN
 117   REWRITE_TAC[INT_POW_ADD; INT_LE_SUB_LADD] THEN
 118   CONV_TAC INT_REDUCE_CONV THEN REPEAT CONJ_TAC THENL
 119    [REWRITE_TAC[GSYM(INT_REDUCE_CONV `&2 * &2 - &1`)] THEN
 120     SPEC_TAC(`&2`,`t:int`) THEN INTEGER_TAC;
 121     INT_ARITH_TAC;
 122     GEN_TAC THEN MATCH_MP_TAC INT_POW_LE_1 THEN INT_ARITH_TAC]);;
 123
 124 let DIVIDES_MERSENNE = prove
 125  (`!m n. (2 EXP m - 1) divides (2 EXP n - 1) <=> m divides n`,
 126   REPEAT GEN_TAC THEN
 127   REWRITE_TAC[DIVIDES_GCD_LEFT; GCD_MERSENNE] THEN
 128   SIMP_TAC[EXP_EQ_0; EQ_EXP; ARITH_EQ; ARITH_RULE
 129    `~(x = 0) /\ ~(y = 0) ==> (x - 1 = y - 1 <=> x = y)`]);;
 130
 131 (* ------------------------------------------------------------------------- *)
 132 (* Application 2: the Fibonacci series.                                      *)
 133 (* ------------------------------------------------------------------------- *)
 134
 135 let fib = define
 136  `fib 0 = 0 /\ fib 1 = 1 /\ !n. fib(n + 2) = fib(n + 1) + fib(n)`;;
 137
 138 let GCD_FIB = prove
 139  (`!m n. gcd(fib m,fib n) = fib(gcd(m,n))`,
 140   MATCH_MP_TAC GCD_RECURRENCE THEN
 141   REPEAT(EXISTS_TAC `1`) THEN REWRITE_TAC[fib; COPRIME_1] THEN ARITH_TAC);;
 142
 143 let FIB_EQ_0 = prove
 144  (`!n. fib n = 0 <=> n = 0`,
 145   MATCH_MP_TAC num_INDUCTION THEN REWRITE_TAC[fib] THEN
 146   MATCH_MP_TAC num_INDUCTION THEN
 147   REWRITE_TAC[fib; ARITH_RULE `SUC(SUC n) = n + 2`; ADD_EQ_0] THEN
 148   SIMP_TAC[ADD1; ADD_EQ_0; ARITH_EQ] THEN
 149   CONV_TAC NUM_REDUCE_CONV THEN REWRITE_TAC[fib; ARITH_EQ]);;
 150
 151 let FIB_INCREASES_LE = prove
 152  (`!m n. m <= n ==> fib m <= fib n`,
 153   MATCH_MP_TAC TRANSITIVE_STEPWISE_LE THEN
 154   REWRITE_TAC[LE_REFL; LE_TRANS] THEN
 155   MATCH_MP_TAC num_INDUCTION THEN REWRITE_TAC[fib; ARITH] THEN
 156   REWRITE_TAC[ADD1; fib; ARITH_RULE `(n + 1) + 1 = n + 2`] THEN
 157   ARITH_TAC);;
 158
 159 let FIB_INCREASES_LT = prove
 160  (`!m n. 2 <= m /\ m < n ==> fib m < fib n`,
 161   INDUCT_TAC THEN REWRITE_TAC[ARITH] THEN
 162   REPEAT STRIP_TAC THEN TRANS_TAC LTE_TRANS `fib(m + 2)` THEN
 163   ASM_SIMP_TAC[FIB_INCREASES_LE; ARITH_RULE `m + 2 <= n <=> SUC m < n`] THEN
 164   REWRITE_TAC[fib; ADD1; ARITH_RULE `m < m + n <=> ~(n = 0)`; FIB_EQ_0] THEN
 165   ASM_ARITH_TAC);;
 166
 167 let FIB_EQ_1 = prove
 168  (`!n. fib n = 1 <=> n = 1 \/ n = 2`,
 169   MATCH_MP_TAC num_INDUCTION THEN REWRITE_TAC[fib; ARITH] THEN
 170   MATCH_MP_TAC num_INDUCTION THEN REWRITE_TAC[fib; ARITH] THEN
 171   REWRITE_TAC[fib; ARITH_RULE `SUC(SUC n) = n + 2`] THEN
 172   REWRITE_TAC[FIB_EQ_0; ADD_EQ_0; ARITH; ARITH_RULE
 173    `m + n = 1 <=> m = 0 /\ n = 1 \/ m = 1 /\ n = 0`] THEN
 174   ARITH_TAC);;
 175
 176 let DIVIDES_FIB = prove
 177  (`!m n. (fib m) divides (fib n) <=> m divides n \/ n = 0 \/ m = 2`,
 178   REPEAT GEN_TAC THEN REWRITE_TAC[DIVIDES_GCD_LEFT; GCD_FIB] THEN
 179   MP_TAC(SPECL [`gcd(m:num,n)`; `m:num`] DIVIDES_LE) THEN REWRITE_TAC[GCD] THEN
 180   ASM_CASES_TAC `m = 0` THEN ASM_REWRITE_TAC[GCD_0; fib; FIB_EQ_0; ARITH] THEN
 181   ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[GCD_0] THEN
 182   ASM_CASES_TAC `gcd(m:num,n) = m` THEN ASM_REWRITE_TAC[LE_LT] THEN
 183   ASM_CASES_TAC `gcd(m:num,n) = 0` THENL
 184    [ASM_MESON_TAC[GCD_ZERO]; ALL_TAC] THEN
 185   ASM_CASES_TAC `m:num = n` THEN ASM_REWRITE_TAC[GCD_REFL; LT_REFL] THEN
 186   ASM_CASES_TAC `2 <= gcd(m,n)` THENL
 187    [MP_TAC(SPECL [`gcd(m:num,n)`; `m:num`] FIB_INCREASES_LT) THEN
 188     ASM_ARITH_TAC;
 189     ASM_CASES_TAC `gcd(m,n) = 1` THENL [ASM_REWRITE_TAC[]; ASM_ARITH_TAC] THEN
 190     DISCH_TAC THEN CONV_TAC(LAND_CONV SYM_CONV) THEN
 191     REWRITE_TAC[FIB_EQ_1; fib] THEN ASM_ARITH_TAC]);;
 192
 193 (* ------------------------------------------------------------------------- *)
 194 (* Application 3: solutions of the Pell equation x^2 = (a^2 - 1) y^2 + 1.    *)
 195 (* All solutions are of the form (pellx a n,pelly a n); see Examples/pell.ml *)
 196 (* ------------------------------------------------------------------------- *)
 197
 198 let pellx = define
 199   `(!a. pellx a 0 = 1) /\
 200    (!a. pellx a 1 = a) /\
 201    (!a n. pellx a (n + 2) = 2 * a * pellx a (n + 1) - pellx a n)`;;
 202
 203 let pelly = define
 204   `(!a. pelly a 0 = 0) /\
 205    (!a. pelly a 1 = 1) /\
 206    (!a n. pelly a (n + 2) = 2 * a * pelly a (n + 1) - pelly a (n))`;;
 207
 208 let PELLY_INCREASES = prove
 209  (`!a n. ~(a = 0) ==> pelly a n <= pelly a (n + 1)`,
 210   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
 211   INDUCT_TAC THEN
 212   ASM_SIMP_TAC[pelly; ARITH; LE_1; ADD1; ARITH_RULE `(n + 1) + 1 = n + 2`] THEN
 213   TRANS_TAC LE_TRANS `2 * pelly a (n + 1) - pelly a n` THEN
 214   CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
 215   MATCH_MP_TAC(ARITH_RULE `a:num <= b ==> a - c <= b - c`) THEN
 216   REWRITE_TAC[MULT_ASSOC; LE_MULT_RCANCEL] THEN ASM_ARITH_TAC);;
 217
 218 let GCD_PELLY = prove
 219  (`!a m n. ~(a = 0) ==> gcd(pelly a m,pelly a n) = pelly a (gcd(m,n))`,
 220   GEN_TAC THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN DISCH_TAC THEN
 221   REWRITE_TAC[GSYM INT_OF_NUM_EQ; NUM_GCD] THEN
 222   MATCH_MP_TAC INT_GCD_RECURRENCE THEN
 223   MAP_EVERY EXISTS_TAC [`&2 * &a:int`; `-- &1:int`] THEN
 224   REWRITE_TAC[pelly; INT_POS; INT_COPRIME_NEG; INT_COPRIME_1] THEN
 225   GEN_TAC THEN REWRITE_TAC[INT_OF_NUM_MUL; MULT_ASSOC] THEN
 226   REWRITE_TAC[INT_ARITH `a + -- &1 * b:int = a - b`] THEN
 227   MATCH_MP_TAC(GSYM INT_OF_NUM_SUB) THEN
 228   TRANS_TAC LE_TRANS `1 * pelly a (n + 1)` THEN
 229   REWRITE_TAC[LE_MULT_RCANCEL] THEN
 230   ASM_SIMP_TAC[MULT_CLAUSES; PELLY_INCREASES] THEN ASM_ARITH_TAC);;