(* ========================================================================= *)
(* Proof that Tarski's axioms for geometry hold in Euclidean space.          *)
(* ========================================================================= *)

needs "Multivariate/convex.ml";;

(* ------------------------------------------------------------------------- *)
(* Axiom 1 (reflexivity for equidistance).                                   *)
(* ------------------------------------------------------------------------- *)

let TARSKI_AXIOM_1_EUCLIDEAN = prove
 (`!a b:real^2. dist(a,b) = dist(b,a)`,
  NORM_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Axiom 2 (transitivity for equidistance).                                  *)
(* ------------------------------------------------------------------------- *)

let TARSKI_AXIOM_2_EUCLIDEAN = prove
 (`!a b p q r s.
        dist(a,b) = dist(p,q) /\ dist(a,b) = dist(r,s)
        ==> dist(p,q) = dist(r,s)`,
  REAL_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Axiom 3 (identity for equidistance).                                      *)
(* ------------------------------------------------------------------------- *)

let TARSKI_AXIOM_3_EUCLIDEAN = prove
 (`!a b c. dist(a,b) = dist(c,c) ==> a = b`,
  NORM_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Axiom 4 (segment construction).                                           *)
(* ------------------------------------------------------------------------- *)

let TARSKI_AXIOM_4_EUCLIDEAN = prove
 (`!a q b c:real^2. ?x:real^2. between a (q,x) /\ dist(a,x) = dist(b,c)`,
  GEOM_ORIGIN_TAC `a:real^2` THEN REPEAT GEN_TAC THEN
  REWRITE_TAC[DIST_0] THEN ASM_CASES_TAC `q:real^2 = vec 0` THENL
   [ASM_SIMP_TAC[BETWEEN_REFL; VECTOR_CHOOSE_SIZE; DIST_POS_LE];
    EXISTS_TAC `--(dist(b:real^2,c) / norm(q) % q):real^2` THEN
    REWRITE_TAC[between; DIST_0] THEN
    REWRITE_TAC[dist; NORM_MUL; NORM_NEG; REAL_ABS_DIV; REAL_ABS_NORM;
                VECTOR_ARITH `q - --(a % q) = (&1 + a) % q`] THEN
    CONJ_TAC THENL
     [MATCH_MP_TAC(REAL_RING `a = &1 + b ==> a * q = q + b * q`) THEN
      SIMP_TAC[REAL_ABS_REFL; REAL_POS; REAL_LE_ADD; REAL_LE_DIV; NORM_POS_LE];
      ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0]]]);;

(* ------------------------------------------------------------------------- *)
(* Axiom 5 (five-segments axiom).                                            *)
(* ------------------------------------------------------------------------- *)

