|
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-1 END 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 - 1 Rule? (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 - 1 Rule? (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 - 1 Rule? (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 - 1 Rule? (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 - 1 Rule? (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 - 1 Rule? (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. |