lib.hl

(* ========================================================================== *)
(*      Formal verification of FPTaylor certificates                          *)
(*                                                                            *)
(*      Author: Alexey Solovyev, University of Utah                           *)
(*                                                                            *)
(*      This file is distributed under the terms of the MIT licence           *)
(* ========================================================================== *)

(* -------------------------------------------------------------------------- *)
(* General theorems and conversions                                           *)
(* -------------------------------------------------------------------------- *)

module Lib = struct

(* --------------------------------------------- *)
(* Definitions                                   *)
(* --------------------------------------------- *)

let delete_at = (GEN_ALL o define) 
  `delete_at i [] = [] /\ delete_at 0 (CONS h t) = t /\ 
  delete_at (SUC i) (CONS h t) = CONS h (delete_at i t)`;;

let rev_table = define 
  `!f i. rev_table (f:num->A) 0 = [] /\
  rev_table f (SUC i) = CONS (f i) (rev_table f i)`;;

let table = new_definition 
  `!f i. table f i = REVERSE (rev_table f i)`;;

let sum_list = new_definition 
  `!s f. sum_list s f = ITLIST (\x r:real. f x + r) s (&0)`;;

let unzip_def = define `!h1 h2 t. (unzip [] = [],[]) /\ 
  (unzip (CONS (h1, h2) t) = CONS h1 (FST (unzip t)), CONS h2 (SND (unzip t)))`;;

(* --------------------------------------------- *)
(* Auxiliary functions                           *)
(* --------------------------------------------- *)

let list_to_pair = function
  | [a; b] -> (a, b)
  | _ -> failwith "list_to_pair";;

let list_to_triple = function
  | [a; b; c] -> (a, b, c)
  | _ -> failwith "list_to_triple";;

(* --------------------------------------------- *)
(* Theorems                                      *)
(* --------------------------------------------- *)

(* --------------------------------------------- *)
(* Misc                                          *)
(* --------------------------------------------- *)

let pair_eq_thm = prove(`!p:A#B. p = FST p, SND p`, REWRITE_TAC[]);;

let let_pair = prove
  (`!Q p:A#B. (let a,b = p in Q a b) <=> Q (FST p) (SND p)`,
   REPEAT GEN_TAC THEN EQ_TAC THENL [
     LET_TAC THEN ASM_REWRITE_TAC[];
     DISCH_THEN (LABEL_TAC "h") THEN LET_TAC THEN
       REMOVE_THEN "h" MP_TAC THEN REWRITE_TAC[]
   ]);;

let let_triple = prove
  (`!Q p:A#B#C. (let a,b,c = p in Q a b c) <=> Q (FST p) (FST (SND p)) (SND (SND p))`,
   REPEAT GEN_TAC THEN EQ_TAC THENL [
     LET_TAC THEN ASM_REWRITE_TAC[];
     DISCH_THEN (LABEL_TAC "h") THEN LET_TAC THEN
       REMOVE_THEN "h" MP_TAC THEN REWRITE_TAC[]
   ]);;

let abs_div_le_1 = prove
  (`!a b. abs (a / b) <= &1 <=> (b = &0 \/ abs a <= abs b)`,
   REPEAT GEN_TAC THEN ASM_CASES_TAC `b = &0` THENL [
     ASM_REWRITE_TAC[real_div; REAL_INV_0; REAL_MUL_RZERO; REAL_ABS_0; REAL_LE_01];
     ALL_TAC
   ] THEN
     REWRITE_TAC[REAL_ABS_DIV] THEN
     ASM_SIMP_TAC[REAL_ARITH `~(b = &0) ==> &0 < abs b`; REAL_LE_LDIV_EQ] THEN
     REWRITE_TAC[REAL_MUL_LID]);;
       
(* --------------------------------------------- *)
(* delete_at properties                          *)
(* --------------------------------------------- *)

let delete_at_eq = prove
  (`!s:(A)list k. ~(k < LENGTH s) ==> delete_at k s = s`,
   LIST_INDUCT_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[LENGTH; delete_at; LT_0; LT_SUC]);;

let length_delete_at = prove
  (`!s:(A)list k. LENGTH (delete_at k s) = LENGTH s - if k < LENGTH s then 1 else 0`,
   LIST_INDUCT_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[LENGTH; delete_at] THEN ARITH_TAC);;

