First pass at speeding up CF automation

basis/ArrayProofScript.sml

@@ -112,7 +112,7 @@ Proof
         ) \\
       once_rewrite_tac[CONS_APPEND] \\
       rewrite_tac[APPEND_ASSOC] \\
-      xapp \\ xsimpl ) \\
+      xapp \\ xsimpl \\ gvs []) \\
   Cases_on `l` >>
   fs [LIST_TYPE_def] >>
   rfs [] >>
@@ -1070,4 +1070,3 @@ Proof
   first_x_assum (irule_at Any)>>
   simp[]
 QED
-

basis/HashtableProofScript.sml

@@ -882,15 +882,15 @@ Proof
       \\qexists_tac `idx`
       \\qexists_tac `vlv`
       \\fs[REF_ARRAY_def]
-      \\xsimpl)
+      \\xsimpl \\ gvs [])
   \\ xlet `POSTv b. &(BOOL (mlmap$null (EL idx buckets)) b) * REF_ARRAY aRef arr2 newBuckets * REF_NUM uRef uv`
     >-(xapp
       \\qexists_tac `REF_ARRAY aRef arr2 newBuckets * REF_NUM uRef uv`
       \\qexists_tac `EL idx buckets`
       \\xsimpl
       \\qexists_tac `a`
       \\qexists_tac `b`
-      \\fs[])
+      \\gvs[])
   THEN1 (xif
   THEN1 (xlet `POSTv usedv. &(NUM uv usedv) * REF_ARRAY aRef arr2 newBuckets * REF_NUM uRef uv`
     >-(xapp
@@ -917,10 +917,9 @@ Proof
     \\qexists_tac `heuristic_size + 1`
     \\xsimpl
     \\qexists_tac `LUPDATE (mlmap$insert (EL (hf k MOD LENGTH buckets) buckets) k v) (hf k MOD LENGTH buckets) buckets`
-    \\`buckets <> []` by simp[NOT_NIL_EQ_LENGTH_NOT_0]
+    \\`buckets <> []` by gvs[NOT_NIL_EQ_LENGTH_NOT_0]
     \\ imp_res_tac list_union_lupdate_insert
-    \\ simp[]
-    \\fs[every_cmp_of_insert, buckets_ok_insert, list_rel_insert, every_map_ok_insert]))
+    \\gvs[every_cmp_of_insert, buckets_ok_insert, list_rel_insert, every_map_ok_insert]))
     \\xcon
     \\xsimpl
     \\qexists_tac `uRef`
@@ -932,10 +931,9 @@ Proof
     \\qexists_tac `heuristic_size`
     \\xsimpl
     \\qexists_tac `LUPDATE (mlmap$insert (EL (hf k MOD LENGTH buckets) buckets) k v) (hf k MOD LENGTH buckets) buckets`
-    \\`buckets <> []` by simp[NOT_NIL_EQ_LENGTH_NOT_0]
+    \\`buckets <> []` by gvs[NOT_NIL_EQ_LENGTH_NOT_0]
     \\ imp_res_tac list_union_lupdate_insert
-    \\ simp[]
-    \\fs[every_cmp_of_insert, buckets_ok_insert, list_rel_insert, every_map_ok_insert])
+    \\gvs[every_cmp_of_insert, buckets_ok_insert, list_rel_insert, every_map_ok_insert])
 QED
 
 Theorem list_app_pairs_spec:
@@ -1349,6 +1347,7 @@ Proof
   \\ `MAP_TYPE a b (EL (hf k MOD LENGTH vlv) buckets)
                    (EL (hf k MOD LENGTH vlv) vlv)`
     by fs[LIST_REL_EL_EQN]
+  \\ simp []
   \\ xlet_auto >- xsimpl
   \\ xlet_auto >- xsimpl
   \\ xlet_auto >- xsimpl

basis/ListProgScript.sml

@@ -184,15 +184,15 @@ Proof
     \\ xcf "tabulate" st
     \\ xlet `POSTv boolv. &BOOL (n >= m) boolv * heap_inv`
       >-(xopb \\ xsimpl \\ fs[NUM_def, INT_def] \\ intLib.COOPER_TAC)
-    \\ xif \\ asm_exists_tac \\ simp[]
+    \\ xif \\ gvs[]
     \\ xapp
     \\ instantiate \\ xsimpl
     \\ `m - n = 0` by simp[] \\ simp[])
   \\ rw[]
   \\ xcf "tabulate" st
   \\ xlet `POSTv boolv. &BOOL (n >= m) boolv * heap_inv`
     >-(xopb \\ xsimpl \\ fs[NUM_def, INT_def] \\ intLib.COOPER_TAC)
