Re: [isabelle] "show" taking very long with goals with many hypothesis



Hi Joachim,

Isabelle tries to unify the shown goal with the subgoals in the order of the goal state.
So, if you prove the goals in the order in which they occur in the goal state, there should not be any false unification attempts. That is, at "case (DApplicationInd ...)", this case really should be the first subgoal. If you skip some cases, e.g., because they can be solved in the final qed(...), then there might be such unnecessary unification attempts. You can rearrange the order of the subgoals with the prefer command before the case; e.g., if DApplicationInd shows the 23rd subgoal, you can use the following.

proof(...)
  ...
next
  prefer 23
  case (DApplicationInd ...)
  ...

However, this is quite ugly and breaks easily, because the number for prefer refers to the current goal state. For maintenance, I recommend that you start with the last subgoal that needs such treatment and end with the first. Then, the numbers remain stable if you find that you have to manually prove another case in between. Still, if you change your formalisation and add new cases in between, you have to adjust the numbers as necessary.

What happens if you try this? Does it speed things up? If not, then it might also be the pretty printing infrastructure which chokes on the mere size of the goal. As more and more data (types, classes, position information, ...) is sent to the prover IDE, the generation and parsing of the data can take considerable time. But from my experience, your goal is still too small for that effect to kick in.

Hope this helps,
Andreas


On 11/06/13 13:57, Joachim Breitner wrote:
Hi,

I have an inductive proof where the induction rule has a lot of very
similar assumptions, due to the Nominal machinery: (Don’t worry about
the details, this is just to give an impression of what I mean by
„many“).

1. ⋀n Γ Γ' Δ Δ' x e y Θ Θ' z e' u xa.
        atom n ♯ xa ⟹
        atom z ♯ xa ⟹
        atom n ♯ Γ ⟹
        atom n ♯ Γ' ⟹
        atom n ♯ Δ ⟹
        atom n ♯ Δ' ⟹
        atom n ♯ x ⟹
        atom n ♯ e ⟹
        atom n ♯ y ⟹
        atom n ♯ Θ ⟹
        atom n ♯ Θ' ⟹
        atom n ♯ z ⟹
        atom z ♯ Γ ⟹
        atom z ♯ Γ' ⟹
        atom z ♯ Δ ⟹
        atom z ♯ Δ' ⟹
        atom z ♯ x ⟹
        atom z ♯ e ⟹
        atom z ♯ y ⟹
        atom z ♯ Θ ⟹
        atom z ♯ Θ' ⟹
        distinctVars (((x, App e y) # Γ') @ Γ) ⟹
        distinctVars (((n, e) # (x, App (Var n) y) # Γ') @ Γ) ⟹
        distinctVars (((n, Lam [z]. e') # (x, App (Var n) y) # Δ') @ Δ) ⟹
        distinctVars (((x, e'[z::=y]) # Δ') @ Δ) ⟹
        distinctVars (Θ' @ Θ) ⟹
        Γ : (n, e) # (x, App (Var n) y) # Γ' ⇓⇧×⇧u⇧d Δ : (n, Lam [z]. e') # (x, App (Var n) y) # Δ' ⟹
        (⋀b. atom b ♯ (Γ, snd (hd ((n, e) # (x, App (Var n) y) # Γ'))) ⟹
             atom b ♯ (Δ, snd (hd ((n, Lam [z]. e') # (x, App (Var n) y) # Δ'))) ∨ b ∈ heapVars Δ) ⟹
        Δ : (x, e'[z::=y]) # Δ' ⇓⇧×⇧u⇧d Θ : Θ' ⟹
        (⋀b. atom b ♯ (Δ, snd (hd ((x, e'[z::=y]) # Δ'))) ⟹
             atom b ♯ (Θ, snd (hd Θ')) ∨ b ∈ heapVars Θ) ⟹
        atom xa ♯ (Γ, snd (hd ((x, App e y) # Γ'))) ⟹ atom xa ♯ (Θ, snd (hd Θ')) ∨ xa ∈ heapVars Θ

I handle the case using a named case:

case (DApplicationInd n Γ Γ' Δ Δ' xa e y Θ Θ' z e' u x)
   [..]
   thus ?case
   proof [..]
   qed

At the "thus", as well as at the "qed", Isabelle sits there for a long
time (minutes) before continuing.

My guess is that there are many ways to unify my assumptions with the
assumptions of the goal, and Isabelle tries a lot of wrong ones before
ruling them out according to the statement shown and the other
assumptions.

Is there a way to help out Isabelle here? And coudn’t the "case Foo"
command somehow ensure that Isabelle will try the „right“ unification
first?

Thanks,
Joachim





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