// Dafny module containing functions and lemmas relating to sums of 
// sequences of integers.
  
module Sum_Through {
  
  /* Evaluates to the sum 0 + 1 + ... + n (of the natural numbers 
  ** zero through n).
  */
  function SumThrough(n: nat): nat
    decreases n
  { if n == 0 then 0 else n + SumThrough(n-1) }
  

  /* Proves the classic result about the sum 0 + 1 + 2 + ... + n.
  */
  lemma {:induction false} SumThroughLemma(n: nat)
    decreases n
    ensures SumThrough(n) == (n*(n+1)) / 2
  {
    if n == 0 {
      calc {
         SumThrough(n);
      ==   // n == 0
         SumThrough(0);
      ==   // defn of SumThrough()
         0;
      ==   // arithmetic
         (0*1) / 2;
      ==   // n == 0
         (n*(n+1)) / 2;
      }
    }
    else {
      calc {
         SumThrough(n);
      ==   // defn of SumThrough
         n + SumThrough(n-1);
      ==   { SumThroughLemma(n-1); }
           // { assert SumThrough(n-1) == ((n-1)*n) / 2; }
         n + ((n-1)*n) / 2;
      ==   // algebra
         (n*(n+1)) / 2;
      }
    }
  }
  

  /* Evaluates to the sum of the smallest n odd natural numbers,
  ** i.e., 1 + 3 + ... + 2n-1
  */
  function SumFirstOdds(n: nat): nat
    decreases n
  {
    if n == 0 then 0
    else 2*n - 1 + SumFirstOdds(n-1)
  }
  
  // Problem SUM.1
  // -------------

  /* Proves that the sum of the smallest n odd natural numbers
  ** (i.e., 1 + 3 + ... + 2n-1) is the square of n.
  */
  lemma {:induction false} SumFirstOddsLemma(n: nat)
    decreases n
    ensures SumFirstOdds(n) == n*n
  {
    // PROOF MISSING
  }
  

  /* Function that computes 1 + 2 + ... + n in a very
  ** roundabout way.
  */ 
  function GoofySumThrough(n: nat): nat
  {
    GoofySumThrough'(n, n, 0)
  }
  
  
  function {:induction false} GoofySumThrough'(n: nat, k: nat, m: nat): nat 
    decreases n, k
    //Note: Dafny is able to prove (without intervention) the next line,
    //      which corresponds to GoofySumThroughLemma'0.  It is needed
    //      in the proof of GoofySumThroughLemma'1(), but oddly, that lemma
    //      is not needed if this ensures clause is not commented out.
    //ensures n != 0 ==> GoofySumThrough'(n,k,m) == GoofySumThrough'(n,0,m+k)
    //ensures n != 0 ==> GoofySumThrough'(n,n,m) == GoofySumThrough'(n-1,n-1,m+n)
    //ensures n != 0 ==> GoofySumThrough'(n,n,m) == GoofySumThrough'(0,0,m+SumThrough(n-1))
  {
    if n == 0 then m+k
    else if k != 0 then GoofySumThrough'(n, k-1, m+1)
    else GoofySumThrough'(n-1, n-1, m)
  }

  // Problem SUM.2(a)
  // ----------------
  
  /* Proves a 0-th lemma regarding the GoofySumThrough'() function.
  */
  lemma {:induction false} GoofySumThroughLemma'0(n: nat, k: nat, m: nat)
    decreases n,k
    ensures GoofySumThrough'(n,k,m) == GoofySumThrough'(n,0,m+k)
  {
    // PROOF MISSING
  }
  
  // Problem SUM.2(b)
  // ----------------

  /* Proves a 1st lemma regarding the GoofySumThrough'() function.
  */
  lemma {:induction false} GoofySumThroughLemma'1(n: nat, m: nat)
    ensures n != 0 ==> GoofySumThrough'(n,n,m) == GoofySumThrough'(n-1,n-1,m+n)
  {
    // PROOF MISSING
  }
  
  // Problem SUM.2(c)
  // ----------------

  /* Proves a 2nd lemma regarding the GoofySumThrough'() function.
  */
  lemma {:induction false} GoofySumThroughLemma'2(n: nat, m: nat)
    ensures GoofySumThrough'(n,n,m) == m + SumThrough(n) 
  {
    // PROOF MISSING
  }
  
  /* Proves that GoofySumThrough() computes the same function
  ** as the more straightforward SumThrough().
  ** It uses the three lemmata proved above.
  */
  lemma {:induction false} GoofySumThroughTheorem(n: nat) 
    ensures GoofySumThrough(n) == SumThrough(n) 
  {
    if n == 0 {
      calc {
        GoofySumThrough(n);
      ==   // n == 0
        GoofySumThrough(0);
      ==   // defn of GoofySumThrough()
        GoofySumThrough'(0,0,0);
      ==   // defn of GoofySumThrough'()
        0;
      ==   // defn of SumThrough()
        SumThrough(0);
      ==   // n == 0
        SumThrough(n);
      }
    }
    else {
      calc {
        GoofySumThrough(n);
      ==   // defn of GoofySumThrough()
        GoofySumThrough'(n,n,0);
      ==    { GoofySumThroughLemma'0(n,n,0); }
        GoofySumThrough'(n,0,n);
      ==   // defn of GoofySumThrough'()
        GoofySumThrough'(n-1,n-1,n);
      ==   { GoofySumThroughLemma'2(n-1,n); }
        GoofySumThrough'(0,0,n+SumThrough(n-1));
      ==   // defn of GoofySumThrough'()
        n + SumThrough(n-1);
      ==   // defn of SumThrough()
        SumThrough(n);
      }
    }
  }

}