let el_delete_at = prove
  (`!s:(A)list i k. i < LENGTH (delete_at k s)
     ==> EL i (delete_at k s) = EL (if i < k then i else SUC i) s`,
   LIST_INDUCT_TAC THEN INDUCT_TAC THEN INDUCT_TAC THEN 
     REWRITE_TAC[LENGTH; delete_at; LT_REFL; ARITH_RULE `~(SUC n < 0)`; EL; HD; TL; LT_0] THEN
     ASM_SIMP_TAC[LT_SUC] THEN COND_CASES_TAC THEN REWRITE_TAC[EL; TL]);;

let length_unzip = prove
  (`!s:(A#B)list. LENGTH (FST (unzip s)) = LENGTH s /\ LENGTH (SND (unzip s)) = LENGTH s`,
  LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; unzip_def] THEN
    MP_TAC (ISPEC `h:A#B` pair_eq_thm) THEN DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
    ASM_REWRITE_TAC[unzip_def; LENGTH]);;

(* --------------------------------------------- *)
(* zip/unzip properties                          *)
(* --------------------------------------------- *)

let unzip_map = prove
  (`!s:(A#B)list. FST (unzip s) = MAP FST s /\ SND (unzip s) = MAP SND s`,
   LIST_INDUCT_TAC THEN REWRITE_TAC[unzip_def; MAP] THEN
     MP_TAC (ISPEC `h:A#B` pair_eq_thm) THEN DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
     ASM_REWRITE_TAC[unzip_def; MAP]);;

let zip_unzip = prove
  (`!s:(A#B)list. ZIP (FST (unzip s)) (SND (unzip s)) = s`,
   LIST_INDUCT_TAC THEN REWRITE_TAC[ZIP; unzip_def] THEN
     MP_TAC (ISPEC `h:A#B` pair_eq_thm) THEN DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
     ASM_REWRITE_TAC[unzip_def; ZIP]);;

let unzip_zip = prove
  (`!(s:(A)list) (t:(B)list). LENGTH s = LENGTH t ==> unzip (ZIP s t) = (s, t)`,
   REPEAT STRIP_TAC THEN
     ONCE_REWRITE_TAC[pair_eq_thm] THEN REWRITE_TAC[PAIR_EQ; unzip_map] THEN
     ASM_SIMP_TAC[MAP_FST_ZIP; MAP_SND_ZIP]);;

let length_zip = prove
  (`!(s:(A)list) (t:(B)list). LENGTH s = LENGTH t ==> LENGTH (ZIP s t) = LENGTH s`,
   REPEAT LIST_INDUCT_TAC THEN ASM_SIMP_TAC[ZIP; LENGTH; SUC_INJ] THEN ARITH_TAC);;

let el_zip = prove
  (`!(s:(A)list) (t:(B)list) i. LENGTH s = LENGTH t /\ i < LENGTH s
      ==> EL i (ZIP s t) = EL i s, EL i t`,
   REPEAT LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ZIP; LENGTH; EL; SUC_INJ] THEN TRY ARITH_TAC THEN
     INDUCT_TAC THEN ASM_SIMP_TAC[EL; HD; TL; LT_SUC]);;

(* --------------------------------------------- *)
(* table properties                              *)
(* --------------------------------------------- *)

let length_reverse = prove
  (`!(s:(A)list). LENGTH (REVERSE s) = LENGTH s`,
   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[LENGTH; REVERSE; LENGTH_APPEND] THEN ARITH_TAC);;

let all_reverse = prove
  (`!P (s:(A)list). ALL P (REVERSE s) <=> ALL P s`,
   GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL; REVERSE; ALL_APPEND; CONJ_ACI]);;

let mem_reverse = prove
  (`!x:A s. MEM x (REVERSE s) <=> MEM x s`,
   GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[MEM; REVERSE; MEM_APPEND; DISJ_ACI]);;

let reverse_nil = prove
  (`!s:(A)list. REVERSE s = [] <=> s = []`,
   REWRITE_TAC[GSYM LENGTH_EQ_NIL; length_reverse]);;

let length_rev_table = prove
  (`!(f:num->A) n. LENGTH (rev_table f n) = n`,
   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[rev_table; LENGTH]);;

let length_table = prove
  (`!(f:num->A) n. LENGTH (table f n) = n`,
   REWRITE_TAC[table; length_rev_table; length_reverse]);;

let hd_append = prove
  (`!s t:(A)list. HD (APPEND s t) = if s = [] then HD t else HD s`,
   LIST_INDUCT_TAC THEN REWRITE_TAC[APPEND; HD; NOT_CONS_NIL]);;

