Re: [isabelle] pattern compatibility: _ = _ foo_sumC _



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 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)





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.