val suffix (#a:Type) (s:seq a) (i:nat{i <= length s}): Tot (s':seq a{length s' = i})
val suffix (#a:Type) (s:seq a) (i:nat{i <= length s}): Tot (s':seq a{length s' = i})
let suffix (#a:Type) (s:seq a) (i:nat{i <= length s}) =
  slice s (length s - i) (length s)
module Zeta.SeqAux
#push-options "--print_universes"

open FStar.Classical
open FStar.Seq
open FStar.Squash

let prefix (#a:Type) (s:seq a) (i:nat{i <= length s}) = slice s 0 i

let prefix_slice #_ _ _ = ()

let lemma_prefix_index (#a:Type) (s:seq a) (i:nat{i <= length s}) (j:nat{j < i}):
  Lemma (requires (True))
        (ensures (index (prefix s i) j == index s j)) =
  lemma_index_slice s 0 i j

let lemma_prefix_prefix (#a:Type) (s:seq a) (i:nat{i <= length s}) (j:nat{j <= i}):
  Lemma (requires (True))
        (ensures (prefix (prefix s i) j == prefix s j)) =
  let pij = prefix (prefix s i) j in
  let pj = prefix s j in
  let pi = prefix s i in
  let aux (k:nat{k < j}):
    Lemma (index pij k == index pj k) =
    lemma_prefix_index s j k;
    lemma_prefix_index s i k;
    lemma_prefix_index pi j k
  in
  forall_intro aux; lemma_eq_intro pij pj

let lemma_fullprefix_equal (#a:Type) (s:seq a):
  Lemma (requires (True))
        (ensures (prefix s (length s) == s)) =
  let n = length s in
  let p = prefix s n in
  let aux (k:nat{k < n}):
    Lemma (index p k == index s k) =
    lemma_prefix_index s n k
  in
  forall_intro aux; lemma_eq_intro s p

let lemma_prefix_append (#a:Type) (s1 s2: seq a):
  Lemma (prefix (append s1 s2) (length s1) == s1) =
  // triggers an SMT pat that provides what we need
  assert(equal (prefix (append s1 s2) (length s1)) s1);
  ()

let lemma_hprefix_append_telem (#a:Type) (s: seq a{length s > 0}):
  Lemma (ensures (let s' = hprefix s in
                  let e = telem s in
                  s == append1 s' e)) =
  let s' = hprefix s in
  let e = telem s in
  lemma_prefix1_append s' e;
  let s2 = append1 s' e in
  assert(length s = length s2);
  let aux (i: seq_index s):
    Lemma (ensures (index s i == index s2 i))
          [SMTPat (index s i == index s2 i)] = ()
  in
  lemma_eq_intro s s2

let lemma_prefix0_empty (#a:Type) (s: seq a):
  Lemma (prefix s 0 == empty #a) = ()

let lemma_prefix_create (#a:Type) (n:nat) (v:a) (i:nat{i <= n}) 
  : Lemma (prefix (create n v) i == create i v)
  = let l1 = prefix (create n v) i in
    let l2 = create i v in
    let aux (k:nat{k < i}) : Lemma (index l1 k == index l2 k) = () in
    forall_intro aux; lemma_eq_intro l1 l2
/
prims.fst.checked FStar.Squash.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Zeta.SeqAux.fst
s: FStar.Seq.Base.seq a -> i: Prims.nat{i <= FStar.Seq.Base.length s}
  -> s': FStar.Seq.Base.seq a {FStar.Seq.Base.length s' = i}
FStar.Seq.Base.seq Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length FStar.Seq.Base.slice Prims.op_Subtraction Prims.op_Equality
let suffix (#a: Type) (s: seq a) (i: nat{i <= length s}) =
  
slice s (length s - i) (length s)