let hd_reverse = prove
  (`!s:(A)list. ~(s = []) ==> HD (REVERSE s) = LAST s`,
   LIST_INDUCT_TAC THEN REWRITE_TAC[REVERSE; HD; LAST] THEN
     COND_CASES_TAC THEN ASM_REWRITE_TAC[REVERSE; APPEND; HD; hd_append] THEN
     ASM_SIMP_TAC[reverse_nil]);;

let el_reverse = prove
  (`!(s:(A)list) i. i < LENGTH s
      ==> EL i (REVERSE s) = EL (LENGTH s - i - 1) s`,
   LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; REVERSE] THENL [ ARITH_TAC; ALL_TAC ] THEN
     REPEAT STRIP_TAC THEN REWRITE_TAC[EL_APPEND; length_reverse] THEN
     COND_CASES_TAC THENL [
       SUBGOAL_THEN `SUC (LENGTH (t:(A)list)) - i - 1 = SUC (LENGTH t - i - 1)` ASSUME_TAC THENL [
	 POP_ASSUM MP_TAC THEN ARITH_TAC;
	 ALL_TAC
       ] THEN
       ASM_SIMP_TAC[EL; TL];
       ALL_TAC
     ] THEN
     ABBREV_TAC `n = LENGTH (t:(A)list)` THEN
     ASM_SIMP_TAC[ARITH_RULE `~(i < n) /\ i < SUC n ==> i - n = 0 /\ SUC n - i - 1 = 0`; EL; HD]);;

let el_rev_table = prove
  (`!(f:num->A) n i. i < n 
      ==> EL i (rev_table f n) = f (n - i - 1)`,
   GEN_TAC THEN INDUCT_TAC THEN INDUCT_TAC THEN REWRITE_TAC[rev_table; EL; HD] THEN TRY ARITH_TAC THENL [
     REWRITE_TAC[ARITH_RULE `SUC n - 0 - 1 = n`];
     ALL_TAC
   ] THEN
     ASM_SIMP_TAC[LT_SUC; TL; ARITH_RULE `SUC n - SUC i - 1 = n - i - 1`]);;