-  \\ xif \\ asm_exists_tac \\ simp[]
+  \\ xif \\ gvs []
   \\ Cases_on`m` \\ fs[]
   \\ rename1`SUC v = SUC m - n`
   \\ `v = m - n` by decide_tac

basis/TextIOProofScript.sml

@@ -937,7 +937,7 @@ Proof
   REVERSE (Cases_on`consistentFS fs`) >-(xpull >> fs[wfFS_def]) >>
   xpull >> rename [`W8ARRAY _ fnm0`] >>
   qmatch_goalsub_abbrev_tac`catfs fs * _` >>
-  rpt(xlet_auto >- xsimpl) >>
+  rpt (xlet_auto >- xsimpl) >>
   qmatch_goalsub_abbrev_tac`W8ARRAY _ fd0` >>
   qmatch_goalsub_rename_tac`W8ARRAY loc fd0` >>
   qmatch_goalsub_abbrev_tac`catfs fs' * _` >>
@@ -1072,10 +1072,9 @@ Proof
      qpat_abbrev_tac `new_events = events ++ _` >>
      qexists_tac `new_events` >> xsimpl) >>
   NTAC 3 (xlet_auto >- xsimpl) >>
-  CASE_TAC >> xif >> instantiate
-  >-(xcon >> fs[IOFS_def,liveFS_def] >> xsimpl) >>
+  xif >-(xcon >> fs [CaseEq"bool"] >> xsimpl) >>
   xlet_auto >-(xcon >> xsimpl) >>
-  xraise >> fs[InvalidFD_exn_def,IOFS_def] >> xsimpl
+  xraise >> fs[InvalidFD_exn_def,IOFS_def,CaseEq"bool"] >> xsimpl
 QED
 
 Theorem closeOut_spec:
@@ -1121,10 +1120,9 @@ Proof
      qpat_abbrev_tac `new_events = events ++ _` >>
      qexists_tac `new_events` >> xsimpl) >>
   NTAC 3 (xlet_auto >- xsimpl) >>
-  CASE_TAC >> xif >> instantiate
-  >-(xcon >> fs[IOFS_def,liveFS_def] >> xsimpl) >>
+  xif >-(xcon >> fs [CaseEq"bool"] >> xsimpl) >>
   xlet_auto >-(xcon >> xsimpl) >>
-  xraise >> fs[InvalidFD_exn_def,IOFS_def] >> xsimpl
+  xraise >> fs[InvalidFD_exn_def,IOFS_def,CaseEq"bool"] >> xsimpl
 QED
 
 Theorem closeIn_STDIO_spec:
@@ -1248,7 +1246,7 @@ Proof
      fs[GSYM n2w2_def] >>
      `(if n < k then n else k) < (2**(2*8))` by fs[] >>
      progress w22n_n2w2 >>
-     xif >> fs[FALSE_def] >> instantiate >> xvar >> xsimpl >>
+     xif >> fs[FALSE_def] >> xvar >> xsimpl >>
      fs[IOFS_def,wfFS_fsupdate,liveFS_fsupdate] >>
      instantiate >> fs[Abbr`fs'`,MIN_DEF,insert_atI_def] >> xsimpl) >>
  (* next element is 0 *)
@@ -1261,7 +1259,7 @@ Proof
                            DROP pos content))`
   >-(qmatch_goalsub_abbrev_tac` _ * _ * IOx _ fs'` >>
      qpat_abbrev_tac `Q = $POSTv _` >>
-     simp [fs_ffi_part_def, IOx_def, IO_def] >>
+     fs [fs_ffi_part_def, IOx_def, IO_def] >>
      xpull >> qunabbrev_tac `Q` >>
      xffi >> xsimpl >>
      fs[IOFS_def,IOx_def,fs_ffi_part_def,
@@ -1771,7 +1769,7 @@ Proof
       qexists_tac `new_events` >> xsimpl) >>
   rpt(xlet_auto >- xsimpl) >>
   xif >> instantiate >> xapp >> xsimpl >> rw[] >> instantiate >>
-  simp[GSYM n2w2_def,w22n_n2w2] >> xsimpl
+  simp[GSYM n2w2_def,w22n_n2w2] >> xsimpl >> gvs []
 QED
 
 Theorem read_into_spec:
@@ -1885,7 +1883,7 @@ Proof
       qexists_tac `new_events` >> xsimpl) >>
    rpt(xlet_auto >- xsimpl) >>
    xif >> instantiate >> xapp >> xsimpl >> rw[] >> instantiate >>
