Email Gateway (Aug 18 2022 at 17:51): Email Gateway (Aug 18 2022 at 17:51):From: 游珍 <yucy0405@163.com>
Dear friends,
I'm an Isabelle newbie trying to verify a statement:
Min(a[0],a[1],…,a[n])+ Min(b[0],b[1],…,b[m])
=Min(a[0]+b[0],a[0]+b[1],…a[0]+b[m], a[1]+a[0],…,a[1]+b[m],....a[n]+b[m])
I have some prombles, the following are my proof;
theory test1
importsMain
begin
(------------Min_list ----------------)
fun Min_list :: "int list \<Rightarrow> nat \<Rightarrow> int"
where
"Min_list a 0 = (a !0)" |
"Min_list a (Suc m) = (if ((a !(Suc m))<(Min_list a m)) then (a !(Suc m)) else (Min_list a m)) "
(------------Is any problem with the definition of fun di_sum? ----------------)
fun di_sum :: "int list \<Rightarrow> nat \<Rightarrow> int list \<Rightarrow> nat \<Rightarrow> int list"
where
"di_sum a 0 b 0 = [(a !0)+(b !0)]" |
"di_sum a 0 b (Suc m) = (di_sum a 0 b m) @ [(a !0)+(b !(Suc m))]" |
"di_sum a (Suc n) b m = (di_sum a n b m) @ (di_sum [a !(Suc n)] 0 b m)"
lemma "(Min_list (a::int list) (n::nat)) + (Min_list (b::int list) (m::nat)) = (Min_list (di_sum a n b m) ((n+(Suc 0))*(m+(Suc 0))-(Suc 0)))"
apply (induct n)
apply (unfold Min_list.simps)
apply (induct m)
apply simp
apply (unfold di_sum.simps)
apply ?????
Which method or rule I can choose? How to use these methods and rules?
Need help!
Thanks in advance!
yucy
Email Gateway (Aug 18 2022 at 17:52):From: bnord <bnord01@googlemail.com>
Hi yucy,
I think first of all you need to restrain your lemma to the case where n
< length a and m < length b. Then maybe your definitions are a bit
complex. Maybe show some lemmas characterizing your functions first. I
would define Min_list and di_list using fold and map as there are many
lemmas helping you to deal with them. Something like:
definition minList :: "int list \<Rightarrow> int" where
"minList a = foldl min (a!0) a"
definition flatten :: "'a list list \<Rightarrow> 'a list" where
"flatten x = foldl (op @) [] x"
definition sumList :: "int list \<Rightarrow> int list \<Rightarrow> int
list" where
"sumList a b = flatten (map (%x. map (%y. x + y) b) a)"
But beware the case of the empty list! You would first want to prove
some lemma about what elements are contained in sumList and maybe some
characterizing minList in terms of it picks the minimal element. Then
your lemma should follow easily.
Sorry I can't recommend any specific methods or rules you could use in
your proof it looks kind of messy at that step, of course you can fight
your way trough it but I wouldn't want to do that.
Regards
Benedikt
Last updated: Apr 26 2024 at 04:17 UTC