Email Gateway (Aug 23 2022 at 08:47): Email Gateway (Aug 23 2022 at 08:47):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Mikhail,
Nonetheless, I am not certain whether/how it resolves the most fundamental
issue. Many constants require some form of the totality of the relation as
a prerequisite for the possibility of a transfer rule to be established,
e.g. 'All/Ex'. At the moment, I use a combination of custom/ad-hoc methods
to avoid having to deal with the transfer of such constants (e.g. by
converting the statements of the theorems to the form that uses Ball/Bex,
while partially relying on tailor-made automation to achieve this).
However, I wonder whether there exists a more native solution (after all,
the premises should always carry sufficient information for the transfer to
succeed).All/Ex and friends are a thorny issue when it comes to transfer. Essentially, transfer
looks at the syntactic structure of the term, decomposes it into atoms and tries to prove
the transferring rule by composing the transfer rules for each following the rules for the
connectives of the terms (application and abstractions). In particular, properties
emerging from the interplay of different constants in the term are not taken into account.
The following example illustrates this issue. The following three statements are logically
equivalent:
(1) Ball A P
(2) !x. x : A --> P x
(3) !!x. x : A ==> P x
For transfer, (1) is the most suitable one because the interplay of quantification,
membership and implication is captured in one constant Ball. This interplay is captured in
Ball's transfer rule, which does not make any assumptions on the relation on the elements.
However, we often write statements of form (3) because they play well with Pure's natural
deduction, and terms of form (2) are generated by various packages and methods (e.g.,
atomize -- and transfer also rewrites (3) into (2) as a preparatory step).
So, if you state your example lemma as follows, everything should work without the need
for bi-totality.
lemma [rule_format]:
includes lifting_syntax
assumes [transfer_rule]: "monoid_eq' C F G"
shows "!a ∈ carrier G. !b ∈ carrier G. a ⊗⇘F⇙ b = a ⊗⇘G⇙ b"
Some preprocessing can get you a long way in this direction. Unfortunately, I haven't
found a one-size-fits-all solution for these problems (and I don't believe that such a
thing exists in general). Given Isabelle's interactive nature, a promising approach is to
identify recurring patterns and then automate these patterns accordingly.
As a side remark, I tried to explain the issue that is described in the
previous paragraph of this email in the last two paragraphs of my previous
email. However, having re-read them, I realized that I missed the point
almost completely: please ignore the last two paragraphs of my previous
email. Nonetheless, the example before the last paragraph is still relevant:lemma carrier_transfer[transfer_rule]:
includes lifting_syntax
shows "(monoid_eq' C ===> rel_set (eq_onp C)) carrier carrier"
unfolding monoid_eq'_def monoid_eq_def eq_onp_def rel_set_def
using monoid_eq.intro monoid_eq.monoid_eq_carrier
by blastlemma [transfer_rule]:
includes lifting_syntax
shows "(eq_onp C ===> eq_onp C ===> (=)) (=) (=)"
unfolding eq_onp_def by auto
Instead of this rule, you want to tell transfer that eq_onp relations are bi-unique. The
rule is missing from the library, but it's in one of my AFP entries:
lemma [transfer_rule]:
includes lifting_syntax
shows "(eq_onp C ===> rel_set (eq_onp C) ===> (=)) (∈) (∈)"
unfolding eq_onp_def rel_set_def by auto
This should also be solved by declaring bi_unique_eq_onp as [transfer_rule].
lemma
includes lifting_syntax
assumes [transfer_rule]: "monoid_eq' C F G"
shows "a ∈ carrier G ⟹ b ∈ carrier G ⟹ a ⊗⇘G⇙ b = a ⊗⇘G⇙ b"
apply transfer
(Transfer.Rel ((eq_onp C ===> (=)) ===> (=)) ?aa25 transfer_forall)
oopsLastly, please accept my apologies for asking so many questions on this
topic lately. The reason for this is that I am trying to be careful to
ensure that the framework for transfer is designed in a more-or-less
canonical manner, as I believe that it has a potential for being
generalized to arbitrary partial equivalence relations on set-based
structures defined using records (or similar). Naturally, I will share it
under the terms of a BSD license when/if it will reach a certain state of
generality and maturity.
No need to apologize. I'm happy to chat about these things.
Best,
Andreas
Email Gateway (Aug 23 2022 at 08:48):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Andreas Lochbihler/All,
Thank you for your reply. I will allow myself to provide several concluding
remarks in an attempt to close this issue.
Nonetheless, I am not certain whether/how it resolves the most fundamental
issue. Many constants require some form of the totality of the relation as
a prerequisite for the possibility of a transfer rule to be established,
e.g. 'All/Ex'. At the moment, I use a combination of custom/ad-hoc methods
to avoid having to deal with the transfer of such constants (e.g. by
converting the statements of the theorems to the form that uses Ball/Bex,
while partially relying on tailor-made automation to achieve this).
However, I wonder whether there exists a more native solution (after all,
the premises should always carry sufficient information for the transfer to
succeed).
All/Ex and friends are a thorny issue when it comes to transfer.
Essentially, transfer
looks at the syntactic structure of the term, decomposes it into atoms and
tries to prove
the transferring rule by composing the transfer rules for each following
the rules for the
connectives of the terms (application and abstractions). In particular,
properties
emerging from the interplay of different constants in the term are not
taken into account.
...
So, if you state your example lemma as follows, everything should work
without the need
for bi-totality.
lemma [rule_format]:
includes lifting_syntax
assumes [transfer_rule]: "monoid_eq' C F G"
shows "!a ∈ carrier G. !b ∈ carrier G. a ⊗⇘F⇙ b = a ⊗⇘G⇙ b"
Thank you for the detailed explanation. Nevertheless, I have to mention
that I am, to a certain degree, familiar with the algorithm that is used by
the Isabelle's transfer tool. Therefore, of course, instead of "for the
transfer to succeed" I should have written "for a transfer-like algorithm
to succeed". In any case, I believe that this was the intended meaning of
the last sentence of the first quoted paragraph above. Also, in the same
paragraph, I mentioned that I was already able to partially automate the
process of the conversion of the goals of the form "!!a b. a ∈ carrier G ⟹
b ∈ carrier G ⟹ a ⊗⇘G⇙ b = a ⊗⇘G⇙ b" to the form "!a ∈ carrier G. !b ∈
carrier G. a ⊗⇘F⇙ b = a ⊗⇘G⇙ b" at the time of writing. However, such
automation only works in very simple cases (by now, I have already
encountered a use case where my methodology fails). Nonetheless, based on
what I have experimented with, it felt like it should be possible to devise
a transfer-like algorithm that would work almost always even if the
totality cannot be guaranteed (i.e. the transfer needs to be established
between two subsets).
Some preprocessing can get you a long way in this direction.
Unfortunately, I haven't
found a one-size-fits-all solution for these problems (and I don't believe
that such a
thing exists in general). Given Isabelle's interactive nature, a promising
approach is to
identify recurring patterns and then automate these patterns accordingly.
I am slightly disappointed. However, at least, that what you have stated
gives me confidence that the problem that I have encountered is far from
being trivial and, currently, there is no canonical solution that would
make it possible to fully automate the transfer of results between two
arbitrary subsets. Nonetheless, it feels like this limitation is a dramatic
gap in the capabilities of the transfer tool (of course, I am aware that
this use case has never been advertised as one of the target applications
of the tool).
Instead of this rule, you want to tell transfer that eq_onp relations are
bi-unique. The
rule is missing from the library, but it's in one of my AFP entries:Undeniably, I can be slightly reckless when writing code for forums/mailing
lists: most certainly, this was not a copy of my working version of the
code :). Thank you for pointing out this flaw.
Having tried every solution that was mentioned in this thread, I decided to
use an explicit relation in favor of the solutions based on undefined.
Nonetheless, I decided not to rely on transfer. Without an algorithm that
is capable of handling the "interplay of quantification, membership and
implication" in a completely automated manner, unfortunately, in my view
(and taking into account my reasonably contrived use cases), it seems to be
more natural to continue without transfer than having to rely on "patchy"
solutions. Quite frankly, I found that a combination of locale
interpretation + additional rules for the classical reasoners + specialized
simpset in the form of a collection of named_theorems works reasonably well
in practice. While, from time to time, I have to use additional Isar code
to handle the equality, most proofs of the related steps look like this:
"(auto simp: eq_simps)", where eq_simps contains theorems of the form "x ∈
carrier F ⟹ y ∈ carrier F ⟹ x ⊗⇘G⇙ y = x ⊗⇘F⇙ y". Naturally, I also
maintain an additional set of introduction rules for the classical
reasoner.
Having said this, it would be very interesting to understand whether it
could be possible to develop a general transfer-like algorithm that could
work without the requirement of the totality of the involved relations,
inferring the information about the membership directly from the
premises/assumptions (perhaps, augmented with some additional
infrastructure). I believe that this could be useful in practice not only
for my particular use case (i.e. equality) but also in many other similar
cases (e.g. consider the problem of the transfer of the results across an
arbitrary isomorphism between two set-based structures).
Kind Regards,
Mikhail Chekhov
On Wed, Apr 22, 2020 at 8:24 AM Andreas Lochbihler <
mail@andreas-lochbihler.de> wrote:
Dear Mikhail,
Nonetheless, I am not certain whether/how it resolves the most
fundamental
issue. Many constants require some form of the totality of the relation
as
a prerequisite for the possibility of a transfer rule to be established,
e.g. 'All/Ex'. At the moment, I use a combination of custom/ad-hoc
methods
to avoid having to deal with the transfer of such constants (e.g. by
converting the statements of the theorems to the form that uses Ball/Bex,
while partially relying on tailor-made automation to achieve this).
However, I wonder whether there exists a more native solution (after all,
the premises should always carry sufficient information for the transfer
to
succeed).All/Ex and friends are a thorny issue when it comes to transfer.
Essentially, transfer
looks at the syntactic structure of the term, decomposes it into atoms and
tries to prove
the transferring rule by composing the transfer rules for each following
the rules for the
connectives of the terms (application and abstractions). In particular,
properties
emerging from the interplay of different constants in the term are not
taken into account.The following example illustrates this issue. The following three
statements are logically
equivalent:(1) Ball A P
(2) !x. x : A --> P x
(3) !!x. x : A ==> P xFor transfer, (1) is the most suitable one because the interplay of
quantification,
membership and implication is captured in one constant Ball. This
interplay is captured in
Ball's transfer rule, which does not make any assumptions on the relation
on the elements.However, we often write statements of form (3) because they play well with
Pure's natural
deduction, and terms of form (2) are generated by various packages and
methods (e.g.,
atomize -- and transfer also rewrites (3) into (2) as a preparatory step).So, if you state your example lemma as follows, everything should work
without the need
for bi-totality.lemma [rule_format]:
includes lifting_syntax
assumes [transfer_rule]: "monoid_eq' C F G"
shows "!a ∈ carrier G. !b ∈ carrier G. a ⊗⇘F⇙ b = a ⊗⇘G⇙ b"Some preprocessing can get you a long way in this direction.
Unfortunately, I haven't
found a one-size-fits-all solution for these problems (and I don't believe
that such a
thing exists in general). Given Isabelle's interactive nature, a promising
approach is to
identify recurring patterns and then automate these patterns accordingly.As a side remark, I tried to explain the issue that is described in the
previous paragraph of this email in the last two paragraphs of my
previous
email. However, having re-read them, I realized that I missed the point
almost completely: please ignore the last two paragraphs of my previous
email. Nonetheless, the example before the last paragraph is still
relevant:lemma carrier_transfer[transfer_rule]:
includes lifting_syntax
shows "(monoid_eq' C ===> rel_set (eq_onp C)) carrier carrier"
unfolding monoid_eq'_def monoid_eq_def eq_onp_def rel_set_def
using monoid_eq.intro monoid_eq.monoid_eq_carrier
by blastlemma [transfer_rule]:
includes lifting_syntax
shows "(eq_onp C ===> eq_onp C ===> (=)) (=) (=)"
unfolding eq_onp_def by auto
Instead of this rule, you want to tell transfer that eq_onp relations are
bi-unique. The
rule is missing from the library, but it's in one of my AFP entries:lemma [transfer_rule]:
includes lifting_syntax
shows "(eq_onp C ===> rel_set (eq_onp C) ===> (=)) (∈) (∈)"
unfolding eq_onp_def rel_set_def by autoThis should also be solved by declaring bi_unique_eq_onp as
[transfer_rule].lemma
includes lifting_syntax
assumes [transfer_rule]: "monoid_eq' C F G"[message truncated]
Email Gateway (Aug 23 2022 at 08:57):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Mikhail,
I'm not surprised that option 2 creates a lot of effort because you change the locale
specification. With option 1, you essentially get congruence rules of the form
monoid_eq F G ==> x : carrier G ==> monoid.foo F x = monoid.foo G x
for all derived concepts that are defined in monoid. Reasoning with such congruence rules
can become cumbersome because the simplifier is not really able to reason with them
natively. Moreover, you need a separate interpretation of monoid_eq for every pair of
monoids you consider. If there are many, the number of interpretations grow quadratically
in the worst case.
Defining the partial quotient as a type is not really feasible because type definitions
must not depend on values in Isabelle/HOL, so you'd have to do the construction for every
fixed monoid separately.
There are two further options that I want to mention. First, you can define a
normalization function normalize :: 'a monoid => 'a => 'a via
normalize F x = (if x : carrier F then x else undefined)
and then lift it to a normalization function on monoid:
normalize_monoid :: 'a monoid => 'a monoid
that restricts the monoid operation to the carrier and sets it to undefined everywhere
else. You can then prove
monoid F ==> normalize_monoid F
and for all operations monoid.foo defined on monoids equations such as the following:
"x : carrier F ==> monoid.foo F x = monoid.foo (normalize_monoid F) x"
If you equip these equations with an assumption
"NO_MATCH (normalize_monoid G) F"
then you can even use them as simp rules without looping.
So whenever you need to exploit the equality of monoids, you can add those equations to
the simpset and switch all involved monoids F to "normalize_monoid F". And for these
normalized monoids, you actually get the equality "normalize_monoid F = normalize_monoid G".
A few caveats of this approach:
This only pays of if you have equalities between many monoids. If there are just two or
three, it's probably not worth the effort.
Going from F to normalize_monoid F works well for declarative proofs where you
explicitly state the equality and then have simp transfer both sides. It does not work
well with exploratory proof styles where you interactively develop the proof like with an
apply script.
The rewriting to normalize_monoid is limited to what simp can do. For example,
replacements under higher-order operators like fold will not work in general because simp
cannot solve the side conditions _ : carrier _, even if you supply congruence rules.
The second approach is to use transfer. You can use your monoid_eq as a the relator for
monoids and then prove appropriate transfer rules for all the operations on monoids. You
should then be able to move from one monoid to the other by declaring the suitable
monoid_eq fact as [transfer_rule] and let transfer do the rest. That's probably what I
would go for.
Best,
Andreas
Email Gateway (Aug 23 2022 at 08:58):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Andreas Lochbihler/All,
Thank you for your reply. It contains very useful advice. However, I will
allow myself to provide several comments and make an attempt to clarify one
part of your answer that I may not have understood.
Defining the partial quotient as a type is not really feasible because type
definitions
must not depend on values in Isabelle/HOL, so you'd have to do the
construction for every
fixed monoid separately.
Of course, you are right, but I omitted an important detail from my
question: I specialize all structures to one particular type. Therefore, I
was able to define a partial quotient type. Nonetheless, such an approach
results in a substantial amount of duplication (moreover, there are other,
more fundamental, complications) and I do not consider it to be the most
practical solution.
...
Reasoning with such congruence rules
can become cumbersome because the simplifier is not really able to reason
with them
natively. Moreover, you need a separate interpretation of monoid_eq for
every pair of
monoids you consider. If there are many, the number of interpretations
grow quadratically
in the worst case.
...
The second approach is to use transfer. You can use your monoid_eq as a
the relator for
monoids and then prove appropriate transfer rules for all the operations
on monoids. You
should then be able to move from one monoid to the other by declaring the
suitable
monoid_eq fact as [transfer_rule] and let transfer do the rest. That's
probably what I
would go for.
If I understood what is stated in your answer correctly, the second
solution that you suggested is not entirely different from the first
approach that I proposed in my question. Naturally, I never suggested that
one should rely on the simplifier/congruence rules exclusively. Indeed, I
rely predominantly on the capabilities of the transfer package to transfer
the results across the members of a given equivalence class (however, I
only mentioned it in passing in the last paragraph of the question and your
answer gave me additional ideas for improvement of my own framework for
transfer). Nonetheless, given what you have stated, I am still not certain
if I am using transfer in the best possible manner. For example, consider
the following framework,
locale monoid_eq = monoid G + monoid F for G F +
assumes monoid_eq_carrier: "carrier G = carrier F"
and monoid_eq_mult:
"x ∈ carrier G ⟹ y ∈ carrier G ⟹ x ⊗⇘G⇙ y = x ⊗⇘F⇙ y"
and monoid_eq_one: "𝟭⇘G⇙ = 𝟭⇘F⇙"
definition monoid_eq_rel ::
"('a, 'b) monoid_scheme ⇒ ('a, 'c) monoid_scheme ⇒ 'a ⇒ 'a ⇒ bool"
where (*redundancy for symmetry :) *) "monoid_eq_rel F G a b =
(a = b ∧ a ∈ carrier F ∧ b ∈ carrier G ∧ monoid_eq F G)"
lemma eq_transfer[transfer_rule]:
includes lifting_syntax
shows "(monoid_eq_rel F G ===> monoid_eq_rel F G ===> (=)) (=) (=)"
unfolding monoid_eq_rel_def
by (intro rel_funI) auto
lemma carrier_transfer[transfer_rule]:
includes lifting_syntax
shows "(monoid_eq ===> (=)) carrier carrier"
unfolding monoid_eq_def
using monoid_eq.intro monoid_eq.monoid_eq_carrier
by blast
lemma mult_transfer[transfer_rule]:
includes lifting_syntax
shows "(monoid_eq_rel F G ===> monoid_eq_rel F G ===> (=)) (mult F) (mult
G)"
proof(intro rel_funI)
fix x y x' y'
assume prems: "monoid_eq_rel F G x y" "monoid_eq_rel F G x' y'"
then have myrel:
"x = y" "x' = y'"
"x ∈ carrier F" "y ∈ carrier G"
"x' ∈ carrier F" "y' ∈ carrier G"
"monoid_eq F G"
unfolding monoid_eq_rel_def by auto
interpret monoid_eq F G by (rule ‹monoid_eq F G›)
show "x ⊗⇘F⇙ x' = y ⊗⇘G⇙ y'" using myrel by (simp add: monoid_eq_mult)
qed
lemma Ball_transfer[transfer_rule]:
includes lifting_syntax
assumes "monoid_eq F G"
shows "((monoid_eq_rel F G ===> (=)) ===> (=))
(Ball (carrier F)) (Ball (carrier G))"
unfolding Ball_def
apply(intro rel_funI, unfold rel_fun_def)
using assms by (metis monoid_eq.monoid_eq_carrier monoid_eq_rel_def)
Now, as you suggested, many results can be conveniently transferred, e.g.
lemma
includes lifting_syntax
assumes [transfer_rule]: "monoid_eq F G"
shows "∀a∈carrier G. ∀b∈carrier G. a ⊗⇘G⇙ b = a ⊗⇘G⇙ b"
apply transfer
(∀a∈carrier F. ∀b∈carrier F. a ⊗⇘F⇙ b = a ⊗⇘F⇙ b)
by simp
However, I am not certain if this exactly what you had in mind when you
wrote your answer. Perhaps, the framework described above be improved
further in some way? I guess, it would make sense to generalize it to
arbitrary partial equivalences. Also, how would one deal with the transfer
of Pure connectives? For example,
lemma
includes lifting_syntax
assumes [transfer_rule]: "monoid_eq F G"
shows "a ∈ carrier G ⟹ b ∈ carrier G ⟹ a ⊗⇘G⇙ b = a ⊗⇘G⇙ b"
apply transfer
(((monoid_eq_rel ?F24 G ===> (=)) ===> (=)) ?aa23 transfer_forall)
by simp
I guess, this problem is also not specific to equality, but any partial
equivalence relation (or, even more generally, any relation between two
arbitrary subsets). I can see that one could automate atomization and
introduction of Pure connectives before and after performing
transfer, respectively. Nonetheless, I am curious whether there exists a
more native solution.
Kind Regards,
Mikhail Chekhov
On Sat, Apr 18, 2020 at 12:18 PM Andreas Lochbihler <
mail@andreas-lochbihler.de> wrote:
Dear Mikhail,
I'm not surprised that option 2 creates a lot of effort because you change
the locale
specification. With option 1, you essentially get congruence rules of the
formmonoid_eq F G ==> x : carrier G ==> monoid.foo F x = monoid.foo G x
for all derived concepts that are defined in monoid. Reasoning with such
congruence rules
can become cumbersome because the simplifier is not really able to reason
with them
natively. Moreover, you need a separate interpretation of monoid_eq for
every pair of
monoids you consider. If there are many, the number of interpretations
grow quadratically
in the worst case.Defining the partial quotient as a type is not really feasible because
type definitions
must not depend on values in Isabelle/HOL, so you'd have to do the
construction for every
fixed monoid separately.There are two further options that I want to mention. First, you can
define a
normalization function normalize :: 'a monoid => 'a => 'a vianormalize F x = (if x : carrier F then x else undefined)
and then lift it to a normalization function on monoid:
normalize_monoid :: 'a monoid => 'a monoid
that restricts the monoid operation to the carrier and sets it to
undefined everywhere
else. You can then provemonoid F ==> normalize_monoid F
and for all operations monoid.foo defined on monoids equations such as the
following:"x : carrier F ==> monoid.foo F x = monoid.foo (normalize_monoid F) x"
If you equip these equations with an assumption
"NO_MATCH (normalize_monoid G) F"
then you can even use them as simp rules without looping.So whenever you need to exploit the equality of monoids, you can add those
equations to
the simpset and switch all involved monoids F to "normalize_monoid F". And
for these
normalized monoids, you actually get the equality "normalize_monoid F =
normalize_monoid G".A few caveats of this approach:
This only pays of if you have equalities between many monoids. If there
are just two or
three, it's probably not worth the effort.Going from F to normalize_monoid F works well for declarative proofs
where you
explicitly state the equality and then have simp transfer both sides. It
does not work
well with exploratory proof styles where you interactively develop the
proof like with an
apply script.The rewriting to normalize_monoid is limited to what simp can do. For
example,
replacements under higher-order operators like fold will not work in
general because simp
cannot solve the side conditions _ : carrier _, even if you supply
congruence rules.The second approach is to use transfer. You can use your monoid_eq as a
the relator for
monoids and then prove appropriate transfer rules for all the operations
on monoids. You
should then be able to move from one monoid to the other by declaring the
suitable
monoid_eq fact as [transfer_rule] and let transfer do the rest. That's
probably what I
would go for.Best,
AndreasOn 17/04/2020 15:09, Mikhail Chekhov wrote:
Dear All,
I have a technical question for those who are well versed in
the formalizaton of applied mathematics in Isabelle/HOL using set-based
reasoning in HOL-Algebra (or similar).I am curious as to what is the canonical approach for dealing with the
equality of algebraic structures (e.g. monoids). Suppose, a given monoid
undergoes a sequence of transformations, the result of these
transformations being an identical monoid (isomorphisms are not good
enough).I am aware of two different solutions, but I am not certain whether there
exist (better) alternatives and which solution would be preferred/more
canonical?
- (Partial) equivalence relation. For example,
locale monoid_eq = monoid G + monoid F for G F +
assumes "carrier G = carrier F"
and "x ∈ carrier G ⟹ y ∈ carrier G ⟹ x ⊗⇘G⇙ y = x ⊗⇘F⇙ y"
and "𝟭⇘G⇙ = 𝟭⇘F⇙"It should also be possible to define a partial quotient type based on
monoid_eq. However, I can imagine that this could result in a substantial
amount of boilerplate code (one would wish to transfer the entire
HOL-Algebra to the new type(s)).
- Augmentation of the monoid locale with an additional condition that
mimics the restriction of the domain of the operation ⊗ to the carrier
set
via undefined. Once this is done, one can use the standard HOL's
eq
[message truncated]
Email Gateway (Aug 23 2022 at 08:58):From: Clemens Ballarin <ballarin@in.tum.de>
If you go for the "undefined" approach, you indeed need to do it
systematically.
In my recent case study [1], for the required quotient constructions, I
only needed to explicitly talk about undefinedness in definitions, not
specifications. With suitable lemmas on undefinedness I found that the
simplifier's splitter was able to deal with the arising proof
obligations mostly automatically. I only needed a few of these lemmas,
and you can find them by searching for "undefined" in the associated
theory files [2]. The study contains a brief discussion on the topic in
section 5.2.
Clemens
[1] http://dx.doi.org/10.1007/s10817-019-09537-9 (unofficial version at
http://www21.in.tum.de/~ballarin/publications/jar2019.pdf)
[2]
https://www.isa-afp.org/browser_info/current/AFP/Jacobson_Basic_Algebra/index.html
Email Gateway (Aug 23 2022 at 08:58):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Mikhail,
If I understood what is stated in your answer correctly, the second solution that you
suggested is not entirely different from the first approach that I proposed in my
question. Naturally, I never suggested that one should rely on the simplifier/congruence
rules exclusively. Indeed, I rely predominantly on the capabilities of the transfer
package to transfer the results across the members of a given equivalence class (however,
I only mentioned it in passing in the last paragraph of the question and your answer gave
me additional ideas for improvement of my own framework for transfer).
Oh sorry, I missed that your mentioning of transfer referred to the transfer method.
Nonetheless, given
what you have stated, I am still not certain if I am using transfer in the best possible
manner. For example, consider the following framework,locale monoid_eq = monoid G + monoid F for G F +
assumes monoid_eq_carrier: "carrier G = carrier F"
and monoid_eq_mult:
"x ∈ carrier G ⟹ y ∈ carrier G ⟹ x ⊗⇘G⇙ y = x ⊗⇘F⇙ y"
and monoid_eq_one: "𝟭⇘G⇙ = 𝟭⇘F⇙"definition monoid_eq_rel ::
"('a, 'b) monoid_scheme ⇒ ('a, 'c) monoid_scheme ⇒ 'a ⇒ 'a ⇒ bool"
where (*redundancy for symmetry :) *) "monoid_eq_rel F G a b =
(a = b ∧ a ∈ carrier F ∧ b ∈ carrier G ∧ monoid_eq F G)"lemma eq_transfer[transfer_rule]:
includes lifting_syntax
shows "(monoid_eq_rel F G ===> monoid_eq_rel F G ===> (=)) (=) (=)"
unfolding monoid_eq_rel_def
by (intro rel_funI) autolemma carrier_transfer[transfer_rule]:
includes lifting_syntax
shows "(monoid_eq ===> (=)) carrier carrier"
unfolding monoid_eq_def
using monoid_eq.intro monoid_eq.monoid_eq_carrier
by blastlemma mult_transfer[transfer_rule]:
includes lifting_syntax
shows "(monoid_eq_rel F G ===> monoid_eq_rel F G ===> (=)) (mult F) (mult G)"
Here you run into the problem that we don't have a dependent function relator (or more
precisely, transfer does not support such a relator). So we cannot state this as a
transfer rule of the form
"(monoid_eq ===> eq_onp C ===> eq_onp C ===> eq_onp C) mult mult"
Fortunately, we only care here about whether elements are contained in a carrier. So how
about defining a relator monoid_eq' by
monoid_eq' C F G = monoid_eq F G & (C = %x. x : carrier G)
Now the carrier predicate C is explicit and we can refer to it in the rules:
"(monoid_eq' C ===> eq_onp C ===> eq_onp C ===> eq_onp C) mult mult"
This has the advantage that we relate only atomic terms, which work better with transfer
than composite terms like "mult F" and "mult G" as in your rule. You should not need
monoid_rel_eq then either and it should work well with the standard transfer rules for
library constants.
Best,
Andreas
Email Gateway (Aug 23 2022 at 08:58):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Andreas Lochbihler/All,
Once again, thank you for your reply.
Oh sorry, I missed that your mentioning of transfer referred to the
transfer method.Most certainly, there is no need to apologize: I was the one who failed to
pose the question in a comprehensive manner :).
Fortunately, we only care here about whether elements are contained in a
carrier. So how
about defining a relator monoid_eq' by
monoid_eq' C F G = monoid_eq F G & (C = %x. x : carrier G)
Now the carrier predicate C is explicit and we can refer to it in the
rules:
"(monoid_eq' C ===> eq_onp C ===> eq_onp C ===> eq_onp C) mult mult"Thank you for your advice. Indeed, this is exactly what I was looking for.
Unfortunately, I was unaware of this method and somehow I did not think of
it when I started working on the framework for transfer.
Nonetheless, I am not certain whether/how it resolves the most fundamental
issue. Many constants require some form of the totality of the relation as
a prerequisite for the possibility of a transfer rule to be established,
e.g. 'All/Ex'. At the moment, I use a combination of custom/ad-hoc methods
to avoid having to deal with the transfer of such constants (e.g. by
converting the statements of the theorems to the form that uses Ball/Bex,
while partially relying on tailor-made automation to achieve this).
However, I wonder whether there exists a more native solution (after all,
the premises should always carry sufficient information for the transfer to
succeed).
As a side remark, I tried to explain the issue that is described in the
previous paragraph of this email in the last two paragraphs of my previous
email. However, having re-read them, I realized that I missed the point
almost completely: please ignore the last two paragraphs of my previous
email. Nonetheless, the example before the last paragraph is still relevant:
lemma carrier_transfer[transfer_rule]:
includes lifting_syntax
shows "(monoid_eq' C ===> rel_set (eq_onp C)) carrier carrier"
unfolding monoid_eq'_def monoid_eq_def eq_onp_def rel_set_def
using monoid_eq.intro monoid_eq.monoid_eq_carrier
by blast
lemma [transfer_rule]:
includes lifting_syntax
shows "(eq_onp C ===> eq_onp C ===> (=)) (=) (=)"
unfolding eq_onp_def by auto
lemma [transfer_rule]:
includes lifting_syntax
shows "(eq_onp C ===> rel_set (eq_onp C) ===> (=)) (∈) (∈)"
unfolding eq_onp_def rel_set_def by auto
lemma
includes lifting_syntax
assumes [transfer_rule]: "monoid_eq' C F G"
shows "a ∈ carrier G ⟹ b ∈ carrier G ⟹ a ⊗⇘G⇙ b = a ⊗⇘G⇙ b"
apply transfer
(Transfer.Rel ((eq_onp C ===> (=)) ===> (=)) ?aa25 transfer_forall)
oops
Lastly, please accept my apologies for asking so many questions on this
topic lately. The reason for this is that I am trying to be careful to
ensure that the framework for transfer is designed in a more-or-less
canonical manner, as I believe that it has a potential for being
generalized to arbitrary partial equivalence relations on set-based
structures defined using records (or similar). Naturally, I will share it
under the terms of a BSD license when/if it will reach a certain state of
generality and maturity.
Kind Regards,
Mikhail Chekhov
On Sun, Apr 19, 2020 at 7:10 PM Andreas Lochbihler <
mail@andreas-lochbihler.de> wrote:
Dear Mikhail,
If I understood what is stated in your answer correctly, the second
solution that you
suggested is not entirely different from the first approach that I
proposed in my
question. Naturally, I never suggested that one should rely on the
simplifier/congruence
rules exclusively. Indeed, I rely predominantly on the capabilities of
the transfer
package to transfer the results across the members of a given
equivalence class (however,
I only mentioned it in passing in the last paragraph of the question and
your answer gave
me additional ideas for improvement of my own framework for transfer).
Oh sorry, I missed that your mentioning of transfer referred to the
transfer method.Nonetheless, given
what you have stated, I am still not certain if I am using transfer in
the best possible
manner. For example, consider the following framework,locale monoid_eq = monoid G + monoid F for G F +
assumes monoid_eq_carrier: "carrier G = carrier F"
and monoid_eq_mult:
"x ∈ carrier G ⟹ y ∈ carrier G ⟹ x ⊗⇘G⇙ y = x ⊗⇘F⇙ y"
and monoid_eq_one: "𝟭⇘G⇙ = 𝟭⇘F⇙"definition monoid_eq_rel ::
"('a, 'b) monoid_scheme ⇒ ('a, 'c) monoid_scheme ⇒ 'a ⇒ 'a ⇒ bool"
where (*redundancy for symmetry :) *) "monoid_eq_rel F G a b =
(a = b ∧ a ∈ carrier F ∧ b ∈ carrier G ∧ monoid_eq F G)"lemma eq_transfer[transfer_rule]:
includes lifting_syntax
shows "(monoid_eq_rel F G ===> monoid_eq_rel F G ===> (=)) (=) (=)"
unfolding monoid_eq_rel_def
by (intro rel_funI) autolemma carrier_transfer[transfer_rule]:
includes lifting_syntax
shows "(monoid_eq ===> (=)) carrier carrier"
unfolding monoid_eq_def
using monoid_eq.intro monoid_eq.monoid_eq_carrier
by blastlemma mult_transfer[transfer_rule]:
includes lifting_syntax
shows "(monoid_eq_rel F G ===> monoid_eq_rel F G ===> (=)) (mult F)
(mult G)"Here you run into the problem that we don't have a dependent function
relator (or more
precisely, transfer does not support such a relator). So we cannot state
this as a
transfer rule of the form"(monoid_eq ===> eq_onp C ===> eq_onp C ===> eq_onp C) mult mult"
Fortunately, we only care here about whether elements are contained in a
carrier. So how
about defining a relator monoid_eq' bymonoid_eq' C F G = monoid_eq F G & (C = %x. x : carrier G)
Now the carrier predicate C is explicit and we can refer to it in the
rules:"(monoid_eq' C ===> eq_onp C ===> eq_onp C ===> eq_onp C) mult mult"
This has the advantage that we relate only atomic terms, which work better
with transfer
than composite terms like "mult F" and "mult G" as in your rule. You
should not need
monoid_rel_eq then either and it should work well with the standard
transfer rules for
library constants.Best,
Andreas
Email Gateway (Aug 23 2022 at 08:58):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Clemens Ballarin/All,
Thank you for providing the references. Indeed, your work does provide an
answer to one of my own old questions on the mailing list, i.e.
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-August/msg00006.html
.
I can hardly claim that my own use of proof automation in conjunction with
'undefined' could not be improved. Nonetheless, there are other reasons why
I am still inclined to prefer the use of an explicit equivalence relation
in conjunction with transfer for my application.
Kind Regards,
Mikhail Chekhov
Last updated: Apr 25 2024 at 04:18 UTC