Tutorial/Vectors.ml

   1 needs "Multivariate/vectors.ml";;
   2
   3 needs "Examples/solovay.ml";;
   4
   5 g `orthogonal (A - B) (C - B)
   6    ==> norm(C - A) pow 2 = norm(B - A) pow 2 + norm(C - B) pow 2`;;
   7
   8 e SOLOVAY_VECTOR_TAC;;
   9 e(CONV_TAC REAL_RING);;
  10
  11 g`!x y:real^N. x dot y <= norm x * norm y`;;
  12 e SOLOVAY_VECTOR_TAC;;
  13
  14 (**** Needs external SDP solver
  15 needs "Examples/sos.ml";;
  16
  17 e(CONV_TAC REAL_SOS);;
  18
  19 let EXAMPLE_0 = prove
  20  (`!a x y:real^N. (y - x) dot (a - y) >= &0 ==> norm(y - a) <= norm(x - a)`,
  21   SOLOVAY_VECTOR_TAC THEN CONV_TAC REAL_SOS);;
  22 ****)
  23
  24 (*** Needs Rqe loaded
  25
  26 needs "Rqe/make.ml";;
  27 let EXAMPLE_10 = prove
  28  (`!x:real^N y.
  29         x dot y > &0
  30         ==> ?u. &0 < u /\
  31                 !v. &0 < v /\ v <= u ==> norm(v % y - x) < norm x`,
  32   SOLOVAY_VECTOR_TAC THEN
  33   W(fun (asl,w) -> MAP_EVERY (fun v -> SPEC_TAC(v,v)) (frees w)) THEN
  34   CONV_TAC REAL_QELIM_CONV);;
  35
  36 ****)
  37
  38 let FORALL_3 = prove
  39  (`(!i. 1 <= i /\ i <= 3 ==> P i) <=> P 1 /\ P 2 /\ P 3`,
  40   MESON_TAC[ARITH_RULE `1 <= i /\ i <= 3 <=> (i = 1) \/ (i = 2) \/ (i = 3)`]);;
  41
  42 let SUM_3 = prove
  43  (`!t. sum(1..3) t = t(1) + t(2) + t(3)`,
  44   REWRITE_TAC[num_CONV `3`; num_CONV `2`; SUM_CLAUSES_NUMSEG] THEN
  45   REWRITE_TAC[SUM_SING_NUMSEG; ARITH; REAL_ADD_ASSOC]);;
  46
  47 let VECTOR_3 = prove
  48  (`(vector [x;y;z] :real^3)$1 = x /\
  49    (vector [x;y;z] :real^3)$2 = y /\
  50    (vector [x;y;z] :real^3)$3 = z`,
  51   SIMP_TAC[vector; LAMBDA_BETA; DIMINDEX_3; LENGTH; ARITH] THEN
  52   REWRITE_TAC[num_CONV `2`; num_CONV `1`; EL; HD; TL]);;
  53
  54 let DOT_VECTOR = prove
  55  (`(vector [x1;y1;z1] :real^3) dot (vector [x2;y2;z2]) =
  56        x1 * x2 + y1 * y2 + z1 * z2`,
  57   REWRITE_TAC[dot; DIMINDEX_3; SUM_3; VECTOR_3]);;
  58
  59 let VECTOR_ZERO = prove
  60  (`(vector [x;y;z] :real^3 = vec 0) <=> x = &0 /\ y = &0 /\ z = &0`,
  61   SIMP_TAC[CART_EQ; DIMINDEX_3; FORALL_3; VEC_COMPONENT; VECTOR_3; ARITH]);;
  62
  63 let ORTHOGONAL_VECTOR = prove
  64  (`orthogonal (vector [x1;y1;z1] :real^3) (vector [x2;y2;z2]) =
  65         (x1 * x2 + y1 * y2 + z1 * z2 = &0)`,
  66   REWRITE_TAC[orthogonal; DOT_VECTOR]);;
  67
  68 parse_as_infix("cross",(20,"right"));;
  69
  70 let cross = new_definition
  71  `(a:real^3) cross (b:real^3) =
  72     vector [a$2 * b$3 - a$3 * b$2;
  73             a$3 * b$1 - a$1 * b$3;
  74             a$1 * b$2 - a$2 * b$1] :real^3`;;
  75
  76 let VEC3_TAC =
  77   SIMP_TAC[CART_EQ; LAMBDA_BETA; FORALL_3; SUM_3; DIMINDEX_3; VECTOR_3;
  78            vector_add; vec; dot; cross; orthogonal; basis; ARITH] THEN
  79   CONV_TAC REAL_RING;;
  80
  81 let VEC3_RULE tm = prove(tm,VEC3_TAC);;
  82
  83 let ORTHOGONAL_CROSS = VEC3_RULE
  84  `!x y. orthogonal (x cross y) x /\ orthogonal (x cross y) y /\
  85         orthogonal x (x cross y) /\ orthogonal y (x cross y)`;;
  86
  87 let LEMMA_0 = VEC3_RULE
  88  `~(basis 1 :real^3 = vec 0) /\
  89   ~(basis 2 :real^3 = vec 0) /\
  90   ~(basis 3 :real^3 = vec 0)`;;
  91
  92 let LEMMA_1 = VEC3_RULE `!u v. u dot (u cross v) = &0`;;
  93
  94 let LEMMA_2 = VEC3_RULE `!u v. v dot (u cross v) = &0`;;
  95
  96 let LEMMA_3 = VEC3_RULE `!u:real^3. vec 0 dot u = &0`;;
  97
  98 let LEMMA_4 = VEC3_RULE `!u:real^3. u dot vec 0 = &0`;;
  99
 100 let LEMMA_5 = VEC3_RULE `!x. x cross x = vec 0`;;
 101
 102 let LEMMA_6 = VEC3_RULE
 103  `!u. ~(u = vec 0)
 104       ==> ~(u cross basis 1 = vec 0) \/
 105           ~(u cross basis 2 = vec 0) \/
 106           ~(u cross basis 3 = vec 0)`;;
 107
 108 let LEMMA_7 = VEC3_RULE
 109  `!u v w. (u cross v = vec 0) ==> (u dot (v cross w) = &0)`;;
 110
 111 let NORMAL_EXISTS = prove
 112  (`!u v:real^3. ?w. ~(w = vec 0) /\ orthogonal u w /\ orthogonal v w`,
 113   REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC
 114    [`u:real^3 = vec 0`; `v:real^3 = vec 0`; `u cross v = vec 0`] THEN
 115   ASM_REWRITE_TAC[orthogonal] THEN
 116   ASM_MESON_TAC[LEMMA_0; LEMMA_1; LEMMA_2; LEMMA_3; LEMMA_4;
 117                 LEMMA_5; LEMMA_6; LEMMA_7]);;