legacy/oldleg/hull_error.ml

   1 (* The following lemmas were removed from hull.ml on
   2    November 11, 2008 by T Hales, because the proofs are in error.
   3    They can be returned to hull.ml when the proofs are corrected.
   4 *)
   5
   6
   7 let VSUM_2 = prove
   8   ( `! (v:num->real^N). vsum (1..2)  v  = (v 1) + (v 2)`,
   9   GEN_TAC THEN REWRITE_TAC[vsum; SUM_2] THEN VECTOR_ARITH_TAC);;
  10
  11
  12 let affcomb_imp_aff = prove
  13   ( `!(S:real^N->bool). affine_comb S ==> affine S`,
  14     GEN_TAC THEN REWRITE_TAC[affine;affine_comb] THEN STRIP_TAC THEN REPEAT GEN_TAC THEN
  15     FIRST_X_ASSUM (MP_TAC o SPECL [`2`;`(\i. if (i=1) then t else (&1-t))`;`(\i. if (i=1) then (u:real^N) else (v:real^N))`])
  16     THEN SIMP_TAC[SUM_2;VSUM_2;ARITH_RULE `~(1=2)/\(!t. t + (&1 - t) = &1)`] THEN MESON_TAC[]);;
  17
  18
  19 let aff_imp_affcomb = prove
  20 ( `!(S:real^N->bool). affine S ==> affine_comb S`,
  21 GEN_TAC THEN REWRITE_TAC[affine;affine_comb] THEN
  22 DISCH_THEN (LABEL_TAC "1") THEN INDUCT_TAC THENL
  23 [ SIMP_TAC[SUM_CLAUSES_NUMSEG; ARITH_RULE `~(1=0) /\ ~ ( &1 = &0)`]; ALL_TAC ] THEN
  24 REPEAT GEN_TAC THEN REWRITE_TAC[ADD1] THEN ASM_CASES_TAC `( n = 0)` THENL
  25 [ ASM_SIMP_TAC[ARITH_RULE `0+1=1`] THEN REWRITE_TAC[SUM_SING_NUMSEG;NUMSEG_SING;VSUM_SING] THEN
  26 STRIP_TAC THEN ASM_SIMP_TAC[VECTOR_MUL_LID] THEN FIRST_ASSUM (MATCH_MP_TAC o SPEC `1`) THEN
  27 REWRITE_TAC[IN_SING; GSYM IN]; ALL_TAC ] THEN
  28 DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "3") (LABEL_TAC "4")) THEN
  29 UNDISCH_TAC (`sum (1..n + 1) (\i. t i) = &1`) THEN UNDISCH_TAC (`~(n=0)`)  THEN
  30 REWRITE_TAC[IMP_IMP] THEN DISCH_THEN (LABEL_TAC "5") THEN
  31 FIRST_ASSUM(MP_TAC o (MATCH_MP comb_trans)) THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
  32 ABBREV_TAC `(f:num->real^N) (i:num) = (&n * (t:num->real) i) % (v:num->real^N) i + (&1 - &n * t i) % v (n + 1)` THEN
  33 FIRST_X_ASSUM ((LABEL_TAC "6") o GSYM) THEN
  34 ABBREV_TAC `(ts:num->real) (i:num) = &1 / &n` THEN
  35 FIRST_X_ASSUM ((LABEL_TAC "7") o GSYM) THEN
  36 FIRST_ASSUM(MATCH_MP_TAC o (SPECL [`(ts:num->real)`;`(f:num->real^N)`])) THEN CONJ_TAC THENL
  37 [ ASM_REWRITE_TAC[SUM_CONST_NUMSEG; ARITH_RULE ` (n+1) - 1 = n`] THEN
  38 USE_THEN "5" (MP_TAC o (MATCH_MP (TAUT ` A/\B ==> A`))) THEN
  39 MESON_TAC[REAL_OF_NUM_NOT_EQ;REAL_DIV_LMUL]; GEN_TAC ] THEN ASM_REWRITE_TAC[] THEN
  40 DISCH_THEN (LABEL_TAC "8") THEN
  41 USE_THEN "1" (MATCH_MP_TAC o (SPECL [`(v:num->real^N) (i:num)`;`(v:num->real^N) ((n:num) +1)`;`(&n * t i):real`])) THEN
  42 CONJ_TAC THENL
  43 [ USE_THEN "4" (MATCH_MP_TAC o (SPEC `i:num`)) THEN UNDISCH_TAC (`(1..n) i`) THEN
  44   REWRITE_TAC[numseg;IN_ELIM_THM] THEN ARITH_TAC;
  45   USE_THEN "4" (MATCH_MP_TAC o (SPEC `(n+1):num`)) THEN UNDISCH_TAC (`(1..n) i`) THEN
  46   REWRITE_TAC[numseg;IN_ELIM_THM] THEN ARITH_TAC]);;
  47
  48
  49 let affine_affcomb = prove
  50 ( ` !(S:real^N->bool). affine(aff_comb S)`,
  51 REWRITE_TAC[affine;aff_comb] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN EXISTS_TAC `(n:num) + (n':num)` THEN
  52 ABBREV_TAC `(ts:num->real) (i:num) = (if ((1..n) i) then ((t:real)*((t':num->real) i)) else (&1 - t)*((t'':num->real)(i - n)) )` THEN
  53 FIRST_X_ASSUM(LABEL_TAC "ts" o GSYM) THEN
  54 EXISTS_TAC `ts : num->real` THEN
  55 ABBREV_TAC `(vs:num->real^N) (i:num) = (if ((1..n) i) then (v':num->real^N) i else (v'':num->real^N) (i - n) )` THEN
  56 FIRST_X_ASSUM(LABEL_TAC "vs" o GSYM) THEN
  57 EXISTS_TAC `vs:num->real^N` THEN REPEAT CONJ_TAC THENL
  58 [ASM_REWRITE_TAC[GSYM (MATCH_MP SUM_COMBINE_R (ARITH_RULE `1 <= n+1 /\ n <= n+n'`))] THEN
  59  REWRITE_TAC[MATCH_MP SUM_CASES (SPEC_ALL FINITE_NUMSEG);IN;numseg;IN_ELIM_THM] THEN
  60 SIMP_TAC[ARITH_RULE `((1 <= i /\ i <= n) /\ ~(1 <= i /\ i <= n))= F`] THEN
  61 SIMP_TAC[ARITH_RULE `((n + 1 <= i /\ i <= n + n')/\1 <= i /\ i <= n)= F`] THEN
  62 SIMP_TAC[ARITH_RULE `((n + 1 <= i /\ i <= n + n') /\ ~(1 <= i /\ i <= n))= (1 + n <= i /\ i <= n' + n)`] THEN
  63 REWRITE_TAC[EMPTY_GSPEC;SUM_CLAUSES;REAL_ADD_LID;REAL_ADD_RID;REAL_ADD_AC] THEN
  64 REWRITE_TAC[SUM_LMUL;SUM_OFFSET;GSYM numseg] THEN
  65 UNDISCH_TAC `sum (1..n) (\i. t' i) = &1` THEN REWRITE_TAC[ETA_AX] THEN DISCH_TAC THEN
  66 ASM_REWRITE_TAC[ARITH_RULE `!(i:num). (i+n)-n=i`;REAL_MUL_RID] THEN ARITH_TAC;
  67 ASM_REWRITE_TAC[VMUL_CASES] THEN REWRITE_TAC [MATCH_MP VSUM_CASES (SPECL [`1`;`n+n':num`] FINITE_NUMSEG)] THEN
  68 REWRITE_TAC [IN;IN_ELIM_THM;numseg] THEN
  69 REWRITE_TAC [ARITH_RULE `((1 <= i /\ i <= n + n') /\ 1 <= i /\ i <= n) = (1 <= i /\ i <= n)`] THEN
  70 REWRITE_TAC [ARITH_RULE `((1 <= i /\ i <= n + n') /\ ~(1 <= i /\ i <= n)) = (1+n <= i /\ i <= n' + n)`] THEN
  71 REWRITE_TAC[GSYM VECTOR_MUL_ASSOC;GSYM numseg;VSUM_LMUL;VSUM_OFFSET;ARITH_RULE `!(i:num).(i+n)-n = i`]; ALL_TAC] THEN
  72 GEN_TAC THEN ASM_REWRITE_TAC[] THEN COND_CASES_TAC THENL
  73 [ UNDISCH_TAC `(1..n) i` ;UNDISCH_TAC `~(1..n) i`] THEN REWRITE_TAC[IMP_IMP;IN;IN_ELIM_THM;numseg] THENL
  74 [REWRITE_TAC[ARITH_RULE `((1 <= i /\ i <= n) /\ 1 <= i /\ i <= n + n')=(1 <= i /\ i <= n)`];
  75  REWRITE_TAC[ARITH_RULE `(~(1 <= i /\ i <= n) /\ 1 <= i /\ i <= n + n')=(1 <= (i - n) /\ (i-n) <= n')`]] THEN
  76 DISCH_TAC THENL
  77 [FIRST_ASSUM(MATCH_MP_TAC o (SPEC `i:num`));FIRST_ASSUM(MATCH_MP_TAC o (SPEC `(i-n):num`))] THEN
  78 ASM_REWRITE_TAC[numseg;IN;IN_ELIM_THM]);;
  79
  80
  81 let aff_eq_affcomb = prove
  82 ( `!(S:real^N->bool). aff S = aff_comb S`,
  83 GEN_TAC THEN MATCH_MP_TAC  SUBSET_ANTISYM THEN CONJ_TAC THENL
  84 [ REWRITE_TAC[aff] THEN MATCH_MP_TAC(hull_SUBSET) THEN MESON_TAC[SUBSET_affcomb;affine_affcomb];
  85   REWRITE_TAC[SUBSET;IN;aff_comb] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
  86   MP_TAC ( MATCH_MP aff_imp_affcomb (SPEC `S:real^N->bool` affine_aff)) THEN
  87   ASM_REWRITE_TAC[affine_comb] THEN DISCH_TAC THEN
  88   FIRST_X_ASSUM(MATCH_MP_TAC o (SPECL [`n:num`;`t:num->real`;`v:num->real^N`])) THEN
  89   ASM_REWRITE_TAC[] THEN GEN_TAC THEN FIRST_X_ASSUM (MP_TAC o (SPEC `i:num`)) THEN
  90   MATCH_MP_TAC(TAUT `(B==>C) ==> ((A==>B)==> A ==> C)`) THEN
  91   MP_TAC (SPEC `S:real^N->bool` SUBSET_aff) THEN MESON_TAC [SUBSET;IN]]);;
  92
  93 let aff_2 = prove (` ! (a:real^N) (b:real^N). aff {a,b} = {u| ?(t:real). u = t % a + (&1 - t) % b}`,
  94 REPEAT GEN_TAC THEN (ABBREV_TAC `(M:real^N ->bool) = {u| ?(t:real). u = t % a + (&1 - t) % b}`) THEN
  95 FIRST_X_ASSUM(LABEL_TAC "M" o GSYM) THEN
  96 MATCH_MP_TAC(SUBSET_ANTISYM) THEN CONJ_TAC THENL
  97 [ REWRITE_TAC[aff] THEN MATCH_MP_TAC(hull_SUBSET) THEN CONJ_TAC THENL
  98   [ ASM_REWRITE_TAC[SET_RULE ` {a,b} SUBSET M <=> (a IN M /\ b IN M)`;IN_ELIM_THM;IN] THEN
  99     CONJ_TAC  THENL [EXISTS_TAC `&1`; EXISTS_TAC `&0`] THEN VECTOR_ARITH_TAC;
 100     ASM_REWRITE_TAC[affine;IN_ELIM_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 101     EXISTS_TAC ` t * t' + (&1- t) * t''` THEN
 102     REWRITE_TAC[ARITH_RULE ` &1 - (t * t' + (&1 - t) * t'') = t * (&1 - t') + (&1 - t) * (&1 - t'')`] THEN
 103     VECTOR_ARITH_TAC
 104   ] ;
 105   ASM_REWRITE_TAC[SUBSET;IN_ELIM_THM;IN;aff_eq_affcomb;aff_comb] THEN GEN_TAC THEN STRIP_TAC THEN
 106   ABBREV_TAC `(ts: num ->real) i = ( if ( i = 1) then t else ( &1 - t))` THEN
 107   FIRST_X_ASSUM(LABEL_TAC "ts" o GSYM) THEN
 108   ABBREV_TAC `(vs: num ->real^N) i = ( if ( i = 1) then a else b)` THEN
 109   FIRST_X_ASSUM(LABEL_TAC "vs" o GSYM) THEN
 110   EXISTS_TAC `2` THEN EXISTS_TAC `(ts:num->real)` THEN EXISTS_TAC ` (vs:num->real^N) ` THEN
 111   ASM_REWRITE_TAC[SUM_2;VSUM_2;ARITH_RULE `~(2=1) /\ (t + &1 - t = &1)`] THEN
 112   GEN_TAC THEN STRIP_TAC THEN COND_CASES_TAC THEN ONCE_REWRITE_TAC[GSYM IN] THEN SET_TAC[]
 113 ]);;
 114
 115
 116
 117 (*
 118
 119
 120 let conv_insert = prove(`!S (v:real^3).
 121      FINITE S ==>
 122      (conv (v INSERT S) = {x | ?s t. (conv S s) /\ &0 <= t /\ t <= &1 /\ (x = t % s + (&1-t) % v)})`,
 123    REWRITE_TAC[conv;affsign;sgn_ge;FUN_EQ_THM;lin_combo;UNION_EMPTY];
 124    SIMP_TAC[FINITE_INSERT;FINITE_RULES;VSUM_CLAUSES;SUM_CLAUSES];
 125    REPEAT STRIP_TAC;
 126    ASM_REWRITE_TAC[elimin IN_INSERT;IN_ELIM_THM];
 127    REWRITE_TAC[TAUT `(p <=> q) = ((p ==> q) /\ (q ==> p))`] ;
 128    (*  *)
 129    DISJ_CASES_TAC (TAUT `(v IN S) \/ ~((v:real^3) IN S)`);;
 130
 131    REPEAT STRIP_TAC;
 132    EXISTS_TAC `x:real^3`;
 133    EXISTS_TAC `&1`;
 134    ASM_REWRITE_TAC[REAL_ARITH `&0 <= (&1) /\ (&1 <= (&1)) /\ (&1 - &1 = &0)`;VECTOR_MUL_LID;VECTOR_MUL_LZERO;VECTOR_ADD_RID;];
 135    ASM_MESON_TAC[];
 136    (* 2 *)
 137    ABBREV_TAC `g = \w. (if (w=v:real^3) then (t* f v + (&1 - t)) else t * f w)`;
 138    EXISTS_TAC `g:real^3->real`;
 139    CONJ_TAC;
 140    EXPAND_TAC "g";
 141    ASM_REWRITE_TAC[];
 142    UNDISCH_TAC `FINITE (S:real^3->bool)`;
 143    (* to here *)
 144
 145
 146
 147 *)
 148
 149