val lemma_mem_count' (#a: eqtype) (s: seq a) (f: (a -> Tot bool))
    : Lemma (requires (forall (i: nat{i < length s}). f (index s i)))
      (ensures (forall (x: a). mem x s ==> f x))
      (decreases (length s))
let rec lemma_mem_count' (#a:eqtype) (s:seq a) (f:a -> Tot bool)
: Lemma
  (requires (forall (i:nat{i<length s}). f (index s i)))
  (ensures (forall (x:a). mem x s ==> f x))
  (decreases (length s))
= if length s = 0
  then ()
  else (let t = i:nat{i<length (tail s)} in
        cut (forall (i:t). index (tail s) i = index s (i + 1));
        lemma_mem_count' (tail s) f)
val lemma_mem_count' (#a: eqtype) (s: seq a) (f: (a -> Tot bool))
    : Lemma (requires (forall (i: nat{i < length s}). f (index s i)))
      (ensures (forall (x: a). mem x s ==> f x))
      (decreases (length s))
let rec lemma_mem_count' (#a: eqtype) (s: seq a) (f: (a -> Tot bool))
    : Lemma (requires (forall (i: nat{i < length s}). f (index s i)))
      (ensures (forall (x: a). mem x s ==> f x))
      (decreases (length s)) =
if length s = 0
then ()
else
  (let t = i: nat{i < length (tail s)} in
    cut (forall (i: t). index (tail s) i = index s (i + 1));
    lemma_mem_count' (tail s) f)
FStar.Seq.Properties.fst.checked
prims.fst.checked FStar.Squash.fsti.checked FStar.Seq.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Properties.fst.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
FStar.Seq.Properties.fst
Prims.eqtype FStar.Seq.Base.seq Prims.bool Prims.op_Equality Prims.int FStar.Seq.Base.length FStar.Seq.Properties.lemma_mem_count' FStar.Seq.Properties.tail Prims.unit Prims.cut Prims.l_Forall Prims.b2t FStar.Seq.Base.index Prims.op_Addition Prims.nat Prims.op_LessThan Prims.squash Prims.l_imp FStar.Seq.Properties.mem Prims.Nil FStar.Pervasives.pattern
(*
   Copyright 2008-2014 Nikhil Swamy and Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module FStar.Seq.Properties

open FStar.Seq.Base
module Seq = FStar.Seq.Base

let lemma_append_inj_l #_ s1 s2 t1 t2 i =
  assert (index s1 i == (index (append s1 s2) i));
  assert (index t1 i == (index (append t1 t2) i))

let lemma_append_inj_r #_ s1 s2 t1 t2 i =
  assert (index s2 i == (index (append s1 s2) (i + length s1)));
  assert (index t2 i == (index (append t1 t2) (i + length t1)))

let lemma_append_len_disj #_ s1 s2 t1 t2 =
  cut (length (append s1 s2) == length s1 + length s2);
  cut (length (append t1 t2) == length t1 + length t2)

let lemma_append_inj #_ s1 s2 t1 t2 =
  lemma_append_len_disj s1 s2 t1 t2;
  FStar.Classical.forall_intro #(i:nat{i < length s1}) #(fun i -> index s1 i == index t1 i) (lemma_append_inj_l s1 s2 t1 t2);
  FStar.Classical.forall_intro #(i:nat{i < length s2}) #(fun i -> index s2 i == index t2 i) (lemma_append_inj_r s1 s2 t1 t2)

let lemma_head_append #_ _ _ = ()

let lemma_tail_append #_ s1 s2 = cut (equal (tail (append s1 s2)) (append (tail s1) s2))

let lemma_cons_inj #_ v1 v2 s1 s2 =
  let t1 = create 1 v1 in
  let t2 = create 1 v2 in
  lemma_append_inj t1 s1 t2 s2;
  assert(index t1 0 == index t2 0)

let lemma_split #_ s i =
  cut (equal (append (fst (split s i)) (snd (split s i)))  s)

let rec mem_index' (#a:eqtype) (x:a) (s:seq a)
    : Lemma (requires (mem x s))
            (ensures (exists i. index s i == x))
            (decreases (length s))
    = if length s = 0 then ()
      else if head s = x then ()
      else mem_index' x (tail s)

let mem_index = mem_index'

let lemma_slice_append #_ _ _ = ()

let rec lemma_slice_first_in_append' (#a:Type) (s1:seq a) (s2:seq a)
  (i:nat{i <= length s1})
: Lemma
  (ensures (equal (slice (append s1 s2) i (length (append s1 s2))) (append (slice s1 i (length s1)) s2)))
  (decreases (length s1))
= if i = 0 then ()
  else lemma_slice_first_in_append' (tail s1) s2 (i - 1)

let lemma_slice_first_in_append = lemma_slice_first_in_append'

let slice_upd #_ s i j k v =
  lemma_eq_intro (slice (upd s k v) i j) (slice s i j)

let upd_slice #_ s i j k v =
  lemma_eq_intro (upd (slice s i j) k v) (slice (upd s (i + k) v) i j)

let lemma_append_cons #_ _ _ = ()

let lemma_tl #_ _ _ = ()

let rec sorted_feq' (#a:Type)
               (f g : (a -> a -> Tot bool))
               (s:seq a{forall x y. f x y == g x y})
   : Lemma (ensures (sorted f s <==> sorted g s))
           (decreases (length s))
   = if length s <= 1 then ()
     else sorted_feq' f g (tail s)

let sorted_feq = sorted_feq'

let rec lemma_append_count' (#a:eqtype) (lo:seq a) (hi:seq a)
: Lemma
  (requires True)
  (ensures (forall x. count x (append lo hi) = (count x lo + count x hi)))
  (decreases (length lo))
= if length lo = 0
  then cut (equal (append lo hi) hi)
  else (cut (equal (cons (head lo) (append (tail lo) hi))
                (append lo hi));
        lemma_append_count' (tail lo) hi;
        let tl_l_h = append (tail lo) hi in
        let lh = cons (head lo) tl_l_h in
        cut (equal (tail lh) tl_l_h))

let lemma_append_count = lemma_append_count'

let lemma_append_count_aux #_ _ lo hi = lemma_append_count lo hi

let lemma_mem_inversion #_ _ = ()

let rec lemma_mem_count' (#a:eqtype) (s:seq a) (f:a -> Tot bool)
: Lemma
  (requires (forall (i:nat{i<length s}). f (index s i)))
  (ensures (forall (x:a). mem x s ==> f x))
val lemma_mem_count' (#a: eqtype) (s: seq a) (f: (a -> Tot bool))
    : Lemma (requires (forall (i: nat{i < length s}). f (index s i)))
      (ensures (forall (x: a). mem x s ==> f x))
      (decreases (length s))
s: FStar.Seq.Base.seq a -> f: (_: a -> Prims.bool)
  -> FStar.Pervasives.Lemma
      (requires forall (i: Prims.nat{i < FStar.Seq.Base.length s}). f (FStar.Seq.Base.index s i))
      (ensures forall (x: a). FStar.Seq.Properties.mem x s ==> f x)
      (decreases FStar.Seq.Base.length s)