# Re: [isabelle] Finite_Set comp_fun_commute

I have that on my radar.

Tobias

Am 20/02/2013 12:40, schrieb John Wickerson:
> 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
>
> On 20 Feb 2013, at 09:10, John Wickerson wrote:
>
>> Awesome! Thanks so much Peter, that's really kind of you.
>>
>> John
>>
>>
>> On 20 Feb 2013, at 01:30, Peter Lammich wrote:
>>
>>> 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 (gA) = 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> gA" 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 (gs) = 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 (gA) = 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
>>>
>>>
>>> On Di, 2013-02-19 at 19:34 +0100, John Wickerson wrote:
>>>> Mm, yes, my mistake. The domain of f should be "g  A" rather than just "A". So the theorem should be:
>>>>
>>>>> lemma fold_image_stronger:
>>>>> assumes "⋀x y. ⟦ x ∈ g  A ; y ∈ g  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"
>>>>
>>>> I think *this* one is true ... (but how to prove it?)
>>>>
>>>> Thanks,
>>>> john
>>>>
>>>> On 19 Feb 2013, at 18:01, Lawrence Paulson wrote:
>>>>
>>>>> Is your desired theorem true?
>>>>>
>>>>> I would find it easier to believe if it also assumed "x : A" and "g  A <= A".
>>>>>
>>>>> Larry Paulson
>>>>>
>>>>>
>>>>> On 19 Feb 2013, at 16:43, John Wickerson <jpw48 at cam.ac.uk> wrote:
>>>>>
>>>>>> 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.
>>>>>>>
>>>>>>> --
>>>>>>> Peter
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>> On 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
>>>>>>>
>>>>>>>
>>>>>>>
>>>>>>
>>>>>>
>>>>>
>>>>
>>>
>>>
>>>
>>
>>
>

`

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.