legacy/oldleg/hull.ml

   1 (*VUONG ANH QUYEN *)\r
   2 (* DEFINITIONS OF AFFINE HULL.                                          *)\r
   3 (* ==================================================================== *)\r
   4 \r
   5 (* -------------------------------------------------------------------- *)\r
   6 (* Two ways to define affine set & affine hull.                        *)\r
   7 (* -------------------------------------------------------------------- *)\r
   8 \r
   9 (* Define as in convex.ml                                               *)\r
  10 (* -------------------------------------------------------------------- *)\r
  11 \r
  12 (* Define using affine combination                                      *)\r
  13 (* -------------------------------------------------------------------- *)\r
  14 \r
  15 let affine_comb = new_definition `!(s:real^N->bool). affine_comb s = ! (n:num) (t:num->real) (v:num->real^N).\r
  16   ( sum (1..n) (\i. t i) = &1)/\(!i. ((1..n) i) ==>(s (v i)))\r
  17   ==> (s (vsum (1..n) (\i. (t i) % (v i))))`;;\r
  18 \r
  19 let aff_comb = new_definition `! (S:real^N -> bool) (w:real^N). aff_comb S w =(\r
  20   ? (n:num) (t:num->real) (v:num->real^N). \r
  21   (  sum (1..n) (\i. t i) = &1 ) /\ \r
  22   (w = vsum (1..n) (\i. (t i) % (v i)))/\ (!i. ((1..n) i) ==> (S (v i))) )`;;\r
  23 \r
  24 (* Some simple properties of affine, aff, affine_comb, aff_comb, hull   *)\r
  25 (* -------------------------------------------------------------------- *)\r
  26 \r
  27 let affine_INTERS = prove \r
  28   ( `(!s. s IN f ==> affine s) ==> affine(INTERS f)`,\r
  29   (REWRITE_TAC[affine;INTERS;IN;IN_ELIM_THM] THEN MESON_TAC[]));;\r
  30 \r
  31 let affine_aff = prove \r
  32   ( `!(s:real^N->bool). affine (aff s)`,\r
  33   (GEN_TAC THEN REWRITE_TAC[aff] THEN MESON_TAC[affine_INTERS;P_HULL]));;\r
  34 \r
  35 let aff_affine = prove\r
  36   ( `!s. affine S ==> aff S = S`,\r
  37   (SIMP_TAC[HULL_EQ;aff;affine_INTERS]));;\r
  38 \r
  39 let SUBSET_hull = prove  \r
  40   (`! s P. s SUBSET (P hull s)`,\r
  41   REPEAT GEN_TAC THEN REWRITE_TAC[SUBSET;hull;IN_INTERS] THEN SET_TAC[]);;\r
  42 \r
  43 let SUBSET_aff = prove \r
  44   ( `!(S:real^N->bool). S SUBSET aff S`, MESON_TAC [SUBSET;aff;SUBSET_hull]);;\r
  45 \r
  46 let SUBSET_affcomb = prove\r
  47 (`!(S:real^N->bool). S SUBSET (aff_comb S)`,\r
  48 GEN_TAC THEN REWRITE_TAC[SUBSET;IN;aff_comb] THEN GEN_TAC THEN STRIP_TAC THEN\r
  49 EXISTS_TAC `1` THEN EXISTS_TAC `(\(i:num). &1)` THEN EXISTS_TAC `(\(i:num). x:real^N)` THEN \r
  50 ASM_SIMP_TAC[SUM_SING_NUMSEG;NUMSEG_SING;VSUM_SING;VECTOR_MUL_LID;IN;IN_SING]);;\r
  51 \r
  52 let aff_SUBSET = prove\r
  53   (`!A B. A SUBSET B ==> aff A SUBSET aff B`,\r
  54   (REPEAT GEN_TAC THEN \r
  55    REWRITE_TAC [aff; hull;SUBSET;IN;INTERS;IN_INTERS;IN_ELIM_THM] THEN MESON_TAC[]));;\r
  56 \r
  57 let INTERS_SUBSET = prove\r
  58 (`!(S:(A->bool)->bool) (u:A->bool). u IN S ==> (INTERS S) SUBSET u`,\r
  59   REPEAT GEN_TAC THEN REWRITE_TAC[SUBSET;IN_INTERS] THEN MESON_TAC[]);;\r
  60 \r
  61 let hull_SUBSET = prove\r
  62 ( `!(P:(A->bool)->bool) (S:A->bool) (u:A->bool). (S SUBSET u)/\(P u) ==> (P hull S) SUBSET u`,\r
  63   REPEAT GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC[hull] THEN MATCH_MP_TAC (INTERS_SUBSET) THEN\r
  64   ASM_REWRITE_TAC[IN;IN_ELIM_THM]);;\r
  65 \r
  66 (* Some lemmas need using                                          *)\r
  67 (* --------------------------------------------------------------- *)\r
  68 \r
  69 \r
  70 (* VSUM_2 -> hull_error.ml *)\r
  71 \r
  72 let REAL_OF_NUM_NOT_EQ = prove\r
  73    ( `!n m. ~(m = n) <=> ~(&m = &n)`, MESON_TAC[REAL_OF_NUM_EQ]);;\r
  74 \r
  75 let VMUL_CASES = prove\r
  76   (`!(P:A->bool) (t:A->real) (t':A->real) (v:A->real^N) (v':A->real^N). (if P i then t i else t' i) % (if P i then v i else v' i) = (if P i then ( t i % v i) else (t' i % v' i))`,\r
  77   REPEAT GEN_TAC THEN REPEAT COND_CASES_TAC THEN ASM_MESON_TAC[]);;\r
  78 \r
  79 (* Relation between affine and affine_comb                         *)\r
  80 (* --------------------------------------------------------------- *)\r
  81 \r
  82 (* affcomb_imp_aff -> hull_error.ml *)\r
  83 \r
  84 \r
  85 let comb_trans = prove (\r
  86   `! (n:num) (t:num->real) (v:num->real^N). \r
  87 ~(n=0)/\(sum (1..n+1) (\i. t i) = &1)==> \r
  88 (vsum (1..n+1) (\i. (t i) % (v i)) = vsum (1..n) (\i. (&1 / &n) % ((&n * (t i)) % (v i) + (&1 - &n * (t i)) % (v (n+1)))))`,\r
  89   REPEAT GEN_TAC THEN \r
  90   REWRITE_TAC[ REAL_OF_NUM_NOT_EQ;VSUM_CMUL_NUMSEG; VECTOR_ADD_LDISTRIB;VSUM_ADD_NUMSEG] THEN\r
  91   REWRITE_TAC[GSYM VSUM_CMUL_NUMSEG; VECTOR_MUL_ASSOC;REAL_MUL_ASSOC;REAL_SUB_LDISTRIB] THEN\r
  92   STRIP_TAC THEN (FIRST_ASSUM (MP_TAC o MATCH_MP REAL_DIV_RMUL)) THEN STRIP_TAC THEN\r
  93   ASM_REWRITE_TAC[REAL_MUL_LID;REAL_MUL_RID] THEN\r
  94   REWRITE_TAC[MATCH_MP VSUM_CLAUSES_RIGHT (ARITH_RULE ` (0 < (n+1))/\(1 <= (n+1))`)] THEN\r
  95   ASM_REWRITE_TAC[ ARITH_RULE `! (n:num). (n + 1)-1 = n`;VSUM_RMUL] THEN\r
  96   ASM_REWRITE_TAC[SUM_CONST_NUMSEG;SUM_SUB_NUMSEG;REAL_MUL_SYM; ARITH_RULE `(n+1) -1 = n`] THEN\r
  97   (UNDISCH_TAC `sum (1..n + 1) (\i. t i) = &1`) THEN\r
  98   ASM_REWRITE_TAC [MATCH_MP SUM_CLAUSES_RIGHT (ARITH_RULE ` (0 < (n+1))/\(1 <= (n+1))`);ARITH_RULE `(n+1) - 1 = n`] THEN\r
  99   STRIP_TAC THEN \r
 100   FIRST_ASSUM (MP_TAC o MATCH_MP (ARITH_RULE ` (a + b= &1) ==> (&1 - a = b)`)) THEN REWRITE_TAC[ETA_AX] THEN\r
 101   MESON_TAC[vsum]);;\r
 102 \r
 103 \r
 104 \r
 105 (* aff_imp_affcomb -> hull_error.ml *)\r
 106 \r
 107 \r
 108 (* The equality between two ways of defining, aff & aff_comb         *)\r
 109 (* ------------------------------------------------------------------*)\r
 110 \r
 111 (* affine_affcomb -> hull_error.ml *)\r
 112 \r
 113 (* aff_eq_affcomb  -> hull_error.ml *)\r
 114 \r
 115 (* convex, added by thales *)\r
 116 \r
 117 let conv0pt = prove(`conv {} = {}:real^A->bool`,\r
 118    REWRITE_TAC[conv;sgn_ge;affsign;UNION_EMPTY;FUN_EQ_THM;elimin NOT_IN_EMPTY;lin_combo;SUM_CLAUSES]\r
 119    THEN REAL_ARITH_TAC);;\r
 120                     \r
 121 let conv1pt = prove(`!u. conv {u:real^A} = {u}`,\r
 122   REWRITE_TAC[conv;sgn_ge;affsign;FUN_EQ_THM;UNION_EMPTY;lin_combo;SUM_SING;VSUM_SING;elimin IN_SING] THEN\r
 123   REPEAT GEN_TAC THEN\r
 124   REWRITE_TAC[TAUT `(p <=> q) = ((p ==> q) /\ (q ==> p))`] THEN\r
 125   REPEAT STRIP_TAC THENL\r
 126   [ASM_MESON_TAC[VECTOR_MUL_LID];\r
 127   ASM_REWRITE_TAC[]] THEN\r
 128   EXISTS_TAC `\ (v:real^A). &1` THEN\r
 129   MESON_TAC[VECTOR_MUL_LID;REAL_ARITH `&0 <= &1`]\r
 130                    );;\r
 131 \r