[PVS-Help] Induction Generalization

[Jiho Noh <jihonoh@xxxxxxxxxxx>]

Hi, All.

I just found this email list, and I hope I can get a help from this listing. I am taking a "Verification" class, and well this is my homework. I am not saying that 'please do my homework' here. I have tried many things, but I have no idea what else I can do. Here is the lemma (6.3c) that I have to prove. 

-----------------------
th_I: THEORY

BEGIN

%%%
%%% Standard development of iterative factorial-with-accumulator.
%%% Start with a "specification" of the factorial function.
%%%

fac(n:nat): RECURSIVE nat = 
  IF n = 0
   THEN 1
   ELSE fac(n-1) * n
  ENDIF
  MEASURE n 

%%%
%%% A few simple facts about the factorial function.
%%%

thm_6_1: THEOREM (FORALL (k:nat): 1 <= fac(k))
thm_6_2: THEOREM (FORALL (k:nat): k <= fac(k))

%%%
%%% In tfac, below, all recursive calls are in the tail position. In operational terms,
%%% tfac "improves" fac because a no space is needed for a recursion stack.  In other
%%% words, tfac is and instance of the "implementation model" for sequential execution.
%%%

tfac(n:nat, m:nat): RECURSIVE nat =
  IF n = 0
   THEN m
   ELSE tfac(n - 1, m * n)
  ENDIF
 MEASURE n


%%%
%%% We should prove, though, that tfac is equivalent to fac.  They are not "equal" because,
%%% for one thing, tfac takes two arguments and fac takes only one.  In fact, tfac(n, m)
%%% only computes fac(n) when m = 1.
%%%
%%% However, in trying to prove this, we run into a problem...

%%% In the inductive case, we'll get something like this:
%%%
%%%   [-1] fac(J) = tfac(J, 1)
%%%      |------------------------
%%%   [1]  (J+1) * fac(J) = tfac(J, J+1)
%%%
%%% To complete the proof, we need to "distribute" J+1 outside fact.  But attempting
%%% to prove this, for just "J+1" will fail.  A _generalization_ is needed...
%%%

lemma_6_3c: LEMMA  (FORALL (m:nat, n:nat, p:nat): tfac(m, n*p) = n * tfac(m, p))

---------------------
Obviously I have to use some kind of generalization procedures. I don't know what generalization in this context means and how. It will be grateful if anyone can guide me to the right path.


Jiho Noh


-- 
노지호 (Jiho Noh)
Mobile: (+1) 812-345-7891  Home(US): (+82) 070-8289-0073  Fax: (+82) 0505-507-0555
Email: jihonoh@indiana.edu