let TARSKI_AXIOM_5_EUCLIDEAN = prove
 (`!a b c x:real^2 a' b' c' x':real^2.
        ~(a = b) /\
        dist(a,b) = dist(a',b') /\
        dist(a,c) = dist(a',c') /\
        dist(b,c) = dist(b',c') /\
        between b (a,x) /\ between b' (a',x') /\ dist(b,x) = dist(b',x')
        ==> dist(c,x) = dist(c',x')`,
  let lemma = prove
   (`!a b x y:real^N.
      ~(b = a) /\ between b (a,x) /\ between b (a,y) /\ dist(b,x) = dist(b,y)
      ==> x = y`,
    REPEAT STRIP_TAC THEN REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP (REWRITE_RULE
     [IMP_CONJ] BETWEEN_EXISTS_EXTENSION))) THEN ASM_SIMP_TAC[] THEN
    REPEAT STRIP_TAC THEN UNDISCH_TAC `dist(b:real^N,x) = dist(b,y)` THEN
    ASM_REWRITE_TAC[NORM_ARITH `dist(b:real^N,b + x) = norm x`; NORM_MUL] THEN
    ASM_SIMP_TAC[REAL_EQ_MUL_RCANCEL; NORM_EQ_0; real_abs; VECTOR_SUB_EQ]) in
  REPEAT STRIP_TAC THEN MP_TAC(ISPECL
   [`a:real^2`; `b:real^2`; `c:real^2`; `a':real^2`; `b':real^2`; `c':real^2`]
   RIGID_TRANSFORMATION_BETWEEN_3) THEN
  ANTS_TAC THENL [ASM_MESON_TAC[DIST_EQ_0; DIST_SYM]; ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `k:real^2`
   (X_CHOOSE_THEN `f:real^2->real^2` (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC))) THEN
  DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN SUBST_ALL_TAC) THEN
  SUBGOAL_THEN `x' = k + (f:real^2->real^2) x` SUBST1_TAC THENL
   [MATCH_MP_TAC lemma THEN MAP_EVERY EXISTS_TAC
      [`k + (f:real^2->real^2) a`; `k + (f:real^2->real^2) b`];
    ALL_TAC] THEN
  ASM_REWRITE_TAC[NORM_ARITH `dist(a + x:real^N,a + y) = dist(x,y)`;
    BETWEEN_TRANSLATION; VECTOR_ARITH `a + x:real^N = a + y <=> x = y`] THEN
  ASM_MESON_TAC[BETWEEN_TRANSLATION; orthogonal_transformation;
                NORM_ARITH `dist(a + x:real^N,a + y) = dist(x,y)`;
                ORTHOGONAL_TRANSFORMATION_ISOMETRY; BETWEEN_LINEAR_IMAGE_EQ;
                DIST_EQ_0; ORTHOGONAL_TRANSFORMATION_INJECTIVE]);;

(* ------------------------------------------------------------------------- *)
(* Axiom 6 (identity for between-ness).                                      *)
(* ------------------------------------------------------------------------- *)

let TARSKI_AXIOM_6_EUCLIDEAN = prove
 (`!a b. between b (a,a) ==> a = b`,
  SIMP_TAC[BETWEEN_REFL_EQ]);;

