Email Gateway (Aug 22 2022 at 15:26): Email Gateway (Aug 22 2022 at 15:26):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I have a looping 'auto' command in the following theory, for a fairly
simple goal (indicated by the fact that the proof can be completed
using 'standard; simp'). I don't know why this is happening, can anyone
figure out what's going on here?
This affects Isabelle2016-1 and c5b19f997214.
Cheers,
Bertram
theory Loop
imports Main
begin
definition refined :: "'a list ⇒ 'b list ⇒ bool" where
"refined ss ts ⟷ length ts = length ss ∧
(∀i j. i < length ss ∧ j < length ts ∧ ss ! i = ss ! j ⟶ ts ! i = ts ! j)"
definition imbalance :: "'a list ⇒ nat" where
"imbalance xs = card { i. i < length xs ∧ (∀j. j < length xs ∧ xs ! i = xs ! j ⟶ i ≤ j) }"
lemma refined_imbalance_mono:
"refined ss ts ⟹ imbalance ss ≥ imbalance ts"
(* apply (auto simp: refined_def imbalance_def intro: card_mono) (* desired proof *) *)
unfolding refined_def imbalance_def
apply (intro card_mono)
apply simp
apply auto (* loops? *)
(* the proof can be completed by the following two commands: *)
apply standard
apply simp
done
end
Email Gateway (Aug 22 2022 at 15:32):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Replying to myself:
I tried to reduce the example, and ended up with the following statement
that causes the simplifier to loop for a trivial goal (solvable by .):
notepad begin
fix P :: "'a ⇒ bool" and f :: "'a ⇒ 'b"
assume "P j ⟹ f i = f j" for i j
then have "P j ⟹ f i = f j" for i j
apply (simp only: )
end
I'm still not sure how to read the resulting simplifier trace, but it's
definitely looping. If I do understand it correctly, the simplifier
turns the premise into a rewrite rule
P ?j1 ⟹ f i ≡ f ?j1
which it then applies to the given P j to obtain f i ≡ f j, and then
f j ≡ f j over and over again. The rewrite rule
P ?j3 ⟹ f ?i3 = f ?j3 ≡ True
that would solve the goal never gets a chance to fire, apparently,
perhaps because of the meta level equality?
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 15:32):From: Tobias Nipkow <nipkow@in.tum.de>
Your analysis is correct. The simplifier gets into a loop because the rules you
have given it allow it to. The simpifier follows a certain fixed strategy and
does not try to detect nontermination if it involves more than one rule.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 15:32):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Tobias Nipkow wrote:
That's a bit unsatisfying. Since those rewrite rules arise from the
premises I guess my only option is to hide the problematic equalities
from the simplifier? At least for my original theory, this works:
definition "hide_eq ss i j ⟷ ss ! i = ss ! j"
lemma refined_imbalance_mono:
"refined ss ts ⟹ imbalance ss ≥ imbalance ts"
by (auto simp: refined_def imbalance_def hide_eq_def[symmetric]
intro: card_mono)
It feels like a dirty trick though.
Cheers,
Bertram
Email Gateway (Aug 22 2022 at 15:33):From: Thomas.Sewell@data61.csiro.au
Hi Bertram.
I had a look at your problem as well.
It is a common difficulty that the simplifier will use premises of the
form "forall x. P x --> x = ..." as
conditional rewrite rules, and they frequently apply far too easily,
leading to indefinite recursion or
to looping.
The version in your notepad happens because the rewrite rule, together
with the extra assumption "P j",
can be used to rewrite "f x" into "f j" for any x, including x=j. The
simplifier doesn't note this is a loop
because it doesn't know until it recurses that the only solution to "P
?x" requires ?x=j.
Sometimes you can work you way through these via apply (simp(no_asm_use))
or apply (simp(no_asm_simp)). That requires a long proof, however,
rather than an easy proof with auto.
One option is to control the use of quantifiers a bit more by providing
classical rules instead.
Here's a proof which works by providing rules for your "refined" predicate:
lemma refined_length_eq:
"refined ss ts ⟹ length ts = length ss"
by (simp add: refined_def)
lemma list_eq_refinedD:
"ss ! i = ss ! j ⟹ refined ss ts ⟹ i < length ss ⟹ j < length ss
⟹ ts ! i = ts ! j"
unfolding refined_def
by metis
lemma refined_imbalance_mono:
"refined ss ts ⟹ imbalance ss ≥ imbalance ts"
(* apply (auto simp: refined_def imbalance_def intro: card_mono) (*
desired proof *) *)
unfolding imbalance_def
apply (auto intro!: card_mono simp: refined_length_eq dest:
list_eq_refinedD)
It took me a couple of rounds to get it to work with standard auto. You
can also try fastforce,
which is a bit more aggressive, or turn up auto's search depth
e.g. (auto 4 4 intro: card_mono simp: refined_length_eq dest:
refined_eq_imp)
Perhaps that helps?
Cheers,
Thomas.
Email Gateway (Aug 22 2022 at 15:33):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Thomas,
I had a look at your problem as well.
Thanks a lot! The idea of using derived properties instead of the
full definition looks like a natural and fairly general way of
avoiding exposing the simplifier to harmful simplification rules.
Cheers,
Bertram
Last updated: Apr 25 2024 at 12:23 UTC