-   simp[GSYM n2w2_def,w22n_n2w2] >> xsimpl
+   simp[GSYM n2w2_def,w22n_n2w2] >> xsimpl >> gvs []
 QED
 
 Theorem read_byte_spec:
@@ -5205,7 +5203,22 @@ Proof
                     TAKE_APPEND1, TAKE_APPEND2, DROP_APPEND, DROP_APPEND1, DROP_APPEND2,
                     DROP_DROP_T]))
   \\ xlet_auto >- xsimpl
-  \\ reverse xif
+  \\ reverse xif \\ fs []
+  >-(xapp \\ CONV_TAC(RESORT_EXISTS_CONV List.rev)
+    \\ map_every qexists_tac [`bactive`,`fd`, `req`, `off`, `buf`] \\ simp[]
+    \\ fs[INSTREAM_BUFFERED_FD_def, REF_NUM_def, instream_buffered_inv_def] \\ xsimpl
+    \\ fs[PULL_EXISTS] \\  CONV_TAC(RESORT_EXISTS_CONV List.rev)
+    \\ map_every qexists_tac [`w`, `r`] \\ xsimpl
+    \\ rpt strip_tac
+    \\ `MIN req (STRLEN content − pos + (w − r)) = req` by simp[MIN_DEF, NOT_LESS]
+    \\ simp[] \\ map_every qexists_tac [`x'`,`x'3'`] \\ simp[]
+    \\ simp[TAKE_TAKE_T] \\ `r + req - w = 0` by fs[NOT_LESS]
+    \\ simp[TAKE_0]
+    \\ `pos + (r + (req + x'³')) − (w + x') = pos` by fs[]
+    \\ rw[] \\ simp[MIN_DEF, MAX_DEF]
+    \\ simp[fsupdate_unchanged] \\ xsimpl \\ fs []
+    \\ `r - w = 0` by fs []
+     \\ asm_rewrite_tac [TAKE_0])
   >-(xapp \\ CONV_TAC(RESORT_EXISTS_CONV List.rev)
     \\ map_every qexists_tac [`bactive`,`fd`, `req`, `off`, `buf`] \\ simp[]
     \\ fs[INSTREAM_BUFFERED_FD_def, REF_NUM_def, instream_buffered_inv_def] \\ xsimpl
@@ -5237,7 +5250,8 @@ Proof
   \\ xpull
   \\ xlet_auto >- xsimpl
   \\ xlet_auto >- xsimpl
-  \\ xlet_auto_spec (SOME input_spec) >- xsimpl
+  \\ simp[]
+  \\ xlet_auto_spec (SOME input_spec) >-  xsimpl
   \\ xlet_auto >- xsimpl
   \\ xlet_auto >- xsimpl
   \\ xlet_auto >- xsimpl
@@ -5725,19 +5739,16 @@ Theorem inputLines_spec:
 Proof
   Induct_on`splitlines (DROP pos content)` \\ rw[]
   >- (
-    `LENGTH content - pos = 0` by simp[]
-    \\ pop_assum SUBST1_TAC
-    \\ `DROP pos content = []` by fs[DROP_NIL]
-    \\ rpt strip_tac
-    \\ xcf_with_def TextIO_inputLines_v_def
+    xcf_with_def TextIO_inputLines_v_def
     \\ `IS_SOME (get_file_content fs fd)` by fs[IS_SOME_EXISTS]
     \\ xlet_auto >- xsimpl
     \\ rfs[std_preludeTheory.OPTION_TYPE_def,lineFD_def]
     \\ xmatch
     \\ xcon
     \\ simp[lineForwardFD_def,fastForwardFD_0]
     \\ xsimpl
-    \\ fs[LIST_TYPE_def])
+    \\ `DROP pos content = []` by fs[DROP_NIL]
+    \\ simp [LIST_TYPE_def])
   \\ qpat_x_assum`_::_ = _`(assume_tac o SYM) \\ fs[]
   \\ rpt strip_tac
   \\ xcf_with_def TextIO_inputLines_v_def
@@ -5925,9 +5936,7 @@ Proof
       first_x_assum match_mp_tac \\
       xlet_auto >- xsimpl \\
       xlet_auto >- xsimpl \\
-      xif \\
-      instantiate \\
-      strip_tac \\
+      xif \\ gvs [] \\
       xlet_auto >- xsimpl \\
       xlet_auto_spec(SOME input_spec)
       >- xsimpl \\

characteristic/cfLetAutoLib.sml

