val permutation_from_equal_counts
      (#a:eqtype)
      (s0:seq a) (s1:seq a{(forall x. count x s0 == count x s1)})
  : Tot (seqperm s0 s1)
let rec permutation_from_equal_counts (#a:eqtype) (s0:seq a) (s1:seq a{(forall x. count x s0 == count x s1)})
  : Tot (seqperm s0 s1)
        (decreases (Seq.length s0))
  = if Seq.length s0 = 0
    then (
      let f : index_fun s0 = fun i -> i in
      reveal_is_permutation_pats s0 s1 f;
      equal_counts_empty s0 s1;
      f
    ) else (
      count_head s0;
      assert (count (Seq.head s0) s0 > 0);
      let pfx, sfx = find (Seq.head s0) s1 in
      introduce forall x. count x (Seq.tail s0) == count x (Seq.append pfx sfx)
      with (
        if x = Seq.head s0
        then  (
          calc (eq2 #int) {
            count x (Seq.tail s0) <: int;
          (==) {
                 assert (s0 `Seq.equal` Seq.cons (Seq.head s0) (Seq.tail s0));
                 lemma_append_count_aux (Seq.head s0) (Seq.create 1 (Seq.head s0)) (Seq.tail s0);
                 count_singleton_one x
               }
            count x s0 - 1 <: int;
          (==) {}
            count x s1 - 1 <: int;
          (==) {}
            count x (Seq.append pfx (Seq.cons (Seq.head s0) sfx)) - 1 <: int;
          (==) { lemma_append_count_aux x pfx (Seq.cons (Seq.head s0) sfx) }
            count x pfx + count x (Seq.cons (Seq.head s0) sfx) - 1 <: int;
          (==) { lemma_append_count_aux x (Seq.create 1 (Seq.head s0)) sfx }
            count x pfx + (count x (Seq.create 1 (Seq.head s0)) + count x sfx) - 1 <: int;
          (==) { count_singleton_one x }
            count x pfx + count x sfx <: int;
          (==) { lemma_append_count_aux x pfx sfx }
            count x (Seq.append pfx sfx) <: int;
          }
        )
        else (
          calc (==) {
            count x (Seq.tail s0);
           (==) {
                  assert (s0 `Seq.equal` Seq.cons (Seq.head s0) (Seq.tail s0));
                  lemma_append_count_aux x (Seq.create 1 (Seq.head s0)) (Seq.tail s0);
                  count_singleton_zero x (Seq.head s0)
                }
            count x s0;
           (==) { }
            count x s1;
           (==) { }
            count x (Seq.append pfx (Seq.cons (Seq.head s0) sfx));
           (==) { lemma_append_count_aux x pfx (Seq.cons (Seq.head s0) sfx) }
            count x pfx + count x (Seq.cons (Seq.head s0) sfx);
          (==) { lemma_append_count_aux x (Seq.create 1 (Seq.head s0)) sfx }
            count x pfx + (count x (Seq.create 1 (Seq.head s0)) + count x sfx) ;
          (==) { count_singleton_zero x (Seq.head s0) }
            count x pfx + count x sfx;
          (==) { lemma_append_count_aux x pfx sfx }
            count x (Seq.append pfx sfx);
          }
        )
      );
      let s1' = (Seq.append pfx sfx) in
      let f' = permutation_from_equal_counts (Seq.tail s0) s1'  in
      reveal_is_permutation_pats (Seq.tail s0) s1' f';
      let n = Seq.length pfx in
      let f : index_fun s0 = adapt_index_fun s0 f' n in
      assert (Seq.length s0 == Seq.length s1);
      let len_eq : squash (Seq.length s0 == Seq.length s1) = () in
      assert (forall x y. x <> y ==> f' x <> f' y);
      let neq =
      introduce forall x y. x <> y ==> f x <> f y
        with (introduce _ ==> _
            with _. (
              if f x = n || f y = n
              then ()
              else if f' (x - 1) < n
              then (
                assert (f x == f' (x - 1));
                if f' (y - 1) < n
                then assert (f y == f' (y - 1))
                else assert (f y == f' (y - 1) + 1)
              )
              else (
                assert (f x == f' (x - 1) + 1);
                if f' (y - 1) < n
                then assert (f y == f' (y - 1))
                else assert (f y == f' (y - 1) + 1)
              )
            )
        )
      in
      let perm_prop =
        introduce forall (i:nat{i < Seq.length s0}). Seq.index s0 i == Seq.index s1 (f i)
        with (
          if i = 0 then ()
          else if f' (i - 1) < n
          then (
            assert (f i == f' (i - 1));
            assert (Seq.index (Seq.tail s0) (i - 1) ==
                    Seq.index s1' (f' (i - 1)))
          )
          else (
            assert (f i = f' (i - 1) + 1);
            assert (Seq.index (Seq.tail s0) (i - 1) ==
                    Seq.index s1' (f' (i - 1)))
          )
        )
      in
      introduce_is_permutation s0 s1 f len_eq neq perm_prop;
      f)
val permutation_from_equal_counts
      (#a:eqtype)
      (s0:seq a) (s1:seq a{(forall x. count x s0 == count x s1)})
  : Tot (seqperm s0 s1)
let rec permutation_from_equal_counts
      (#a: eqtype)
      (s0: seq a)
      (s1: seq a {(forall x. count x s0 == count x s1)})
    : Tot (seqperm s0 s1) (decreases (Seq.length s0)) =
if Seq.length s0 = 0
then
  (let f:index_fun s0 = fun i -> i in
    reveal_is_permutation_pats s0 s1 f;
    equal_counts_empty s0 s1;
    f)
else
  (count_head s0;
    assert (count (Seq.head s0) s0 > 0);
    let pfx, sfx = find (Seq.head s0) s1 in
    introduce forall x . count x (Seq.tail s0) == count x (Seq.append pfx sfx)
    with (if x = Seq.head s0
      then
        (calc (eq2 #int) {
            count x (Seq.tail s0) <: int;
            ( == ) { (assert (s0 `Seq.equal` (Seq.cons (Seq.head s0) (Seq.tail s0)));
              lemma_append_count_aux (Seq.head s0) (Seq.create 1 (Seq.head s0)) (Seq.tail s0);
              count_singleton_one x) }
            count x s0 - 1 <: int;
            ( == ) { () }
            count x s1 - 1 <: int;
            ( == ) { () }
            count x (Seq.append pfx (Seq.cons (Seq.head s0) sfx)) - 1 <: int;
            ( == ) { lemma_append_count_aux x pfx (Seq.cons (Seq.head s0) sfx) }
            count x pfx + count x (Seq.cons (Seq.head s0) sfx) - 1 <: int;
            ( == ) { lemma_append_count_aux x (Seq.create 1 (Seq.head s0)) sfx }
            count x pfx + (count x (Seq.create 1 (Seq.head s0)) + count x sfx) - 1 <: int;
            ( == ) { count_singleton_one x }
            count x pfx + count x sfx <: int;
            ( == ) { lemma_append_count_aux x pfx sfx }
            count x (Seq.append pfx sfx) <: int;
          })
      else
        (calc ( == ) {
            count x (Seq.tail s0);
            ( == ) { (assert (s0 `Seq.equal` (Seq.cons (Seq.head s0) (Seq.tail s0)));
              lemma_append_count_aux x (Seq.create 1 (Seq.head s0)) (Seq.tail s0);
              count_singleton_zero x (Seq.head s0)) }
            count x s0;
            ( == ) { () }
            count x s1;
            ( == ) { () }
            count x (Seq.append pfx (Seq.cons (Seq.head s0) sfx));
            ( == ) { lemma_append_count_aux x pfx (Seq.cons (Seq.head s0) sfx) }
            count x pfx + count x (Seq.cons (Seq.head s0) sfx);
            ( == ) { lemma_append_count_aux x (Seq.create 1 (Seq.head s0)) sfx }
            count x pfx + (count x (Seq.create 1 (Seq.head s0)) + count x sfx);
            ( == ) { count_singleton_zero x (Seq.head s0) }
            count x pfx + count x sfx;
            ( == ) { lemma_append_count_aux x pfx sfx }
            count x (Seq.append pfx sfx);
          }));
    let s1' = (Seq.append pfx sfx) in
    let f' = permutation_from_equal_counts (Seq.tail s0) s1' in
    reveal_is_permutation_pats (Seq.tail s0) s1' f';
    let n = Seq.length pfx in
    let f:index_fun s0 = adapt_index_fun s0 f' n in
    assert (Seq.length s0 == Seq.length s1);
    let len_eq:squash (Seq.length s0 == Seq.length s1) = () in
    assert (forall x y. x <> y ==> f' x <> f' y);
    let neq =
      introduce forall x y . x <> y ==> f x <> f y
      with (introduce _ ==> _
        with _. (if f x = n || f y = n
          then ()
          else
            if f' (x - 1) < n
            then
              (assert (f x == f' (x - 1));
                if f' (y - 1) < n
                then assert (f y == f' (y - 1))
                else assert (f y == f' (y - 1) + 1))
            else
              (assert (f x == f' (x - 1) + 1);
                if f' (y - 1) < n
                then assert (f y == f' (y - 1))
                else assert (f y == f' (y - 1) + 1))))
    in
    let perm_prop =
      introduce forall (i: nat{i < Seq.length s0}) . Seq.index s0 i == Seq.index s1 (f i)
      with (if i = 0
        then ()
        else
          if f' (i - 1) < n
          then
            (assert (f i == f' (i - 1));
              assert (Seq.index (Seq.tail s0) (i - 1) == Seq.index s1' (f' (i - 1))))
          else
            (assert (f i = f' (i - 1) + 1);
              assert (Seq.index (Seq.tail s0) (i - 1) == Seq.index s1' (f' (i - 1)))))
    in
    introduce_is_permutation s0 s1 f len_eq neq perm_prop;
    f)
FStar.Seq.Permutation.fst.checked
prims.fst.checked FStar.Seq.Equiv.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 FStar.Algebra.CommMonoid.Equiv.fst.checked
FStar.Seq.Permutation.fst
Prims.eqtype FStar.Seq.Base.seq Prims.l_Forall Prims.eq2 Prims.nat FStar.Seq.Properties.count Prims.op_Equality Prims.int FStar.Seq.Base.length Prims.unit FStar.Seq.Permutation.equal_counts_empty FStar.Seq.Permutation.reveal_is_permutation_pats FStar.Seq.Permutation.index_fun FStar.IntegerIntervals.under Prims.bool FStar.Seq.Permutation.introduce_is_permutation Prims.squash Prims.b2t Prims.op_LessThan FStar.Seq.Base.index FStar.Classical.Sugar.forall_intro Prims.op_Subtraction Prims._assert FStar.Seq.Properties.tail Prims.l_or FStar.IntegerIntervals.interval_condition Prims.op_Addition Prims.l_imp Prims.op_disEquality FStar.Classical.Sugar.implies_intro Prims.op_BarBar Prims.op_GreaterThanOrEqual FStar.Seq.Permutation.adapt_index_fun FStar.Seq.Permutation.seqperm FStar.Seq.Permutation.permutation_from_equal_counts FStar.Seq.Base.append FStar.Seq.Properties.head FStar.Calc.calc_finish Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step FStar.Seq.Base.create FStar.Seq.Properties.cons FStar.Calc.calc_init FStar.Calc.calc_pack FStar.Seq.Permutation.count_singleton_one FStar.Seq.Properties.lemma_append_count_aux FStar.Seq.Base.equal FStar.Seq.Permutation.count_singleton_zero FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.fst FStar.Pervasives.Native.snd FStar.Seq.Permutation.find Prims.op_GreaterThan FStar.Seq.Permutation.count_head
(*
   Copyright 2021-2022 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.

   Authors: N. Swamy, A. Rastogi, A. Rozanov
*)
module FStar.Seq.Permutation
open FStar.Seq
open FStar.Calc

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

           Seq.length s0 == Seq.length s1 /\

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

           (forall (i:nat{i < Seq.length s0}).
              Seq.index s0 i == Seq.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 < Seq.length (Seq.append s0 s1))
    (ensures (
      let s = Seq.append s0 (Seq.cons x s1) in
      let s' = Seq.append s0 s1 in
      let n = Seq.length s0 in
      if j < n then Seq.index s' j == Seq.index s j
      else Seq.index s' j == Seq.index s (j + 1)
    ))
  = let n = Seq.length (Seq.append s0 s1) in
    if j < n then ()
    else ()

#push-options "--fuel 2 --ifuel 0 --z3rlimit_factor 2"
let rec find (#a:eqtype) (x:a) (s:seq a{ count x s > 0 })
  : Tot (frags:(seq a & seq a) {
      let s' = Seq.append (fst frags) (snd frags) in
      let n = Seq.length (fst frags) in
      s `Seq.equal` Seq.append (fst frags) (Seq.cons x (snd frags))
    }) (decreases (Seq.length s))
  = if Seq.head s = x
    then Seq.empty, Seq.tail s
    else (
      let pfx, sfx = find x (Seq.tail s) in
      assert (Seq.equal (Seq.tail s)
                        (Seq.append pfx (Seq.cons x sfx)));
      assert (Seq.equal s
                        (Seq.cons (Seq.head s) (Seq.tail s)));
      Seq.cons (Seq.head s) pfx, sfx
    )
#pop-options

let introduce_is_permutation (#a:Type) (s0:seq a) (s1:seq a)
                             (f:index_fun s0)
                             (_:squash (Seq.length s0 == Seq.length s1))
                             (_:squash (forall x y. x <> y ==> f x <> f y))
                             (_:squash (forall (i:nat{i < Seq.length s0}). Seq.index s0 i == Seq.index s1 (f i)))
   : Lemma
     (ensures
       is_permutation s0 s1 f)
   = reveal_is_permutation_nopats s0 s1 f

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

           Seq.length s0 == Seq.length s1 /\

           (forall x y. {:pattern f x; f y } x <> y ==> f x <> f y) /\

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

let adapt_index_fun (s:Seq.seq 'a { Seq.length s > 0 })
                    (f:index_fun (Seq.tail s))
                    (n:nat{n < Seq.length s})
  : index_fun s
  = fun i -> if i = 0
          then n
          else if f (i - 1) < n
          then f (i - 1)
          else f (i - 1) + 1

let count_singleton_one (#a:eqtype) (x:a)
  : Lemma (count x (Seq.create 1 x) == 1)
  = ()
let count_singleton_zero (#a:eqtype) (x y:a)
  : Lemma (x =!= y ==> count x (Seq.create 1 y) == 0)
  = ()
let equal_counts_empty (#a:eqtype) (s0 s1:seq a)
  : Lemma
    (requires Seq.length s0 == 0 /\ (forall x. count x s0 == count x s1))
    (ensures  Seq.length s1 == 0)
  = if Seq.length s1 > 0 then
    assert (count (Seq.head s1) s1 > 0)
let count_head (#a:eqtype) (x:seq a{ Seq.length x > 0 })
  : Lemma (count (Seq.head x) x > 0)
  = ()


#push-options "--fuel 0"
#restart-solver
let rec permutation_from_equal_counts (#a:eqtype) (s0:seq a) (s1:seq a{(forall x. count x s0 == count x s1)})
  : Tot (seqperm s0 s1)
val permutation_from_equal_counts
      (#a:eqtype)
      (s0:seq a) (s1:seq a{(forall x. count x s0 == count x s1)})
  : Tot (seqperm s0 s1)

    s0: FStar.Seq.Base.seq a ->
    s1:
      FStar.Seq.Base.seq a
        {forall (x: a). FStar.Seq.Properties.count x s0 == FStar.Seq.Properties.count x s1}
  -> Prims.Tot (FStar.Seq.Permutation.seqperm s0 s1)