text_formalization/local/LDURDPN.hl

   1 (* ========================================================================== *)\r
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)\r
   3 (*                                                                            *)\r
   4 (* Chapter: Local Fan                                                   *)\r
   5 (* Author: Nguyen Quang Truong                                          *)\r
   6 (* Date: 2010-05-09                                                           *)\r
   7 (* ========================================================================== *)\r
   8 \r
   9 (* ========== snapshot 1631 ============= *)\r
  10 flyspeck_needs "local/LVDUCXU.hl";; \r
  11 \r
  12 \r
  13 module type Ldurdpn_type = sig\r
  14 \r
  15 end;;\r
  16 \r
  17    \r
  18 module Ldurdpn = struct\r
  19 \r
  20 open Lvducxu;;\r
  21 open Sphere;;\r
  22 open Trigonometry1;;\r
  23 open Trigonometry2;;\r
  24 open Hypermap;;\r
  25 open Fan;;\r
  26 open Prove_by_refinement;;\r
  27 open Wrgcvdr_cizmrrh;;\r
  28 \r
  29 \r
  30 let SUBSET_P_HULL = prove(` (S:A -> bool) SUBSET P hull S`,\r
  31 REWRITE_TAC[HULL_SUBSET]);;\r
  32 \r
  33 let IN_HULL_INSERT = prove(`!x:A. x IN P hull ( x INSERT S ) `,\r
  34 GEN_TAC THEN \r
  35 MATCH_MP_TAC (SET_RULE` x IN S /\ S SUBSET P hull S ==> x IN P hull S `) THEN \r
  36 REWRITE_TAC[IN_INSERT; SUBSET_P_HULL]);;\r
  37 \r
  38 \r
  39 \r
  40 let VECTOR_SCALE_CHANGE = prove(` ~( a = &0 ) ==> \r
  41 ( a % x = y <=> x = &1 / a % y ) `,\r
  42 DISCH_TAC THEN EQ_TAC THENL [\r
  43 DISCH_THEN (SUBST1_TAC o SYM) THEN \r
  44 REWRITE_TAC[VECTOR_MUL_ASSOC] THEN \r
  45 ASM_SIMP_TAC[REAL_FIELD` ~( a = &0) ==> &1 / a * a = &1 `; VECTOR_MUL_LID];\r
  46 SIMP_TAC[VECTOR_MUL_ASSOC] THEN \r
  47 ASM_SIMP_TAC[REAL_FIELD` ~( a = &0) ==> a * &1 / a = &1 `; VECTOR_MUL_LID]]);;\r
  48 \r
  49 \r
  50 \r
  51 let AFF_CONV0_IN_AFF_LT = prove_by_refinement(\r
  52 ` ~collinear {vec 0, u, v} ==>\r
  53 ~(aff {vec 0, u} INTER conv0 {v, w} = {})\r
  54  ==> w IN aff_lt {vec 0, u} {v} `,\r
  55 [NHANH th3a;\r
  56 SIMP_TAC[AFF_LT_2_1; Geomdetail.CONV0_SET2; AFF2];\r
  57 REWRITE_TAC[SET_RULE` ~( a INTER b = {}) <=> ? x. x IN a /\ x IN b`;\r
  58 IN_ELIM_THM];\r
  59 REPEAT STRIP_TAC;\r
  60 DOWN;\r
  61 ASM_REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID];\r
  62 PAT_ONCE_REWRITE_TAC `\x. x ==> y` \r
  63 [VECTOR_ARITH` x = a + (b:real^N) <=> b = x + -- a `];\r
  64 ASSUME_TAC2 (REAL_ARITH` &0 < b ==> ~( b = &0 ) `);\r
  65 DOWN;\r
  66 SIMP_TAC[VECTOR_SCALE_CHANGE];\r
  67 REPEAT STRIP_TAC;\r
  68 REWRITE_TAC[VECTOR_MUL_ASSOC; VECTOR_ADD_LDISTRIB; GSYM VECTOR_MUL_LNEG];\r
  69 SUBGOAL_THEN ` (&1 / b * --a) < &0 ` MP_TAC;\r
  70 REWRITE_TAC[REAL_ARITH` &1 / b * --a < &0 <=> &0 < a / b `];\r
  71 MATCH_MP_TAC REAL_LT_DIV;\r
  72 ASM_REWRITE_TAC[];\r
  73 MESON_TAC[REAL_ARITH` (&1 - a - b ) + a + b = &1 `]]);;\r
  74 \r
  75 \r
  76 let LDURDPN = prove_by_refinement\r
  77 (` ~ collinear {vec 0, (u:real^3), v} /\ ~ collinear {vec 0, u, w}\r
  78 ==> ( azim (vec 0) u v w = pi <=> (? A. plane A /\\r
  79 {vec 0, u, v, w} SUBSET A) /\ ~( aff {vec 0, u} INTER conv0 {v, w} = {}) )`,\r
  80 [SIMP_TAC[AZIM_EQ_PI_ALT];\r
  81 STRIP_TAC;\r
  82 EQ_TAC;\r
  83 UNDISCH_TAC ` ~collinear {vec 0, (u:real^3), v}`;\r
  84 NHANH th3;\r
  85 SIMP_TAC[AFF_LT_2_1; plane];\r
  86 STRIP_TAC THEN STRIP_TAC;\r
  87 DOWN;\r
  88 REWRITE_TAC[IN_ELIM_THM];\r
  89 STRIP_TAC;\r
  90 CONJ_TAC;\r
  91 EXISTS_TAC ` affine hull {vec 0, (u:real^3), v}`;\r
  92 REWRITE_TAC[AFFINE_HULL_3; INSERT_SUBSET; EMPTY_SUBSET];\r
  93 CONJ_TAC;\r
  94 EXISTS_TAC `(vec 0):real^3 `;\r
  95 EXISTS_TAC ` u:real^3 `;\r
  96 EXISTS_TAC `v:real^3 `;\r
  97 ASM_REWRITE_TAC[];\r
  98 REWRITE_TAC[GSYM AFFINE_HULL_3];\r
  99 NGOAC;\r
 100 CONJ_TAC;\r
 101 MESON_TAC[INSERT_COMM; IN_HULL_INSERT];\r
 102 REWRITE_TAC[AFFINE_HULL_3; IN_ELIM_THM];\r
 103 DOWN THEN DOWN THEN PHA;\r
 104 MESON_TAC[];\r
 105 REWRITE_TAC[SET_RULE` ~( x INTER y = {}) <=> ?a. a IN x /\ a IN y`];\r
 106 EXISTS_TAC ` ( &1 / (&1 - t3)) % ((w:real^3) - t3 % v ) `;\r
 107 REWRITE_TAC[AFF2; Geomdetail.CONV0_SET2; IN_ELIM_THM];\r
 108 CONJ_TAC;\r
 109 EXISTS_TAC ` ( &1 / (&1 - t3)) * t1 `;\r
 110 REWRITE_TAC[GSYM VECTOR_MUL_ASSOC];\r
 111 ASM_SIMP_TAC[\r
 112 REAL_FIELD` t3 < &0 ==> &1 - &1 / (&1 - t3) * t1 = \r
 113 &1 / (&1 - t3) * (&1 - t3 - t1 ) `];\r
 114 REWRITE_TAC[GSYM VECTOR_ADD_LDISTRIB; GSYM VECTOR_MUL_ASSOC];\r
 115 MATCH_MP_TAC (MESON[]` x = y ==> f x = f y`);\r
 116 ASM_SIMP_TAC[REAL_RING` t1 + t2 + t3 = &1 ==> &1 - t3 - t1 = t2 `];\r
 117 VECTOR_ARITH_TAC;\r
 118 EXISTS_TAC ` ( &1 / (&1 - t3)) * ( -- t3) `;\r
 119 EXISTS_TAC ` ( &1 / (&1 - t3))  `;\r
 120 CONJ_TAC;\r
 121 MATCH_MP_TAC REAL_LT_MUL;\r
 122 ASM_REWRITE_TAC[GSYM (REAL_FIELD` t3 < &0 <=> &0 < -- t3 `)];\r
 123 MATCH_MP_TAC REAL_LT_DIV;\r
 124 ASM_REAL_ARITH_TAC;\r
 125 CONJ_TAC;\r
 126 MATCH_MP_TAC REAL_LT_DIV;\r
 127 ASM_REAL_ARITH_TAC;\r
 128 ASM_SIMP_TAC[\r
 129 REAL_FIELD` t3 < &0 ==> &1 / (&1 - t3) * --t3 + &1 / (&1 - t3) = &1 `];\r
 130 VECTOR_ARITH_TAC;\r
 131 ASM_SIMP_TAC[AFF_CONV0_IN_AFF_LT]]);;\r
 132 \r
 133 end;;\r