Email Gateway (Aug 18 2022 at 16:00): Email Gateway (Aug 18 2022 at 16:00):From: Alexander Krauss <krauss@in.tum.de>
I have some more issues with the Function package, this time with the
domintros option.
[...]
I’m not sure if this is a bug in in the Function package, or an
unavoidable limitation.
It is an unavoidable limitation of the specific implementation, i.e., a
bug. I know it for a long time, and it is (again) caused by some
uncontrolled forward simplification (which is from the devil, but I
didn't know how bad it was when I wrote the code). Maybe it is time for
a new attempt of improving this... I'll have a look.
Alex
Email Gateway (Aug 18 2022 at 16:01):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
I have some more issues with the Function package, this time with the
domintros option. Consider this (not very useful) example:
function (sequential,domintros) f where
"f v b = (if v = 1 then f 0 b else f (Suc v) b)"
apply pat_completeness
apply auto
done
The generated domintros rule is too weak:
thm f.domintros(1)[no_vars]
⟦f_dom (0, b); v ≠ Suc 0 ⟹ f_dom (Suc v, b)⟧ ⟹ f_dom (v, b)
Note that the f_rel intros are correct:
thm f_rel.intros[no_vars]
v = 1 ⟹ f_rel (0, b) (v, b)
v ≠ 1 ⟹ f_rel (Suc v, b) (v, b)
I can work around the issue by wrapping the condition of the if
statement in the identity function and removing it temporarily from the
simpset:
declare id_apply[simp del]
function (sequential,domintros) f' where
"f' v b = (if id (v = 0) then f' 0 b else f' (Suc v) b)"
apply pat_completeness
apply auto
done
declare id_apply[simp]
yields
thm f'.domintros(1)[no_vars]
⟦id (v = 0) ⟹ f'_dom (0, b); ¬ id (v = 0) ⟹ f'_dom (Suc v, b)⟧
⟹ f'_dom (v, b)
A probably related problem is that
function (sequential,domintros) f where
"f l = (case l of [a,b,0] ⇒ f [a+b])"
apply pat_completeness
apply auto
done
gives the domintro rule
thm f.domintros(1)[no_vars]
(⋀a aa. f_dom [a + aa]) ⟹ f_dom l [?]
where I am missing the connection between l and a,aa.
I’m not sure if this is a bug in in the Function package, or an
unavoidable limitation.
Thanks,
Joachim
signature.asc
Last updated: Apr 26 2024 at 01:06 UTC