(* ------------------------------------------------------------------------- *)
(* Axiom 7 (Pasch's axiom).                                                  *)
(* ------------------------------------------------------------------------- *)

let TARSKI_AXIOM_7_EUCLIDEAN = prove
 (`!a b c p q:real^2.
        between p (a,c) /\ between q (b,c)
        ==> ?x. between x (p,b) /\ between x (q,a)`,
  REPEAT GEN_TAC THEN ASM_CASES_TAC `q:real^2 = c` THENL
   [ASM_MESON_TAC[BETWEEN_REFL; BETWEEN_SYM]; POP_ASSUM MP_TAC] THEN
  ASM_CASES_TAC `p:real^2 = a /\ b:real^2 = q` THENL
   [ASM_MESON_TAC[BETWEEN_REFL; BETWEEN_SYM]; POP_ASSUM MP_TAC] THEN
  GEOM_ORIGIN_TAC `a:real^2` THEN GEOM_NORMALIZE_TAC `q:real^2` THEN
  CONJ_TAC THENL
   [ONCE_REWRITE_TAC[CONJ_SYM] THEN REWRITE_TAC[BETWEEN_REFL_EQ] THEN
    REWRITE_TAC[UNWIND_THM2; between; DIST_0] THEN NORM_ARITH_TAC;
    ALL_TAC] THEN
  GEOM_BASIS_MULTIPLE_TAC 1 `q:real^2` THEN SIMP_TAC
   [NORM_MUL; NORM_BASIS; real_abs; DIMINDEX_2; ARITH; REAL_MUL_RID] THEN
  GEN_TAC THEN REPEAT(DISCH_THEN(K ALL_TAC)) THEN SIMP_TAC[VECTOR_MUL_LID] THEN
  REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[BETWEEN_SYM] THEN DISCH_TAC THEN
  DISCH_TAC THEN DISCH_THEN(CONJUNCTS_THEN2
   (X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC o
     REWRITE_RULE[BETWEEN_IN_SEGMENT; IN_SEGMENT])
   (MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ] BETWEEN_EXISTS_EXTENSION))) THEN
  ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `e:real` THEN
  STRIP_TAC THEN ASM_REWRITE_TAC[BETWEEN_IN_SEGMENT; IN_SEGMENT] THEN
  REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
  SUBGOAL_THEN `&0 < &1 - d + e` ASSUME_TAC THENL
   [ASM_CASES_TAC `d = &1 /\ e = &0` THENL [ALL_TAC; ASM_REAL_ARITH_TAC] THEN
    REPEAT(FIRST_X_ASSUM(MP_TAC o check (is_eq o concl))) THEN
    ASM_REWRITE_TAC[REAL_SUB_REFL; VECTOR_MUL_LZERO; VECTOR_MUL_RZERO] THEN
    ASM_REWRITE_TAC[VECTOR_ADD_RID; IMP_IMP];
    EXISTS_TAC `(&1 - d + e - d * e) / (&1 - d + e) % basis 1:real^2` THEN
    CONJ_TAC THENL
     [EXISTS_TAC `e / (&1 - d + e)` THEN
      ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ] THEN
      REPEAT(CONJ_TAC THENL [ASM_REAL_ARITH_TAC; ALL_TAC]) THEN
      SIMP_TAC[CART_EQ; DIMINDEX_2; FORALL_2; BASIS_COMPONENT; VEC_COMPONENT;
       ARITH; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
       VECTOR_SUB_COMPONENT] THEN
      UNDISCH_TAC `&0 < &1 - d + e` THEN CONV_TAC REAL_FIELD;
      EXISTS_TAC `(&1 - d + e - d * e) / (&1 - d + e)` THEN
      ASM_SIMP_TAC[REAL_LE_LDIV_EQ; REAL_LE_RDIV_EQ] THEN
      SUBGOAL_THEN `&0 <= (&1 - d) * (&1 + e) /\ &0 <= d * e` MP_TAC THENL
       [CONJ_TAC THEN MATCH_MP_TAC REAL_LE_MUL; ALL_TAC] THEN
      ASM_REAL_ARITH_TAC]]);;

(* ------------------------------------------------------------------------- *)
(* Axiom 8 (lower 2-dimensional axiom).                                      *)
(* ------------------------------------------------------------------------- *)

let TARSKI_AXIOM_8_EUCLIDEAN = prove
 (`?a b c:real^2. ~between b (a,c) /\ ~between c (b,a) /\ ~between a (c,b)`,
  REWRITE_TAC[GSYM DE_MORGAN_THM] THEN ONCE_REWRITE_TAC[BETWEEN_SYM] THEN
  REWRITE_TAC[GSYM COLLINEAR_BETWEEN_CASES; COLLINEAR_3_2D] THEN
  MAP_EVERY EXISTS_TAC
   [`vec 0:real^2`; `basis 1:real^2`; `basis 2:real^2`] THEN
  SIMP_TAC[BASIS_COMPONENT; VEC_COMPONENT; DIMINDEX_2; ARITH] THEN
  CONV_TAC REAL_RAT_REDUCE_CONV);;

(* ------------------------------------------------------------------------- *)
(* Axiom 9 (upper 2-dimensional axiom).                                      *)
(* ------------------------------------------------------------------------- *)

let TARSKI_AXIOM_9_EUCLIDEAN = prove
 (`!p q a b c:real^2.
        ~(p = q) /\
        dist(a,p) = dist(a,q) /\ dist(b,p) = dist(b,q) /\ dist(c,p) = dist(c,q)
        ==> between b (a,c) \/ between c (b,a) \/ between a (c,b)`,
  REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[BETWEEN_SYM] THEN
  REWRITE_TAC[GSYM COLLINEAR_BETWEEN_CASES] THEN
  REWRITE_TAC[dist; NORM_EQ; NORM_ARITH
    `~(p = q) <=> ~(norm(p - q) = &0)`] THEN
  ONCE_REWRITE_TAC[REAL_RING `~(x = &0) <=> ~(x pow 2 = &0)`] THEN
  REWRITE_TAC[NORM_POW_2; COLLINEAR_3_2D] THEN
  REWRITE_TAC[DOT_2; VECTOR_SUB_COMPONENT] THEN
  CONV_TAC REAL_FIELD);;

