Email Gateway (Aug 23 2022 at 08:34): Email Gateway (Aug 23 2022 at 08:34):From: Tjark Weber <tjark.weber@it.uu.se>
Hi,
The function command supports non-constructor patterns. Is it possible
to use patterns that are ambiguous, i.e., that could match in several
ways?
Consider the following (simplified) example:
function f :: "nat ⇒ nat" where
"f 0 = 0"
| "f 1 = 0"
| "a > 0 ⟹ b > 0 ⟹ f (a + b) = f a + f b"
apply (metis less_imp_add_positive less_one linorder_neqE_nat)
apply simp+
oops
This should define a function f that is 0 everywhere. However, the last
proof obligation that is generated contains f_sumC, and I am not sure
how to prove it.
Best,
Tjark
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Email Gateway (Aug 23 2022 at 08:34):From: Dominique Unruh <unruh@ut.ee>
Hi,
I don't know if there is a better way, but when I stumbled upon the
_sumC problem, the best I found was the following approach:
Make the function manually unambiguous:
function f :: "nat ⇒ nat" where
f0: "f 0 = 0"
| f1: "f 1 = 0"
| fplus_raw: "a+b \neq 0 ==> a > 0 ⟹ b > 0 ⟹ f (a + b) = f a + f b"
This defines the same function as yours, but of course it is
inconvenient because it has the added premise in the fplus_raw rule
(which is used for simplification).
Then I would prove
lemma fplus[simp]: "a > 0 ⟹ b > 0 ⟹ f (a + b) = f a + f b"
This should work because now you can do induction and everything you need.
And finally I would remove fplus_raw from the simplifier via:
declare fplus_raw[simp del]
This should more or less approximate the situation as if you had defined
the function without the extra premise in the first place, I think.
Best wishes,
Dominique.
Email Gateway (Aug 23 2022 at 08:34):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Tjark and Dominique,
I don't think the function package can handle such cases out-of-the-box. Dominique, your solution does not remove the inherent ambiguity from the sum case, which is reflected in the goal:
/\ a b aa ba. 0 < a ==> 0 < b ==> 0 < aa ==> 0 < ba ==> a + b = aa + ba ==>
f_sumC a + f_sumC b = f_sumC aa + f_sumC ba
The most "automatic" solution I can see for such situations is to identify a reusable iteration pattern:
fun iter_nat_monoid_add :: "'a::monoid_add ⇒ nat ⇒ 'a" where
"iter_nat_monoid_add a 0 = 0"
|"iter_nat_monoid_add a (Suc 0) = a"
|"iter_nat_monoid_add a (Suc (Suc n)) = iter_nat_monoid_add a (Suc n) + a"
lemma iter_nat_monoid_add_add:
"iter_nat_monoid_add a (m+n) = iter_nat_monoid_add a m + iter_nat_monoid_add a n"
proof (induct n arbitrary: m)
case (Suc n m)
then show ?case
apply(cases m, simp_all)
by (metis Suc_funpow add.assoc add_Suc funpow_0 iter_nat_monoid_add.simps(2)
iter_nat_monoid_add.simps(3))
qed simp
definition f :: "nat ⇒ nat" where
"f = iter_nat_monoid_add 0"
lemma f_simps: "f 0 = 0" "f 1 = 0" "f (a + b) = f a + f b"
using iter_nat_monoid_add_add unfolding f_def by auto
Best wishes,
Andrei
Email Gateway (Aug 23 2022 at 08:35):From: Dominique Unruh <unruh@ut.ee>
Hi,
you were right, my solution didn't work as stated, I thought the
ambiguity was between different cases (in which case my solution can be
used), and not within a single case. For the latter, my trick can be
modified: We need to make sure that the premise of that case fires only
for one single pair a,b for each sum a+b. This can be achieved by adding
the premise "(a,b) = (SOME (a',b'). a' > 0 ∧ b' > 0 ∧ a'+b' = a+b)"
(this basically says: assume that a,b equals some arbitrarily chosen
fixed a,b from all possible a,b that have the same sum".
Then the case distinctness can be proven relatively easily. However,
proving "f (a+b) = f a + f b" takes a bit of work. I worked this out in
the attached theory file.
Andrei's solution is certainly simpler in this case. But in case
Andrei's solution does not work for some other cases, I am adding mine
as well. (In the present case, an even simpler approach works:
definition "f x = 0" lemma f_simps: "f 0 = 0" "f 1 = 0" "f (a + b) = f a
Best wishes,
Dominique.
Scratch.thy
Last updated: Apr 27 2024 at 01:05 UTC