(* for derivatives in 6 dimensions *)

let HAS_SIZE_6 = define_finite_type 6;;

let DIMINDEX_6 = MATCH_MP DIMINDEX_UNIQUE HAS_SIZE_6;;

let lift_6 = new_definition `lift_6 (f:real->real->real->real->real->real->real) = 
  (\ (v:real^6). lift (f (v$1) (v$2) (v$3) (v$4) (v$5) (v$6)) )`;;

let drop_6 = new_definition `drop_6 (f:real^6->real^1) = 
  (\x1 x2 x3 x4 x5 x6. drop (f (vector [x1;x2;x3;x4;x5;x6])))`;;

let lambda_ext = prove_by_refinement(
  `!P Q.  (!i. 1 <= i /\ i <= dimindex (:B) ==> ((P:num->A) i = Q i)) =
    (((lambda i. P i):A^B) = (lambda i. Q i))`,
  (* {{{ proof *)
  [
REPEAT STRIP_TAC ;
REWRITE_TAC [GSYM LAMBDA_UNIQUE];
SIMP_TAC [LAMBDA_BETA];
MESON_TAC []
  ]);;
  (* }}} *)

let vector6 = prove_by_refinement(
  `!(v:real^6). vector [v$1; v$2; v$3; v$4; v$5; v$6] = v`,
  (* {{{ proof *)
  [
REWRITE_TAC [vector;GSYM LAMBDA_UNIQUE];
REWRITE_TAC [DIMINDEX_6;ARITH_RULE `1 <= i /\ i <=6 <=> (i=1 \/ i=2 \/ i=3 \/ i=4 \/ i=5 \/ i=6)`];
REPEAT STRIP_TAC  THEN ASM_REWRITE_TAC[EL;HD;TL;ARITH_RULE `1-1=0 /\ 2 - 1 = SUC 0 /\ 3 - 1 =  SUC (SUC 0) /\ 4 - 1 = SUC (SUC(SUC 0)) /\ 5 - 1 = SUC (SUC(SUC(SUC 0))) /\ 6 - 1 = SUC(SUC(SUC(SUC(SUC 0))))`]
  ]);;
  (* }}} *)

let vector6_comp = prove_by_refinement(
  `!x1 x2 x3 x4 x5 x6.
    (vector:(A)list -> A^6) [x1;x2;x3;x4;x5;x6]$1 = x1 /\
    (vector:(A)list -> A^6) [x1;x2;x3;x4;x5;x6]$2 = x2 /\
    (vector:(A)list -> A^6) [x1;x2;x3;x4;x5;x6]$3 = x3 /\
    (vector:(A)list -> A^6) [x1;x2;x3;x4;x5;x6]$4 = x4 /\
    (vector:(A)list -> A^6) [x1;x2;x3;x4;x5;x6]$5 = x5 /\
    (vector:(A)list -> A^6) [x1;x2;x3;x4;x5;x6]$6 = x6 
 `,
  (* {{{ proof *)
  [
REWRITE_TAC [vector];
SIMP_TAC [REWRITE_RULE[DIMINDEX_6] (INST_TYPE[`:6`,`:B`] LAMBDA_BETA); ARITH_RULE `1 <= 1 /\ 1 <=6 /\ 1 <= 2 /\ 2 <= 6 /\ 1 <= 3 /\ 3 <= 6 /\ 1 <= 4 /\ 4 <= 6 /\ 1 <= 5 /\ 5 <= 6 /\ 1 <= 6 /\ 6 <= 6 `;EL;HD;TL;ARITH_RULE `1-1=0 /\ 2 - 1 = SUC 0 /\ 3 - 1 =  SUC (SUC 0) /\ 4 - 1 = SUC (SUC(SUC 0)) /\ 5 - 1 = SUC (SUC(SUC(SUC 0))) /\ 6 - 1 = SUC(SUC(SUC(SUC(SUC 0))))`]
  ]);;
  (* }}} *)


let lift6_drop6 = prove_by_refinement(
  `!f. lift_6 (drop_6 f) = f`,
  (* {{{ proof *)
  [
REWRITE_TAC [lift_6;drop_6;lift;drop];
GEN_TAC ;
ONCE_REWRITE_TAC[FUN_EQ_THM];
BETA_TAC;
GEN_TAC ;
REWRITE_TAC [(GSYM VECTOR_ONE)];
AP_TERM_TAC ;
REWRITE_TAC [vector6]
  ]);;
  (* }}} *)

let drop6_lift6 = prove_by_refinement(
  `!f. drop_6 (lift_6 f) = f`,
  (* {{{ proof *)
  [
REWRITE_TAC [lift_6;drop_6;vector6_comp;LIFT_DROP];
GEN_TAC ;
REPEAT (MATCH_MP_TAC EQ_EXT THEN GEN_TAC);
BETA_TAC;
REWRITE_TAC []
  ]);;
  (* }}} *)


(* f'' is the Hessian, viewed as a bilinear function at x.
   I plan to use this always on a product X of compact intervals in 6-d, 
   such that X SUBSET P.  We should be able to take `s = (:real^6)` in every case. *)


let derived_form2a = new_definition `derived_form2a
   p (f:real^6->real) (f':real^6->real^6->real) 
   (f'':real^6 -> real^6 ->real^6 ->real) (x:real^6) (s:real^6->bool) = 
   ((!(y:real^6). p y ==> ((has_derivative) (lift o f) (lift o (f' y)) (at y)) ) /\  
  (!t.   p x ==> (has_derivative) (\u. lift (f' u t)) (\t'. lift (f'' x t t')) (at x within s)) /\
   (!(y:real^6) t t'. p y ==> (continuous) (\u. lift (f'' u t t')) (at y within s)))
   `;;


let derived_form2b = new_definition `derived_form2b 
   p (f:real^6->real) (f':real^6->real^6->real) 
   (f'':real^6 -> real^6 ->real^6 ->real) (x:real^6) (s:real^6->bool) = 
   ((!(y:real^6). p y ==> ((has_derivative) (lift o f) (lift o (f' y)) (at y)) ) /\  
  (!t.   p x ==> (has_derivative) (\u. lift (f' u t)) (\t'. lift (f'' x t t')) (at x within s)) /\ ( open p) /\
   (!(y:real^6) t t'. p y ==> (continuous) (\u. lift (f'' u t t')) (at y within s)))
   `;;

(* Theorems needed:

   1. Clairaut's theorem on equality of mixed partials.
   This uses the continuity and openness assumptions, so they have beeen added
   to derived_form2b.
   Many proofs are available, google search "Equality of Mixed Partials"
   For example, http://www.math.ubc.ca/~feldman/m226/mixed.pdf

   2. Multivariate Taylor's theorem,
   This can be deduced from REAL_TAYLOR by 
   taking t-derivative along a line segement `\t. f(x + t % v)`

   3. Identification of Hessian as a bilinear function with the
   matrix of second partials. This should follow from JACOBIAN_WORKS.

   Tactic needed:
   Automatic generation of derived_form2b from f.
 *)


(*
let mixed_equal = prove_by_refinement(
  `!f f' f'' x s.  derived_form2b p f f' f'' x s ==>
    (!t t'. p y ==> f'' y t t' = f'' y t' t)`,
  (* {{{ proof *)
  [
  ]);;
  (* }}} *)
*)