val foldm_snoc_append (#a:Type) (#eq:CE.equiv a) (m:CE.cm a eq) (s1 s2: seq a)
  : Lemma
    (ensures eq.eq (foldm_snoc m (append s1 s2))
                   (m.mult (foldm_snoc m s1) (foldm_snoc m s2)))
let rec foldm_snoc_append #a #eq (m:CE.cm a eq) (s1 s2: seq a)
  : Lemma
    (ensures eq.eq (foldm_snoc m (append s1 s2))
                   (m.mult (foldm_snoc m s1) (foldm_snoc m s2)))
    (decreases (Seq.length s2))
  = CE.elim_eq_laws eq;
    elim_monoid_laws m;
    if Seq.length s2 = 0
    then assert (Seq.append s1 s2 `Seq.equal` s1)
    else (
      let s2', last = Seq.un_snoc s2 in
      calc (eq.eq)
      {
        foldm_snoc m (append s1 s2);
        (eq.eq) { assert (Seq.equal (append s1 s2)
                         (Seq.snoc (append s1 s2') last)) }
        foldm_snoc m (Seq.snoc (append s1 s2') last);
        (eq.eq) { assert (Seq.equal (fst (Seq.un_snoc (append s1 s2))) (append s1 s2')) }

        m.mult last (foldm_snoc m (append s1 s2'));
        (eq.eq) { foldm_snoc_append m s1 s2';
                  m.congruence last (foldm_snoc m (append s1 s2'))
                               last (m.mult (foldm_snoc m s1) (foldm_snoc m s2')) }
        m.mult last (m.mult (foldm_snoc m s1) (foldm_snoc m s2'));
        (eq.eq) { x_yz_to_y_xz m last (foldm_snoc m s1) (foldm_snoc m s2') }
        m.mult (foldm_snoc m s1) (m.mult last (foldm_snoc m s2'));
        (eq.eq) { }
        m.mult (foldm_snoc m s1) (foldm_snoc m s2);
      })
val foldm_snoc_append (#a:Type) (#eq:CE.equiv a) (m:CE.cm a eq) (s1 s2: seq a)
  : Lemma
    (ensures eq.eq (foldm_snoc m (append s1 s2))
                   (m.mult (foldm_snoc m s1) (foldm_snoc m s2)))
let rec foldm_snoc_append #a #eq (m: CE.cm a eq) (s1: seq a) (s2: seq a)
    : Lemma
      (ensures eq.eq (foldm_snoc m (append s1 s2)) (m.mult (foldm_snoc m s1) (foldm_snoc m s2)))
      (decreases (Seq.length s2)) =
CE.elim_eq_laws eq;
elim_monoid_laws m;
if Seq.length s2 = 0
then assert ((Seq.append s1 s2) `Seq.equal` s1)
else
  (let s2', last = Seq.un_snoc s2 in
    calc (eq.eq) {
      foldm_snoc m (append s1 s2);
      (eq.eq) { assert (Seq.equal (append s1 s2) (Seq.snoc (append s1 s2') last)) }
      foldm_snoc m (Seq.snoc (append s1 s2') last);
      (eq.eq) { assert (Seq.equal (fst (Seq.un_snoc (append s1 s2))) (append s1 s2')) }
      m.mult last (foldm_snoc m (append s1 s2'));
      (eq.eq) { (foldm_snoc_append m s1 s2';
        m.congruence last
          (foldm_snoc m (append s1 s2'))
          last
          (m.mult (foldm_snoc m s1) (foldm_snoc m s2'))) }
      m.mult last (m.mult (foldm_snoc m s1) (foldm_snoc m s2'));
      (eq.eq) { x_yz_to_y_xz m last (foldm_snoc m s1) (foldm_snoc m s2') }
      m.mult (foldm_snoc m s1) (m.mult last (foldm_snoc m s2'));
      (eq.eq) { () }
      m.mult (foldm_snoc m s1) (foldm_snoc m s2);
    })
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
FStar.Algebra.CommMonoid.Equiv.equiv FStar.Algebra.CommMonoid.Equiv.cm FStar.Seq.Base.seq Prims.op_Equality Prims.int FStar.Seq.Base.length Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.append Prims.bool FStar.Calc.calc_finish FStar.Algebra.CommMonoid.Equiv.__proj__EQ__item__eq FStar.Seq.Permutation.foldm_snoc FStar.Algebra.CommMonoid.Equiv.__proj__CM__item__mult Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Seq.Properties.snoc FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash FStar.Pervasives.Native.fst FStar.Seq.Properties.un_snoc FStar.Algebra.CommMonoid.Equiv.__proj__CM__item__congruence FStar.Seq.Permutation.foldm_snoc_append FStar.Seq.Permutation.x_yz_to_y_xz FStar.Pervasives.Native.tuple2 Prims.eq2 FStar.Pervasives.Native.snd FStar.Seq.Permutation.elim_monoid_laws FStar.Algebra.CommMonoid.Equiv.elim_eq_laws Prims.l_True FStar.Pervasives.pattern
(*
   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)
        (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)
#pop-options


module CE = FStar.Algebra.CommMonoid.Equiv

let elim_monoid_laws #a #eq (m:CE.cm a eq)
  : Lemma (
          (forall x y. {:pattern m.mult x y}  eq.eq (m.mult x y) (m.mult y x)) /\
          (forall x y z.{:pattern (m.mult x (m.mult y z))} eq.eq (m.mult x (m.mult y z)) (m.mult (m.mult x y) z)) /\
          (forall x.{:pattern (m.mult x m.unit)} eq.eq (m.mult x m.unit) x)
    )
  = introduce forall x y. eq.eq (m.mult x y) (m.mult y x)
    with ( m.commutativity x y );

    introduce forall x y z. eq.eq (m.mult x (m.mult y z)) (m.mult (m.mult x y) z)
    with ( m.associativity x y z;
           eq.symmetry (m.mult (m.mult x y) z) (m.mult x (m.mult y z)) );

    introduce forall x. eq.eq (m.mult x m.unit) x
    with ( CE.right_identity eq m x )

let rec foldm_snoc_unit_seq (#a:Type) (#eq:CE.equiv a) (m:CE.cm a eq) (s:Seq.seq a)
  : Lemma (requires Seq.equal s (Seq.create (Seq.length s) m.unit))
          (ensures eq.eq (foldm_snoc m s) m.unit)
          (decreases Seq.length s)
  = CE.elim_eq_laws eq;
    elim_monoid_laws m;
    if Seq.length s = 0
    then ()
    else let s_tl, _ = un_snoc s in
         foldm_snoc_unit_seq m s_tl

#push-options "--fuel 2"
let foldm_snoc_singleton (#a:_) #eq (m:CE.cm a eq) (x:a)
  : Lemma (eq.eq (foldm_snoc m (Seq.create 1 x)) x)
  = elim_monoid_laws m
#pop-options

let x_yz_to_y_xz #a #eq (m:CE.cm a eq) (x y z:a)
  : Lemma ((x `m.mult` (y `m.mult` z))
             `eq.eq`
           (y `m.mult` (x `m.mult` z)))
  = CE.elim_eq_laws eq;
    elim_monoid_laws m;
    calc (eq.eq) {
      x `m.mult` (y `m.mult` z);
      (eq.eq) { m.commutativity x (y `m.mult` z) }
      (y `m.mult` z) `m.mult` x;
      (eq.eq) { m.associativity y z x }
      y `m.mult` (z `m.mult` x);
      (eq.eq) { m.congruence y (z `m.mult` x) y (x `m.mult` z) }
      y `m.mult` (x `m.mult` z);
    }

#push-options "--fuel 1 --ifuel 0 --z3rlimit_factor 2"
let rec foldm_snoc_append #a #eq (m:CE.cm a eq) (s1 s2: seq a)
  : Lemma
    (ensures eq.eq (foldm_snoc m (append s1 s2))
                   (m.mult (foldm_snoc m s1) (foldm_snoc m s2)))
val foldm_snoc_append (#a:Type) (#eq:CE.equiv a) (m:CE.cm a eq) (s1 s2: seq a)
  : Lemma
    (ensures eq.eq (foldm_snoc m (append s1 s2))
                   (m.mult (foldm_snoc m s1) (foldm_snoc m s2)))
m: FStar.Algebra.CommMonoid.Equiv.cm a eq -> s1: FStar.Seq.Base.seq a -> s2: FStar.Seq.Base.seq a
  -> FStar.Pervasives.Lemma
      (ensures
        EQ?.eq eq
          (FStar.Seq.Permutation.foldm_snoc m (FStar.Seq.Base.append s1 s2))
          (CM?.mult m
              (FStar.Seq.Permutation.foldm_snoc m s1)
              (FStar.Seq.Permutation.foldm_snoc m s2))) (decreases FStar.Seq.Base.length s2)