worked on chapter 5

chap_5/e5_1.dfy

@@ -0,0 +1,34 @@
+function More(x: int): int {
+if x <= 0 then 1 else More(x - 2) + 3
+}
+
+lemma {:induction false} Increasing(x: int)
+    decreases x
+    ensures x < More(x)
+{ // 0:
+  // x is an int, x can be any value.
+    if x <= 0 { // 1: x <= 0 Therefore More(x) == 1 => x <= 0 < 1 == More(x) => x < More(x)
+    } else { // 2: Work back to basecase, x > 0 ==> repeated x - 2 eventually enters basecase. 
+        Increasing(x-2);
+    }
+}
+
+method ExampleLemmaUse(a: int) {
+    // var b := More(a);
+    // Increasing(a);
+    // Increasing(b);
+    // var c := More(b);
+    // assert 2 <= c - a;
+
+    Increasing(a); // this call is along all control paths
+    var b := More(a);
+    Increasing(b);
+    b := More(b);
+    // Increasing(b);
+    // if a < 1000 {
+    //     Increasing(More(a)); // we learn More(a) < More(More(a))
+    //     // only here, i.e., when a < 1000
+    //     assert 2 <= b - a; // this verifies
+    // }
+    assert 2 <= b - a; // this does not verify
+}

chap_5/e5_3.dfy

@@ -0,0 +1,83 @@
+lemma ex_1a(x: int, y: int) 
+    ensures 5*x - 3 * (y + x) == 2*x - 3*y
+{
+    calc {
+        5 * x -3 * (y + x);
+    ==  // Distributivity of Multiplication
+        5 * x -3 * y - 3 * x;
+    == // Commutativity
+        5 * x - 3 * x - 3 * y;
+    == // Addition
+        2 * x - 3*y;
+    }
+}
+lemma ex_1b(x: int, y: int) 
+    ensures 2 * (x + 4*y + 7) - 10 == 2*x + 8*y + 4
+{
+    calc {
+        2 * (x + 4*y + 7) - 10;
+    == // Distributivity of Multiplication
+        2 * x + 2 * 4 * y + 2 * 7 - 10;
+    == // Multiplication of integers
+        2 * x + 8 * y + 14 - 10;
+    == // Addition of integers
+        2*x + 8*y + 4;
+    }
+}
+
+lemma ex_1c(x: int, y: int) 
+    ensures 7*x + 5 < (x + 3) * (x + 4)
+    {
+    calc {
+        7*x + 5;
+    < 
+        7*x + 12;
+    <= {assert x * x >= 0;}
+        7*x + 12 + x * x;
+    ==
+        x * x + 3 * x + 4 * x + 12;
+    ==
+        (x + 3) * (x + 4);
+    }
+}
+
+// E5.6
+
+function Ack(m: nat, n: nat): nat
+    decreases m, n
+{
+    if m == 0 then
+        n + 1
+    else if n == 0 then
+        Ack(m - 1, 1)
+    else
+        Ack(m - 1, Ack(m, n - 1))
+}
+
+lemma {:induction false} IncreasingAck(n: nat)
+    ensures Ack(1, n) == n + 2
+{
+    if n == 0 {
+        calc {
+            Ack(1, n);
+        ==
+            Ack(0, 1);
+        ==
+            2;
+        }
+    } else {
+        calc {
+            Ack(1, n);
+        == // last else branch of Ack
+            Ack(0, Ack(1, n - 1));
+        == { IncreasingAck(n - 1);}
+            Ack(0, n - 1 + 2);
+        ==
+            Ack(0, n + 1);
+        ==
+            n + 1 + 1;
+        ==
+            n + 2;
+        }
+    }
+}

chap_5/e5_6.dfy

