Mathias Fleury (Sep 12 2020 at 08:39): Mathias Fleury (Sep 12 2020 at 08:39):I have an unusual use case: I check the proofs generated by the SMT solver veriT (so once I have pushed my work, there will be a veriT_smt and an smt tactic). There is one rule that appears very often, namely ?P ≠ ?Q ∨ ¬ ?P ∨ ?Q with some (potentially large) P and Q.
What is the fastest way to convert the term to a theorem? I have tried various things and never managed to get below 10ms (on my computer), but replaying such steps is so trivial that I find 10ms already too much.
Here is a real example if you want to play with it:
If you don't have imported List.thy, uncomment Nil and cons at the top:
context
fixes piecewise_C1 :: "('real :: {one,zero,ord} ⇒ 'a :: {one,zero,ord}) ⇒ 'real set ⇒ bool" and
joinpaths :: "('real ⇒ 'a) ⇒ ('real ⇒ 'a) ⇒ 'real ⇒ 'a" (* and
cons :: ‹'a ⇒ 'b ⇒ 'b› and
Nil :: ‹'b› *)
begin
notation piecewise_C1 (infixr "piecewise'_C1'_differentiable'_on" 50)
notation joinpaths (infixr "+++" 75)
(* notation cons (infixr "#" 75)
notation Nil ("[]" 80) *)
lemma XX:
‹((∀veriT_vr2 veriT_vr3.
(veriT_vr2 = rec_join veriT_vr3 ∧
([] = veriT_vr3 ∧ (λuu. 0) = veriT_vr2 ⟶ False) ∧
(∀veriT_vr4.
veriT_vr3 = veriT_vr4 # [] ∧
veriT_vr2 = coeff_cube_to_path veriT_vr4 ⟶
False) ∧
(∀veriT_vr4 veriT_vr5 veriT_vr6.
veriT_vr3 = veriT_vr4 # veriT_vr5 # veriT_vr6 ∧
veriT_vr2 =
coeff_cube_to_path veriT_vr4 +++
rec_join (veriT_vr5 # veriT_vr6) ⟶
False) ⟶
False) =
(rec_join veriT_vr3 = rec_join veriT_vr3 ∧
([] = veriT_vr3 ∧ (λuu. 0) = rec_join veriT_vr3 ⟶
False) ∧
(∀veriT_vr4.
veriT_vr3 = veriT_vr4 # [] ∧
rec_join veriT_vr3 = coeff_cube_to_path veriT_vr4 ⟶
False) ∧
(∀veriT_vr4 veriT_vr5 veriT_vr6.
veriT_vr3 = veriT_vr4 # veriT_vr5 # veriT_vr6 ∧
rec_join veriT_vr3 =
coeff_cube_to_path veriT_vr4 +++
rec_join (veriT_vr5 # veriT_vr6) ⟶
False) ⟶
False)) ∧
(∀veriT_vr3.
rec_join veriT_vr3 = rec_join veriT_vr3 ∧
([] = veriT_vr3 ∧ (λuu. 0) = rec_join veriT_vr3 ⟶ False) ∧
(∀veriT_vr4.
veriT_vr3 = veriT_vr4 # [] ∧
rec_join veriT_vr3 = coeff_cube_to_path veriT_vr4 ⟶
False) ∧
(∀veriT_vr4 veriT_vr5 veriT_vr6.
veriT_vr3 = veriT_vr4 # veriT_vr5 # veriT_vr6 ∧
rec_join veriT_vr3 =
coeff_cube_to_path veriT_vr4 +++
rec_join (veriT_vr5 # veriT_vr6) ⟶
False) ⟶
False) ≠
(∀veriT_vr3.
rec_join veriT_vr3 = rec_join veriT_vr3 ∧
([] = veriT_vr3 ∧ (λuu. 0) = rec_join veriT_vr3 ⟶ False) ∧
(∀veriT_vr4.
veriT_vr3 = veriT_vr4 # [] ∧
rec_join veriT_vr3 = coeff_cube_to_path veriT_vr4 ⟶
False) ∧
(∀veriT_vr4 veriT_vr5 veriT_vr6.
veriT_vr3 = veriT_vr4 # veriT_vr5 # veriT_vr6 ∧
rec_join veriT_vr3 =
coeff_cube_to_path veriT_vr4 +++
rec_join (veriT_vr5 # veriT_vr6) ⟶
False) ⟶
False)) ≠
False ∨
¬ ((∀veriT_vr2 veriT_vr3.
(veriT_vr2 = rec_join veriT_vr3 ∧
([] = veriT_vr3 ∧ (λuu. 0) = veriT_vr2 ⟶ False) ∧
(∀veriT_vr4.
veriT_vr3 = veriT_vr4 # [] ∧
veriT_vr2 = coeff_cube_to_path veriT_vr4 ⟶
False) ∧
(∀veriT_vr4 veriT_vr5 veriT_vr6.
veriT_vr3 = veriT_vr4 # veriT_vr5 # veriT_vr6 ∧
veriT_vr2 =
coeff_cube_to_path veriT_vr4 +++
rec_join (veriT_vr5 # veriT_vr6) ⟶
False) ⟶
False) =
(rec_join veriT_vr3 = rec_join veriT_vr3 ∧
([] = veriT_vr3 ∧ (λuu. 0) = rec_join veriT_vr3 ⟶
False) ∧
(∀veriT_vr4.
veriT_vr3 = veriT_vr4 # [] ∧
rec_join veriT_vr3 = coeff_cube_to_path veriT_vr4 ⟶
False) ∧
(∀veriT_vr4 veriT_vr5 veriT_vr6.
veriT_vr3 = veriT_vr4 # veriT_vr5 # veriT_vr6 ∧
rec_join veriT_vr3 =
coeff_cube_to_path veriT_vr4 +++
rec_join (veriT_vr5 # veriT_vr6) ⟶
False) ⟶
False)) ∧
(∀veriT_vr3.
rec_join veriT_vr3 = rec_join veriT_vr3 ∧
([] = veriT_vr3 ∧ (λuu. 0) = rec_join veriT_vr3 ⟶
False) ∧
(∀veriT_vr4.
veriT_vr3 = veriT_vr4 # [] ∧
rec_join veriT_vr3 = coeff_cube_to_path veriT_vr4 ⟶
False) ∧
(∀veriT_vr4 veriT_vr5 veriT_vr6.
veriT_vr3 = veriT_vr4 # veriT_vr5 # veriT_vr6 ∧
rec_join veriT_vr3 =
coeff_cube_to_path veriT_vr4 +++
rec_join (veriT_vr5 # veriT_vr6) ⟶
False) ⟶
False) ≠
(∀veriT_vr3.
rec_join veriT_vr3 = rec_join veriT_vr3 ∧
([] = veriT_vr3 ∧ (λuu. 0) = rec_join veriT_vr3 ⟶
False) ∧
(∀veriT_vr4.
veriT_vr3 = veriT_vr4 # [] ∧
rec_join veriT_vr3 = coeff_cube_to_path veriT_vr4 ⟶
False) ∧
(∀veriT_vr4 veriT_vr5 veriT_vr6.
veriT_vr3 = veriT_vr4 # veriT_vr5 # veriT_vr6 ∧
rec_join veriT_vr3 =
coeff_cube_to_path veriT_vr4 +++
rec_join (veriT_vr5 # veriT_vr6) ⟶
False) ⟶
False)) ∨
False ›
sorry
ML ‹
val X = Thm.prop_of @{thm XX}
val thm = @{lemma ‹⋀a b. (a ≠ b) ∨ ¬a ∨ b› by blast+}
fun chrono' f n =
if n = 0 then []
else
let val start = Timing.start ()
val _ = f @{context}
val total = Time.toMilliseconds (#elapsed (Timing.result start))
in total :: chrono' f (n-1) end
fun chrono f =
let val n = 10000 in
fold (curry (op +)) (chrono' f n) n
end
›
ML "ML_Heap.share_common_data ()"
(*If you like tactics, try it here by replacing match_tac*)
ML ‹chrono (fn _ => SMT_Replay_Methods.prove @{context} X
(fn ctxt => (match_tac ctxt [thm])))›
ML "ML_Heap.share_common_data ()"
ML ‹
chrono (fn ctxt => SMT_Replay_Methods.match_instantiate ctxt X thm)›
ML "ML_Heap.share_common_data ()"
(*find P and Q and instantiate them directly*)
ML ‹
let
fun f ((* Const ("HOL.Trueprop", _) *) _ $
((* Const ("HOL.disj", _) *) _ $
((* Const ("HOL.Not",_) *) _ $
((* Const ("HOL.eq", _) *) _$ t1 $ t2)) $ _ ))
ctxt = Thm.instantiate ([], [((("Q", 0), @{typ bool}), Thm.cterm_of ctxt t2), ((("P", 0), @{typ bool}), Thm.cterm_of ctxt t1)])
in
chrono (f @{context} X)
end›
ML "ML_Heap.share_common_data ()"
(*fastest solution*)
ML ‹
chrono (fn ctxt => SMT_Replay_Methods.match_instantiate ctxt X thm)›
end
Last updated: Apr 20 2024 at 12:26 UTC