let el_table = prove
  (`!(f:num->A) n i. i < n ==> EL i (table f n) = f i`,
   REPEAT STRIP_TAC THEN REWRITE_TAC[table] THEN
     ASM_SIMP_TAC[length_reverse; length_rev_table; el_reverse] THEN
     ASM_SIMP_TAC[el_rev_table; ARITH_RULE `i < n ==> n - i - 1 < n`] THEN
     AP_TERM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;

(* --------------------------------------------- *)
(* sum_list properties                           *)
(* --------------------------------------------- *)

let sum_list_nil = prove
  (`!f. sum_list [] f = &0`,
   REWRITE_TAC[sum_list; ITLIST]);;

let sum_list_cons = prove
  (`!h t f. sum_list (CONS h t) f = f h + sum_list t f`,
   REWRITE_TAC[sum_list; ITLIST]);;

let sum_list_append = prove
  (`!f s1 s2. sum_list (APPEND s1 s2) f = sum_list s1 f + sum_list s2 f`,
   GEN_TAC THEN LIST_INDUCT_TAC THEN 
     ASM_REWRITE_TAC[APPEND; sum_list_cons; sum_list_nil; REAL_ADD_LID; REAL_ADD_ASSOC]);;

let sum_list_reverse = prove
  (`!f s:(A)list. sum_list (REVERSE s) f = sum_list s f`,
   GEN_TAC THEN LIST_INDUCT_TAC THEN 
     ASM_REWRITE_TAC[sum_list_cons; sum_list_nil; REVERSE; sum_list_append] THEN
     REAL_ARITH_TAC);;

let sum_list_map = prove
  (`!h s f. sum_list (MAP h s) f = sum_list s (f o h)`,
   GEN_TAC THEN LIST_INDUCT_TAC THEN 
     ASM_REWRITE_TAC[MAP; sum_list_nil; sum_list_cons; o_THM]);;

let sum_list_sum = prove
  (`!(s:(A)list) f. sum_list s f = 
      if s = [] then &0 else sum (0..LENGTH s - 1) (\i. f (EL i s))`,
   LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[sum_list_nil; sum_list_cons; NOT_CONS_NIL] THEN
     GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[LENGTH; SUC_SUB1] THENL [
       REWRITE_TAC[NUMSEG_SING; SUM_SING; EL; HD; REAL_ADD_RID];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `0 <= LENGTH (t:(A)list) /\ (LENGTH t - 1) + 1 = LENGTH t` STRIP_ASSUME_TAC THENL [
       ASM_REWRITE_TAC[LE_0; ARITH_RULE `(n - 1) + 1 = n <=> ~(n = 0)`; LENGTH_EQ_NIL];
       ALL_TAC
     ] THEN
     ASM_SIMP_TAC[SUM_CLAUSES_LEFT; EL; HD] THEN
     FIRST_ASSUM (fun th -> ONCE_REWRITE_TAC[GSYM th]) THEN
     ASM_REWRITE_TAC[SUM_OFFSET; GSYM ADD1; EL; TL]);;

let sum_list_sum_alt = prove
  (`!(s:(A)list) f. sum_list s f = sum (1..LENGTH s) (\i. f (EL (i - 1) s))`,
   REPEAT GEN_TAC THEN REWRITE_TAC[sum_list_sum] THEN
     COND_CASES_TAC THENL [
       ASM_REWRITE_TAC[LENGTH; SUM_CLAUSES_NUMSEG; ARITH_RULE `~(1 = 0)`];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `1..LENGTH (s:(A)list) = 0 + 1..(LENGTH s - 1) + 1` ASSUME_TAC THENL [
       REWRITE_TAC[ADD] THEN AP_TERM_TAC THEN
	 ASM_REWRITE_TAC[ARITH_RULE `n = (n - 1) + 1 <=> ~(n = 0)`; LENGTH_EQ_NIL];
       ALL_TAC
     ] THEN
     ASM_REWRITE_TAC[SUM_OFFSET; ARITH_RULE `(i + 1) - 1 = i`]);;

let sum_list_add = prove
  (`!f g s:(A)list. sum_list s (\x. f x + g x) = sum_list s f + sum_list s g`,
   SIMP_TAC[sum_list_sum_alt; SUM_ADD; FINITE_NUMSEG]);;

let sum_list_sub = prove
  (`!f g s:(A)list. sum_list s (\x. f x - g x) = sum_list s f - sum_list s g`,
   SIMP_TAC[sum_list_sum_alt; SUM_SUB; FINITE_NUMSEG]);;

let sum_list_eq_0 = prove
  (`!f s:(A)list. ALL (\x. f x = &0) s ==> sum_list s f = &0`,
  GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_SIMP_TAC[ALL; sum_list_nil; sum_list_cons; REAL_ADD_LID]);;

let sum_list_0 = prove
  (`!s:(A)list. sum_list s (\x. &0) = &0`,
   REWRITE_TAC[sum_list_sum_alt; SUM_0]);;

let sum_list_lmul = prove
  (`!f c s:(A)list. sum_list s (\x. c * f x) = c * sum_list s f`,
   REWRITE_TAC[sum_list_sum_alt; SUM_LMUL]);;

let sum_list_rmul = prove
  (`!f c s:(A)list. sum_list s (\x. f x * c) = sum_list s f * c`,
   REWRITE_TAC[sum_list_sum_alt; SUM_RMUL]);;

let sum_list_neg = prove
  (`!f s:(A)list. --sum_list s f = sum_list s (\x. --f x)`,
   REWRITE_TAC[sum_list_sum_alt; SUM_NEG]);;

let sum_list_le = prove
  (`!f g s:(A)list. ALL (\x. f x <= g x) s ==> sum_list s f <= sum_list s g`,
   GEN_TAC THEN GEN_TAC THEN
     LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL; sum_list_nil; sum_list_cons; REAL_LE_REFL] THEN
     STRIP_TAC THEN MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_SIMP_TAC[]);;

let sum_list_lt = prove
  (`!f g s:(A)list. ALL (\x. f x <= g x) s /\ EX (\x. f x < g x) s
   ==> sum_list s f < sum_list s g`,
   GEN_TAC THEN GEN_TAC THEN
     LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL; sum_list_nil; sum_list_cons; EX] THEN
     STRIP_TAC THENL [
       MATCH_MP_TAC REAL_LTE_ADD2 THEN ASM_SIMP_TAC[sum_list_le];
       MATCH_MP_TAC REAL_LET_ADD2 THEN ASM_SIMP_TAC[]
     ]);;

let sum_list_lt_all = prove
  (`!f g s:(A)list. ~(s = []) /\ ALL (\x. f x < g x) s
     ==> sum_list s f < sum_list s g`,
   GEN_TAC THEN GEN_TAC THEN
     LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL; sum_list_nil; sum_list_cons; NOT_CONS_NIL] THEN
     STRIP_TAC THEN ASM_CASES_TAC `t:(A)list = []` THENL [
       MATCH_MP_TAC REAL_LTE_ADD2 THEN ASM_REWRITE_TAC[sum_list_nil; REAL_LE_REFL];
       MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_SIMP_TAC[]
     ]);;

