Stream: Beginner Questions

Topic: Why can't I unfold definitions from inside locales?

James Hanson (Apr 02 2024 at 17:56):

When I try to unfold a definition from inside a locale, Isabelle doesn't throw any errors but it also doesn't actually unfold the definition. What is happening here?

locale foo =
  fixes
    foo :: 'a and
    f :: "'a \<Rightarrow> 'a"
  assumes
    foo_fixed: "f foo = foo"

definition (in foo)
  f5 :: "'a \<Rightarrow> 'a"
  where "f5 x \<equiv> f (f (f (f (f x))))"

lemma "0 = 1"
proof -
  have "foo.f5 = foo.f5 \<circ> foo.f5"
    unfolding foo.f5_def

At this point the proof state is still this:

proof (prove)
goal (1 subgoal):
 1. foo.f5 = foo.f5 ∘ foo.f5

Wenda Li (Apr 02 2024 at 18:44):

unfolding will not throw an error even if Isabelle cannot progress. By examining the definition of f5 with

thm foo.f5_def

we know foo.f5_def is foo ?foo ?f ⟹ foo.f5 ?f ?x ≡ ?f (?f (?f (?f (?f ?x)))), which is a conditional rewrite. Normally, the unfolding keyword requires us to eliminate the conditions first. However, a more serious problem here is that even a manual rewrite will fail:

apply (subst foo.f5_def)

This means that foo.f5 ?f ?x (the left hand side of foo.f5_def) cannot be unified with any sub-expression of the target proposition foo.f5 = foo.f5 \<circ> foo.f5.

To summarise, the problem here is less about locale (which may introduce extra assumptions like foo ?foo ?f that makes a certain definition unsuitable for unfolding); instead, it is that the target proposition (foo.f5 = foo.f5 \<circ> foo.f5) cannot be rewritten with foo.f5_def.

James Hanson (Apr 04 2024 at 19:20):

Thank you. I hadn't appreciated the fact that definitions inside locales were conditional on the locale predicate.

Mathias Fleury (Apr 04 2024 at 19:54):

BTW, this is the reason why you often see one locale name XX_opts (no assumptions) and the real one called XX(with assumptions). So definition are put in the XX_opts to make unfolding easy.

Last updated: May 06 2024 at 16:21 UTC