(* ========================================================================= *)
(*               Formalization of Electromagnetic Optics                     *)
(*                                                                           *)
(*            (c) Copyright, Sanaz Khan Afshar & Vincent Aravantinos 2011-13 *)
(*                           Hardware Verification Group,                    *)
(*                           Concordia University                            *)
(*                                                                           *)
(*                Contact:   <s_khanaf@encs.concordia.ca>                    *)
(*                           <vincent@encs.concordia.ca>                     *)
(*                                                                           *)
(* Proving that (!x. A*e^(iax)+B*e^(ibx)=C*e^(icx)) ==> a=b=c /\ A+B=C       *)
(* Several versions of this result are proved that are useful in proofs.     *)
(* ========================================================================= *)



(** DERIVATION OF FUNCTIONS WITH REAL ARGUMENTS AND COMPLEX VALUES
 *
 * The proof of the lemma requires derivation of functions whose argument is 
 * real but whose value is complex. The theoretical background to do this in
 * HOL-Light is already present in the library, but the automation is not well
 * developped. In addition, we need several intermediate results which are
 * available only for complex derivations or only for general derivation, etc.
 * Hence we need a bit of work before getting the results we want.
 *)

let REAL_CMUL_TO_VECTOR_MUL = prove
  (`!a x. a * Cx x = x % a`,
  REWRITE_TAC[complex_mul;RE_DEF;IM_DEF;CX_DEF;complex;CART_EQ;DIMINDEX_2;
    FORALL_2;VECTOR_2;VECTOR_MUL_COMPONENT] THEN SIMPLE_COMPLEX_ARITH_TAC);;

let LINEAR_REAL_CMUL = prove
  (`!a. linear (\x. a * Cx (drop x))`,
  REWRITE_TAC[REAL_CMUL_TO_VECTOR_MUL;linear;drop;VECTOR_ADD_COMPONENT;
    VECTOR_MUL_COMPONENT]
  THEN VECTOR_ARITH_TAC);;

let HAS_VECTOR_DERIVATIVE_REAL_CMUL = prove
  (`!a x. ((\x. a * Cx (drop x)) has_vector_derivative a) (at x)`,
  SIMP_TAC[has_vector_derivative;GSYM REAL_CMUL_TO_VECTOR_MUL;
    HAS_DERIVATIVE_LINEAR;LINEAR_REAL_CMUL]);;

let HAS_COMPLEX_DERIVATIVE_MUL_CEXP = prove
  (`!a z. ((\z. a * cexp z) has_complex_derivative (a * cexp z)) (at z)`,
  REPEAT GEN_TAC THEN COMPLEX_DIFF_TAC THEN SIMPLE_COMPLEX_ARITH_TAC);;

let HAS_VECTOR_DERIVATIVE_CEXP = prove
  (`!A a x. ((\x. A * cexp(a * Cx(drop x))) has_vector_derivative (A * a *
    cexp (a * Cx(drop x)))) (at x)`,
  REWRITE_TAC[has_vector_derivative; GSYM (REWRITE_CONV[o_DEF] 
    `(\x. A * cexp x) o (\x. a * Cx(drop x))`); GSYM REAL_CMUL_TO_VECTOR_MUL]
  THEN SUBGOAL_THEN
    `!A a x. (\x'. (A * a * cexp (a * Cx (drop x))) * Cx (drop x')) = (\x'. A *
      cexp(a * Cx(drop x)) * x') o (\x. a * Cx(drop x))` (SINGLE REWRITE_TAC)
  THENL ON_FIRST_GOAL (REWRITE_TAC[o_DEF;FUN_EQ_THM]
    THEN SIMPLE_COMPLEX_ARITH_TAC)
  THEN REPEAT GEN_TAC THEN MATCH_MP_TAC DIFF_CHAIN_AT THEN CONJ_TAC 
  THENL [
    REWRITE_TAC[REAL_CMUL_TO_VECTOR_MUL;GSYM has_vector_derivative]
    THEN REWRITE_TAC[GSYM REAL_CMUL_TO_VECTOR_MUL;
      HAS_VECTOR_DERIVATIVE_REAL_CMUL];
    REWRITE_TAC[] THEN MATCH_ACCEPT_TAC (REWRITE_RULE[has_complex_derivative;
      GSYM COMPLEX_MUL_ASSOC] HAS_COMPLEX_DERIVATIVE_MUL_CEXP);
  ]);;