(* ------------------------------------------------------------------------- *)
(* Axiom 10 (Euclidean axiom).                                               *)
(* ------------------------------------------------------------------------- *)

let TARSKI_AXIOM_10_EUCLIDEAN = prove
 (`!a b c d t:real^N.
        between d (a,t) /\ between d (b,c) /\ ~(a = d)
        ==> ?x y. between b (a,x) /\ between c (a,y) /\ between t (x,y)`,
  REPEAT GEN_TAC THEN GEOM_ORIGIN_TAC `a:real^N` THEN REPEAT STRIP_TAC THEN
  MP_TAC(ISPECL [`vec 0:real^N`; `d:real^N`; `t:real^N`]
        BETWEEN_EXISTS_EXTENSION) THEN
  ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM; VECTOR_ARITH
   `d + u % (d - vec 0):real^N = (&1 + u) % d`] THEN
  X_GEN_TAC `u:real` THEN STRIP_TAC THEN
  MAP_EVERY EXISTS_TAC [`(&1 + u) % b:real^N`; `(&1 + u) % c:real^N`] THEN
  ASM_REWRITE_TAC[between; dist; GSYM VECTOR_SUB_LDISTRIB] THEN
  ASM_REWRITE_TAC[VECTOR_SUB_LZERO; NORM_NEG;
                  VECTOR_ARITH `b - (&1 + u) % b:real^N = --(u % b)`] THEN
  ASM_SIMP_TAC[NORM_MUL; REAL_LE_ADD; REAL_POS; real_abs] THEN
  REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; REAL_EQ_MUL_LCANCEL] THEN
  ASM_REWRITE_TAC[GSYM dist; GSYM between] THEN REAL_ARITH_TAC);;

(* ------------------------------------------------------------------------- *)
(* Axiom 11 (Continuity).                                                    *)
(* ------------------------------------------------------------------------- *)

