Email Gateway (Aug 19 2022 at 14:37): Email Gateway (Aug 19 2022 at 14:37):From: "Roger H." <s57076@hotmail.com>
Hi,
how can i prove
set l1 ⊆ {Suc 0, 2, 3} ⟶ set l2 ⊆ {Suc 0, 2, 3, 4} ⟶ set (addlists l1 l2) ⊆ {Suc 0, 2, 3, 4, 5, 6, 7}
(by the way
fun addlists :: "nat list => nat list => nat list" where
"addlists [] [] = []" |
"addlists (x#xs) [] = undefined" |
"addlists [] (x#xs) = undefined" |
"addlists (x#xs) (y#ys) = (x+y) # (addlists xs ys)"
)
Many thanks!
Email Gateway (Aug 19 2022 at 14:37):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
you can't (hopefully), because it's simply not true. Running nitpick
will provide you with a counterexample, such as l1 = [3], l2 = [].
You need the additional assumption that l1 and l2 have the same length.
Then it works by simple induction over the function definition:
lemma
assumes "length l1 = length l2" "set l1 ⊆ {Suc 0, 2, 3}" "set l2 ⊆
{Suc 0, 2, 3, 4}"
shows "set (addlists l1 l2) ⊆ {Suc 0, 2, 3, 4, 5, 6, 7}"
using assms by (induction l1 l2 rule: addlists.induct) auto
Note that you could also define your addlists function in terms of
existing functions, like this:
definition "addlists xs ys = [x + y. (x,y) ← zip xs ys]"
which is syntactic sugar for
definition "addlists xs ys = map (λ(x,y). x + y) (zip xs ys)"
This is equivalent to your function if the two lists have the same
length, otherwise the longer list is implicitly “truncated”, as is the
definition of zip. With this definition, your lemma goes through even
without the additional assumption that the lengths are equal. You can do
the induction with the rule list_induct2' (which is the same as your
addlists.induct).
Cheers,
Manuel
Last updated: Nov 21 2024 at 12:39 UTC