Adding pascals identity and prefix sums

proofs/pascal_triangle.dfy

@@ -0,0 +1,7 @@
+include "../testcases/pascal_triangle.dfy"
+
+lemma {:induction false} combination_symmetry(n: nat, k: nat)
+    requires k <= n
+    ensures combination(n, k) == combination(n, n - k)
+{
+}

proofs/prefix_sum.dfy

@@ -0,0 +1,31 @@
+include "../testcases/prefix_sum.dfy"
+
+// --- tiny helpers ----------------------------------------------------------
+
+lemma sum_seq_append(a: seq<int>, b: seq<int>)
+  ensures sum_seq(a + b) == sum_seq(a) + sum_seq(b)
+  decreases a
+{
+
+}
+
+
+// snoc means appending one element to the end of a sequence
+// prefix[0..i+1] = prefix[0..i] + [arr[i]]
+// use the append lemma above
+lemma sum_seq_prefix_snoc(arr: seq<int>, i: int)
+  requires 0 <= i < |arr|
+  ensures  sum_seq(arr[0..i+1]) == sum_seq(arr[0..i]) + arr[i]
+{
+
+}
+
+// Write out the algorithm for a prefix sum. Use the lemma above
+// to prove that your algorithm creates the next element in the prefix sum.
+
+method prefix_sum_impl(arr: seq<int>) returns (out: seq<int>)
+  ensures |out| == |arr|
+  ensures forall i :: 0 <= i < |arr| ==> out[i] == sum_seq(arr[0..i+1])
+{
+
+}

testcases/pascal_triangle.dfy

@@ -0,0 +1,8 @@
+function {:induction false} combination(n: nat, k: nat): (result: nat)
+    requires k <= n
+    decreases n, k
+{
+    if k == 0 || k == n then 1
+    else if k > n then 0
+    else combination(n - 1, k - 1) + combination(n - 1, k)
+}

testcases/prefix_sum.dfy

@@ -0,0 +1,6 @@
+// --- spec used in proofs ---------------------------------------------------
+function {:induction false} sum_seq(s: seq<int>): int
+  decreases s
+{
+  if |s| == 0 then 0 else s[0] + sum_seq(s[1..])
+}