@@ -808,9 +808,12 @@ fun xlet_subst_parameters env app_info asl let_pre app_spec  =
       val params_tm_list = List.map (get_value env) params_expr_list
 
       (* NOT SURE if proper way: rewrite the values to prevent conflicts with the
-         parameters found by xapp_spec *)
+         parameters found by xapp_spec
+         TODO: commented out, unclear if it is helpful.
+      *)
+      (*
       val asl_thms = List.map ASSUME asl
-      val params_tm_list = List.map (fn x => CONV_TERM (SIMP_CONV bool_ss asl_thms) x) params_tm_list
+      val params_tm_list = List.map (fn x => CONV_TERM (SIMP_CONV bool_ss asl_thms) x) params_tm_list *)
       (*************************************************)
 
       (* Find the app variable *)

characteristic/cfTacticsLib.sml

@@ -169,6 +169,13 @@ val xlocal =
     first_assum MATCH_ACCEPT_TAC,
     (HO_MATCH_MP_TAC app_local \\ fs [] \\ NO_TAC),
     (HO_MATCH_ACCEPT_TAC cf_cases_local \\ NO_TAC),
+    (asm_rewrite_tac (cf_defs) \\
+     CONV_TAC (ONCE_DEPTH_CONV BETA_CONV) \\
+     rewrite_tac [local_is_local] \\
+     NO_TAC),
+    (* The previous tactic hopefully takes care of the goal;
+     * however, for backwards compatibility we might as well
+     * keep this around. *)
     (fs (local_is_local :: cf_defs) \\ NO_TAC)
   ] (* todo: is_local_pred *)
 
@@ -202,16 +209,17 @@ val xsimpl =
 
 (* [xlet] *)
 
-fun xlet_core cont0 cont1 cont2 =
+fun xlet_core cont0 qname =
   xpull_check_not_needed \\
   head_unfold cf_let_def \\
   irule local_elim \\ hnf \\
-  simp [namespaceTheory.nsOptBind_def] \\
+  rewrite_tac [namespaceTheory.nsOptBind_def] \\
   cont0 \\
   rpt CONJ_TAC THENL [
     all_tac,
     TRY (MATCH_ACCEPT_TAC cfHeapsBaseTheory.SEP_IMPPOSTv_inv_POSTv_left),
-    cont1 \\ cont2
+    (qx_gen_tac qname \\ simp_tac (srw_ss()) [])
+    \\ TRY xpull
   ]
 
 val res_CASE_tm =
@@ -263,8 +271,7 @@ fun xlet Q (g as (asl, w)) = let
 in
   xlet_core
     (qexists_tac Q)
-    (qx_gen_tac qname \\ simp [])
-    (TRY xpull)
+    qname
     g
 end
 
@@ -576,7 +583,9 @@ val xif_base =
   head_unfold cf_if_def \\
   irule local_elim \\ hnf \\
   reduce_tac \\
-  TRY (asm_exists_tac \\ simp [] \\ conj_tac \\ DISCH_TAC)
+  TRY (asm_exists_tac
+       \\ full_simp_tac std_ss []
+       \\ conj_tac \\ DISCH_TAC)
 
 val xif = xif_base
 

examples/array_searchProgScript.sml

@@ -464,6 +464,7 @@ Proof
       fs[] >>
       `start ≤ ((finish + start) DIV 2)` by fs[X_LE_DIV] >>
       imp_res_tac LIST_REL_EL_EQN >> fs[]) >>
+
   xlet `POSTv bv . ARRAY arr_v elem_vs * &BOOL F bv` (* d *)
   >- (xapp >> xsimpl >>
       qexists_tac `EL ((finish + start) DIV 2) elems` >>
@@ -498,6 +499,7 @@ Proof
       fs[DIV_LT_X]) >>
   qabbrev_tac `mid = (finish + start) DIV 2` >> fs[] >>
   qabbrev_tac `sub_list = DROP start (TAKE finish elems)` >>
+
   xif
   >- ( (* LOWER CASE - value in left half of sub_list *)
   qabbrev_tac `rec_len = mid - start` >>
@@ -618,6 +620,7 @@ Proof
   >- (qsuff_tac `mid < finish` >> fs[] >>
       UNABBREV_TAC "mid" >> fs[] >>
       fs[DIV_LT_X])
+  >- gvs []
   >-  fs[EVERY2_DROP]
   >- (
     qexists_tac `u` >> fs[] >>
@@ -655,4 +658,3 @@ Proof
     )
   )
 QED
-

examples/lpr_checker/array/lpr_arrayFullProgScript.sml

@@ -1598,7 +1598,6 @@ Proof
       intLib.ARITH_TAC)>>
     rw[]>>rpt(pairarg_tac>>fs[])>>
     metis_tac[])>>
-
   every_case_tac>>gvs[SUM_TYPE_def]
   >- (
     xmatch>>