let TARSKI_AXIOM_11_EUCLIDEAN = prove
 (`!X Y:real^2->bool.
        (?a. !x y. x IN X /\ y IN Y ==> between x (a,y))
        ==> (?b. !x y. x IN X /\ y IN Y ==> between b (x,y))`,
  REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN GEOM_ORIGIN_TAC `a:real^2` THEN
  REPEAT GEN_TAC THEN ASM_CASES_TAC `!x:real^2. x IN X ==> x = vec 0` THENL
   [ASM_MESON_TAC[BETWEEN_REFL]; POP_ASSUM MP_TAC] THEN
  ASM_CASES_TAC `Y:real^2->bool = {}` THEN ASM_REWRITE_TAC[NOT_IN_EMPTY] THEN
  SUBGOAL_THEN `?c:real^2. c IN Y` (CHOOSE_THEN MP_TAC) THENL
   [ASM SET_TAC[]; REPEAT(POP_ASSUM MP_TAC)] THEN
  GEOM_BASIS_MULTIPLE_TAC 1 `c:real^2` THEN
  X_GEN_TAC `c:real` THEN DISCH_TAC THEN REPEAT GEN_TAC THEN
  DISCH_TAC THEN DISCH_TAC THEN REWRITE_TAC[NOT_FORALL_THM; NOT_IMP] THEN
  DISCH_THEN(X_CHOOSE_THEN `z:real^2` STRIP_ASSUME_TAC) THEN
  DISCH_THEN(LABEL_TAC "*") THEN
  SUBGOAL_THEN `X SUBSET IMAGE (\c. c % basis 1:real^2) {c | &0 <= c} /\
                Y SUBSET IMAGE (\c. c % basis 1:real^2) {c | &0 <= c}`
  MP_TAC THENL
   [REWRITE_TAC[SUBSET; IN_IMAGE; IN_ELIM_THM] THEN
    MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL
     [X_GEN_TAC `x:real^2` THEN DISCH_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL
       [`x:real^2`; `c % basis 1:real^2`]) THEN
      ASM_REWRITE_TAC[BETWEEN_IN_SEGMENT; IN_SEGMENT] THEN
      REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; IN_ELIM_THM] THEN
      ASM_MESON_TAC[VECTOR_MUL_ASSOC; REAL_LE_MUL];
      DISCH_THEN(MP_TAC o SPEC `z:real^2`) THEN ASM_REWRITE_TAC[] THEN
      DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN
      UNDISCH_TAC `~(z:real^2 = vec 0)` THEN
      ASM_REWRITE_TAC[VECTOR_MUL_EQ_0; DE_MORGAN_THM] THEN
      STRIP_TAC THEN X_GEN_TAC `y:real^2` THEN DISCH_TAC THEN
      REMOVE_THEN "*" (MP_TAC o SPECL [`z:real^2`; `y:real^2`]) THEN
      ASM_REWRITE_TAC[VECTOR_MUL_ASSOC] THEN
      REWRITE_TAC[BETWEEN_IN_SEGMENT; IN_SEGMENT] THEN
      REWRITE_TAC[VECTOR_MUL_RZERO; VECTOR_ADD_LID; IN_ELIM_THM] THEN
      DISCH_THEN(X_CHOOSE_THEN `u:real` MP_TAC) THEN
      ASM_CASES_TAC `u = &0` THEN
      ASM_REWRITE_TAC[VECTOR_MUL_LZERO; VECTOR_MUL_EQ_0] THEN
      STRIP_TAC THEN EXISTS_TAC `inv(u) * d:real` THEN
      ASM_REWRITE_TAC[GSYM VECTOR_MUL_ASSOC] THEN
      ASM_SIMP_TAC[REAL_LE_MUL; REAL_LE_INV_EQ; VECTOR_MUL_ASSOC] THEN
      ASM_SIMP_TAC[REAL_MUL_LINV; VECTOR_MUL_LID]];
    REWRITE_TAC[SUBSET_IMAGE] THEN REWRITE_TAC[SUBSET; IN_ELIM_THM] THEN
    DISCH_THEN(CONJUNCTS_THEN2
     (X_CHOOSE_THEN `s:real->bool` STRIP_ASSUME_TAC)
     (X_CHOOSE_THEN `t:real->bool` STRIP_ASSUME_TAC)) THEN
    REMOVE_THEN "*" MP_TAC THEN
    ASM_REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM; FORALL_IN_IMAGE] THEN
    DISCH_THEN(fun th ->
      EXISTS_TAC `sup s % basis 1 :real^2` THEN MP_TAC th) THEN
    REWRITE_TAC[between; dist; NORM_ARITH `norm(vec 0 - x) = norm x`] THEN
    REWRITE_TAC[GSYM VECTOR_SUB_RDISTRIB; NORM_MUL] THEN
    SIMP_TAC[NORM_BASIS; DIMINDEX_GE_1; LE_REFL; REAL_MUL_RID] THEN
    ASM_SIMP_TAC[REAL_ARITH
     `&0 <= x /\ &0 <= y ==> (abs y = abs x + abs(x - y) <=> x <= y)`] THEN
    DISCH_TAC THEN X_GEN_TAC `x:real` THEN DISCH_TAC THEN
    X_GEN_TAC `y:real` THEN DISCH_TAC THEN MATCH_MP_TAC(REAL_ARITH
     `x <= s /\ s <= y ==> abs(x - y) = abs(x - s) + abs(s - y)`) THEN
    MP_TAC(SPEC `s:real->bool` SUP) THEN
    ASM_MESON_TAC[IMAGE_EQ_EMPTY; MEMBER_NOT_EMPTY]]);;