(* ========================================================================= *)
(*               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))`,
let HAS_VECTOR_DERIVATIVE_REAL_CMUL = 
prove (`!a x. ((\x. a * Cx (drop x)) has_vector_derivative a) (at x)`,
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]; ]);;