let sum_list_pos_le = prove
  (`!f s:(A)list. ALL (\x. &0 <= f x) s ==> &0 <= sum_list s f`,
   GEN_TAC THEN 
     LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL; sum_list_nil; sum_list_cons; REAL_LE_REFL] THEN
     STRIP_TAC THEN MATCH_MP_TAC REAL_LE_ADD THEN ASM_SIMP_TAC[]);;

let sum_list_pos_lt = prove
  (`!f s:(A)list. ALL (\x. &0 <= f x) s /\ EX (\x. &0 < f x) s
     ==> &0 < sum_list s f`,
   GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL; sum_list_nil; sum_list_cons; EX] THEN
     STRIP_TAC THENL [
       MATCH_MP_TAC REAL_LTE_ADD THEN ASM_SIMP_TAC[sum_list_pos_le];
       MATCH_MP_TAC REAL_LET_ADD THEN ASM_SIMP_TAC[]
     ]);;

let sum_list_pos_lt_all = prove
  (`!f s:(A)list. ~(s = []) /\ ALL (\x. &0 < f x) s ==> &0 < sum_list s f`,
   GEN_TAC THEN 
     LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL; sum_list_nil; sum_list_cons; NOT_CONS_NIL] THEN
     STRIP_TAC THEN ASM_CASES_TAC `t:(A)list = []` THENL [
       MATCH_MP_TAC REAL_LTE_ADD THEN ASM_REWRITE_TAC[sum_list_nil; REAL_LE_REFL];
       MATCH_MP_TAC REAL_LT_ADD THEN ASM_SIMP_TAC[]
     ]);;

let sum_list_eq = prove
  (`!f g s:(A)list. ALL (\x. f x = g x) s ==> sum_list s f = sum_list s g`,
   GEN_TAC THEN GEN_TAC THEN
     LIST_INDUCT_TAC THEN REWRITE_TAC[ALL; sum_list_nil; sum_list_cons] THEN
     REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REAL_EQ_ADD_LCANCEL] THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;

let sum_list_abs = prove
  (`!f s:(A)list. abs (sum_list s f) <= sum_list s (\x. abs (f x))`,
   SIMP_TAC[sum_list_sum_alt; SUM_ABS; FINITE_NUMSEG]);;

 let sum_list_abs_le = prove
  (`!f g (s:(A)list). ALL (\x. abs (f x) <= g x) s
     ==> abs (sum_list s f) <= sum_list s g`,
   REWRITE_TAC[sum_list_sum_alt; GSYM ALL_EL] THEN REPEAT STRIP_TAC THEN
     MATCH_MP_TAC SUM_ABS_LE THEN REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
     REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
     ASM_ARITH_TAC);;

let sum_list_const = prove
  (`!c s:(A)list. sum_list s (\x. c) = &(LENGTH s) * c`,
   SIMP_TAC[sum_list_sum_alt; SUM_CONST; FINITE_NUMSEG; CARD_NUMSEG; ARITH_RULE `(a + 1) - 1 = a`]);;

let sum_list_pos_bound = prove
  (`!f b s:(A)list. ALL (\x. &0 <= f x) s /\ sum_list s f <= b
     ==> ALL (\x. f x <= b) s`,
   GEN_TAC THEN GEN_TAC THEN
     LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL; sum_list_nil; sum_list_cons] THEN STRIP_TAC THEN
     FIRST_ASSUM (ASSUME_TAC o MATCH_MP sum_list_pos_le) THEN
     FIRST_X_ASSUM (MP_TAC o MATCH_MP (REAL_ARITH `!x y. x + y <= b ==> &0 <= x /\ &0 <= y ==> x <= b /\ y <= b`)) THEN
     ASM_SIMP_TAC[]);;

let sum_list_pos_eq_0 = prove
  (`!f s:(A)list. ALL (\x. &0 <= f x) s /\ sum_list s f = &0
      ==> ALL (\x. f x = &0) s`,
   REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_ARITH `!x. x = &0 <=> &0 <= x /\ x <= &0`] THEN
     ASM_REWRITE_TAC[GSYM AND_ALL] THEN MATCH_MP_TAC sum_list_pos_bound THEN
     ASM_SIMP_TAC[REAL_ARITH `x = &0 ==> x <= &0`]);;

