%%%    NAME/LOGIN-ID    Camil Staps / s4498062
%%%    ACKNOWLEDGMENTS:

th_E: 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_E_0: LEMMA (FORALL (k:nat): k>=1 IMPLIES fac(k) < fac(k+1))

thm_E_1: THEOREM (FORALL (k:nat): 1 <= fac(k))
thm_E_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_E_3: LEMMA  (FORALL (m:nat, n:nat): tfac(m, n) = n * fac(m))

%%%
%%% On the strength of this lemma, we can prove the correctness of tfac.

th_E_4: THEOREM  (FORALL (k:nat): fac(k) = tfac(k, 1))

%%%
%%% Below, we'll do the same standard development for iterative the Fibonacci function.
%%% Except this time, YOU have to find the appropriate lemma!  Although there are several
%%% reasonable possibilities for the needed lemma, it is not easy to think of one.
%%%
%%% Remember that the lemma must GENERALIZE the desired result.
%%%

fib(n:nat): RECURSIVE nat =
  (IF    n = 0 THEN 1
   ELSIF n = 1 THEN 1
               ELSE fib(n - 1) + fib(n - 2)
   ENDIF)
  MEASURE n

%%%
%%% Tail-recursive version of fib.
%%%

tfib(n:nat, m:nat, p:nat): RECURSIVE nat =
  (IF n = 0
    THEN m
    ELSE tfib(n - 1, p, p + m)
    ENDIF)
  MEASURE n

%%%
%%% YOU will need to discover a nontrivial lemma to prove thm.
%%% Place your lemma just below, before thm_E_6.
%%%

lem_E_Camil_2: LEMMA
  (FORALL (i:nat, m:nat, p:nat):
    tfib(i, m, p) =
      IF    i = 0 THEN m
      ELSIF i = 1 THEN p
                  ELSE fib(i-2)*m + fib(i-1)*p
      ENDIF)

thm_E_6: THEOREM
  (FORALL (i:nat):
    tfib(i, 1, 1) = fib(i))

END th_E