let HAS_VECTOR_DERIVATIVE_SUM_CEXP = prove
  (`!A B a b x. ((\x. A * cexp(a * Cx(drop x)) + B * cexp(b * Cx(drop x)))
    has_vector_derivative (A * a * cexp (a * Cx(drop x)) + B * b * cexp (b *
      Cx(drop x)))) (at x)`,
  REPEAT GEN_TAC THEN MATCH_MP_TAC HAS_VECTOR_DERIVATIVE_ADD THEN CONJ_TAC
  THEN MATCH_ACCEPT_TAC HAS_VECTOR_DERIVATIVE_CEXP);;


(** MAIN RESULT *)

let WAVE_SUM_EQ_CORE = prove 
  (`!a b c A B C. ~(A = Cx(&0)) /\ ~(B = Cx(&0)) /\ ~(C = Cx(&0))
  /\ (!x. A * cexp (a * Cx x) + B * cexp (b * Cx x) = C * cexp (c * Cx x))
  ==> a = b /\ b = c /\ A + B = C`,
  REPEAT GEN_TAC THEN STRIP_TAC
  THEN SUBGOAL_THEN
    `!x. a * A * cexp (a*Cx x) + b * B * cexp (b*Cx x) = c * C * cexp (c*Cx x)`
    ASSUME_TAC
	THENL ON_FIRST_GOAL 
    (REWRITE_TAC[FORALL_DROP] THEN GEN_TAC 
    THEN MATCH_MP_TAC VECTOR_DERIVATIVE_UNIQUE_AT
    THEN MAP_EVERY EXISTS_TAC [`\x. C * cexp (c * Cx(drop x))`;`x:real^1`]
    THEN REWRITE_TAC
      [MESON[COMPLEX_MUL_AC] `!A a. a * A * cexp x = A * a * cexp x`]
    THEN CONJ_TAC THEN TRY (MATCH_ACCEPT_TAC HAS_VECTOR_DERIVATIVE_CEXP)
    THEN POP_ASSUM (fun x -> REWRITE_TAC[GSYM x]) 
    THEN MATCH_ACCEPT_TAC HAS_VECTOR_DERIVATIVE_SUM_CEXP)
  THEN SUBGOAL_THEN `!x. a pow 2 * A * cexp (a*Cx x) + b
    pow 2 * B * cexp (b*Cx x) = c pow 2 * C * cexp (c*Cx x)` ASSUME_TAC
  THENL ON_FIRST_GOAL 
    (REWRITE_TAC[FORALL_DROP] THEN GEN_TAC 
    THEN MATCH_MP_TAC VECTOR_DERIVATIVE_UNIQUE_AT
    THEN MAP_EVERY EXISTS_TAC [`\x.(C * c) * cexp (c * Cx(drop x))`;`x:real^1`]
    THEN REWRITE_TAC[COMPLEX_POW_2]
    THEN REWRITE_TAC
      [MESON[COMPLEX_MUL_AC] `!A a. (a*a) * A * cexp x = (A*a)*a*cexp x`]
    THEN CONJ_TAC THEN TRY (MATCH_ACCEPT_TAC HAS_VECTOR_DERIVATIVE_CEXP)
    THEN
      let assoc_on_cexp =
        MESON[COMPLEX_MUL_AC] `!C c. (C*c) * cexp x = c*C*cexp x`
      in
      REWRITE_TAC[assoc_on_cexp]
    THEN POP_ASSUM (fun x -> REWRITE_TAC[GSYM x; GSYM assoc_on_cexp])
    THEN REWRITE_TAC
      [MESON[COMPLEX_MUL_AC] `!A a. (a*A*a) * cexp x = (A*a)*a*cexp x`]
    THEN MATCH_ACCEPT_TAC HAS_VECTOR_DERIVATIVE_SUM_CEXP)
  THEN RULE_ASSUM_TAC (try_or_id (REWRITE_RULE[COMPLEX_MUL_RZERO;
    COMPLEX_ADD_RID;CEXP_0;COMPLEX_MUL_RID] o SPEC `&0`))
  THEN SUBGOAL_THEN
    `(a*A+b*B) pow 2 = a pow 2 * A pow 2 + b pow 2 * B pow 2 + Cx(&2)*a*b*A*B`
    MP_TAC
  THENL ON_FIRST_GOAL
    (REWRITE_TAC[COMPLEX_POW_2] THEN SIMPLE_COMPLEX_ARITH_TAC)
  THEN SUBGOAL_THEN
    `(a*A+b*B) pow 2 = a pow 2 * A pow 2 + b pow 2 * B pow 2 + a pow 2 * A *
      B + b pow 2 * A * B :complex` 
    (SINGLE REWRITE_TAC)
  THENL ON_FIRST_GOAL 
    (GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [COMPLEX_POW_2]
    THEN ASM
      (GEN_REWRITE_TAC (RATOR_CONV o RAND_CONV o RATOR_CONV o DEPTH_CONV)) []
    THEN FIND_ASSUM (SINGLE REWRITE_TAC o GSYM) `A+B=C:complex`
    THEN FIND_ASSUM (SINGLE REWRITE_TAC) `a * A + b * B = c * C:complex`
    THEN SUBGOAL_TAC "" `(c * (A + B)) * c * C = (A+B) * c pow 2 * C:complex`
      [REWRITE_TAC[COMPLEX_POW_2] THEN SIMPLE_COMPLEX_ARITH_TAC]
    THEN POP_ASSUM (SINGLE REWRITE_TAC)
    THEN FIND_ASSUM (SINGLE REWRITE_TAC o GSYM)
      (`a pow 2 * A + b pow 2 * B = c pow 2 * C:complex`)
    THEN REWRITE_TAC[COMPLEX_POW_2] THEN SIMPLE_COMPLEX_ARITH_TAC)
  THEN REWRITE_TAC[COMPLEX_EQ_ADD_LCANCEL]
  THEN SUBGOAL_THEN `a pow 2 * A * B + b pow 2 * A * B = Cx (&2) * a * b * A *
    B <=> (a-b) pow 2 * A * B = Cx(&0)` (SINGLE REWRITE_TAC)
  THENL ON_FIRST_GOAL
    (REWRITE_TAC[COMPLEX_POW_2] THEN SIMPLE_COMPLEX_ARITH_TAC)
  THEN REWRITE_TAC[COMPLEX_ENTIRE]
  THEN RULE_ASSUM_TAC (SINGLE PURE_REWRITE_RULE (TAUT `~p <=> (p<=>F)`))
  THEN ASM_REWRITE_TAC[COMPLEX_POW_2;COMPLEX_ENTIRE;COMPLEX_SUB_0]
  THEN DISCH_THEN (fun x -> REWRITE_ASSUMPTIONS[x;GSYM COMPLEX_ADD_LDISTRIB]
    THEN REWRITE_TAC[x])
  THEN POP_ASSUM (K ALL_TAC) THEN POP_ASSUM MP_TAC
  THEN ASM_REWRITE_TAC[COMPLEX_EQ_MUL_RCANCEL]);;


