Email Gateway (Aug 22 2022 at 20:07): Email Gateway (Aug 22 2022 at 20:07):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
In my work on formalizing process calculi I tripped over an issue with
Isabelle’s locale support that I don’t fully understand. I’d like to
illustrate this issue here with some example code that is much simpler
than my actual code but still illustrates the point.
Let’s first introduce a locale that describes an involution, which we
call negation.
locale negation =
fixes neg :: "'a ⇒ 'a" ("⊖ _" [81] 80)
assumes neg_neg: "⊖ (⊖ x) = x"
Next, we define a locale that captures structures with a zero and a
subtraction. Any such structure gives rise to a negation and this
negation has the property that it turns zero into zero.
locale zero_subtraction =
fixes zero :: 'a ("𝟬")
fixes sub :: "['a, 'a] ⇒ 'a" (infixl "⊖" 65)
assumes sub_sub: "x ⊖ (x ⊖ y) = y"
assumes sub_zero_2: "x ⊖ 𝟬 = x"
begin
abbreviation neg :: "'a ⇒ 'a" ("⊖ _" [81] 80) where
"⊖ x ≡ 𝟬 ⊖ x"
sublocale negation neg
proof
fix x
show "𝟬 ⊖ (𝟬 ⊖ x) = x" using sub_sub .
qed
lemma neg_zero:
shows "⊖ 𝟬 = 𝟬"
using sub_zero_2 .
end
Finally, we introduce a locale that captures structures with a negation,
a zero, and an addition. We import the negation locale to provide the
negation structure. Since we can construct subtraction from negation and
addition, we introduce a corresponding sublocale relationship. This
would give us another instance of the negation locale through the
zero_subtraction locale, albeit with the same negation operator. To
prevent this, we use rewrites.
locale negation_zero_addition =
negation neg for neg :: "'a ⇒ 'a" ("⊖ _" [81] 80) +
fixes zero :: 'a ("𝟬")
fixes add :: "['a, 'a] ⇒ 'a" (infixl "⊕" 65)
assumes add_zero_1: "𝟬 ⊕ x = x"
assumes add_zero_2: "x ⊕ 𝟬 = x"
assumes neg_add: "⊖ (x ⊕ y) = (⊖ x) ⊕ (⊖ y)"
assumes add_cancel: "x ⊕ ((⊖ x) ⊕ y) = y"
begin
abbreviation sub :: "['a, 'a] ⇒ 'a" (infixl "⊖" 65) where
"x ⊖ y ≡ x ⊕ (⊖ y)"
sublocale zero_subtraction zero sub
rewrites "zero_subtraction.neg zero sub = neg"
proof unfold_locales
fix x and y
have "x ⊕ (⊖ (x ⊕ (⊖ y))) = x ⊕ ((⊖ x) ⊕ (⊖ (⊖ y)))"
(is "?l = _")
by (simp add: neg_add)
also have "… = ⊖ (⊖ y)"
using add_cancel .
also have "… = y" (is "_ = ?r")
using neg_neg .
finally show "?l = ?r" .
next
fix x
have "x ⊕ (⊖ 𝟬) = (⊖ (⊖ x)) ⊕ (⊖ 𝟬)" (is "?l = _")
by (simp add: neg_neg)
also have "… = ⊖ (⊖ x ⊕ 𝟬)"
by (simp add: neg_add)
also have "… = ⊖ (⊖ x)"
by (simp add: add_zero_2)
also have "… = x" (is "_ = ?r")
using neg_neg .
finally show "?l = ?r" .
next
show "(λx. 𝟬 ⊕ (⊖ x)) = (λx. ⊖ x)"
by (simp add: add_zero_1)
qed
end
Now let’s have an interpretation.
interpretation int:
negation_zero_addition ‹uminus :: int ⇒ int› ‹0› ‹(+)›
by unfold_locales simp_all
I would like to prove that integer negation applied to the integer 0 is
the integer 0 again, using neg_zero. However, that doesn’t work.
lemma "- (0 :: int) = 0"
using int.neg_zero
oops
The problem is that the goal refers to the negation operator of int,
while int.neg_zero refers to the negation operator that is derived
from zero and subtraction (where subtraction in turn is derived from
negation and addition). Both negation operators are equal, and I have
communicated this equality by means of rewrites, but Isabelle
apparently doesn’t make use of it.
How can I use facts like int.neg_zero in proofs of lemmas like the
above one?
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:08):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Wolfgang Jeltsch,
Given that there has not been an official answer for more than one day, at
least, I can offer a plausible practical solution. Nevertheless, please
keep in mind that I am not familiar with the implementation details of the
locale interpretation and the associated rewrite algorithms (if you still
insist on getting to the heart of the matter, it should possible to debug
the source code).
Using only the abbreviation ⊖ from negation_zero_addition, the suggested
rewrite rule is 'zero_subtraction.neg 𝟬 sub=neg', which stands for '(⊖)
𝟬=neg' (see print_abbrevs). The theorem neg_zero is '((⊖) 𝟬) 𝟬 = 𝟬'
after the interpretation inside the context of negation_zero_addition.
Trying to (for example) unfold '((⊖) 𝟬) 𝟬 = 𝟬' with '(⊖) 𝟬=neg' leaves
the theorem in the same state:
lemma subst1: "(⊖) 𝟬 ≡ neg" by (simp add: add_zero_1)
lemma subst2: "(⊖) 𝟬 x ≡ neg x" by (simp add: add_zero_1)
lemma thm1: "((⊖) 𝟬) 𝟬 ≡ 𝟬" sorry
lemma thm2: "f ((⊖) 𝟬) ≡ f ((⊖) 𝟬)" by simp
thm thm1[unfolded subst1] (unfold 'fails': ((⊖) 𝟬) 𝟬 ≡ 𝟬)
thm thm1[unfolded subst2] (unfold 'succeeds': ⊖ 𝟬 ≡ 𝟬)
thm thm2[unfolded subst1] (unfold 'succeeds': ?f neg ≡ ?f neg)
thm thm2[unfolded subst2] (unfold 'succeeds': ?f neg ≡ ?f neg)
I can only speculate as to whether the mechanism used for rewriting during
the locale interpretation is not entirely different from the technique used
in the example above. As you can also see from the code listing above, the
rewrite rule '(⊖) 𝟬 x ≡ neg x' achieves the desired effect. Using the
abbreviation zero_subtraction.neg, this rule becomes 'zero_subtraction.neg
𝟬 sub x= neg x'. However, it may be even safer to replace the abbreviation
zero_subtraction.neg with a predefined constant (see the code listing
below). In this case, 'zero_subtraction.neg 𝟬 sub= neg' is, most likely,
the best available option: I expect that with this rule all plausible
algorithms would agree on the intuitively desired solution unanimously.
It would be useful for me if someone who knows the details of the
implementation could confirm/correct/provide further explanation of any
aspects of what is stated above.
Thank you
locale negation =
fixes neg :: "'a ⇒ 'a" ("⊖ _" [81] 80)
assumes neg_neg: "⊖ (⊖ x) = x"
locale zero_subtraction =
fixes zero :: 'a ("𝟬")
fixes sub :: "['a, 'a] ⇒ 'a" (infixl "⊖" 65)
assumes sub_sub: "x ⊖ (x ⊖ y) = y"
assumes sub_zero_2: "x ⊖ 𝟬 = x"
begin
definition neg :: "'a ⇒ 'a" ("⊖ _" [81] 80) where
"⊖ x ≡ 𝟬 ⊖ x"
sublocale negation neg
proof
fix x
show "⊖ (⊖ x) = x" unfolding neg_def using sub_sub .
qed
lemma neg_zero:
shows "⊖ 𝟬 = 𝟬"
unfolding neg_def using sub_zero_2 .
end
locale negation_zero_addition =
negation neg for neg :: "'a ⇒ 'a" ("⊖ _" [81] 80) +
fixes zero :: 'a ("𝟬")
fixes add :: "['a, 'a] ⇒ 'a" (infixl "⊕" 65)
assumes add_zero_1: "𝟬 ⊕ x = x"
assumes add_zero_2: "x ⊕ 𝟬 = x"
assumes neg_add: "⊖ (x ⊕ y) = (⊖ x) ⊕ (⊖ y)"
assumes add_cancel: "x ⊕ ((⊖ x) ⊕ y) = y"
begin
abbreviation sub :: "['a, 'a] ⇒ 'a" (infixl "⊖" 65) where
"x ⊖ y ≡ x ⊕ (⊖ y)"
lemma zs: "zero_subtraction zero sub"
proof unfold_locales
fix x and y
have "x ⊕ (⊖ (x ⊕ (⊖ y))) = x ⊕ ((⊖ x) ⊕ (⊖ (⊖ y)))"
(is "?l = _")
by (simp add: neg_add)
also have "… = ⊖ (⊖ y)"
using add_cancel .
also have "… = y" (is "_ = ?r")
using neg_neg .
finally show "?l = ?r" .
next
fix x
have "x ⊕ (⊖ 𝟬) = (⊖ (⊖ x)) ⊕ (⊖ 𝟬)" (is "?l = _")
by (simp add: neg_neg)
also have "… = ⊖ (⊖ x ⊕ 𝟬)"
by (simp add: neg_add)
also have "… = ⊖ (⊖ x)"
by (simp add: add_zero_2)
also have "… = x" (is "_ = ?r")
using neg_neg .
finally show "?l = ?r" .
qed
sublocale zero_subtraction zero sub
rewrites "zero_subtraction.neg zero sub = neg"
apply(rule zs)
unfolding zero_subtraction.neg_def[OF zs]
by (simp add: add_zero_1)
thm neg_zero (* ⊖ 𝟬 = 𝟬 *)
end
interpretation int:
negation_zero_addition ‹uminus :: int ⇒ int› ‹0› ‹(+)›
by unfold_locales simp_all
thm int.neg_zero (* - 0 = 0 *)
Email Gateway (Aug 22 2022 at 20:08):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Wolfgang,
The problem is that you have abbreviations on the left-hand sides of your rewrites instead
of definitions. Abbreviations are just for pretty-printing; in the underlying term
representation, abbreviations are unfolded (and implicitly beta-reduced). If you change
the abbreviations into definitions, then the rewriting works as expected. Let's look into
what's happening:
The term sub in zero_subtraction expands to λx y. (+) x (uminus y).
So the rewrite rule "zero_subtraction.neg zero sub = neg" becomes in the interpretation
λx. int.sub 0 x = uminus
This has a lambda on the left, i.e., it is not a proper higher-order rewrite rule. It will
only kick in if there is a lambda abstraction in the term. However, in the theorem
neg_zero, the beta redex "(λx. int.sub 0 x) 0" has already been reduced so int.sub 0 0. So
the rewrite rule will not trigger. If you turn the abbreviations into definitions, there
will be no trouble with implicit beta-reductions and eta-expansions.
Alternatively, you can add the eta-expanded version of the rewrite rule:
sublocale zero_subtraction zero sub
rewrites "zero_subtraction.neg zero sub = neg"
and "zero_subtraction.neg zero sub x = neg x"
Then it works as expected.
Hope this helps
Andreas
Email Gateway (Aug 22 2022 at 20:08):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Thanks a lot for your explanation.
I cannot say that I fully understand what’s going on, but I think I have
at least some idea.
Apparently, the problem has more to do with rewriting in general than
with rewriting introduced by rewrites clauses. I understand that
defining (⊖) as an abbreviation via x ⊖ y ≡ x ⊕ ((⊖) y) doesn’t play
well with using a partial application of it in the rewrite rule (⊖) 𝟬
= neg. While (⊖) 𝟬 looks like an innocent partial application, it i
s in fact λy. 𝟬 ⊕ ((⊖) y), and thus the rewrite rule doesn’t match i
n places where (⊖) is fully applied, because full applications of
abbreviations don’t use λ.
When using definition instead of abbreviation, rewriting takes place
in all your above four examples. I think I’ll fix my issue by switching
from abbreviation to definition for (⊖).
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:08):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Thanks for this detailed explanation. It seems that the thoughts I just
sent as a response to mailing-list anonymous went in the right
direction. :smile:
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 20:09):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Wolfgang Jeltsch,
Thank you for your reply. Indeed, my initial intention was to write a
reply with the fully expanded abbreviations (initially, in writing the
reply I analysed the structure of the terms in ML and used
Conv.rewrs_conv instead of the attribute ‘unfolded'). However, I
thought that the structure of the terms would be apparent anyway,
because there was only one abbreviation left to expand.
Unfortunately, I have not studied, specifically, the HRS algorithms
(apparently) used for rewriting in lambda calculus/Isabelle.
Therefore, I did not wish to speculate any further as to why λy. 𝟬 ⊕
((⊖) y) is not suitable as the lhs of a rule. In any case, the answer
by Andreas Lochbihler provides a more complete explanation.
Thank you
Email Gateway (Aug 22 2022 at 20:09):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I apologise for posting the same message twice. The mistake is related
to making the first attempt to use a different email client that would
enable the modification of the email headers (related to my previous
post https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-July/msg00110.html).
I will make every attempt to ensure that this does not happen again.
Thank you
Last updated: Apr 25 2024 at 12:23 UTC