share/contrib/Zeilberger/zb_prover.mac

   1 /* Proves and Test for "parGosper" and "Gosper"        */
   2 /* by Fabrizio Caruso                                  */
   3
   4
   5
   6 /* It proves the result of Gosper's algorithm                  */
   7 /*                                                             */
   8 /* Remark: The level of verbosity depends on "gs_prove_detail" */
   9
  10 gs_prove(expr,k,cert) :=
  11   block([rhs],
  12
  13   if expr = NON_HYPERGEOMETRIC then
  14      (
  15      if gs_prove_detail>= PROOF_LOW then
  16        (
  17        print("The input is not hypergeometric in ", k),
  18        print("There is no proof for this case.")
  19        ),
  20      return(false)
  21      )
  22   else
  23     if expr = NO_HYP_SOL then
  24        (
  25        if gs_prove_detail>=PROOF_LOW then
  26          (
  27          print("Gosper's algorithn found that"),
  28          print("there is no hypergemetric antidifference for ", expr),
  29          print("There is no proof for this case.")
  30          ),
  31        return(false)
  32        )
  33     else
  34        (
  35        if gs_prove_detail>=PROOF_MEDIUM then
  36          (
  37          print("Gosper's algorithm found the antidifference: ", cert*expr),
  38          print("This means we must have: "),
  39          print(expr, " = ", subst(k+1,k,cert*expr)-cert*expr),
  40          print("which can be proved by dividing both members by ", expr),
  41          print("and checking the resulting equality between rational functions")
  42          ),
  43        rhs : shiftQuo(expr,k)*subst(k+1,k,cert)-cert,
  44        if gs_prove_detail>=PROOF_HIGH then
  45          (
  46          print("Namely: "),
  47          print("1 =",rhs)
  48          ),
  49        return(is(1=factor(xthru(rhs))))
  50        )
  51 );
  52
  53
  54 /* Routines related to the proof writer for Zeilberger's algorithm */
  55
  56 zb_meaning(zb_in,k,n,zb_cert,zb_rec) :=
  57   block([j__],
  58
  59     print(sum(zb_rec[j__]*subst(n+j__-1,n,zb_in),j__,1,length(zb_rec))," = "),
  60     print(subst(k+1,k,zb_cert*zb_in)-zb_cert*zb_in,";")
  61     );
  62
  63 zb_reduced_meaning(zb_in,k,n,zb_cert,zb_rec) :=
  64   block([i__,j__],
  65
  66     return([sum(zb_rec[j__]*product(subst(n+i__-1,n,shiftQuo(zb_in,n)),i__,1,j__-1),j__,1,length(zb_rec)),
  67             subst(k+1,k,zb_cert)*shiftQuo(zb_in,k)-zb_cert])
  68     );
  69
  70 zb_test_equalityAux(eq_pair) :=
  71   block([lhs,rhs],
  72
  73   lhs : rat(eq_pair[1]),
  74   rhs : rat(eq_pair[2]),
  75
  76   if lhs=rhs then
  77     return(true)
  78   else
  79     return([lhs,rhs])
  80   );
  81
  82
  83 zb_test_equality(eq_pair) :=
  84   block([test_res],
  85
  86   test_res : zb_test_equalityAux(eq_pair),
  87   if test_res = true then
  88     return(true)
  89   else
  90     (
  91     if zb_prove_detail>=PROOF_LOW then
  92       (
  93       print("lhs : ", test_res[1]),
  94       print("rhs : ", test_res[2])
  95       ),
  96
  97     return(false)
  98     )
  99   );
 100
 101
 102 /* It proves the result of Zeilbeger's algorithm       */
 103 /*                                                     */
 104 /* The level of verbosity depends on "zb_prove_detail" */
 105
 106 /* zb_prove(zb_in,k,n,zb_out) := */
 107 zb_prove([args]):=
 108   block([i,j,zb_red,zb_in,zb_out,proof,undecided,k,n],
 109     zb_in:first(args),
 110     k:second(args),
 111     n:third(args),
 112     if length(args)=3 then
 113       (
 114       zb_out:Zeilberger(zb_in,k,n)
 115       )
 116     else
 117       (
 118       zb_out:fourth(args)
 119       ),
 120     if length(zb_out) = 0 then
 121       (
 122       if zb_prove_detail>=PROOF_LOW then
 123         (
 124         print("Zeilberger's algorithm could not find a recurrence for the given order."),
 125         print("This DOES NOT mean that such a recurrence with the given order does not exist."),
 126         print("Zeilberger's algorithm DOES NOT always find the minimal order recurrence"),
 127         print("but it will find a recurrence for a higher order if a recurrence exists."),
 128         print("Suggestion: "),
 129         print("Sometimes rewriting the summand can produce a lower order recurrence."),
 130         print("There is no proof for this case.")
 131         ),
 132
 133       return(false)
 134       )
 135     else
 136       if zb_out=[NON_PROPER_HYPERGEOMETRIC] then
 137         (
 138         if zb_prove_detail>= PROOF_LOW then
 139            (
 140            print(zb_in, " is not proper hypergeometric in ", n, " and ", k),
 141            print("There is no proof for this case.")
 142            ),
 143         return(false)
 144         )
 145       else
 146        if length(zb_out) = 1 then
 147          (
 148          if zb_prove_detail>=PROOF_MEDIUM then
 149            (
 150             print("The result contains one recurrence for ", zb_in, ": "),
 151             print(" "),
 152             zb_meaning(zb_in,k,n,zb_out[1][1],zb_out[1][2]),
 153             print(" "),
 154             print("which we can prove by dividing both members of the equality by ", zb_in),
 155             print("and checking the resulting equality between rational functions.")
 156             ),
 157          zb_red : zb_reduced_meaning(zb_in,k,n,zb_out[1][1],zb_out[1][2]),
 158          if zb_prove_detail>= PROOF_HIGH then
 159             (
 160             print("Namely it is equivalent to test the equality between: "),
 161
 162             print(zb_red[1], " and ", zb_red[2]),
 163
 164             print(" ")
 165             ),
 166          return(zb_test_equality(zb_red))
 167          )
 168        else
 169          (
 170          proof : true,
 171          print("The result contains ", length(zb_out),
 172                " recurrences for ", zb_in, ": "),
 173          print(" "),
 174          for i : 1 thru length(zb_out) do
 175            (
 176            if zb_prove_detail>=PROOF_MEDIUM then
 177              (
 178              print("(",i,")"),
 179              zb_meaning(zb_in,k,n,zb_out[i][1],zb_out[i][2]),
 180              print(" "),
 181              print("which we can proved by dividing both members of the equality by ", zb_in),
 182              print("and checking the resulting equality between rational functions.")
 183              ),
 184
 185              zb_red : zb_reduced_meaning(zb_in,k,n,zb_out[1][1],zb_out[1][2]),
 186
 187
 188            if zb_prove_detail >= PROOF_HIGH then
 189               (
 190               print("Namely it is equivalent to test the equality between: "),
 191               print(zb_red[1], " and ", zb_red[2]),
 192               print(" ")
 193               ),
 194            if(zb_test_equality(zb_red)) then
 195              print("which has been tested to be true")
 196            else
 197              (
 198              print("which has been tested to be FALSE!!!"),
 199              proof: false
 200              ),
 201            print("------------------------------------------------------------------------")
 202            ),
 203          return(proof)
 204         )
 205     );
 206
 207
 208
 209 /* It tests the result of "parGosper"                                               */
 210 /* As input it takes a list of quadruples of the form :                             */
 211 /* [hypergeometric term, summation variable, recurrence variable, recurrence order] */
 212 /*                                                                                  */
 213 /* Remark: The level of verbosity is decided by the value of "zb_prove_detail"      */
 214
 215 zb_test(test_set) :=
 216   block([i,res,zb_prove_res,zb_res],
 217
 218     res : [],
 219     if zb_prove_detail >= PROOF_LOW then
 220       print("This benchmark contains : ", length(test_set), " elements"),
 221     for i : 1 thru length(test_set) do
 222       (
 223       if zb_prove_detail>= PROOF_LOW then
 224         (
 225         print("(", i,")"),
 226         print("computing the solution...")
 227         ),
 228       zb_res : parGosper(test_set[i][1],
 229                          test_set[i][2],test_set[i][3],
 230                          test_set[i][4]),
 231
 232       if zb_prove_detail >= PROOF_LOW then
 233         if zb_res = [] then
 234            print("no solution")
 235         else
 236            if zb_res = [NON_PROPER_HYPERGEOMETRIC] then
 237               print("the input is not hypergeometric")
 238            else
 239               print("non-empty solution found"),
 240
 241       if zb_prove_detail >= PROOF_LOW then
 242         print("checking the solution..."),
 243       zb_prove_res : zb_prove(test_set[i][1],test_set[i][2],test_set[i][3],zb_res),
 244       res : endcons(zb_prove_res,res),
 245       if zb_prove_res then
 246         (
 247         if zb_prove_detail >= PROOF_LOW then
 248           print("test passed")
 249         )
 250       else
 251         (
 252         test_flag : false,
 253         if zb_prove_detail >= PROOF_LOW then
 254           print("test failed!")
 255         ),
 256       print("---------------------------------------------------------------")
 257       ), /* end for */
 258      if apply("and",res) then
 259        (
 260        if zb_prove_detail>= PROOF_LOW then
 261          print("all tests passed"),
 262        return(true)
 263        )
 264      else
 265         (
 266         if zb_prove_detail>= PROOF_LOW then
 267           print("some test was not passed!"),
 268          return(false)
 269         )
 270      );
 271