Email Gateway (Dec 27 2020 at 15:58): Email Gateway (Dec 27 2020 at 15:58):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear All,
I have several questions about the availability of certain types of proof
methods for Isabelle (I guess, these questions can also be seen as
reference requests).
I am working on a certain applied formalization study. This work is carried
out in the object logic ZFC in HOL. The type of reasoning that it requires
is very similar to the type of reasoning that is used in HOL-Algebra. When
I started my work on this project, I relied, primarily, on the tools that
combine classical reasoning with simplification, such as auto. However, I
found myself struggling more and more in my attempts to provide appropriate
sets of simp/intro/dest/elim rules that would not cause significant delays
and loops when solving typical set-based goals. Besides, my proof code
seemed to be unnecessarily verbose. However, please do not view this as a
criticism of the aforementioned proof tools: I can hardly claim to have an
extensive knowledge of the analytical properties of the involved algorithms.
Problem 1
From the manual of the simplifier: "conditions in conditional rewrite rules
are solved recursively before the rewrite rule is applied". Empirically, I
have established that it could be useful to be able to treat rewriting in
the same manner as intro-resolution, allowing the side conditions of the
rewrite rules to be resolved both using rewriting or intro-resolution after
the application of the rewrite rule to a given goal (of course, this is
also meant to be done recursively). I devised a prototype method based on
this algorithm (CS in
https://gitlab.com/user9716869/Isabelle-Complement-Library). For my own
needs, practically, I found this type of 'coupling' of rewriting and
intro-resolution to be exceptionally capable at solving complex goals in
comparison with some of the existing tools that seem to combine
simplification and classical reasoning that I tried before (by now, for my
own needs, I rely on the methods provided by CS almost exclusively in a
reasonably sizeable development).
Unfortunately, my formal background in the area of the algorithms that are
used in the common proof tools is, somewhat, limited (I have always been
far more interested in the applications of the proof assistants to the
development of formally verified software and applied formalization of
mathematics, rather than the technology behind them). Thus, I have little
doubt that I have reinvented the wheel. My primary question is whether any
of the existing proof tools already provide access to the algorithm that I
have described.
Problem 2
I would like to know if there exist any reasonably generic proof tools for
Isabelle that would take into account associativity implicitly. Somehow,
when performing rewriting, I would like to be able to treat ((ab)c)d,
(ab)(cd), ... as members of the same equivalence class with respect to the
relation induced by the associativity. Therefore, if there is an additional
rewrite rule b(cd)=e (again, treated with respect to the same equivalence
relation), it would be immediately applicable to any form of abcd,
immediately yielding ae. Intuitively, it seems that this strategy could
work rather well for the types of problems that I am facing regularly, and
I am considering implementing it within the scope of the aforementioned
proof tools. However, I am slightly concerned about whether there already
exist canonical implementations or better alternative solutions (please
note, however, that my setting is, effectively, a partial semigroup).
Kind Regards,
Mikhail Chekhov
Email Gateway (Dec 28 2020 at 11:07):From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Mikhail, this sounds intriguing, though intro-resolution and conditional rewriting will behave similarly in many cases. Do you have simple examples to demonstrate where intro-rewriting works better? I imagine they may involve variable instantiation (i.e. P(x) ==> l=r, where x is not mentioned in l).
Larry
Email Gateway (Dec 28 2020 at 16:06):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Lawrence Paulson,
this sounds intriguing, though intro-resolution and conditional rewriting
will behave similarly in many cases.Would it possible to suggest a reference that explains this in more detail?
I have a certain degree of familiarity with the conventional theory of
abstract/term rewriting, but I am not certain how would one go about
establishing analytical properties of a set of intro+simp rules for a
method like auto.
Do you have simple examples to demonstrate where intro-rewriting works
better? I imagine they may involve variable instantiation (i.e. P(x) ==>
l=r, where x is not mentioned in l).Effectively, you have already proposed one such example. An expanded
variant stated in Isabelle/HOL can be found in Appendix A after my
signature.
Indeed, I use this type of pattern quite frequently in my work. For
example, I have introduced predicates that indicate that a given entity is
a function from a to b. Also, similar predicates exist for
injective/surjective/bijective functions and, even more generally, for
various specific arrows in arbitrary categories. Practically, I found it
unwieldy to use different predicates to distinguish the arrows with a
specified domain or codomain only, or stating their domain/codomain
explicitly in the statements of theorems, or using additional
'composability' predicates: when using the latter two methodologies it also
seems to be difficult to establish a good set of rewriting/introduction
rules for reasons unrelated to the choice of the method/strategy for
rewriting/introduction. Besides, the chosen methodology leads to (what I
would consider being) a very natural textbook-like style of presentation.
For example, to state that the horizontal composition of (horizontally
composable) natural isomorphisms is a natural isomorphism, I may use
something similar to (Ξ± is a size parameter; see
https://en.wikipedia.org/wiki/Strict_2-category for the source of the
inspiration for the notation):
assumes "π : π' β¦iso π' : π
β¦β¦βΞ±β β"
and "π : π β¦iso π : π β¦β¦βΞ±β π
"
shows "π β π : π' β π β¦iso π' β π : π β¦β¦βΞ±β β"
However, given these conventions, a natural form of the associativity law
for the horizontal transformations now looks like
assumes "π : π'' β¦ π'' : β β¦β¦βΞ±β π"
and "π : π' β¦ π' : π
β¦β¦βΞ±β β"
and "π : π β¦ π : π β¦β¦βΞ±β π
"
shows "(π β π) β π = π β (π β π)"
This does cause a problem when trying to use it in conjunction with
intro-resolution and conditional rewriting. However, cs_concl copes with it
reasonably well for relatively complex use cases.
There is another practical aspect that may lead to problems when using
intro-resolution + simp: I am not certain whether it is a good idea to
maintain a large collection of theorems that state how various predicates
are related to each other in the form of a simpset. Consider the following
example:
context
fixes P Q R f b
assumes [intro, cs_intros]: "P x βΉ Q x"
and [intro, cs_intros]: "Q x βΉ R x"
and [simp, intro, cs_simps]: "R x βΉ f x = b"
and Qb: "Q b"
begin
lemma
assumes "P x"
shows "Q (f x)"
using assms Qb oops (by simp, auto, force, fast, fastforce, blast)
lemma
assumes "P x"
shows "Q (f x)"
using assms Qb by (cs_concl cs_simp: cs_simps cs_intro: cs_intros)
end
In this case, if "P x βΉ Q x" and "Q x βΉ R x" are part of the simpset, then
the example works. However, I am not certain whether one can always
replace/augment intro with simp in this way and how practical is it in
general. Is it possible to build upon this example to ensure that
simp rules cannot be used instead of introduction? Could simp eliminate the
side conditions that one does not want to be eliminated when proving other
theorems? I thought that I have observed such problems with this
methodology when working with simp/auto, but I cannot find a way to produce
a minimal example in this instance. Perhaps, there was a way around them.
However, one of the most pleasant aspects of the strategy employed in
cs_concl is that one no longer needs to think about whether a rule should
be declared as simp, intro, or both. Effectively, intro-resolution is used
exclusively, making it easier to predict how the method will behave with a
given set of rules.
Kind Regards,
Mikhail Chekhov
Appendix A
named_theorems cs_simps
named_theorems cs_intros
definition surj_from_to
where "surj_from_to a b f = (f ` a = b)"
context
fixes f c P
assumes f[intro, simp, cs_simps]: "surj_from_to a b f βΉ x β a βΉ f x = c +
x"
and [intro, simp, cs_intros]: "P a b x βΉ surj_from_to a b f"
and [intro, simp, cs_intros]: "P a b x βΉ c + x = x"
begin
lemma
assumes "P a b x" and "x β a"
shows "f x = x"
using assms oops (by simp, auto, force, fast, fastforce, blast)
lemma
assumes "P a b x" and "x β a"
shows "f x = x"
using assms by (cs_concl cs_simp: cs_simps cs_intro: cs_intros)
end
On Mon, Dec 28, 2020 at 1:07 PM Lawrence Paulson <lp15@cam.ac.uk> wrote:
Dear Mikhail, this sounds intriguing, though intro-resolution and
conditional rewriting will behave similarly in many cases. Do you have
simple examples to demonstrate where intro-rewriting works better? I
imagine they may involve variable instantiation (i.e. P(x) ==> l=r, where x
is not mentioned in l).Larry
On 27 Dec 2020, at 15:58, Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
wrote:From the manual of the simplifier: "conditions in conditional rewrite
rules are solved recursively before the rewrite rule is applied".
Empirically, I have established that it could be useful to be able to treat
rewriting in the same manner as intro-resolution, allowing the side
conditions of the rewrite rules to be resolved both using rewriting or
intro-resolution after the application of the rewrite rule to a given goal
(of course, this is also meant to be done recursively). I devised a
prototype method based on this algorithm (CS in
https://gitlab.com/user9716869/Isabelle-Complement-Library). For my own
needs, practically, I found this type of 'coupling' of rewriting and
intro-resolution to be exceptionally capable at solving complex goals in
comparison with some of the existing tools that seem to combine
simplification and classical reasoning that I tried before (by now, for my
own needs, I rely on the methods provided by CS almost exclusively in a
reasonably sizeable development).
Email Gateway (Dec 29 2020 at 12:38):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Lawrence Paulson/All,
Once again, I apologize for my haste. It seems that I have developed a bad
habit of trying to minimize the time spent on writing the replies for the
mailing list, leading to various embarrassing misprints and mistakes. Of
course, the excerpt "a natural form of the associativity law for the
horizontal transformations" should read "a natural form of the
associativity law for the horizontal composition of natural
transformations". I noticed that there is quite a number of other minor
inconsistencies and misprints in my last email. However, hopefully, they do
not interfere with the meaning that I was trying to convey.
Kind Regards,
Mikhail Chekhov
Email Gateway (Jan 01 2021 at 16:29):From: Lawrence Paulson <lp15@cam.ac.uk>
It sounds like youβve been able to combine your proof method with Isabelle2020 in order to create your category theory development. And a usable formalisation of category theory would be an impressive achievement.
Maybe the way forward is for you to complete your example and contribute it to the AFP. Material from AFP entries sometimes finds its way into the Isabelle sources, and a fully-worked example would give us a good basis for evaluating this idea.
Larry
Email Gateway (Jan 01 2021 at 19:55):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Lawrence Paulson,
Email Gateway (Jan 01 2021 at 21:45):From: Mikhail Chekhov <mikhail.chekhov.w@gmail.com>
Dear Lawrence Paulson/All,
I would like to make one minor remark with regard to the last quoted
statement. The method that I was referring to in my original post (albeit,
for now, in a very rough zero-order form) is available from the, so-called,
Isabelle Complement Library (
https://gitlab.com/user9716869/Isabelle-Complement-Library). It is likely
that I will be looking to submit this library to the AFP in a reasonable
time frame as part of another project, not related to my work on the
formalization of category theory. Thus, I anticipate that it will be
possible to evaluate the idea related to the method fairly soon. However, I
would be extremely surprised if there was anything original about it: to
me, it seems like it combines rewriting and introduction in the simplest
and the most natural manner. Thus, I am still hopeful that a more mature
implementation of this algorithm is already available somewhere.
Kind Regards,
Mikhail Chekhov
Email Gateway (Jan 02 2021 at 11:14):From: Lawrence Paulson <lp15@cam.ac.uk>
Well, obviously auto and force combine rewriting and introduction, but not as I think you intend (to support conditional rewriting).
Larry
Email Gateway (Jan 04 2021 at 17:23):From: Thomas Sewell <tals4@cam.ac.uk>
Hi Mikhail.
I think it's worth mentioning a simple trick relevant to associativity.
As you say, the problem is, how do you apply a rewrite of the form
"b . c = r" to a goal "a . b . c . d"? It's annoying to have to instruct
Isabelle to somehow gather the b and c together. Let's suppose "." is
associative and that "a . b . c . d" is syntax for "a . (b . (c . d))".
The simple trick is to also derive the rule "b . c . x = r . x".
This modified rule will apply to the original goal in normal form
without
having to first gather "(b . c)" together.
The variant form of each rule can usually be derived as a one-liner,
since
it just amounts to generalising via some congruence and then rewriting
into
normal form. Here's a worked example for conjunction, which works in
Isabelle/HOL:
lemma less_and_greater:
fixes x :: nat
shows "(x < y β§ x > y) = False"
by auto
lemmas conj_left_cong = conj_cong[OF _ refl]
lemmas less_and_greater2 = less_and_greater[THEN conj_left_cong,
simplified conj_assoc]
lemma
fixes x :: nat
shows
"~ (A β§ (B β§ x < y) β§ (x > y β§ x β€ Suc 12) β§ C)"
apply (simp only: conj_assoc)
apply (simp only: less_and_greater2)
apply simp
done
From time to time somebody asks about rewriting modulo associativity
and commutativity, which might sometimes be really useful. My
understanding
is that this problem has been studied in other tools, that solutions
exist,
that performance is a major issue, and that no implementation for
Isabelle currently exists.
Cheers,
Thomas.
Last updated: Jul 15 2022 at 23:21 UTC