let sum_list_sing = prove
  (`!f x:A. sum_list [x] f = f x`,
   REWRITE_TAC[sum_list_cons; sum_list_nil; REAL_ADD_RID]);;

let sum_list_swap = prove
  (`!f:A->B->real s t.
    sum_list s (\i. sum_list t (f i)) = sum_list t (\j. sum_list s (\i. f i j))`,
     GEN_TAC THEN REPEAT LIST_INDUCT_TAC THEN 
       REWRITE_TAC[sum_list_nil; sum_list_cons; sum_list_0; REAL_ADD_LID] THEN
       ASM_REWRITE_TAC[sum_list_add; ETA_AX] THEN REAL_ARITH_TAC);;

let sum_list_restrict = prove
  (`!f s:(A)list. sum_list s (\x. if MEM x s then f x else &0) = sum_list s f`,
   REPEAT GEN_TAC THEN MATCH_MP_TAC sum_list_eq THEN SIMP_TAC[GSYM ALL_MEM]);;

let sum_list_bound = prove
  (`!f b s:(A)list. ALL (\x. f x <= b) s ==> sum_list s f <= &(LENGTH s) * b`,
   GEN_TAC THEN GEN_TAC THEN
     LIST_INDUCT_TAC THEN 
     REWRITE_TAC[ALL; sum_list_nil; sum_list_cons; LENGTH; REAL_MUL_LZERO; REAL_LE_REFL] THEN
     STRIP_TAC THEN REWRITE_TAC[ARITH_RULE `SUC n = 1 + n`] THEN
     REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_ADD_RDISTRIB; REAL_MUL_LID] THEN
     MATCH_MP_TAC REAL_LE_ADD2 THEN ASM_SIMP_TAC[]);;

let sum_list_bound_gen = prove
  (`!f b s:(A)list. ~(s = []) /\ ALL (\x. f x <= b / &(LENGTH s)) s
     ==> sum_list s f <= b`,
   REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `b = &(LENGTH (s:(A)list)) * (b / &(LENGTH s))` MP_TAC THENL [
       ASM_SIMP_TAC[real_div; REAL_MUL_AC; REAL_MUL_LINV; REAL_OF_NUM_EQ; REAL_MUL_RID];
       ALL_TAC
     ] THEN
     DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
     MATCH_MP_TAC sum_list_bound THEN ASM_REWRITE_TAC[]);;

let sum_list_abs_bound = prove
  (`!f b s:(A)list. ALL (\x. abs (f x) <= b) s
     ==> abs (sum_list s f) <= &(LENGTH s) * b`,
   REPEAT STRIP_TAC THEN
     MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `sum_list s (\x:A. abs (f x))` THEN
     ASM_SIMP_TAC[sum_list_abs; sum_list_bound]);;

let sum_list_bound_lt = prove
  (`!f b s:(A)list. ALL (\x. f x <= b) s /\ EX (\x. f x < b) s
     ==> sum_list s f < &(LENGTH s) * b`,
   GEN_TAC THEN GEN_TAC THEN
     LIST_INDUCT_TAC THEN 
     REWRITE_TAC[ALL; EX; sum_list_nil; sum_list_cons; LENGTH; REAL_MUL_LZERO; REAL_LE_REFL] THEN
     REWRITE_TAC[ARITH_RULE `SUC n = 1 + n`] THEN
     REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_ADD_RDISTRIB; REAL_MUL_LID] THEN
     STRIP_TAC THENL [
       MATCH_MP_TAC REAL_LTE_ADD2 THEN ASM_SIMP_TAC[sum_list_bound];
       MATCH_MP_TAC REAL_LET_ADD2 THEN ASM_SIMP_TAC[]
     ]);;

let sum_list_bound_lt_all = prove
  (`!f b s:(A)list. ~(s = []) /\ ALL (\x. f x < b) s
     ==> sum_list s f < &(LENGTH s) * b`,
   GEN_TAC THEN GEN_TAC THEN
     LIST_INDUCT_TAC THEN 
     REWRITE_TAC[ALL; EX; sum_list_nil; sum_list_cons; LENGTH; REAL_MUL_LZERO; REAL_LE_REFL] THEN
     REWRITE_TAC[NOT_CONS_NIL; ARITH_RULE `SUC n = 1 + n`] THEN
     REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_ADD_RDISTRIB; REAL_MUL_LID] THEN
     STRIP_TAC THEN ASM_CASES_TAC `t:(A)list = []` THENL [
       ASM_REWRITE_TAC[LENGTH; sum_list_nil; REAL_MUL_LZERO; REAL_ADD_RID];
       MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_SIMP_TAC[]
     ]);;

