Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] "show" taking very long with goals with many h...

view this post on Zulip Email Gateway (Aug 19 2022 at 11:15):

From: Joachim Breitner <breitner@kit.edu>
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
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 11:15):

From: Joachim Breitner <breitner@kit.edu>
Hi,

this does not seem to be the problem here, as I do prove the subgoals in
the order they occur: Even if I discharge all other cases before, the
show takes long. So I still believe it is a problem with the large(?)
number of variables and similar assumptions.

Sorry for not providing a minimal example, but the real code is, for
example, here:
http://afp.sourceforge.net/browser_info/current/HOL/HOLCF/Nominal2/Launchbury/LaunchburyStacked.html
(Lemma reds_fresh', case DApplication, first "thus").

Greetings,
Joachim
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 11:16):

From: Joachim Breitner <breitner@kit.edu>
Hi,

here is one:

theory Scratch imports Main begin

consts foo :: "nat => bool"
consts bar :: "nat => nat => nat => nat => nat => nat => nat => nat => bool"
consts A :: bool
consts B :: bool

lemma ind_rule[case_names CaseName]: "(⋀a b c d e f g h .
foo a ⟹
foo b ⟹
foo c ⟹
foo d ⟹
foo e ⟹
foo f ⟹
foo g ⟹
foo h ⟹
bar a b c d e f g h ⟹
A) ⟹ B" sorry

lemma B
proof (induction rule: ind_rule)
case (CaseName a b c d e f g h)
show A (* This takes very long *)
apply (rule ccontr)
sorry (* This also *)
qed

end

Adding another parameter makes it take longer than I’d like to wait,
while after removing a parameter, things are fast enough so that I
woudn’t bother.

Greetings,
Joachim
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 11:16):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Joachim,

I think you are right that unification is the bottle neck. In your minimal example, you
can speed things up by using a different order of the assumptions. If "bar ..." comes
first, show is instantaneous. This might also work your application with Nominal2, but you
either have to adjust the induction rule (such that the freshness constraints come at the
end) or use the manual "fix-assume-show" style instead of "case".

Andreas

view this post on Zulip Email Gateway (Aug 19 2022 at 11:36):

From: Makarius <makarius@sketis.net>
Apart from that publicly visible application, Larry has shown me his
private project which is all very huge and slow due to Nominal2. There
are Simplifier invocations that take minutes due to all these small
Nominal2 freshness particles.

We should probably move over this thread over to isabelle-dev, to sort out
both the performance issues of Nominal2 and the question if it manages
become part of the next Isabelle release, which will happen quite soon
after the summer. (I am myself not an active participant of the nominal
mailing list.)

Makarius

Last updated: Apr 19 2024 at 01:05 UTC