Speedup EQF_INTRO

[ordinarymath]

Here is some testing scripts

val test_cand = DB.apropos ``~ _``
         |> map snd |> map #1
         |> map SPEC_ALL
         |> map CONJUNCTS
         |> flatten
         |> map SPEC_ALL
         |> map CONJUNCTS
         |> flatten
val cand = test_cand
         |> filter (fn thm => is_neg (concl (thm)))
val ERR = mk_HOL_ERR "Drule"

local
   val Fth = ASSUME F
in
   fun EQF_INTRO th =
      IMP_ANTISYM_RULE (NOT_ELIM th)
                       (DISCH F (CONTR (dest_neg (concl th)) Fth))
      handle HOL_ERR _ => raise ERR "EQF_INTRO" ""
end

local 
   val eq_F = el 4 $ CONJUNCTS $ SPEC_ALL EQ_CLAUSES; 
   val eq_F' =  SYM eq_F 
   val t = (dest_neg o fst o dest_eq) (concl eq_F') 
in 
   fun alt1_EQF_INTRO th = 
     let val t' = dest_neg (concl th) 
     in 
     EQ_MP (INST[t |-> t'] eq_F') th 
     end 
     handle HOL_ERR _ => raise ERR "EQF_INTRO" ""
end 

local
   val eq_F = el 4 $ CONJUNCTS $ SPEC_ALL EQ_CLAUSES;
   val eq_F' = SYM eq_F
   val t = (dest_neg o fst o dest_eq) (concl eq_F')
   (*  ∀t. ¬t ⇔ (t ⇔ F) *)
   val eq_F' = GEN t eq_F'
in
   fun alt2_EQF_INTRO th =
     let val t' = dest_neg (concl th)
     in
     EQ_MP (SPEC t' eq_F') th
     end
end
local
fun same f1 f2 x =
  case (total f1 x,total f2 x) of
    (SOME a,SOME b ) => aconv (concl a) (concl b)
  | (NONE,NONE) => true
  | _ => false
in
List.all (same EQF_INTRO alt1_EQF_INTRO)  test_cand
List.all (same EQF_INTRO alt2_EQF_INTRO)  test_cand
end

fun test f 0 arg = ()
  | test f n arg = (let val _ = f arg in test f (n - 1) arg end)

val t1 = test (map EQF_INTRO)
val t2 = test (map alt1_EQF_INTRO)
val t3 = test (map alt2_EQF_INTRO)
Count.apply (EQF_INTRO) (ASSUME `` ~ x``)
Count.apply (alt2_EQF_INTRO) (ASSUME `` ~ x``)
(*Note if starting from fresh session warm up by sending stuff*)
val a = Count.apply (t1 10000) cand
val b = Count.apply (t2 10000) cand
val c = Count.apply (t3 10000) cand

[ordinarymath]

Here are some numbers for my machine

val a = Count.apply (t1 10000) cand (* 1.6s*)
val b = Count.apply (t2 10000) cand (* 0.52213s *)
val c = Count.apply (t3 10000) cand (* 0.39270s *)

[mn200]

Curious that the one with SPEC does better than INST. Anyway, happy to merge once you've sorted out the errors.

[ordinarymath]

There's a bunch of indirection of creating a binarymap is my guess

[ordinarymath]

I've realized that IMP_ANTISYM_RULE is really bad because the first SPEC could be a really big term and now the second SPEC needs to traverse that whole term

[ordinarymath]

SYM_CONV also faces the same problem

[ordinarymath]

I have no idea how to fix this

[ordinarymath]

Or more like I don't know the proper way to fix this. I can make opentheory kernel use the old version of EQF_INTRO but I have no idea whats causing the failure

[ordinarymath]

Is this th60 failing or th61 failing?

Proof of 
 
 Data_List_concat Data_List_nil = Data_List_nil ∧
 ∀h t.
   Data_List_concat (Data_List_cons h t) =
   Data_List_append h (Data_List_concat t)
 
 failed.
 Failed to prove theorem th61.

[ordinarymath]

HOL/src/boss/prove_base_assumsScript.sml

Lines 1088 to 1104 in e0253e9

	(* |- (!P. Data_List_any P Data_List_nil <=> F) /\
	!P h t.
	Data_List_any P (Data_List_cons h t) <=> P h \/ Data_List_any P t
	*)
	val th60 = store_thm
	("th60", el 60 goals |> concl,
	conj_tac >- MATCH_ACCEPT_TAC (EQF_INTRO (SPEC_ALL any_nil))
	\\ MATCH_ACCEPT_TAC any_cons);
	val concat_nil = hd(amatch``Data_List_concat Data_List_nil``);
	val concat_cons = hd(amatch``Data_List_concat (Data_List_cons _ _)``);
	(* |- (T <> F) /\ (F <> T) *)
	val th61 = store_thm
	("th61", el 61 goals |> concl,
	PURE_REWRITE_TAC[iff_F,not_not,iff_T,not_F,and_T]);

[ordinarymath]

HOL/src/boss/prove_base_assumsScript.sml

Lines 1099 to 1115 in e0253e9

	(* |- (T <> F) /\ (F <> T) *)
	val th61 = store_thm
	("th61", el 61 goals |> concl,
	PURE_REWRITE_TAC[iff_F,not_not,iff_T,not_F,and_T]);
	val BOOL_EQ_DISTINCT = th61;
	(* |- Data_List_concat Data_List_nil = Data_List_nil /\
	!h t.
	Data_List_concat (Data_List_cons h t) =
	Data_List_append h (Data_List_concat t)
	*)
	val th62 = store_thm
	("th62", el 62 goals |> concl,
	conj_tac >- MATCH_ACCEPT_TAC concat_nil
	\\ MATCH_ACCEPT_TAC concat_cons);

or th62

[ordinarymath]

Ok goals is generated and can change and 61 |- (T <> F) /\ (F <> T) magically vanished