let sum_list_bound_lt_gen = prove
  (`!f b s:(A)list. ~(s = []) /\ ALL (\x. f x < b / &(LENGTH s)) s
     ==> sum_list s f < b`,
   REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN REPEAT STRIP_TAC THEN
     SUBGOAL_THEN `b = &(LENGTH (s:(A)list)) * (b / &(LENGTH s))` MP_TAC THENL [
       ASM_SIMP_TAC[real_div; REAL_MUL_AC; REAL_MUL_LINV; REAL_OF_NUM_EQ; REAL_MUL_RID];
       ALL_TAC
     ] THEN
     DISCH_THEN (fun th -> ONCE_REWRITE_TAC[th]) THEN
     MATCH_MP_TAC sum_list_bound_lt_all THEN ASM_REWRITE_TAC[GSYM LENGTH_EQ_NIL]);;

let sum_list_delete_at = prove
  (`!f k s:(A)list. k < LENGTH s ==>
     sum_list (delete_at k s) f = sum_list s f - f (EL k s)`,
   GEN_TAC THEN INDUCT_TAC THEN LIST_INDUCT_TAC THEN 
     REWRITE_TAC[delete_at; LENGTH; sum_list_nil; sum_list_cons; 
		 LT_REFL; EL; HD; ARITH_RULE `~(SUC k < 0)`] THENL [
       REAL_ARITH_TAC;
       ASM_SIMP_TAC[LT_SUC; TL] THEN REAL_ARITH_TAC
     ]);;

let length_eq_sum_list = prove
  (`!s:(A)list. &(LENGTH s) = sum_list s (\x. &1)`,
   SIMP_TAC[sum_list_sum_alt; GSYM CARD_EQ_SUM; FINITE_NUMSEG; CARD_NUMSEG; ARITH_RULE `(a + 1) - 1 = a`]);;

let sum_list_closed = prove
  (`!P f s:(A)list. P (&0) /\ (!x y. P x /\ P y ==> P (x + y)) /\
     ALL (\x. P (f x)) s
     ==> P (sum_list s f)`,
   GEN_TAC THEN GEN_TAC THEN
     LIST_INDUCT_TAC THEN ASM_SIMP_TAC[sum_list_nil; sum_list_cons; ALL]);;

(* --------------------------------------------- *)
(* MAP/MAP2/ALL2 properties                      *)
(* --------------------------------------------- *)

let MAP_MAP = prove
  (`!(f:A->B) (h:C->A) s. MAP f (MAP h s) = MAP (\x. f (h x)) s`,
   GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[MAP]);;

let MAP2_MAP_ZIP = prove
  (`!(f:A->B->C) s1 s2. LENGTH s1 = LENGTH s2 
      ==> MAP2 f s1 s2 = MAP (\p. f (FST p) (SND p)) (ZIP s1 s2)`,
   GEN_TAC THEN REPEAT LIST_INDUCT_TAC THEN 
     REWRITE_TAC[MAP; MAP2; LENGTH; ZIP] THEN TRY ARITH_TAC THEN
     REWRITE_TAC[SUC_INJ] THEN DISCH_TAC THEN ASM_SIMP_TAC[]);;
     
let MAP2_MAP = prove
  (`!(f:A->B->C) (h1:D->A) (h2:E->B) s1 s2. LENGTH s1 = LENGTH s2
      ==> MAP2 f (MAP h1 s1) (MAP h2 s2) = MAP2 (\x y. f (h1 x) (h2 y)) s1 s2`,
   GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN 
     REPEAT LIST_INDUCT_TAC THEN REWRITE_TAC[MAP; MAP2; LENGTH] THEN TRY ARITH_TAC THEN
     REWRITE_TAC[SUC_INJ] THEN DISCH_TAC THEN ASM_SIMP_TAC[]);;

let MAP2_MAP_1 = prove
  (`!(f:A->B->C) (h:D->A) s1 s2. LENGTH s1 = LENGTH s2
      ==> MAP2 f (MAP h s1) s2 = MAP2 (\x y. f (h x) y) s1 s2`,
   GEN_TAC THEN GEN_TAC THEN
     REPEAT LIST_INDUCT_TAC THEN REWRITE_TAC[MAP; MAP2; LENGTH] THEN TRY ARITH_TAC THEN
     REWRITE_TAC[SUC_INJ] THEN DISCH_TAC THEN ASM_SIMP_TAC[]);;

