1 files changed, 109 insertions, 0 deletions
diff --git a/assignment7/E.pvs b/assignment7/E.pvs
new file mode 100644
index 0000000..5f02082
--- /dev/null
+++ b/assignment7/E.pvs
@@ -0,0 +1,109 @@
+%%%    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
+