formal_ineqs/list/more_list.hl

   1 (* =========================================================== *)\r
   2 (* Additional list definitions and theorems                    *)\r
   3 (* Author: Alexey Solovyev                                     *)\r
   4 (* Date: 2012-10-27                                            *)\r
   5 (* =========================================================== *)\r
   6 \r
   7 module More_list = struct\r
   8 \r
   9 (* definitions *)\r
  10 let REVERSE_TABLE  = define `(REVERSE_TABLE (f:num->A) 0 = []) /\\r
  11    (REVERSE_TABLE f (SUC i) = CONS (f i)  ( REVERSE_TABLE f i))`;; \r
  12   \r
  13 let TABLE = new_definition `!(f:num->A) k. TABLE f k = REVERSE (REVERSE_TABLE f k)`;;\r
  14 \r
  15 let l_seq = new_definition `l_seq n m = TABLE (\i. n + i) ((m + 1) - n)`;;\r
  16 \r
  17 (* lemmas *)\r
  18 let LENGTH_REVERSE_TABLE = prove(`!(f:num->A) n. LENGTH (REVERSE_TABLE f n) = n`,\r
  19    GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[REVERSE_TABLE; LENGTH]);;\r
  20 \r
  21 let LENGTH_REVERSE = prove(`!(l:(A)list). LENGTH (REVERSE l) = LENGTH l`,\r
  22    MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[REVERSE] THEN\r
  23      REPEAT STRIP_TAC THEN\r
  24      ASM_REWRITE_TAC[LENGTH_APPEND; LENGTH] THEN\r
  25      ARITH_TAC);;\r
  26 \r
  27 let LENGTH_TABLE = prove(`!(f:num->A) n. LENGTH (TABLE f n) = n`,\r
  28    REWRITE_TAC[TABLE; LENGTH_REVERSE; LENGTH_REVERSE_TABLE]);;\r
  29 \r
  30 let EL_TABLE = prove(`!(f:num->A) n i. i < n ==> EL i (TABLE f n) = f i`,\r
  31    REPEAT GEN_TAC THEN SPEC_TAC (`n:num`, `n:num`) THEN\r
  32      INDUCT_TAC THENL [ ARITH_TAC; ALL_TAC ] THEN\r
  33      REWRITE_TAC[TABLE; REVERSE_TABLE; REVERSE; EL_APPEND] THEN\r
  34      REWRITE_TAC[GSYM TABLE; LENGTH_TABLE] THEN\r
  35      DISCH_TAC THEN COND_CASES_TAC THENL\r
  36      [\r
  37        FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];\r
  38        ALL_TAC\r
  39      ] THEN\r
  40      SUBGOAL_THEN `i = n:num` (fun th -> REWRITE_TAC[th]) THENL\r
  41      [\r
  42        POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN\r
  43          ARITH_TAC;\r
  44        ALL_TAC\r
  45      ] THEN\r
  46      REWRITE_TAC[ARITH_RULE `n - n = 0`; EL; HD]);;\r
  47 \r
  48 let LIST_EL_EQ = prove(`!ul vl:(A)list. ul = vl <=> \r
  49                (LENGTH ul = LENGTH vl /\ (!j. j < LENGTH ul ==> EL j ul = EL j vl))`,\r
  50    REPEAT STRIP_TAC THEN\r
  51      EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN\r
  52      POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN\r
  53      SPEC_TAC (`vl:(A)list`, `vl:(A)list`) THEN SPEC_TAC (`ul:(A)list`, `ul:(A)list`) THEN\r
  54      LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN SIMP_TAC[LENGTH_EQ_NIL; EQ_SYM_EQ; LENGTH; ARITH_RULE `~(0 = SUC a)`] THEN\r
  55      POP_ASSUM (fun th -> ALL_TAC) THEN\r
  56      REWRITE_TAC[ARITH_RULE `SUC a = SUC b <=> a = b`] THEN\r
  57      REPEAT STRIP_TAC THEN\r
  58      FIRST_X_ASSUM (MP_TAC o SPEC `t':(A)list`) THEN\r
  59      ASM_REWRITE_TAC[] THEN\r
  60      ANTS_TAC THENL\r
  61      [\r
  62        REPEAT STRIP_TAC THEN\r
  63          FIRST_X_ASSUM (MP_TAC o SPEC `SUC j`) THEN\r
  64          ASM_REWRITE_TAC[ARITH_RULE `SUC a < SUC b <=> a < b`; EL; TL];\r
  65        ALL_TAC\r
  66      ] THEN\r
  67      DISCH_TAC THEN\r
  68      FIRST_X_ASSUM (MP_TAC o SPEC `0`) THEN\r
  69      ASM_SIMP_TAC[ARITH_RULE `0 < SUC a`; EL; HD]);;\r
  70 \r
  71 \r
  72 let LENGTH_L_SEQ = prove(`LENGTH (l_seq n m) = (m + 1) - n`, REWRITE_TAC[l_seq; LENGTH_TABLE]);;\r
  73 \r
  74 let EL_L_SEQ = prove(`!i m n. i < (m + 1) - n ==> EL i (l_seq n m) = n + i`,\r
  75   REWRITE_TAC[l_seq] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC EL_TABLE THEN ASM_REWRITE_TAC[]);;\r
  76   \r
  77 let L_SEQ_NIL = prove(`!n m. l_seq n m = [] <=> (m < n)`,\r
  78   GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[GSYM LENGTH_EQ_NIL; LENGTH_L_SEQ] THEN ARITH_TAC);;\r
  79   \r
  80 let L_SEQ_NN = prove(`!n. l_seq n n = [n]`,\r
  81   GEN_TAC THEN REWRITE_TAC[l_seq; ARITH_RULE `(n + 1) - n = 1`; ONE; TABLE; REVERSE_TABLE; REVERSE] THEN\r
  82     REWRITE_TAC[APPEND; ADD_0]);;\r
  83 \r
  84 let L_SEQ_CONS = prove(`!n m. n <= m ==> l_seq n m = CONS n (l_seq (n + 1) m)`,\r
  85   REPEAT STRIP_TAC THEN\r
  86     REWRITE_TAC[LIST_EL_EQ; LENGTH_L_SEQ; LENGTH] THEN CONJ_TAC THENL\r
  87     [\r
  88       ASM_ARITH_TAC;\r
  89       ALL_TAC\r
  90     ] THEN\r
  91     INDUCT_TAC THENL\r
  92     [\r
  93       ASM_SIMP_TAC[EL_L_SEQ] THEN ASM_REWRITE_TAC[EL; HD] THEN ARITH_TAC;\r
  94       DISCH_TAC THEN\r
  95         ASM_SIMP_TAC[EL_L_SEQ] THEN ASM_REWRITE_TAC[EL; TL] THEN\r
  96         MP_TAC (SPECL [`j:num`; `m:num`; `n + 1`] EL_L_SEQ) THEN ANTS_TAC THENL\r
  97         [\r
  98           ASM_ARITH_TAC;\r
  99           ALL_TAC\r
 100         ] THEN\r
 101         DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN ARITH_TAC\r
 102     ]);;\r
 103 \r
 104 \r
 105 let LENGTH_BUTLAST = prove(`!l. LENGTH (BUTLAST l) = LENGTH l - 1`,\r
 106    MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[BUTLAST; LENGTH; ARITH] THEN REPEAT STRIP_TAC THEN\r
 107      COND_CASES_TAC THEN ASM_REWRITE_TAC[LENGTH; ARITH] THEN\r
 108      POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN\r
 109      ARITH_TAC);;\r
 110 \r
 111 let EL_BUTLAST = prove(`!(l:(A)list) i. i < LENGTH l - 1 ==> EL i (BUTLAST l) = EL i l`,\r
 112    MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[BUTLAST; LENGTH] THEN REPEAT STRIP_TAC THEN\r
 113      COND_CASES_TAC THENL\r
 114      [\r
 115        UNDISCH_TAC `i < SUC (LENGTH (a1:(A)list)) - 1` THEN\r
 116          ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC;\r
 117        ALL_TAC\r
 118      ] THEN\r
 119      REWRITE_TAC[EL_CONS] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN\r
 120      FIRST_X_ASSUM (MP_TAC o SPEC `i - 1`) THEN\r
 121      ANTS_TAC THENL\r
 122      [\r
 123        ASM_ARITH_TAC;\r
 124        ALL_TAC\r
 125      ] THEN\r
 126      REWRITE_TAC[]);;\r
 127 \r
 128 end;;\r