val conj : f1: (_: a -> Prims.bool) -> f2: (_: a -> Prims.bool) -> x: a -> Prims.bool
let conj (#a:Type) (f1 f2: a -> bool) (x: a) =
  f1 x && f2 x
module Zeta.SeqAux

open FStar.Seq

(* Legitimate values of an index of a sequence *)
inline_for_extraction
type seq_index (#a:Type) (s:seq a) = i:nat{i < length s}

(* Prefix of a sequence *)
val prefix (#a:Type) (s:seq a) (i:nat{i <= length s}): Tot (s':seq a{length s' = i})

let hprefix (#a:Type) (s:seq a{length s > 0}): seq a = 
  prefix s (length s - 1)

let telem (#a:Type) (s:seq a{length s > 0}): a =
  index s (length s - 1)

(* append a single element to the end of a sequence *)
let append1 (#a:Type) (s:seq a) (x:a): s':(seq a){length s' = length s + 1} =
  append s (create 1 x)

val prefix_slice (#a:Type) (s:Seq.seq a) (i:nat{i <= Seq.length s})
  : Lemma (Seq.equal (prefix s i) (Seq.slice s 0 i))

val 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))
        [SMTPat (index (prefix s i) j)]

val 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))
        [SMTPat (prefix (prefix s i) j)]

val lemma_fullprefix_equal (#a:Type) (s:seq a):
  Lemma (requires (True))
        (ensures (prefix s (length s) == s))
        [SMTPat (prefix s (length s))]

val lemma_prefix_append (#a:Type) (s1 s2: seq a):
  Lemma (requires (True))
        (ensures (prefix (append s1 s2) (length s1) == s1))

let lemma_prefix1_append (#a:Type) (s: seq a) (x:a):
  Lemma (prefix (append1 s x) (length s) == s) =
  lemma_prefix_append s (create 1 x)

val 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))
        [SMTPat (hprefix s); SMTPat (prefix s (length s - 1))]

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

val lemma_prefix_create (#a:Type) (n:nat) (v:a) (i:nat{i <= n}) 
: Lemma (prefix (create n v) i == create i v)

(* is ps a prefix of s *)
let is_prefix (#a:Type) (s:seq a) (ps: seq a): Type0 =
  length ps <= length s /\
  ps == prefix s (length ps)

let prefix_of (#a:Type) (s0 s1:seq a) = is_prefix s1 s0

(* Suffix of a sequence *)
val suffix (#a:Type) (s:seq a) (i:nat{i <= length s}): Tot (s':seq a{length s' = i})

val 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)))
      [SMTPat (index (suffix s i) j)]

(* projection - a subsequence of the original sequence *)
val proj (#a:Type u#a): seq a -> seq a -> Type u#a

(* mapping from a subsequence index to the corresponding index in the base sequence *)
val proj_index_map (#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})

let proj_index_map_exists (#a:Type) (ss: seq a) (s: seq a{proj ss s}) (i:seq_index ss)
: Lemma (exists (j:seq_index s). index s j == index ss i)
= let p : squash (proj ss s) = FStar.Squash.get_proof (proj ss s) in
  let _ : squash (exists (j:seq_index s). index s j == index ss i) = 
    FStar.Squash.bind_squash p (fun p -> 
      let k = proj_index_map ss s p i in
      assert (index s k == index ss i))
  in
  ()

(* the mapping we construct above is monotonic *)
val 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))

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

(* subsequence of s obtained by applying a filter *)
val filter (#a:Type) (f:a -> bool) (s:seq a): Tot (seq a)

(* filter is a projection *)
val lemma_filter_is_proj (#a:Type) (f:a -> bool) (s:seq a)
  : squash (proj (filter f s) s)

(* constructive version of the lemma_filter_is_proj *)
val filter_is_proj_prf (#a:Type) (f:a -> bool) (s:seq a): Tot (proj (filter f s) s)

(* every index in the filtered sequence satisfies the filter predicate *)
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_correct_all (#a:Type) (f:a -> bool) (s:seq a):
Lemma (requires (True))
      (ensures (forall (i:(seq_index (filter f s))). f (index (filter f s) i) = true))

val lemma_filter_all_not (#a:Type) (f:a -> bool) (s:seq a):
Lemma (requires filter f s `equal` empty)
      (ensures forall (i:seq_index s). not (f (index s i)))

val lemma_filter_all_not_inv (#a:Type) (f:a->bool) (s:seq a)
: Lemma (requires (forall (i:seq_index s). not (f (index s i))))
        (ensures (equal (filter f s) empty))

val lemma_filter_exists (#a:Type) (f:a -> bool) (s:seq a):
Lemma (requires (exists (i:seq_index s). f (index s i)))
      (ensures (length (filter f s) > 0))

val lemma_filter_unique (#a:Type) (f:a->bool) (s: seq a) (i:seq_index s)
: Lemma (requires (f (index s i) /\ (forall j. j <> i ==> not (f (index s j)))))
        (ensures (filter f s == create 1 (index s i)))

(* mapping from filtered subseq to satisfying indexes *)
val filter_index_map (#a:Type) (f:a -> bool) (s:seq a) (i:seq_index (filter f s)):
Tot (j:seq_index s{index s j == index (filter f s) i})

(* Mapping from original seq to filtered subseq for satisfying indexes *)
val filter_index_inv_map (#a:Type) (f:a -> bool) (s:seq a) (i:seq_index s{f (index s i)}):
Tot (j:seq_index (filter f s){index s i == index (filter f s) j})

inline_for_extraction
let refine #a (f:a -> bool) = x:a{f x}

type all (#a:Type) (f:a -> bool) (s: seq a) =
forall (i:seq_index s). f (index s i)

(* if we know that every element of a seq satisfies f, then the same sequence is a sequence over
* the refinement defined by f *)
val seq_refine (#a:Type) (f:a -> bool) (s:seq a{all f s}): Tot (seq (refine f))

val lemma_seq_refine_len (#a:Type) (f:a->bool) (s:seq a{all f s}):
Lemma (requires True)
      (ensures (length (seq_refine f s) = length s))
      [SMTPat (seq_refine f s)]

val lemma_seq_refine_equal (#a:Type) (f:a->bool) (s:seq a{all f s}) (i:seq_index s):
Lemma (requires True)
      (ensures (index (seq_refine f s) i == index s i))
      [SMTPat (index (seq_refine f s) i)]

let filter_refine (#a:Type) (f:a -> bool) (s: seq a): Tot (seq (refine f)) =
let fs = filter f s in
seq_refine f fs

(* filter_index_map is injective *)
val lemma_filter_index_map_monotonic (#a:Type) (f:a -> bool) (s:seq a)
(i:seq_index (filter f s))(j:seq_index (filter f s){j > i}):
Lemma (filter_index_map f s i < filter_index_map f s j)

(* Inverse mapping is injective *)
val lemma_filter_index_inv_map_monotonic (#a:Type) (f:a -> bool) (s: seq a)
(i:seq_index s) (j: seq_index s {j > i}):
    Lemma (requires (f (index s i) /\ f (index s j)))
          (ensures (filter_index_inv_map f s i < filter_index_inv_map f s j))

val lemma_filter_maps_correct (#a:Type) (f:a -> bool) (s: seq a) (i:seq_index s):
  Lemma (requires (f (index s i)))
        (ensures (filter_index_map f s (filter_index_inv_map f s i) = i))

val lemma_filter_maps_correct2 (#a:Type) (f:a -> bool) (s: seq a) (i: seq_index (filter f s)):
  Lemma (requires(True))
        (ensures (filter_index_inv_map f s (filter_index_map f s i) = i))
        [SMTPat (filter_index_map f s i)]

val lemma_filter_empty (#a:Type) (f:a -> bool):
  Lemma (filter f (empty #a) == empty #a)

val lemma_filter_prefix (#a:Type) (f:a -> bool) (s: seq a) (ps: seq a{is_prefix s ps}):
  Lemma (is_prefix (filter f s) (filter f ps))

val lemma_filter_prefix_comm (#a:Type) (f:a->bool) (s: seq a) (i:seq_index s):
  Lemma (requires (f (index s i)))
        (ensures (filter f (prefix s i) == prefix (filter f s) (filter_index_inv_map f s i)))

val lemma_filter_prefix_comm2 (#a:Type) (f:a->bool) (s: seq a) (i:seq_index s):
  Lemma (requires (f (index s i)))
        (ensures (filter f (prefix s (i+1)) == prefix (filter f s) (1 + (filter_index_inv_map f s i))))

val lemma_filter_extend1 (#a:Type) (f:a -> bool) (s:seq a{length s > 0}):
  Lemma (requires (not (f (index s (length s - 1)))))
        (ensures (filter f s == filter f (prefix s (length s - 1))))

val lemma_filter_extend2 (#a:Type) (f:a -> bool) (s:seq a{length s > 0}):
  Lemma (requires (f (index s (length s - 1))))
        (ensures (filter f s == append1 (filter f (prefix s (length s - 1))) (index s (length s - 1))))

val lemma_filter_update_length (#a:Type) (f:a -> bool) (s:seq a) (i:seq_index s) (v:a)
  : Lemma (requires (f v == f (index s i)))
          (ensures (length (filter f s) = length (filter f (upd s i v))))
          [SMTPat (length (filter f (upd s i v)))]

val lemma_filter_update_index_eq (#a:Type) (f:a -> bool) (s:seq a) (i:seq_index s) (v:a)
  : Lemma (requires (f v /\ f (index s i)))
          (ensures (index (filter f (upd s i v)) (filter_index_inv_map f s i) == v))

(*
val lemma_filter_update_index_neq (#a:Type) (f:a -> bool) (s:seq a) (i:seq_index s) (v:a) (j:seq_index (filter f s))
  : Lemma (requires (f v = f (index s i) /\ filter_index_map f s j <> i))
          (ensures (index (filter f s) j = index (filter f (upd s i v)) j))
*)

let ext_pred (#a:Type) (f1 f2:a -> bool) =
  forall x. f1 x = f2 x

val lemma_filter_extensionality (#a:Type) (f1 f2:a -> bool) (s:seq a):
  Lemma (requires (ext_pred f1 f2))
        (ensures (filter f1 s == filter f2 s))
/
prims.fst.checked FStar.Squash.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Zeta.SeqAux.fsti
f1: (_: a -> Prims.bool) -> f2: (_: a -> Prims.bool) -> x: a -> Prims.bool
Prims.bool Prims.op_AmpAmp
let conj (#a: Type) (f1 f2: (a -> bool)) (x: a) =
  
f1 x && f2 x