Re: [isabelle] Finite_Set comp_fun_commute



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 (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 = f`s"
>> obtains x' s' where "s=insert x' s'" and "x'\<notin>s'" 
>>   and "x = f x'" and "r = f`s'" 
>> proof -
>> from E have "x\<in>f`s" 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 (g`s) r
>> \<longleftrightarrow> fold_graph (f o g) a s r"
>> proof
>> case goal1 
>> from goal1(2,1) show ?case
>> proof (induct "g`s" 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=g`A'"
>>     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 (g`A) 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
>> 
>> 
>> 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.