Sequence partial sums lemma

Sandbox.fst

module Sandbox


open FStar.Seq
open FStar.IntegerIntervals

let rec subseq_from_indices (#n: nat) (s: seq nat {length s == n})
                                    (h: seq (under n))
  : Tot (seq nat) (decreases length h) = 
  if length h = 0 then empty
  else cons (index s (index h 0)) (subseq_from_indices s (tail h))

let rec subseq_from_indices_equality #n (s1 s2: (s:seq nat{length s == n}))
                                        (h: seq (under n))
  : Lemma (requires forall (i: under (length h)). index s1 (index h i) == index s2 (index h i))
          (ensures subseq_from_indices s1 h == subseq_from_indices s2 h) 
          (decreases length h) = 
  if length h > 1 then subseq_from_indices_equality s1 s2 (tail h)

let subseq_from_indices_tail #n (s: seq nat{length s == n})
                                (h: seq (under n){ length h > 0 })
  : Lemma (ensures tail (subseq_from_indices s h) == subseq_from_indices s (tail h))
          (decreases length h) = // trivial matter but faster than eq_elim call 
    lemma_eq_elim (tail (subseq_from_indices s h)) (subseq_from_indices s (tail h))

let rec sum_among (#n: nat) (s: seq nat{length s == n})
                          (h: seq (under n))
  : Tot nat (decreases length h) =
  if length h = 0 then 0
  else (index s (head h)) + (sum_among s (tail h))

let rec sum_among_lemma (#n: nat) (s1 s2: (z:seq nat{length z == n}))
                            (h: seq (under n))
  : Lemma (requires forall (i: under (length h)). index s1 (index h i) == index s2 (index h i))
          (ensures sum_among s1 h == sum_among s2 h)
          (decreases length h) = 
  if length h > 1 then sum_among_lemma s1 s2 (tail h) 

let rec seq_sum (x: seq nat) : Tot nat (decreases length x) = 
  if length x = 0 then 0 else (head x) + seq_sum (tail x)
 
let rec partial_sum_lemma (#n: nat) (s1 s2: (z:seq nat{length z=n})) 
                          (h: seq (under n)) 
                          (k: under (length h))
  : Lemma (requires forall (i: under (length h)). 
                      ((i <> k) ==> (index s1 (index h i) == index s2 (index h i))) /\
                      ((i == k) ==> index s1 (index h i) < index s2 (index h i)))
          (ensures sum_among s1 h < sum_among s2 h) 
          (decreases length h) =
  if length h > 1 then begin
    if k = 0 then begin
      assert (forall (j: under (length h){j > 0}). index s1 (index h j) == index s2 (index h j)); 
      sum_among_lemma s1 s2 (tail h);
      assert (sum_among s1 (tail h) == sum_among s2 (tail h));
      ()
    end
    else partial_sum_lemma s1 s2 (tail h) (k-1)
  end // this is ok

let rec subseq_lemma (#n: nat) (s1 s2: (z:seq nat{length z=n})) 
                       (h: seq (under n)) 
                       (k: under (length h))
  : Lemma (requires forall (i: under (length h)). 
                      ((i <> k) ==> (index s1 (index h i) == index s2 (index h i))) /\
                      ((i == k) ==> index s1 (index h i) < index s2 (index h i)))
          (ensures seq_sum (subseq_from_indices s1 h) < seq_sum (subseq_from_indices s2 h)) 
          (decreases length h) =
  if length h > 1 then begin
    subseq_from_indices_tail s1 h; 
    subseq_from_indices_tail s2 h; 
    if k = 0 then subseq_from_indices_equality s1 s2 (tail h) 
             else subseq_lemma s1 s2 (tail h) (k-1) 
  end // this is also ok