let MAP2_MAP_2 = prove
  (`!(f:A->B->C) (h:D->B) s1 s2. LENGTH s1 = LENGTH s2
      ==> MAP2 f s1 (MAP h s2) = MAP2 (\x y. f x (h y)) s1 s2`,
   GEN_TAC THEN GEN_TAC THEN
     REPEAT LIST_INDUCT_TAC THEN REWRITE_TAC[MAP; MAP2; LENGTH] THEN TRY ARITH_TAC THEN
     REWRITE_TAC[SUC_INJ] THEN DISCH_TAC THEN ASM_SIMP_TAC[]);;

let ALL2_LENGTH_EQ = prove
  (`!s t (P:A->B->bool). ALL2 P s t ==> LENGTH s = LENGTH t`,
   REPEAT LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL2; LENGTH] THEN
     REPEAT STRIP_TAC THEN AP_TERM_TAC THEN
     FIRST_X_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `P:A->B->bool` THEN ASM_REWRITE_TAC[]);;

let all2_all_zip = prove
  (`!s t (P:A->B->bool). LENGTH s = LENGTH t
      ==> ALL2 P s t = ALL (\p. P (FST p) (SND p)) (ZIP s t)`,
   REPEAT LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ALL2; ALL; ZIP; LENGTH] THEN TRY ARITH_TAC THEN
     REWRITE_TAC[SUC_INJ] THEN REPEAT STRIP_TAC THEN
     REWRITE_TAC[TAUT `((A /\ B) <=> (A /\ C)) <=> (~A \/ (B <=> C))`] THEN DISJ2_TAC THEN
     ASM_SIMP_TAC[]);;

let all2_el = prove
  (`!s t (P:A->B->bool). ALL2 P s t <=> 
     (LENGTH s = LENGTH t /\ !i. i < LENGTH s ==> P (EL i s) (EL i t))`,
   REPEAT STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
     FIRST_ASSUM (MP_TAC o MATCH_MP ALL2_LENGTH_EQ) THEN SIMP_TAC[] THEN DISCH_TAC THEN
       FIRST_ASSUM (MP_TAC o ISPEC `P:A->B->bool` o MATCH_MP all2_all_zip) THEN
       ASM_SIMP_TAC[GSYM ALL_EL; length_zip; el_zip];
     ALL_TAC
   ] THEN
     ASM_SIMP_TAC[all2_all_zip; GSYM ALL_EL; length_zip; el_zip]);;
     
(* --------------------------------------------- *)
(* Extra properties                              *)
(* --------------------------------------------- *)
    
let sum_list_le_gen = prove
  (`!(s:(A)list) (t:(B)list) f g. ALL2 (\a b. f a <= g b) s t
     ==> sum_list s f <= sum_list t g`,
   REWRITE_TAC[all2_el; sum_list_sum_alt] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
     MATCH_MP_TAC SUM_LE THEN REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN
     REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
     ASM_ARITH_TAC);;

let all_delete_at_imp = prove
  (`!s:(A)list k P. ALL P s ==> ALL P (delete_at k s)`,
   LIST_INDUCT_TAC THEN INDUCT_TAC THEN ASM_SIMP_TAC[ALL; delete_at]);;


(* --------------------------------------------- *)
(* Conversions                                   *)
(* --------------------------------------------- *)

let rec EL_CONV tm =
  let n_tm, list_tm = dest_binary "EL" tm in
    try
      let suc_th = num_CONV n_tm in
      let conv = GEN_REWRITE_CONV LAND_CONV [suc_th] THENC REWRITE_CONV[EL; TL; HD] in
	if dest_small_numeral n_tm = 1 then
	  conv tm
	else
	  (conv THENC EL_CONV) tm
    with Failure _ ->
      REWRITE_CONV[EL; HD] tm;;

let rec delete_at_conv tm =
  let n_tm, list_tm = dest_binary "delete_at" tm in
    try
      let suc_th = num_CONV n_tm in
      let conv = GEN_REWRITE_CONV LAND_CONV [suc_th] THENC REWRITE_CONV[delete_at] in
	if dest_small_numeral n_tm = 1 then
	  conv tm
	else
	  (conv THENC RAND_CONV delete_at_conv) tm
    with Failure _ ->
      REWRITE_CONV[delete_at] tm;;

end;;