Email Gateway (Aug 22 2022 at 09:24): Email Gateway (Aug 22 2022 at 09:24):From: Tjark Weber <tjark.weber@it.uu.se>
The attached lemma about well-foundedness of relational composition
featured prominently in a recent termination proof of mine. If the
lemma is not available already, I would like to propose it for
inclusion in HOL/Wellfounded.thy (or some derived theory).
I discovered the lemma and proof myself, but I suspect that the result
is well-known. Pointers to the literature would be appreciated.
Best,
Tjark
===== 8< =====
lemma wf_relcomp_compatible:
assumes "wf R" and "R O S \<subseteq> S O R"
shows "wf (S O R)"
proof (rule wfI_pf)
fix A assume A: "A \<subseteq> (S O R) A"
{
fix n have "(S ^^ n) A \<subseteq> R (S ^^ Suc n) A"
proof (induction n)
case 0 show ?case
using A by (simp add: relcomp_Image)
next
case (Suc n)
then have "S (S ^^ n) A \<subseteq> S R (S ^^ Suc n)
A"
by (metis Image_mono subsetCI)
also have "\<dots> \<subseteq> R S (S ^^ Suc n) A"
using assms(2) by (metis (no_types, hide_lams) Image_mono
order_refl relcomp_Image)
finally show ?case
by (metis relcomp_Image relpow.simps(2))
qed
}
then have "(\<Union>n. (S ^^ n) A) \<subseteq> R (\<Union>n. (S
^^ n) A)"
by blast
then have "(\<Union>n. (S ^^ n) A) = {}"
using assms(1) by (metis wfE_pf)
then show "A = {}"
using relpow.simps(1) by blast
qed
Email Gateway (Aug 22 2022 at 09:26):From: Tobias Nipkow <nipkow@in.tum.de>
I am not aware of this lemma from the literature, but maybe our friends in
Innsbruck are?
I'll be happy to include it in HOL/Wellfounded.thy if you do me the favour of
getting rid of metis - it is not available at that theory yet. Maybe somebody
can also think of a more telling name suffix than "_compatible".
Thanks
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 09:26):From: Tjark Weber <tjark.weber@it.uu.se>
Tobias,
On Sun, 2015-04-26 at 09:24 +0200, Tobias Nipkow wrote:
I'll be happy to include it in HOL/Wellfounded.thy if you do me the favour of
getting rid of metis - it is not available at that theory yet.
Certainly. A proof that uses only simp and blast is attached.
Maybe somebody can also think of a more telling name suffix than "_compatible".
This was inspired by the existing lemma wf_union_compatible. Of course,
it is a terrible name.
Best,
Tjark
===== 8< =====
lemma wf_relcomp_compatible:
assumes "wf R" and "R O S \<subseteq> S O R"
shows "wf (S O R)"
proof (rule wfI_pf)
fix A assume A: "A \<subseteq> (S O R) A"
{
fix n have "(S ^^ n) A \<subseteq> R (S ^^ Suc n) A"
proof (induction n)
case 0 show ?case
using A by (simp add: relcomp_Image)
next
case (Suc n)
then have "S (S ^^ n) A \<subseteq> S R (S ^^ Suc n)
A"
by (simp add: Image_mono)
also have "\<dots> \<subseteq> R S (S ^^ Suc n) A"
using assms(2) by (simp add: Image_mono O_assoc
relcomp_Image[symmetric] relcomp_mono)
finally show ?case
by (simp add: relcomp_Image)
qed
}
then have "(\<Union>n. (S ^^ n) A) \<subseteq> R (\<Union>n. (S
^^ n) A)"
by blast
then have "(\<Union>n. (S ^^ n) A) = {}"
using assms(1) by (simp only: wfE_pf)
then show "A = {}"
using relpow.simps(1) by blast
qed
Email Gateway (Aug 22 2022 at 09:27):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Tjark and Tobias,
This is my first impression: I've definitely seen this fact applied
(although implicitly) and think it counts as, as they say, "folklore".
Especially so, since the paper "proof" is trivial ;):
Assume: RS RS RS RS RS RS ...
Rearrange into: R SR SR SR SR SR ...
Apply "RS <= SR": R RS RS RS RS RS ...
Repeat this process to obtain: R R R R R R ...
Contradiction.
I checked IsaFoR by hypersearch but didn't find anything that looks
alike immediately. That is, I'm not aware of any formalized proof.
After investigating a little further, I found some relevant literature.
Commutation has been investigated by Rosen [3], but as far as I can tell
on a short glance only w.r.t. confluence. Bachmair and Dershowitz [2]
pronounce "RS <= SR" as "R commutes over S" (whereas "commutation"
without "over" would result in a "diamond" diagram). And Geser [1]
(which was the reference I started from) at least comments about
something similar to your lemma on page 38:
If R is Noetherian, it is more convenient to check for strict
local commutation than for quasi-commutation: They are
equivalent, and checking for strict local commutation is
less complex ...
But also here I did not find a proof by skimming through. Maybe a closer
look would reveal something.
[1] Alfons Geser. Relative Termination. PhD-Thesis. 1990.
[2] Leo Bachmair, Nachum Dershowitz. Commutation, Transformation, and
Termination. CADE. 1986. http://dx.doi.org/10.1007/3-540-16780-3_76
[3] Barry K. Rosen. Tree-Manipulating Systems and Church-Rosser
Theorems. J. ACM (JACM) 20(1):160-187 (1973).
http://doi.acm.org/10.1145/321738.321750
cheers
chris
Email Gateway (Aug 22 2022 at 09:27):From: Christian Sternagel <c.sternagel@gmail.com>
Okay, here is a little bit more:
The following is Lemma 2 from Bachmair and Dershowitz 1986 (I left the
hard part of the proof as an exercise ;) ... I hope it works similar to
what Tjark did before, but since it was proved on paper it has to be
correct \o/ right?):
lemma qc_wf_relto_iff:
assumes "R O S ⊆ S O (R ∪ S)⇧*" -- ‹R quasi-commutes over S›
shows "wf (S⇧* O R O S⇧*) ⟷ wf R"
proof
assume "wf (S⇧* O R O S⇧*)"
moreover have "R ⊆ S⇧* O R O S⇧*" by auto
ultimately show "wf R" using wf_subset by auto
next
assume "wf R"
then show "wf (S⇧* O R O S⇧*)" sorry
qed
It can be used to proof "Tjark's Lemma" :)
corollary
assumes "wf R" and "R O S ⊆ S O R"
shows "wf (S O R)"
proof -
have "R O S ⊆ S O (R ∪ S)⇧*" using ‹R O S ⊆ S O R› by auto
then have "wf (S⇧* O R O S⇧*)"
using ‹wf R› by (simp add: qc_wf_relto_iff)
moreover have "S O R ⊆ S⇧* O R O S⇧*" by auto
ultimately show ?thesis using wf_subset by auto
qed
Depending on who you cite the "subset assumption" could be called:
R strictly locally commutes over S (Geser, PhD); which actually
denotes: R O S ⊆ S^* O R^+
...
hope this helps
chris
Email Gateway (Aug 22 2022 at 09:27):From: Tjark Weber <tjark.weber@it.uu.se>
Christian,
Thank you for the detailed literature search. Of course, I am all for
adding the much more general lemma to Wellfounded.thy.
I can try to complete the formal proof later this week. (If somebody
else wants to go ahead with this right now, I certainly don't mind.)
Best,
Tjark
Email Gateway (Aug 22 2022 at 09:28):From: Tobias Nipkow <nipkow@in.tum.de>
I have just added it. You are welcome to send me an improved version later.
Tobias
smime.p7s
Email Gateway (Aug 22 2022 at 09:28):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
Hi Tjark / Christian,
I'm confused by the notation here.
Firstly, R O S:
doesn't this mean, that where (a, b) in S and (b, c) in R, then (a, c)
in R 0 S ?
Secondly, wf R - doesn't this mean that there is no infinite chain
..... an ... a1 a0
such that each (a_{n+1}, a_n) in R ?
So using this notation,
let R = (n, n+1) for all n (naturals)
let S = (n+1, n) for all n
Then R O S = {(n, n) | n >= 1}
S O R = {(n, n) | n >= 0}
Anyhow, in
http://users.cecs.anu.edu.au/~jeremy/isabelle/2005/gen/WfUn.{thy,ML}
I have proofs of
"(s O r <= r O s^*) --> wf r --> wf (r O s^*)"
and "(s O r <= r O s^*) --> wf r --> wf (s^* O r)"
(they're called
wf_movl_comp and wf_movl_comp2)
(obviously, wf (r O s) = wf (s O r))
(proofs are in Isabelle2005)
I now see in that file I have a note:
(* note - can't get result
"(r O s <= s^* O r) ==> wf r ==> wf (s^* O r)", eg
E = {(x, y) | x >= 0, 0 <= y <= x}
(x, y) >_r (x, y+1) - so r is wf
(x, y) >_s (x+1, y) - so r O s, s O r not wf
In r O s, (x, y) > (x+1, y+1) but only if y < x
In s O r, (x, y) > (x+1, y+1) always
So (r O s <= s O r) *)
As for the paper proof below - what does it mean? It seems to
correspond to the theorem stated if
RS RS ...
means x0 >R x1 >S x2 >R x3 >S x4 ...
in which case wf R means R R R R ... is not possible, but then
haven't you actually applied SR <= RS, not RS <= SR?
Even if I've got conused somewhere above I can't see how you and I could
have both proved results, in Isabelle, one of which seems to be wrong.
Has the definition of wf or of O changed since 2005?
Cheers,
Jeremy
Email Gateway (Aug 22 2022 at 09:28):From: Christian Sternagel <c.sternagel@gmail.com>
Just for the record: Sorry, I introduced a typo in my (sorry) lemma.
(Actually hinted at by quickcheck, since my formulation is not correct.)
The problem was (once again) to adapt the orientation from the rewriting
literature (where "smaller" is on the right) to the orientation of "wf"
(where "smaller" is on the left).
It should actually be:
lemma qc_wf_relto_iff:
assumes "R O S ⊆ (R ∪ S)⇧* O R"
shows "wf (S⇧* O R O S⇧*) ⟷ wf R"
...
This still implies Tjark's lemma and I hope it is provable ;) (I'll give
it a try).
cheers
chris
Email Gateway (Aug 22 2022 at 09:28):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Jeremy,
Without having read everything below in detail: Yes, the definition of O
has changed. At the moment:
(x, z) : R O S <--> EX y. (x, y) : R & (y, z) : S
As to your other remarks, I'm sure that I have many typos in everything
that was not checked by Isabelle ;). I'll look into it later.
cheers
chris
Email Gateway (Aug 22 2022 at 09:28):From: Christian Sternagel <c.sternagel@gmail.com>
Please find attached a formalization (thanks to Bertram for pointless
induction having a point ;)), alas, it still relies on Regexp. Maybe
someone would like to rectify this?
cheers
chris
Bla.thy
Email Gateway (Aug 22 2022 at 10:06):From: Tjark Weber <tjark.weber@it.uu.se>
Tobias (and Christian),
Attached is a proof of Bachmair and Dershowitz's Lemma 2 that should
work in the context of Wellfounded.thy.
If you decide to add this lemma to Wellfounded.thy, I would suggest
that the lemma that I provided earlier (which you added in
https://isabelle.in.tum.de/repos/isabelle/rev/f0fc2378a479) could
perhaps be removed again. As Christian pointed out, it is an easy
corollary of this much more general result.
Best,
Tjark
Scratch.thy
Last updated: Nov 21 2024 at 12:39 UTC