val count_singleton_zero (#a: eqtype) (x y: a) : Lemma (x =!= y ==> count x (singleton y) == 0)
let count_singleton_zero (#a:eqtype) (x y:a)
  : Lemma (x =!= y ==> count x (singleton y) == 0)
  = reveal_opaque (`%count) (count #a)
val count_singleton_zero (#a: eqtype) (x y: a) : Lemma (x =!= y ==> count x (singleton y) == 0)
let count_singleton_zero (#a: eqtype) (x y: a) : Lemma (x =!= y ==> count x (singleton y) == 0) =
reveal_opaque (`%count) (count #a)
FStar.Sequence.Permutation.fst.checked
prims.fst.checked FStar.Sequence.Util.fst.checked FStar.Sequence.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked FStar.Calc.fsti.checked FStar.Algebra.CommMonoid.fst.checked
FStar.Sequence.Permutation.fst
Prims.eqtype FStar.Pervasives.reveal_opaque FStar.Sequence.Base.seq Prims.nat FStar.Sequence.Util.count Prims.unit Prims.l_True Prims.squash Prims.l_imp Prims.l_not Prims.eq2 Prims.int FStar.Sequence.Base.singleton Prims.Nil FStar.Pervasives.pattern
(*
   Copyright 2021 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.

   Author: N. Swamy
*)
module FStar.Sequence.Permutation
open FStar.Sequence
open FStar.Calc
open FStar.Sequence.Util
module S = FStar.Sequence

////////////////////////////////////////////////////////////////////////////////
[@@"opaque_to_smt"]
let is_permutation (#a:Type) (s0:seq a) (s1:seq a) (f:index_fun s0) =
  S.length s0 == S.length s1 /\
  (forall x y. // {:pattern f x; f y}
  x <> y ==> f x <> f y) /\
  (forall (i:nat{i < S.length s0}). // {:pattern (S.index s1 (f i))}
      S.index s0 i == S.index s1 (f i))

let reveal_is_permutation #a (s0 s1:seq a) (f:index_fun s0)
  = reveal_opaque (`%is_permutation) (is_permutation s0 s1 f)

let reveal_is_permutation_nopats (#a:Type) (s0 s1:seq a) (f:index_fun s0)
  : Lemma (is_permutation s0 s1 f <==>

           S.length s0 == S.length s1 /\

           (forall x y. x <> y ==> f x <> f y) /\

           (forall (i:nat{i < S.length s0}).
              S.index s0 i == S.index s1 (f i)))
   = reveal_is_permutation s0 s1 f



let split3_index (#a:eqtype) (s0:seq a) (x:a) (s1:seq a) (j:nat)
  : Lemma
    (requires j < S.length (S.append s0 s1))
    (ensures (
      let s = S.append s0 (cons x s1) in
      let s' = S.append s0 s1 in
      let n = S.length s0 in
      if j < n then S.index s' j == S.index s j
      else S.index s' j == S.index s (j + 1)
    ))
  = let n = S.length (S.append s0 s1) in
    if j < n then ()
    else ()


let rec find (#a:eqtype) (x:a) (s:seq a{ count x s > 0 })
  : Tot (frags:(seq a & seq a) {
      let s' = S.append (fst frags) (snd frags) in
      let n = S.length (fst frags) in
      s `S.equal` S.append (fst frags) (cons x (snd frags))
    }) (decreases (S.length s))
  = reveal_opaque (`%count) (count #a);
    if head s = x
    then S.empty, tail s
    else (
      let pfx, sfx = find x (tail s) in
      assert (S.equal (tail s)
                        (S.append pfx (cons x sfx)));
      assert (S.equal s
                        (cons (head s) (tail s)));
      cons (head s) pfx, sfx
    )

let count_singleton_one (#a:eqtype) (x:a)
  : Lemma (count x (singleton x) == 1)
  = reveal_opaque (`%count) (count #a)
let count_singleton_zero (#a:eqtype) (x y:a)
val count_singleton_zero (#a: eqtype) (x y: a) : Lemma (x =!= y ==> count x (singleton y) == 0)
x: a -> y: a
  -> FStar.Pervasives.Lemma
    (ensures ~(x == y) ==> FStar.Sequence.Util.count x (FStar.Sequence.Base.singleton y) == 0)