legacy/linear_program/LinProg.ml

   1 (*Define the notion of solution*)
   2 let is_solution = define `is_solution xs (cs,b) <=>
   3          LENGTH xs = LENGTH cs /\
   4          ITLIST2 (\c x s. c * x + s) cs xs (&0) = b`;;
   5
   6 (*Useful tactic supporting double list induction -- written by John Harrison*)
   7 let LIST2_INDUCT_TAC =
   8   let list2_INDUCT = prove
   9    (`!P:(A)list->(B)list->bool.
  10          P [] [] /\
  11          (!h1 t1 h2 t2. P t1 t2 ==> P (CONS h1 t1) (CONS h2 t2))
  12          ==> !l1 l2. LENGTH l1 = LENGTH l2 ==> P l1 l2`,
  13      GEN_TAC THEN STRIP_TAC THEN
  14      LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN
  15      ASM_SIMP_TAC[LENGTH; NOT_SUC; SUC_INJ]) in
  16   MATCH_MP_TAC list2_INDUCT THEN
  17   CONJ_TAC THENL [ALL_TAC; REPLICATE_TAC 4 GEN_TAC THEN DISCH_TAC];;
  18
  19 (*Prove the most basic theorem of multiplying both sides with the same non-zero integer (homogeneity)*)
  20 let homogeneity_thm = prove(`!a b xs cs. ( ~(a = &0) ) ==> ( is_solution xs (cs,b) <=> is_solution xs ( MAP (\c. a*c) cs, a*b ) )`,
  21 REPEAT GEN_TAC THEN
  22 REWRITE_TAC[is_solution; LENGTH_MAP] THEN
  23 REWRITE_TAC[TAUT` (a/\b<=>a/\c) = (a ==> (b<=>c))`] THEN
  24 REPEAT DISCH_TAC THEN
  25 UNDISCH_TAC `~(a = &0)` THEN
  26 SPEC_TAC (`b:real`, `b:real`) THEN
  27 SPEC_TAC (`a:real`, `a:real`) THEN
  28 UNDISCH_TAC `LENGTH (xs:real list) = LENGTH (cs:real list)` THEN
  29 SPEC_TAC (`cs: real list`,`cs: real list`) THEN
  30 SPEC_TAC (`xs: real list`,`xs: real list`) THEN
  31 LIST2_INDUCT_TAC THENL [
  32         REPEAT GEN_TAC THEN
  33         REWRITE_TAC[MAP; ITLIST2] THEN
  34         REWRITE_TAC[REAL_FIELD `~(a = &0) ==> (&0 = b <=> &0 = a * b)`];
  35
  36         REWRITE_TAC[MAP; ITLIST2] THEN
  37         REWRITE_TAC[ARITH_RULE `(a:real)+b=c <=> b=c-a`] THEN
  38         REWRITE_TAC[ARITH_RULE `((a:real)* b) * c = a * (b * c)`] THEN
  39         REWRITE_TAC[ARITH_RULE `(a:real) * b - a * c = a * (b - c)`] THEN
  40         ASM_SIMP_TAC[]
  41 ] );;
  42