Email Gateway (Aug 19 2022 at 10:15): Email Gateway (Aug 19 2022 at 10:15):From: John Wickerson <jpw48@cam.ac.uk>
Dear Isabelle,
This question is directed at anybody familiar with the Finite_Set theory...
http://isabelle.in.tum.de/library/HOL/Finite_Set.html
... in particular, the Finite_Set.fold functional. Consider the term
Finite_Set.fold f s A
Various lemmas (e.g. Finite_Set.comp_fun_commute.fold_image) require me to show that f satisfies the "comp_fun_commute" property, i.e.
(1) f x o f y = f y o f x
for all x and y. This is too strong a requirement for me. I can show that (1) holds for all x and y in A, but not for all x and y in general. Morally, I should only have to show that f commutes when given inputs drawn from A.
It would be quite a bit of hassle for me to convert these lemmas to stronger versions. So I was wondering if anybody has come across this problem before, or knows how to easily strengthen these lemmas, or has any other advice on this topic?
Thanks,
john
Email Gateway (Aug 19 2022 at 10:15):From: Peter Lammich <lammich@in.tum.de>
Hi.
An alternative is to use an invariant rule, i.e., something like:
I s a0 !!x s a. [| I s a; x\in s |] ==> I (s-{x}) (f x a)
------------------------------------------------------------ if finite s
I {} (fold f s a0)
or, alternatively, show that your proposition holds for folding over any
distinct list representing the set:
!!l. [| distinct l; set l = s |] ==> P (foldl f l a0)
-------------------------------------------------------- if finite s
P (fold f s a0)
Both rules (modulo my typos) should be provable by induction over the
finite set s.
Email Gateway (Aug 19 2022 at 10:15):From: John Wickerson <jpw48@cam.ac.uk>
Hi Peter, thanks very much for this. Forgive me if I'm mistaken, but I don't understand how either of these approaches would help. I think I would still need to reason about terms like
fold f s (insert a A)
in order to complete the induction, and I can't reason about such terms without knowing that f satisfies the "comp_fun_commute" property.
Let me state my problem more concretely...
Finite_Set provides the following lemma (the first assumption comes from the context "comp_fun_commute"):
lemma fold_image:
assumes "⋀x y. f x ∘ f y = f y ∘ f x"
assumes "finite A" and "inj_on g A"
shows "fold f x (g ` A) = fold (f ∘ g) x A"
But I want the following lemma:
lemma fold_image_stronger:
assumes "⋀x y. ⟦ x ∈ A ; y ∈ A ⟧ ⟹ f x ∘ f y = f y ∘ f x"
assumes "finite A" and "inj_on g A"
shows "fold f x (g ` A) = fold (f ∘ g) x A"
How might I prove it? It's tricky because all the other lemmas about Finite_Set.fold are in the "comp_fun_commute" context where
⋀x y. f x ∘ f y = f y ∘ f x
holds, whereas I only have the weaker property
⋀x y. ⟦ x ∈ A ; y ∈ A ⟧ ⟹ f x ∘ f y = f y ∘ f x
available to me.
Thanks very much,
john
On 19 Feb 2013, at 16:38, Peter Lammich wrote:
Hi.
An alternative is to use an invariant rule, i.e., something like:
I s a0 !!x s a. [| I s a; x\in s |] ==> I (s-{x}) (f x a)
------------------------------------------------------------ if finite s
I {} (fold f s a0)or, alternatively, show that your proposition holds for folding over any
distinct list representing the set:!!l. [| distinct l; set l = s |] ==> P (foldl f l a0)
-------------------------------------------------------- if finite s
P (fold f s a0)Both rules (modulo my typos) should be provable by induction over the
finite set s.--
PeterOn Di, 2013-02-19 at 16:01 +0100, John Wickerson wrote:
Dear Isabelle,
This question is directed at anybody familiar with the Finite_Set theory...
http://isabelle.in.tum.de/library/HOL/Finite_Set.html
... in particular, the Finite_Set.fold functional. Consider the term
Finite_Set.fold f s A
Various lemmas (e.g. Finite_Set.comp_fun_commute.fold_image) require me to show that f satisfies the "comp_fun_commute" property, i.e.
(1) f x o f y = f y o f x
for all x and y. This is too strong a requirement for me. I can show that (1) holds for all x and y in A, but not for all x and y in general. Morally, I should only have to show that f commutes when given inputs drawn from A.
It would be quite a bit of hassle for me to convert these lemmas to stronger versions. So I was wondering if anybody has come across this problem before, or knows how to easily strengthen these lemmas, or has any other advice on this topic?
Thanks,
john
Email Gateway (Aug 19 2022 at 10:15):From: Lawrence Paulson <lp15@cam.ac.uk>
Is your desired theorem true?
I would find it easier to believe if it also assumed "x : A" and "g ` A <= A".
Larry Paulson
Email Gateway (Aug 19 2022 at 10:15):From: John Wickerson <jpw48@cam.ac.uk>
Mm, yes, my mistake. The domain of f should be "g ` A" rather than just "A". So the theorem should be:
Email Gateway (Aug 19 2022 at 10:16):From: Peter Lammich <lammich@in.tum.de>
Hi John.
Sorry for the confusion with the invariant rules. They hold (if the
property P admits only one result) but are probably not very useful to
prove your stronger fold_image rule.
To prove that (even a stronger one) you can exploit the fact that the
definition of fold does not depend on this strange locale with too
strong assumptions, but on an inductively defined predicate fold_graph,
that contains the results of all possible fold orderings.
Here is the proof of your fold_image_stronger, but you do not need the
first two assumptions at all!
Please excuse the aux-lemmas and the not very elaborated proofs:
theorem fold_image_even_stronger:
assumes I: "inj_on g A"
shows "Finite_Set.fold f x (g`A) = Finite_Set.fold (f o g) x A"
oops (*Proof comes below, first need to show some aux-lemmas *)
lemma inj_img_insertE:
assumes I: "inj_on f s"
assumes N: "x\<notin>r"
assumes E: "insert x r = fs"
obtains x' s' where "s=insert x' s'" and "x'\<notin>s'"
and "x = f x'" and "r = fs'"
proof -
from E have "x\<in>fs" by auto
then obtain x' where "x'\<in>s" and "x = f x'" by auto
hence "s = insert x' (s - {x'})" by auto
have "r = f(s - {x'})" apply auto
apply (metis (no_types) Diff_insert_absorb E I N
s = insert x' (s - {x'}) x = f x' image_insert inj_on_insert
insertI1 insert_Diff1)
by (metis E I x = f x' x' \<in> s imageI inj_on_contraD insertE)
show ?thesis
apply rule
apply fact
apply simp
apply fact+
done
qed
lemma fold_graph_image:
"inj_on g s \<Longrightarrow> fold_graph f a (gs) r
\<longleftrightarrow> fold_graph (f o g) a s r"
proof
case goal1
from goal1(2,1) show ?case
proof (induct "gs" r arbitrary: s rule: fold_graph.induct)
case emptyI thus ?case by (auto intro: fold_graph.emptyI)
next
case (insertI x A r s)
with inj_img_insertE obtain x' A' where
"x'\<notin>A'" and [simp]: "s = insert x' A'" "x = g x'" "A=gA'"
by metis
with insertI.hyps(3)[of A'] insertI.prems
have FG: "fold_graph (f o g) a A' r"
by auto
from fold_graph.insertI[OF x'\<notin>A' FG]
show ?case by simp
qed
next
case goal2
from goal2(2,1) show ?case
proof (induct rule: fold_graph.induct)
case emptyI thus ?case by (auto intro: fold_graph.emptyI)
next
case (insertI x A r)
hence FG: "fold_graph f a (gA) r" by simp
from x\<notin>A insertI.prems have N: "g x \<notin> g`A" by auto
from fold_graph.insertI[OF N FG] show ?case by simp
qed
qed
lemma fold_graph_image':
"inj_on g s \<Longrightarrow> fold_graph f a (g`s) = fold_graph (f o
g) a s"
by (rule ext) (rule fold_graph_image)
theorem fold_image_even_stronger:
assumes I: "inj_on g A"
shows "Finite_Set.fold f x (g`A) = Finite_Set.fold (f o g) x A"
unfolding Finite_Set.fold_def
by (simp add: fold_graph_image'[OF I, of f x])
Best,
Peter
Email Gateway (Aug 19 2022 at 10:16):From: John Wickerson <jpw48@cam.ac.uk>
Awesome! Thanks so much Peter, that's really kind of you.
John
Email Gateway (Aug 19 2022 at 10:16):From: John Wickerson <jpw48@cam.ac.uk>
Just a thought: since "fold_image_even_stronger" needs only a subset of the assumptions needed by "Finite_Set.fold_image", perhaps your new theorem should replace the one in the HOL library?
john
Email Gateway (Aug 19 2022 at 10:17):From: Tobias Nipkow <nipkow@in.tum.de>
I have that on my radar.
Tobias
Last updated: Apr 19 2024 at 08:19 UTC