@@ -0,0 +1,65 @@
+function Mult(x: nat, y: nat): nat {
+    if y == 0 then 0 else x + Mult(x, y - 1)
+}
+
+lemma {:induction false} MultCommutative(x: nat, y: nat)
+    ensures Mult(x, y) == Mult(y, x)
+{
+    if x == y {
+    } else if x == 0 {
+        MultCommutative(x, y - 1);
+    } else if y < x {
+        MultCommutative(y, x);
+    } else {
+        calc {
+            Mult(x, y);
+        == //Def. Mult
+            x + Mult(x, y - 1);
+        == {MultCommutative(x, y - 1);} 
+            x + Mult(y - 1, x);
+        ==
+            x + y - 1 + Mult(y - 1, x - 1);
+        ==
+            x - 1 + y + Mult(y - 1, x - 1);
+        == {MultCommutative(x - 1, y - 1);}
+            x - 1 + y + Mult(x - 1, y - 1);
+        ==
+            y + Mult(x - 1, y);
+        == {MultCommutative(x - 1, y);}
+            y + Mult(y, x - 1);
+        ==
+            Mult(y, x);
+
+        }
+    }
+}
+
+lemma {:induction false} MultCommutative'(x: nat, y: nat) 
+    ensures Mult(x, y) == Mult(y, x)
+    decreases x + y
+{
+    if x == y {// Trivial
+    } else if x == 0 {
+        MultCommutative'(x, y - 1);
+    } else if y == 0 {
+        MultCommutative'(y, x - 1);
+    } else { // x < y
+        calc {
+            Mult(x, y);
+        == // def. Mult
+            x + Mult(x, y - 1);
+        == {MultCommutative'(y - 1, x);}
+            x + Mult(y - 1, x) ;
+        == // def. Mult
+            x + y - 1 + Mult(y - 1, x - 1);
+        == {MultCommutative'(y - 1, x  -1);}
+            y + x - 1 + Mult(x - 1, y - 1);
+        == // def. Mult
+            y + Mult(x - 1, y);
+        == {MultCommutative'(x - 1, y);}
+            y + Mult(y, x - 1);
+        == // def. Mult
+            Mult(y, x);
+        }
+    }
+}

chap_5/e5_7.dfy

@@ -0,0 +1,90 @@
+datatype Tree<T> =  Leaf(data: T)
+                    | Node(left: Tree<T>, right: Tree<T>)
+
+function Mirror<T>(t: Tree<T>): Tree<T> {
+    match t
+    case Leaf(_) => t
+    case Node(left, right) 
+        => Node(Mirror(right), Mirror(left))
+}
+
+lemma {:induction false} MirrorMirror<T>(t: Tree<T>)
+    ensures Mirror(Mirror(t)) == t
+{
+    match t
+    case Leaf(_) =>
+        // trivial
+    case Node(left, right) =>
+        calc {
+            Mirror(Mirror(Node(left, right)));
+        == 
+            Mirror(Node(Mirror(right), Mirror(left)));
+        ==  
+            Node(Mirror(Mirror(left)),Mirror(Mirror(right)));
+        == {MirrorMirror(left); MirrorMirror(right);}
+            Node(left, right);
+        }
+}
+
+function Size<T>(t: Tree<T>): nat {
+    match t
+    case Leaf(_) => 1
+    case Node(left, right) => Size(left) + Size(right)
+}
+
+lemma {:induction false} MirrorSize<T>(t: Tree<T>)
+    ensures Size(Mirror(t)) == Size(t)
+{
+    match t
+    case Leaf(_) =>
+    case Node(left, right) =>
+        calc {
+            Size(Mirror(Node(left, right)));
+        ==  // def. Mirror
+            Size(Node(Mirror(right), Mirror(left)));
+        ==  // def. Size
+            Size(Mirror(right)) + Size(Mirror(left));
+        == {MirrorSize(right); MirrorSize(left);}
+            Size(right) + Size(left);
+        == // arithmatic
+            Size(left) + Size(right);
+        == // def. size
+            Size(Node(left, right));
+        }
+}
+
+method test() {
+    assert multiset([1, 2]) == multiset([2, 1]);
+}
+
+// method Seperate(a: array<int>, key: int) returns (pivot: nat)
+//     requires a.Length >= 1
+//     modifies a
+//     ensures multiset(a[..]) == multiset(old(a[..]))
+//     ensures 0 <= pivot <= a.Length
+//     ensures forall i | 0 <= i < pivot :: a[i] <= key
+//     ensures forall i | pivot <= i < a.Length :: key < a[i]
+// {
+//     var lo: nat, hi: nat := 0, a.Length - 1;
+//     while lo < hi
+//         decreases hi - lo
+//         invariant 0 <= lo <= hi < a.Length
+//         invariant forall i | 0 <= i < lo :: a[i] <= key
+//         invariant forall i | hi < i < a.Length :: key < a[i]
+//         invariant multiset(a[..]) == multiset(old(a[..]))
+//     {
+//         if a[lo] <= key {
+//             lo := lo + 1;
+//         } else if key < a[hi] {
+//             hi := hi - 1;
+//         } else {
+//             assert a[lo] in multiset(a[..]);
+//             assert a[hi] in multiset(a[..]);
+//             a[lo], a[hi] := a[hi], a[lo];
+//             assert a[lo] in multiset(a[..]);
+//             assert a[hi] in multiset(a[..]);
+//             lo := lo + 1;
+//         }
+//     }
+//     pivot := lo;
+// }

chap_5/e5_7_2.dfy

@@ -0,0 +1,134 @@
+datatype BYTree = BlueLeaf | YellowLeaf | Node(left: BYTree, right: BYTree)
+
+function ReverseColors(t: BYTree): BYTree {
+    match t
+    case BlueLeaf => YellowLeaf
+    case YellowLeaf => BlueLeaf 
+    case Node(left, right) => BYTree.Node(ReverseColors(left), ReverseColors(right))
+}
+
+lemma {:induction false} ReverseColorsInvolution(t: BYTree)
+    ensures ReverseColors(ReverseColors(t)) == t
+{     
+    match t
+    case BlueLeaf =>
+    case YellowLeaf =>
+    case Node(left, right) =>
+        calc {
+            ReverseColors(ReverseColors(Node(left,right)));
+        ==
+            ReverseColors(Node(ReverseColors(left), ReverseColors(right)));
+        ==  
+            Node(ReverseColors(ReverseColors(left)), ReverseColors(ReverseColors(right)));
+        ==  {ReverseColorsInvolution(left); ReverseColorsInvolution(right);}
+            Node(left, right);
+        }
+}
+
+function LeafCount(t: BYTree): nat 
+{
+    match t
+    case BlueLeaf | YellowLeaf => 1
+    case Node(left, right) => LeafCount(left) + LeafCount(right)
+}
+
+lemma {:induction false} ReversePreserveLeafCount(t: BYTree) 
+    ensures LeafCount(ReverseColors(t)) == LeafCount(t)
+    decreases t
+{
+    match t
+    case BlueLeaf =>
+    case YellowLeaf =>
+    case Node(left, right) => 
+        calc {
+            LeafCount(ReverseColors(Node(left, right)));
+        ==
+            LeafCount(Node(ReverseColors(left), ReverseColors(right)));
+        ==
+            LeafCount(ReverseColors(left)) + LeafCount(ReverseColors(right));
+        ==  {ReversePreserveLeafCount(left); ReversePreserveLeafCount(right);}
+            LeafCount(left) + LeafCount(right);
+        ==
+            LeafCount(Node(left, right));
+        }
+}
+
+function Oceanize(t: BYTree): BYTree {
+    match t
+        case BlueLeaf | YellowLeaf => BlueLeaf
+        case Node(left, right) => Node(Oceanize(left), Oceanize(right))
+}
+
+lemma {:induction false} IdempotentOceanize(t: BYTree) 
+    ensures Oceanize(t) == Oceanize(Oceanize(t))
+    decreases t
+{
+    match t
+    case BlueLeaf => 
+        calc {
+            Oceanize(Oceanize(BlueLeaf));
+        ==
+            Oceanize(BlueLeaf);
+        ==
+            BlueLeaf;
+        }
+    case YellowLeaf =>
+        calc {
+            Oceanize(Oceanize(YellowLeaf));
+        ==
+            Oceanize(BlueLeaf);
+        ==
+            BlueLeaf;
+        ==
+            Oceanize(YellowLeaf);
+        }
+        
+    case Node(left, right) =>
+        calc {
+            Oceanize(Node(left, right));
+        ==
+            Node(Oceanize(left), Oceanize(right));
+        ==  {IdempotentOceanize(left); IdempotentOceanize(right);}
+            Node(Oceanize(Oceanize(left)), Oceanize(Oceanize(right)));
+        ==
+            Oceanize(Node(Oceanize(left), Oceanize(right)));
+        ==
+            Oceanize(Oceanize(Node(left,right)));
+        }
+}
+
+function BlueCount(t: BYTree): nat {
+    match t
+    case BlueLeaf => 1
+    case YellowLeaf => 0
+    case Node(left, right) =>
+        BlueCount(left) + BlueCount(right)
+}
+
+lemma {:induction false} BlueCountBound(t: BYTree) 
+    ensures BlueCount(t) <= BlueCount(Oceanize(t))
+{
+    match t
+    case BlueLeaf => 
+        calc {
+            BlueCount(BlueLeaf);
+        ==
+            BlueCount(Oceanize(BlueLeaf));
+        }
+    case YellowLeaf =>
+        calc {
+            BlueCount(YellowLeaf);
+        <
+            BlueCount(BlueLeaf);
+        ==
+            BlueCount(Oceanize(YellowLeaf));
+        }
+    case Node(left, right) =>
+        calc {
+            BlueCount(Node(left, right));
+        ==
+            BlueCount(left) + BlueCount(right);
+        <= {BlueCountBound(left); BlueCountBound(right);}
+            BlueCount(Oceanize(left)) + BlueCount(Oceanize(right));
+        }
+}