[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Induction Generalization
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.
%%% Standard development of iterative factorial-with-accumulator.
%%% Start with a "specification" of the factorial function.
fac(n:nat): RECURSIVE nat =
IF n = 0
ELSE fac(n-1) * 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
ELSE tfac(n - 1, m * 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)
%%%  (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)
Mobile: (+1) 812-345-7891 Home(US): (+82) 070-8289-0073 Fax: (+82) 0505-507-0555