val lemma_filter_correct1 (#a: Type) (f:a -> bool) (s:seq a) (i:seq_index (filter f s)):
Lemma (requires (True))
      (ensures (f (index (filter f s) i) = true))
      [SMTPat (f (index (filter f s) i))]
val lemma_filter_correct1 (#a: Type) (f:a -> bool) (s:seq a) (i:seq_index (filter f s)):
Lemma (requires (True))
      (ensures (f (index (filter f s) i) = true))
      [SMTPat (f (index (filter f s) i))]
let lemma_filter_correct1 (#a: Type) (f:a -> bool) (s:seq a) (i:seq_index (filter f s)):
  Lemma (requires (True))
        (ensures (f (index (filter f s) i) = true)) = lemma_filter_correct1_aux f s i
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

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

let lemma_suffix_index (#a:Type) (s:seq a) (i:nat{i <= length s}) (j:nat{j < i}):
  Lemma (requires (True))
        (ensures (index (suffix s i) j == index s (length s - i + j))) =
  lemma_index_slice s (length s - i) (length s) j

let lemma_prefix_suffix (#a:Type) (s:seq a) (i:nat{i <= length s}):
  Lemma (requires (True))
        (ensures (append (prefix s i) (suffix s (length s - i)) == s)) =
  assert(equal (append (prefix s i) (suffix s (length s - i))) s);
  ()

type proj (#a:Type u#a): seq a -> seq a -> Type u#a =
  | PrjEmpty: proj (empty #a) (empty #a)
  | PrjIncl: ss: seq a -> s:seq a -> prf:proj ss s -> x:a -> proj (append1 ss x) (append1 s x)
  | PrjSkip: ss: seq a -> s:seq a -> prf:proj ss s -> x:a -> proj ss (append1 s x)

let rec proj_index_map_aux (#a:Type) (ss: seq a) (s: seq a) (prf:proj ss s) (i:seq_index ss) :
  Tot (j:seq_index s{index s j == index ss i})
  (decreases (length s))
  =
  let n = length s in
  let ns = length ss in
  match prf with
  | PrjIncl ss' s' prf' e ->
    if i = ns - 1 then
      n - 1
    else
      proj_index_map_aux ss' s' prf' i
  | PrjSkip ss' s' prf' x -> proj_index_map_aux ss' s' prf' i

let proj_index_map (#a:Type) (ss s: seq a) (prf: proj ss s) (i: seq_index ss) =
  proj_index_map_aux ss s prf i

(* the mapping we construct above is monotonic *)
let rec lemma_proj_monotonic_aux (#a:Type) (ss s: seq a) (prf: proj ss s) (i1 i2: seq_index ss):
  Lemma (requires (i1 < i2))
        (ensures (proj_index_map ss s prf i1 < proj_index_map ss s prf i2))
        (decreases prf) =
  match prf with
  | PrjIncl ss' s' prf' _ ->
    if i2 = length ss - 1 then ()
    else lemma_proj_monotonic_aux ss' s' prf' i1 i2
  | PrjSkip ss' s' prf' _ -> lemma_proj_monotonic_aux ss' s' prf' i1 i2

let lemma_proj_monotonic (#a:Type) (ss s: seq a) (prf: proj ss s) (i1 i2: seq_index ss):
  Lemma (requires (i1 < i2))
        (ensures (proj_index_map ss s prf i1 < proj_index_map ss s prf i2)) =
  lemma_proj_monotonic_aux ss s prf i1 i2

let rec lemma_proj_length_aux (#a:Type) (ss s: seq a) (prf: proj ss s):
  Lemma (requires (True))
        (ensures (length ss <= length s))
        (decreases prf) =
  match prf with
  | PrjEmpty -> ()
  | PrjIncl ss' s' prf' _ -> lemma_proj_length_aux ss' s' prf'
  | PrjSkip ss' s' prf' _ -> lemma_proj_length_aux ss' s' prf'

let lemma_as_squash #a #b (lem: (a -> Lemma b)) (x:a)
  : GTot (squash b)
  = lem x

let lemma_proj_length (#a:Type) (ss: seq a) (s:seq a{proj ss s}):
  Lemma (requires (True))
        (ensures (length ss <= length s)) =
  bind_squash () (lemma_as_squash #(proj ss s) #(length ss <= length s) (lemma_proj_length_aux ss s))

let rec filter_aux (#a:Type) (f:a -> bool) (s:seq a) : Tot (seq a)
  (decreases (length s)) =
  let n = length s in
  if n = 0 then empty
  else
    let e = index s (n - 1) in
    if f e then
      append1 (filter_aux f (prefix s (n - 1))) e
    else
      filter_aux f (prefix s (n - 1))

let filter (#a:Type) (f:a -> bool) (s:seq a) : Tot (seq a)  = filter_aux f s

let rec filter_is_proj_aux (#a:Type) (f:a -> bool) (s:seq a): Tot (proj (filter f s) s)
  (decreases (length s)) =
  let n = length s in
  let fs = filter f s in
  if n = 0 then (
    lemma_empty s;
    PrjEmpty #a
  )
  else (

    let e = index s (n - 1) in
    let s' = prefix s (n - 1) in
    let fs' = filter f s' in
    assert (equal (append1 s' e) s);
    let prf = filter_is_proj_aux f s' in
    if f e then
      PrjIncl fs' s' prf e
    else
      PrjSkip fs' s' prf e
  )

let lemma_filter_is_proj (#a:Type) (f:a -> bool) (s:seq a):
  squash (proj (filter f s) s) = return_squash (filter_is_proj_aux f s)

let filter_is_proj_prf (#a:Type) (f:a -> bool) (s: seq a) = filter_is_proj_aux f s

(* every index in the filtered sequence satisfies the filter predicate *)
let rec lemma_filter_correct1_aux (#a: Type) (f:a -> bool) (s:seq a) (i:seq_index (filter f s)):
  Lemma (requires (True))
        (ensures (f (index (filter f s) i) = true))
        (decreases (length s)) =
  let n = length s in
  let fs = filter f s in
  if n = 0 then ()
  else
    let s' = prefix s (n - 1) in
    let e = index s (n - 1) in
    if f e then
      if i = (length fs) - 1 then ()
      else
        lemma_filter_correct1_aux f s' i
    else
      lemma_filter_correct1_aux f s' i
/
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

    f: (_: a -> Prims.bool) ->
    s: FStar.Seq.Base.seq a ->
    i: Zeta.SeqAux.seq_index (Zeta.SeqAux.filter f s)
  -> FStar.Pervasives.Lemma (ensures f (FStar.Seq.Base.index (Zeta.SeqAux.filter f s) i) = true)
      [SMTPat (f (FStar.Seq.Base.index (Zeta.SeqAux.filter f s) i))]
Prims.bool FStar.Seq.Base.seq Zeta.SeqAux.seq_index Zeta.SeqAux.filter Zeta.SeqAux.lemma_filter_correct1_aux Prims.unit Prims.l_True Prims.squash Prims.b2t Prims.op_Equality FStar.Seq.Base.index Prims.Nil FStar.Pervasives.pattern
let lemma_filter_correct1 (#a: Type) (f: (a -> bool)) (s: seq a) (i: seq_index (filter f s))
    : Lemma (requires (True)) (ensures (f (index (filter f s) i) = true)) =
  
lemma_filter_correct1_aux f s i