Re: [isabelle] rule is sometimes very slow



On Tue, 2 Dec 2014, Lars Noschinski wrote:

theory Scratch imports Main
begin

abbreviation funswapid :: "'a ⇒ 'a ⇒ 'a ⇒ 'a" (infix "⇌⇩F" 90) where
 "x ⇌⇩F y ≡ Fun.swap x y id"

notepad begin
 fix uv uw vu vw wu wv f GM HM m n a
 assume "(vw ⇌⇩F vu ∘ f HM ^^ Suc m ∘ (uw ⇌⇩F uv ∘ vw ⇌⇩F vu)) a = (f
GM ^^ Suc n) a"
 then have "∃m. (vw ⇌⇩F vu ∘ f HM ^^ Suc m ∘ (uw ⇌⇩F uv ∘ vw ⇌⇩F vu)) a
= (f GM ^^ Suc n) a"
   by (rule exI)
end

The proof step "rule exI" takes several seconds to complete on my
machine (in Isabelle 2014). Similar proofs, like

  by (rule_tac exI)
  by -  (rule exI)
  by - (erule exI)
  by metis
  by blast

are instantaneous, as expected. I looked a bit into the implementation
of rule and it seems that most time is spend
in evaluating the result of

  Drule.multi_resolves facts @{thms exI}

Drule.multi_resolves is not relevant here, it is merely a wrapper for Thm.biresolution, i.e. the main rule composition principle of Isabelle/Pure.


The key difference of the structured form

  then have "∃m. P m" by (rule exI)

compared to the other ones above is the order of higher-order unification attempts. The 'then' means that some fact is unified with the premise of exI, which is the worst-case situation ?P ?x and thus can go amiss.

Only in the second stage, the closed conclusion ∃. P m contributes more specific unification constraints.


This problem has been there in Isar proofs since 1998/1999, and until today I don't know a better way. The HO-unification code of Isabelle is ultimately a mystery to me.


	Makarius

----------------------------------------------------------------------------
                  http://stop-ttip.org  1,070,319 people so far
----------------------------------------------------------------------------


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.