(** WEAKER RESULTS
 * - with only two exponentials (WAVE_SUM_EQ_SINGLE)
 * - with B possibly equal to zero (WAVE_SUM_EQ_WEAK1)
 * - with C possibly equal to zero (WAVE_SUM_EQ_WEAK2)
 *)
let WAVE_SUM_EQ_SINGLE = prove 
  (`!a b A B.
    ~(A = Cx(&0)) /\ (!x. A * cexp (a * Cx x) = B * cexp (b * Cx x))
    ==> a = b /\ A = B`,
  REPEAT GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN `~(B = Cx(&0))` ASSUME_TAC
  THENL ON_FIRST_GOAL (POP_ASSUM (fun x -> ASM_REWRITE_TAC[REWRITE_RULE
    [COMPLEX_MUL_RZERO;CEXP_0;COMPLEX_MUL_RID] (SPEC `&0` (GSYM x))]))
  THEN SUBGOAL_THEN
    `!x. A * cexp (a * Cx x) + A * cexp (a * Cx x) 
      = (Cx(&2)*B) * cexp (b * Cx x)` 
    ASSUME_TAC
  THENL ON_FIRST_GOAL (GEN_TAC THEN POP_ASSUM (K ALL_TAC)
    THEN POP_ASSUM (MP_TAC o SPEC_ALL) THEN SIMPLE_COMPLEX_ARITH_TAC)
  THEN SUBGOAL_THEN `~(Cx(&2)*B=Cx(&0))` ASSUME_TAC 
  THENL ON_FIRST_GOAL
    (POP_ASSUM (K ALL_TAC) THEN POP_ASSUM MP_TAC THEN SIMPLE_COMPLEX_ARITH_TAC)
  THEN ASM_MESON_TAC
    [WAVE_SUM_EQ_CORE;SIMPLE_COMPLEX_ARITH `A + A = Cx(&2) * B <=> A = B`]);;

