[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# [PVS-Help] Question

 Hi, I've got a question regarding proof subgoals generated. My aim is to prove the following:verify_for: THEORY   BEGIN          i,n,m,y: VAR nat    count(i,n): RECURSIVE nat =    (if n=0 then 0      elsif i=0 then count(1,n)     elsif i=n then n     else i+count(i+1,n)     endif)     MEASURE i    x: VAR posint     form_sum: AXIOM count(y,n) = (n-y+1)*(n+y)/2     difference: THEOREM x<=n AND x-1>=0 IMPLIES count(x-1,n)-count(x,n) = x-1END verify_for-------------The proof looked like this:  |-------{1}   FORALL (n: nat, x: posint):        x <= n AND x - 1 >= 0 IMPLIES count(x - 1, n) - count(x, n) = x - 1Rule? (induct "x")Inducting on x on formula 1,this yields  3 subgoals: difference.1 :    |-------{1}   x!1 > 0{2}   FORALL (n: nat):        x!1 <= n AND x!1 - 1 >= 0 IMPLIES         count(x!1 - 1, n) - count(x!1, n) = x!1 - 1Rule? (skolem!)Skolemizing,this simplifies to: difference.1 :    |-------[1]   x!1 > 0{2}   x!1 <= n!1 AND x!1 - 1 >= 0 IMPLIES       count(x!1 - 1, n!1) - count(x!1, n!1) = x!1 - 1Rule? (use "form_sum")Using lemma form_sum,this simplifies to: difference.1 :  {-1}  count(x!1, n!1) = (n!1 - x!1 + 1) * (n!1 + x!1) / 2  |-------[1]   x!1 > 0[2]   x!1 <= n!1 AND x!1 - 1 > = 0 IMPLIES       count(x!1 - 1, n!1) - count(x!1, n!1) = x!1 - 1Rule? (lemma "form_sum")Applying form_sum this simplifies to: difference.1 :  {-1}  FORALL (n, y: nat): count(y, n) = (n - y + 1) * (n + y) / 2[-2]  count(x!1, n!1) = (n!1 - x!1 + 1) * (n!1 + x!1) / 2  |-------[1]   x!1 > 0[2]   x!1 <= n!1 AND x!1 - 1 >= 0 IMPLIES       count(x!1 - 1, n!1) - count(x!1, n!1) = x!1 - 1Rule? (inst -1 "n!1" "x!1-1")Instantiating the top quantifier in -1 with the terms:  n!1, x!1-1,this simplifies to: difference.1 :  {-1}  count(x!1 - 1, n!1) = (n!1 - (x!1 - 1) + 1) * (n!1 + (x!1 - 1)) / 2[-2]  count(x!1, n!1) = (n!1 - x!1 + 1) * (n!1 + x!1) / 2  |-------[1]   x!1 > 0[2]   x!1 <= n!1 AND x!1 - 1 >= 0 IMPLIES  & nbsp;    count(x!1 - 1, n!1) - count(x!1, n!1) = x!1 - 1Rule? (assert)Simplifying, rewriting, and recording with decision procedures,This completes the proof of difference.1.difference.2 :    |-------{1}   0 > 0 IMPLIES       (FORALL (n: nat):          0 <= n AND 0 - 1 >= 0 IMPLIES           count(0 - 1, n) - count(0, n) = 0 - 1)Rule? (assert)Simplifying, rewriting, and recording with decision procedures,This completes the proof of difference.2.difference.3 :  ...This completes the proof of difference.3.Q.E.D.-----------My question is, why would difference.2 be generated as a subgoal when x is specified to be a positive integer in the first place? In an attempt to get over and done with this proof, I inserted the command (assert) but I'm still troubled over why it was generated in the first place.Thx.With Windows Live, you can organize, edit, and share your photos.