Email Gateway (Nov 01 2023 at 19:29): Email Gateway (Nov 01 2023 at 19:29):From: Vincent Jackson <vjjac@student.unimelb.edu.au>
Hello all,
I have run into a bug in Isabelle2023/HOL with induct. The issue is that
induct doesn't fully generalise the variables in the inductive case that
it generates. (Even though it generalises the same variable in other
situations.) I suspect the issue has something to do with how the
rewrite is performed, higher order unification, as there are several
warnings of 'Unification bound exceeded' in the output buffer.
Here is a minimised example of the strange behaviour:
inductive ipred :: ‹'a ⇒ 'a ⇒ bool› where
ipred0: ‹ipred r g›
lemma induct_variable_fail:
fixes p3 :: ‹('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool›
assumes
‹ipred r g›
‹∀g'. p1 g' g ⟶ p2 (s1 a r g') (f1 (s2 g' r r) (s2 a r g'))›
‹∀g'. p3 g' g ⟶ p4 (s1 a (f2 r a) (f3 r g)) (f4 r r r g g' g' a)›
shows
‹ipred r (f5 r a a)›
using assms
proof (induct arbitrary: a rule: ipred.induct)
case (ipred0 r g)
then show ?case sorry
qed
The behaviour that I was expecting was that both /g/s in the inductive
premises would be bound (green/gold) variables, but instead, one of them
is an unbound (blue) variable. More curiously, if a /g/ is given as an
argument to /p2/, it is generalised correctly, even though the /g/ under
/p1/ is not.
The example is fairly fragile. Deleting any of the variables makes the
issue disappear, making the type variables different in the inductive
predicate also removes the issue, as does removing /p3/'s fixes
declaration. However, the issue does persist when reordering the variables.
I would be interested to know why this is happening, as the behaviour is
unintuitive. For now, I am using a logically equivalent assumption that
correctly generalises to get around the issue. But it would be better if
this situation was generalised correctly.
Thanks,
Vincent
--
Vincent Jackson
PhD Student
School of Computing and Information Systems
University of Melbourne
--
P.S. In case it is relevant, here's a minimal version of the actual
lemma I am proving
unbundle lattice_syntax
inductive rgsat :: ‹'c ⇒ ('h ⇒ 'h ⇒ bool) ⇒ ('h ⇒ 'h ⇒ bool) ⇒ ('h ⇒ bool) ⇒ ('h ⇒ bool) ⇒ bool› where
‹rgsat a b c d e›
definition wsstable :: ‹('a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ bool)› ("⌈ _ ⌉⇘_⇙" [0,0] 90) where
‹wsstable a b ≡ undefined›
definition sepconj :: ‹('a ⇒ bool) ⇒ ('a ⇒ bool) ⇒ ('a ⇒ bool)› (infixl ‹**› 88) where
‹sepconj a b ≡ undefined›
lemma rgsat_frame:
assumes
‹rgsat c r g p q›
‹∀p g'. g' ≤ g ⟶ (⌈ p f ⌉⇘r ⊔ g'⇙ ≤ ⌈ p ⌉⇘r ⊔ g'⇙ ⌈ f ⌉⇘r ⊔ g'⇙)›
‹∀p g'. g' ≤ g ⟶ (⌈ p ⌈ f ⌉⇘r ⊔ g⇙ ⌉⇘r ⊔ g'⇙ ≤ ⌈ p ⌉⇘r ⊔ g'⇙ ⌈ ⌈ f ⌉⇘r ⊔ g⇙ ⌉⇘r ⊔ g'⇙)›
shows
‹rgsat c r g (p f) (q ⌈ f ⌉⇘r ⊔ g⇙)›
using assms
apply (induct arbitrary: f rule: rgsat.induct)
oops
Email Gateway (Nov 02 2023 at 12:17):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Vincent, I took a look and I wasn't able to reproduce the output, or the warning, with the default settings. The unification search bound is by default set to 60. I was able to cause a number of perverse behaviours by setting it to lower values. If they are really low, the induction method doesn't terminate, and if they are say 45 then you get the warnings you mentioned and a different output with those g issues. Possibly an ancestor theory is modifying this bound. (That’s a mistake: such changes should be confined to local contexts.)
So my suggestion is to try the following (possibly with a bigger number):
declare [[unify_search_bound=60]]
Also, try this if the tracing messages are annoying:
declare [[unify_trace_bound=100]]
Larry Paulson
Email Gateway (Nov 02 2023 at 13:39):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,
According to a quick grep:
$ grep -r unify_search_bound *
thys/PLM/TAO_1_Embedding.thy:declare [[unify_search_bound = 40]] (*
prevent unification bound errors *)
Actually I think all of
declare [[smt_solver = cvc4]]
declare [[simp_depth_limit = 10]] (* prevent the simplifier from running
forever *)
declare [[unify_search_bound = 40]] (* prevent unification bound errors *)
should be removed from that theory (I checked, and they are not
necessary anyway).
I see also various changes of simp_depth_limit in the AFP and I don't
think that it is a good idea to have them in a non-local context…
$ grep -r simp_depth_limit * | grep declare
ArrowImpossibilityGS/Thys/Arrow_Order.thy:declare [[simp_depth_limit = 2]]
ArrowImpossibilityGS/Thys/Arrow_Order.thy:declare [[simp_depth_limit = 50]]
NormByEval/NBE.thy:declare [[simp_depth_limit = 10]]
NormByEval/NBE.thy:declare [[simp_depth_limit = 50]]
PLM/TAO_1_Embedding.thy:declare [[simp_depth_limit = 10]] (* prevent the
simplifier from running forever *)
Ramsey-Infinite/Ramsey.thy:declare [[simp_depth_limit = 5]]
Mathias
Email Gateway (Nov 02 2023 at 18:40):From: Lawrence Paulson <lp15@cam.ac.uk>
Already gone!
Larry
Email Gateway (Nov 04 2023 at 15:25):From: Vincent Jackson <vjjac@student.unimelb.edu.au>
Thanks, this is indeed the source of the issue.
I am using the defaults, but there appears to be some sort of difference
between Isabelle's behaviour on my computer and yours. If I increase the
bound to 61, the issue disappears on my computer.
In any case, I now know how to solve this issue when it occurs.
Thanks again for your assistance,
Vincent
Last updated: Apr 28 2024 at 16:17 UTC