let WAVE_SUM_EQ_WEAK1 = prove 
  (`!a b c A B C.
    ~(A = Cx(&0)) /\ ~(C = Cx(&0))
    /\ (!x. A * cexp (a * Cx x) + B * cexp (b * Cx x) = C * cexp (c * Cx x)) 
    ==> a = c /\ A + B = C`,
  REPEAT GEN_TAC THEN ASM_CASES_TAC `B = Cx(&0)` THENL [
    ASM_REWRITE_TAC[COMPLEX_MUL_LZERO;COMPLEX_ADD_RID]
    THEN MESON_TAC[WAVE_SUM_EQ_SINGLE];
    REPEAT STRIP_TAC
    THENL ON_FIRST_GOAL (MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `b:complex`)
    THEN ASM_MESON_TAC[WAVE_SUM_EQ_CORE];
  ]);;

let WAVE_SUM_EQ_WEAK2 = prove 
  (`!a b c A B C.
    ~(A = Cx(&0)) /\ ~(B = Cx(&0)) 
    /\ (!x. A * cexp (a * Cx x) + B * cexp (b * Cx x) = C * cexp (c * Cx x)) 
    ==> a = b /\ A + B = C`,
  REPEAT GEN_TAC THEN ASM_CASES_TAC `C = Cx(&0)` THENL [
    ASM_REWRITE_TAC[COMPLEX_MUL_LZERO;COMPLEX_LNEG_UNIQ;COMPLEX_NEG_LMUL]
    THEN MESON_TAC[WAVE_SUM_EQ_SINGLE;COMPLEX_NEG_EQ_0];
    ASM_MESON_TAC[WAVE_SUM_EQ_CORE];
  ]);;


