Email Gateway (Aug 19 2022 at 10:52): Email Gateway (Aug 19 2022 at 10:52):From: Walther Neuper <wneuper@ist.tugraz.at>
Using the function package I cannot prove pattern compatibility with
unary occurrence of "*_sumC" in the proof obligation, which I see happen
quite often, e.g.[1].
Interestingly, the example on p.2 of the "Tutorial on Function
Definition" is solved automatically by "fun", but "function" creates
that kind of obligation, which is NOT provable "by auto":
function sep :: "'a ? 'a list ? 'a list" where
"sep a (x # y # xs) = x # a # sep a (y # xs)"
| "sep a xs = xs"
apply pat_completeness
apply simp
defer
apply simp
------------------------------------------
proof (prove): step 4
goal (1 subgoal):
1. ?a x y xs aa xsa.
(a, x # y # xs) = (aa, xsa) ?
x # a # sep_sumC (a, y # xs) = xsa
For learning how to prove this kind of obligations it seems very helpful
to have the above example proved explicitly --- is there some of the
experts, who could spend a few minutes on that, please ?
Walther
PS: I scanned the documentation without findings: did I overlook something?
And I scanned the mailing list with some findings [2/3, 4/5], but
without coming to a clue.
[1] the rhs of the conclusion contains dvd_up_sumC, the lhs does not; so
one needs some properties of dvd_up_sumC for proving equality, e.g
"dvd_up_sumC (ds, rest) = ds mod rest" (which easily can be proved under
the assumptions given):
3. ?d p ds ps.
([d], [p]) = (ds, ps) ?
(p mod d = 0) =
(let ds = drop_lc0 ds; ps = drop_lc0 ps; d000 = replicate
(length ps - length ds) 0 @ ds;
quot = GCD_Poly_FP.lcoeff ps div2 GCD_Poly_FP.lcoeff d000;
rest = drop_lc0 (ps minus_up (d000 mult_ups quot))
in if rest = [] then True
else if quot ? 0 ? length ds ? length rest then dvd_up_sumC
(ds, rest) else False)
[2]
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-March/msg00023.html
[3]
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-March/msg00026.html
[4]
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-February/msg00001.html
[5]
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-February/msg00002.html
Email Gateway (Aug 19 2022 at 10:52):From: Christian Sternagel <c.sternagel@gmail.com>
Dear Walter,
function (sequential) ...
instead of just
function ...
does the trick (together with pat_completeness and auto). Without the
sequential option the defining equations must be disjoint and complete.
See also "isabelle doc functions".
cheers
chris
Email Gateway (Aug 19 2022 at 10:52):From: Walther Neuper <wneuper@ist.tugraz.at>
Christian,
thanks for reply !
Your suggestion ...
function (sequential) ...
instead of just
function ...
does the trick (together with pat_completeness and auto).
helped me to pin down my problem: "function (sequential) sep ... "
creates these obligations for pattern compatibility:
goal (6 subgoals):
1. ?a x y xs aa xa ya xsa.
(a, x # y # xs) = (aa, xa # ya # xsa) ?
x # a # sep_sumC (a, y # xs) = xa # aa # sep_sumC (aa, ya # xsa)
2. ?a x y xs aa. (a, x # y # xs) = (aa, []) ? x # a # sep_sumC (a,
y # xs) = []
3. ?a x y xs aa v. (a, x # y # xs) = (aa, [v]) ? x # a # sep_sumC
(a, y # xs) = [v]
4. ?a aa. (a, []) = (aa, []) ? [] = []
5. ?a aa v. (a, []) = (aa, [v]) ? [] = [v]
6. ?a v aa va. (a, [v]) = (aa, [va]) ? [v] = [va]
My interest was for 'mixed' obligations like 3./4. above, where "_sumC"
occurs only once: I wanted to prove the equalities (which is impossible
without knowledge about "_sumC") under the assumptions.
Now I see (thanks to your help!), that these obligations are proved
using the fact that the assumptions, "(a, x # y # xs) = (aa, [])" and
"(a, x # y # xs) = (aa, [v])", are not satisfiable ('ex falso
qodlibet'). The simplifier knows theorems like "List.inject",
"List.distinct_2" etc good enough to end up with
a # sep_sumC (a, y # xs) = [] ? False
In the case of the function I am trying to define [1], I get 15
obligations: the 11 'non-mixed' obligations are solved "by simp" (which
each takes a few seconds for each).
However, the 4 'mixed' obligations cannot be proved "by simp" (which
loop somewhere I can not yet identify in the trace), although they all
have non-satisfiable assumptions...
1. ?d p v vb vc ps. ([d], [p]) = (v # vb # vc, ps) ? ...
2. ?d p ds v vb vc. ([d], [p]) = (ds, v # vb # vc) ? ...
3. ?ps v vb vc psa. ([], ps) = (v # vb # vc, psa) ? ...
4. ?ds dsa v vb vc. (ds, []) = (dsa, v # vb # vc) ? ...
So, instead of tweaking the simplifier, it seems to suffice to show the
assumptions not satisfiable ;-))) ... thanks a lot !!!
Walther
[1] I am stuck with dvd for univariate polynomials:
function (sequential) dvd_unipoly :: "unipoly ? unipoly ? bool"
(infixl "dvd'_unipoly" 70) where
"[d] dvd_unipoly [p] = ((¦d¦ ? ¦p¦) & (p mod d = 0))"
| "ds dvd_unipoly ps =
(let
ds = drop_lc0 ds; ps = drop_lc0 ps;
d000 = (List.replicate (List.length ps - List.length ds) 0) @ ds;
quot = (lcoeff ps) div2 (lcoeff d000);
rest = drop_lc0 (ps minus_up (d000 mult_ups quot))
in
if rest = [] then True else
if quot ? 0 & List.length ds ? List.length rest then ds
dvd_unipoly rest else False)"
On 04/13/2013 05:52 PM, Walther Neuper wrote:
Using the function package I cannot prove pattern compatibility with
unary occurrence of "*_sumC" in the proof obligation, which I see happen
quite often, e.g.[1].Interestingly, the example on p.2 of the "Tutorial on Function
Definition" is solved automatically by "fun", but "function" creates
that kind of obligation, which is NOT provable "by auto":function sep :: "'a ? 'a list ? 'a list" where
"sep a (x # y # xs) = x # a # sep a (y # xs)"
| "sep a xs = xs"
apply pat_completeness
apply simp
defer
apply simp
------------------------------------------
proof (prove): step 4goal (1 subgoal):
1. ?a x y xs aa xsa.
(a, x # y # xs) = (aa, xsa) ?
x # a # sep_sumC (a, y # xs) = xsaFor learning how to prove this kind of obligations it seems very helpful
to have the above example proved explicitly --- is there some of the
experts, who could spend a few minutes on that, please ?Walther
PS: I scanned the documentation without findings: did I overlook
something?
And I scanned the mailing list with some findings [2/3, 4/5], but
without coming to a clue.[1] the rhs of the conclusion contains dvd_up_sumC, the lhs does not; so
one needs some properties of dvd_up_sumC for proving equality, e.g
"dvd_up_sumC (ds, rest) = ds mod rest" (which easily can be proved under
the assumptions given):
3. /\ d p ds ps.
([d], [p]) = (ds, ps) ==>
(p mod d = 0) =
(let ds = drop_lc0 ds; ps = drop_lc0 ps; d000 = replicate
(length ps - length ds) 0 @ ds;
quot = GCD_Poly_FP.lcoeff ps div2 GCD_Poly_FP.lcoeff d000;
rest = drop_lc0 (ps minus_up (d000 mult_ups quot))
in if rest = [] then True
else if quot ? 0 ? length ds ? length rest then
dvd_up_sumC (ds, rest) else False)
Last updated: Apr 25 2024 at 20:15 UTC