Tutorial/Custom_tactics.ml

   1 needs "Tutorial/Vectors.ml";;
   2
   3 let points =
   4 [((0, -1), (0, -1), (2, 0)); ((0, -1), (0, 0), (2, 0));
   5  ((0, -1), (0, 1), (2, 0)); ((0, -1), (2, 0), (0, -1));
   6  ((0, -1), (2, 0), (0, 0)); ((0, -1), (2, 0), (0, 1));
   7  ((0, 0), (0, -1), (2, 0)); ((0, 0), (0, 0), (2, 0));
   8  ((0, 0), (0, 1), (2, 0)); ((0, 0), (2, 0), (-2, 0));
   9  ((0, 0), (2, 0), (0, -1)); ((0, 0), (2, 0), (0, 0));
  10  ((0, 0), (2, 0), (0, 1)); ((0, 0), (2, 0), (2, 0));
  11  ((0, 1), (0, -1), (2, 0)); ((0, 1), (0, 0), (2, 0));
  12  ((0, 1), (0, 1), (2, 0)); ((0, 1), (2, 0), (0, -1));
  13  ((0, 1), (2, 0), (0, 0)); ((0, 1), (2, 0), (0, 1));
  14  ((2, 0), (-2, 0), (0, 0)); ((2, 0), (0, -1), (0, -1));
  15  ((2, 0), (0, -1), (0, 0)); ((2, 0), (0, -1), (0, 1));
  16  ((2, 0), (0, 0), (-2, 0)); ((2, 0), (0, 0), (0, -1));
  17  ((2, 0), (0, 0), (0, 0)); ((2, 0), (0, 0), (0, 1));
  18  ((2, 0), (0, 0), (2, 0)); ((2, 0), (0, 1), (0, -1));
  19  ((2, 0), (0, 1), (0, 0)); ((2, 0), (0, 1), (0, 1));
  20  ((2, 0), (2, 0), (0, 0))];;
  21
  22 let ortho =
  23   let mult (x1,y1) (x2,y2) = (x1 * x2 + 2 * y1 * y2,x1 * y2 + y1 * x2)
  24   and add (x1,y1) (x2,y2) = (x1 + x2,y1 + y2) in
  25   let dot (x1,y1,z1) (x2,y2,z2) =
  26     end_itlist add [mult x1 x2; mult y1 y2; mult z1 z2] in
  27   fun (v1,v2) -> dot v1 v2 = (0,0);;
  28
  29 let opairs = filter ortho (allpairs (fun a b -> a,b) points points);;
  30
  31 let otrips = filter (fun (a,b,c) -> ortho(a,b) & ortho(a,c))
  32                     (allpairs (fun a (b,c) -> a,b,c) points opairs);;
  33
  34 let hol_of_value =
  35   let tm0 = `&0` and tm1 = `&2` and tm2 = `-- &2`
  36   and tm3 = `sqrt(&2)` and tm4 = `--sqrt(&2)` in
  37   function 0,0 -> tm0 | 2,0 -> tm1 | -2,0 -> tm2 | 0,1 -> tm3 | 0,-1 -> tm4;;
  38
  39 let hol_of_point =
  40   let ptm = `vector:(real)list->real^3` in
  41   fun (x,y,z) -> mk_comb(ptm,mk_flist(map hol_of_value [x;y;z]));;
  42
  43 let SQRT_2_POW = prove
  44  (`sqrt(&2) pow 2 = &2`,
  45   SIMP_TAC[SQRT_POW_2; REAL_POS]);;
  46
  47 let PROVE_NONTRIVIAL =
  48   let ptm = `~(x :real^3 = vec 0)` and xtm = `x:real^3` in
  49   fun x -> prove(vsubst [hol_of_point x,xtm] ptm,
  50                  GEN_REWRITE_TAC RAND_CONV [VECTOR_ZERO] THEN
  51                  MP_TAC SQRT_2_POW THEN CONV_TAC REAL_RING);;
  52
  53 let PROVE_ORTHOGONAL =
  54   let ptm = `orthogonal:real^3->real^3->bool` in
  55   fun (x,y) ->
  56    prove(list_mk_comb(ptm,[hol_of_point x;hol_of_point y]),
  57          ONCE_REWRITE_TAC[ORTHOGONAL_VECTOR] THEN
  58          MP_TAC SQRT_2_POW THEN CONV_TAC REAL_RING);;
  59
  60 let ppoint = let p = `P:real^3->bool` in fun v -> mk_comb(p,hol_of_point v);;
  61
  62 let DEDUCE_POINT_TAC pts =
  63   FIRST_X_ASSUM MATCH_MP_TAC THEN
  64   MAP_EVERY EXISTS_TAC (map hol_of_point pts) THEN
  65   ASM_REWRITE_TAC[];;
  66
  67 let rec KOCHEN_SPECKER_TAC set_0 set_1 =
  68   if intersect set_0 set_1 <> [] then
  69     let p = ppoint(hd(intersect set_0 set_1)) in
  70     let th1 = ASSUME(mk_neg p) and th2 = ASSUME p in
  71     ACCEPT_TAC(EQ_MP (EQF_INTRO th1) th2)
  72   else
  73     let prf_1 = filter (fun (a,b) -> mem a set_0) opairs
  74     and prf_0 = filter (fun (a,b,c) -> mem a set_1 & mem b set_1) otrips in
  75     let new_1 = map snd prf_1 and new_0 = map (fun (a,b,c) -> c) prf_0 in
  76     let set_0' = union new_0 set_0 and set_1' = union new_1 set_1 in
  77     let del_0 = subtract set_0' set_0 and del_1 = subtract set_1' set_1 in
  78     if del_0 <> [] or del_1 <> [] then
  79        let prv_0 x =
  80          let a,b,_ = find (fun (a,b,c) -> c = x) prf_0 in DEDUCE_POINT_TAC [a;b]
  81        and prv_1 x =
  82          let a,_ = find (fun (a,c) -> c = x) prf_1 in DEDUCE_POINT_TAC [a] in
  83       let newuns = list_mk_conj
  84         (map ppoint del_1 @ map (mk_neg o ppoint) del_0)
  85       and tacs = map prv_1 del_1 @ map prv_0 del_0 in
  86       SUBGOAL_THEN newuns STRIP_ASSUME_TAC THENL
  87        [REPEAT CONJ_TAC THENL tacs; ALL_TAC] THEN
  88       KOCHEN_SPECKER_TAC set_0' set_1'
  89     else
  90       let v = find (fun i -> not(mem i set_0) & not(mem i set_1)) points in
  91       ASM_CASES_TAC (ppoint v) THENL
  92        [KOCHEN_SPECKER_TAC set_0 (v::set_1);
  93         KOCHEN_SPECKER_TAC (v::set_0) set_1];;
  94
  95 let KOCHEN_SPECKER_LEMMA = prove
  96  (`!P. (!x y:real^3. ~(x = vec 0) /\ ~(y = vec 0) /\ orthogonal x y /\
  97                      ~(P x) ==> P y) /\
  98        (!x y z. ~(x = vec 0) /\ ~(y = vec 0) /\ ~(z = vec 0) /\
  99                 orthogonal x y /\ orthogonal x z /\ orthogonal y z /\
 100                 P x /\ P y ==> ~(P z))
 101        ==> F`,
 102   REPEAT STRIP_TAC THEN
 103   MAP_EVERY (ASSUME_TAC o PROVE_NONTRIVIAL) points THEN
 104   MAP_EVERY (ASSUME_TAC o PROVE_ORTHOGONAL) opairs THEN
 105   KOCHEN_SPECKER_TAC [] []);;
 106
 107 let NONTRIVIAL_CROSS = prove
 108  (`!x y. orthogonal x y /\ ~(x = vec 0) /\ ~(y = vec 0)
 109          ==> ~(x cross y = vec 0)`,
 110   REWRITE_TAC[GSYM DOT_EQ_0] THEN VEC3_TAC);;
 111
 112 let KOCHEN_SPECKER_PARADOX = prove
 113  (`~(?spin:real^3->num.
 114         !x y z. ~(x = vec 0) /\ ~(y = vec 0) /\ ~(z = vec 0) /\
 115                 orthogonal x y /\ orthogonal x z /\ orthogonal y z
 116                 ==> (spin x = 0) /\ (spin y = 1) /\ (spin z = 1) \/
 117                     (spin x = 1) /\ (spin y = 0) /\ (spin z = 1) \/
 118                     (spin x = 1) /\ (spin y = 1) /\ (spin z = 0))`,
 119   REPEAT STRIP_TAC THEN
 120   MP_TAC(SPEC `\x:real^3. spin(x) = 1` KOCHEN_SPECKER_LEMMA) THEN
 121   ASM_REWRITE_TAC[] THEN CONJ_TAC THEN
 122   POP_ASSUM MP_TAC THEN REPEAT(MATCH_MP_TAC MONO_FORALL THEN GEN_TAC) THEN
 123   DISCH_THEN(fun th -> STRIP_TAC THEN MP_TAC th) THEN
 124   ASM_MESON_TAC[ARITH_RULE `~(1 = 0)`; NONTRIVIAL_CROSS; ORTHOGONAL_CROSS]);;