(** VECTORIAL VERSIONS OF THE ABOVE THEOREMS **)
let VEC_WAVE_SUM_EQ_CORE = prove
  (`!a b c A B C:complex^N.
    ~(A = cvector_zero) /\ ~(B = cvector_zero) /\ ~(C = cvector_zero)
    /\ (!x. cexp (a * Cx x) % A + cexp (b * Cx x) % B = cexp (c * Cx x) % C)
    ==> a = b /\ b = c /\ A + B = C`,
  REWRITE_TAC[CVECTOR_NON_ZERO;IMP_CONJ;
    MESON[] `(a ==> b/\c/\d) <=> (a==>b/\c) /\ (b/\c==>a==>d)`]
  THEN REPEAT GEN_TAC 
  THEN MAP_EVERY (DISCH_THEN o X_CHOOSE_TAC) [`i:num`;`j:num`;`k:num`]
  THEN CONJ_TAC
  THENL ON_FIRST_GOAL (MAP_EVERY ASM_CASES_TAC [`i=(j:num)`;`j=(k:num)`])
  THENL
    let cexp_SYM = SIMPLE_COMPLEX_ARITH `cexp x * y = y * cexp x` in
    let PROJECT_ON t =
      MAP_ANTECEDENT (SPEC t o ONCE_REWRITE_RULE[SWAP_FORALL_THM] o
        ONCE_REWRITE_RULE[CART_EQ])
      THEN ASM_REWRITE_TAC[CVECTOR_MUL_COMPONENT;CVECTOR_ADD_COMPONENT;cexp_SYM]
    in
    let CONJ1_FIRST = MESON[] `(a ==> b/\c) <=> ((a==>b)/\(b==>a==>c))` in
    [
      PROJECT_ON `i:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_CORE];
      REWRITE_TAC[CONJ1_FIRST] THEN CONJ_TAC
      THENL [
        PROJECT_ON `i:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_WEAK2];
        DISCH_THEN (fun x -> REWRITE_TAC[x;GSYM CVECTOR_ADD_LDISTRIB])
        THEN PROJECT_ON `k:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_SINGLE];
      ];
      REWRITE_TAC[MESON[] `(a ==> b/\c) <=> ((a==>c)/\(c==>a==>b))`]
      THEN CONJ_TAC
      THENL [
        PROJECT_ON `j:num` THEN ONCE_REWRITE_TAC[COMPLEX_ADD_SYM]
        THEN ASM_MESON_TAC[WAVE_SUM_EQ_WEAK1];
        DISCH_THEN (fun x -> 
          REWRITE_TAC[x;CVECTOR_ARITH `!x:complex^N. x +y=z <=> x=z-y`;
          GSYM CVECTOR_SUB_LDISTRIB])
        THEN PROJECT_ON `i:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_SINGLE];
      ];
      ASM_CASES_TAC `(C:complex^N)$i = Cx(&0)`
      THENL [
        REWRITE_TAC[CONJ1_FIRST] THEN CONJ_TAC
        THENL [
          PROJECT_ON `i:num`
          THEN REWRITE_TAC[COMPLEX_MUL_LZERO;COMPLEX_LNEG_UNIQ;
            COMPLEX_NEG_LMUL]
          THEN ASM_MESON_TAC[WAVE_SUM_EQ_SINGLE];
          DISCH_THEN (fun x -> REWRITE_TAC[x;GSYM CVECTOR_ADD_LDISTRIB])
          THEN PROJECT_ON `k:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_SINGLE];
        ];
        ONCE_REWRITE_TAC[MESON[] `a=b/\b=c <=> a=c /\ (a=b/\b=c)`]
        THEN REWRITE_TAC
          [MESON[] `(a==>b/\c/\d) <=> (a==>b) /\ (b==>a==>c/\d)`]
        THEN CONJ_TAC
        THENL [
          PROJECT_ON `i:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_WEAK1];
          DISCH_THEN (fun x ->
            REWRITE_TAC[x;CVECTOR_ARITH `!x:complex^N. x +y=z <=> y=z-x`;
              GSYM CVECTOR_SUB_LDISTRIB])
          THEN PROJECT_ON `j:num` THEN ASM_MESON_TAC[WAVE_SUM_EQ_SINGLE]
        ];
      ];
      REPLICATE_TAC 2 (DISCH_THEN (SINGLE REWRITE_TAC))
      THEN REWRITE_TAC
        [CVECTOR_ARITH `x % X + x % Y = x % Z <=> x % (X+Y-Z) = cvector_zero`;
          CVECTOR_MUL_EQ_0;CEXP_NZ]
      THEN CVECTOR_ARITH_TAC
    ]);;

let VEC_WAVE_SUM_EQ_SINGLE = prove 
  (`!a b A B:complex^N.
    ~(A = cvector_zero) /\ (!x. cexp (a * Cx x) % A = cexp (b * Cx x) % B) 
    ==> a = b /\ A = B`,
  REPEAT GEN_TAC THEN STRIP_TAC
  THEN SUBGOAL_THEN `~(B:complex^N = cvector_zero)` ASSUME_TAC
  THENL ON_FIRST_GOAL (POP_ASSUM (fun x -> ASM_REWRITE_TAC[
    REWRITE_RULE[COMPLEX_MUL_RZERO;CEXP_0;CVECTOR_MUL_ID]
      (SPEC `&0` (GSYM x))]))
  THEN SUBGOAL_THEN
    `!x. cexp (a * Cx x) % (A:complex^N) + cexp (a * Cx x) % A
      = cexp (b * Cx x) % (Cx(&2) % B)` 
    ASSUME_TAC
  THENL ON_FIRST_GOAL (GEN_TAC THEN POP_ASSUM (K ALL_TAC)
    THEN POP_ASSUM (MP_TAC o SPEC_ALL) THEN CVECTOR_ARITH_TAC)
  THEN SUBGOAL_THEN `~(Cx(&2) % (B:complex^N) = cvector_zero)` ASSUME_TAC
  THENL ON_FIRST_GOAL (POP_ASSUM (K ALL_TAC) THEN POP_ASSUM MP_TAC
  THEN REWRITE_TAC[CVECTOR_MUL_EQ_0;SIMPLE_COMPLEX_ARITH `~(Cx(&2) = Cx(&0))`])
  THEN ASM_MESON_TAC
    [VEC_WAVE_SUM_EQ_CORE;CVECTOR_ARITH `A + A = Cx(&2) % B <=> A = B`]);;

let VEC_WAVE_SUM_EQ_WEAK1 = prove 
  (`!a b c A B C:complex^N.
    ~(A = cvector_zero) /\ ~(C = cvector_zero)
    /\ (!x. cexp (a * Cx x) % A + cexp (b * Cx x) % B = cexp (c * Cx x) % C) 
    ==> a = c /\ A + B = C`,
  REPEAT GEN_TAC THEN ASM_CASES_TAC `(B:complex^N) = cvector_zero` THENL [
    ASM_REWRITE_TAC[CVECTOR_MUL_RZERO;CVECTOR_ADD_ID]
    THEN MESON_TAC[VEC_WAVE_SUM_EQ_SINGLE];
    REPEAT STRIP_TAC
    THENL ON_FIRST_GOAL (MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `b:complex`)
    THEN ASM_MESON_TAC[VEC_WAVE_SUM_EQ_CORE];
  ]);;

let VEC_WAVE_SUM_EQ_WEAK2 = prove 
  (`!a b c A B C:complex^N.
    ~(A = cvector_zero) /\ ~(B = cvector_zero)
    /\ (!x. cexp (a * Cx x) % A + cexp (b * Cx x) % B = cexp (c * Cx x) % C) 
    ==> a = b /\ A + B = C`,
  REPEAT GEN_TAC THEN ASM_CASES_TAC `(C:complex^N) = cvector_zero` 
  THENL [
    ASM_REWRITE_TAC[CVECTOR_MUL_RZERO;
      CVECTOR_ARITH `x+y = cvector_zero <=> x= --y`;GSYM CVECTOR_MUL_RNEG]
    THEN MESON_TAC[VEC_WAVE_SUM_EQ_SINGLE];
    ASM_MESON_TAC[VEC_WAVE_SUM_EQ_CORE];
  ]);;