val lift_swap_cons (#a: eqtype) (n: nat) (h: a) (xs: list a) (s: swap (length xs + n))
    : Lemma (requires n <= s)
      (ensures apply_swap_aux n (h :: xs) (s + 1) == h :: (apply_swap_aux n xs s))
      (decreases xs)
let rec lift_swap_cons (#a:eqtype) (n:nat) (h:a) (xs:list a) (s:swap (length xs + n)) : Lemma
  (requires n <= s)
  (ensures apply_swap_aux n (h::xs) (s + 1) == h::(apply_swap_aux n xs s))
  (decreases xs)
  =
  match xs with
  | [] -> ()
  | x::xt -> if n < s then lift_swap_cons (n + 1) x xt s
val lift_swap_cons (#a: eqtype) (n: nat) (h: a) (xs: list a) (s: swap (length xs + n))
    : Lemma (requires n <= s)
      (ensures apply_swap_aux n (h :: xs) (s + 1) == h :: (apply_swap_aux n xs s))
      (decreases xs)
let rec lift_swap_cons (#a: eqtype) (n: nat) (h: a) (xs: list a) (s: swap (length xs + n))
    : Lemma (requires n <= s)
      (ensures apply_swap_aux n (h :: xs) (s + 1) == h :: (apply_swap_aux n xs s))
      (decreases xs) =
match xs with
| [] -> ()
| x :: xt -> if n < s then lift_swap_cons (n + 1) x xt s
FStar.Tactics.CanonCommSwaps.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
FStar.Tactics.CanonCommSwaps.fst
Prims.eqtype Prims.nat Prims.list FStar.Tactics.CanonCommSwaps.swap Prims.op_Addition FStar.List.Tot.Base.length Prims.op_LessThan FStar.Tactics.CanonCommSwaps.lift_swap_cons Prims.bool Prims.unit Prims.b2t Prims.op_LessThanOrEqual Prims.squash Prims.eq2 FStar.Tactics.CanonCommSwaps.apply_swap_aux Prims.Cons Prims.Nil FStar.Pervasives.pattern
(*
   Copyright 2008-2018 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.Tactics.CanonCommSwaps

open FStar.List.Tot

let swap (n:nat) :Type = x:nat{x < n-1}

let rec apply_swap_aux (#a:Type) (n:nat) (xs:list a) (s:swap (length xs + n)) :
    Pure (list a) (requires True)
                  (ensures (fun zs -> length zs == length xs)) (decreases xs) =
  match xs with
  | [] | [_] -> xs
  | x1 :: x2 :: xs' -> if n = (s <: nat)
                       then x2 :: x1 :: xs'
                       else x1 :: apply_swap_aux (n+1) (x2 :: xs') s

let apply_swap (#a:Type) = apply_swap_aux #a 0

let rec apply_swaps (#a:Type) (xs:list a) (ss:list (swap (length xs))) :
    Pure (list a) (requires True)
                  (ensures (fun zs -> length zs == length xs)) (decreases ss) =
  match ss with
  | [] -> xs
  | s::ss' -> apply_swaps (apply_swap xs s) ss'

let equal_counts (#a:eqtype) (xs ys:list a) : Type0 =
  (forall (e:a).{:pattern (count e xs) \/ (count e ys)} count e xs == count e ys)

let extend_equal_counts (#a:eqtype) (h:a) (xs ys:list a) : Lemma
  (requires equal_counts xs ys)
  (ensures equal_counts (h::xs) (h::ys))
  =
  ()

let retract_equal_counts (#a:eqtype) (h:a) (xs ys:list a) : Lemma
  (requires equal_counts (h::xs) (h::ys))
  (ensures equal_counts xs ys)
  =
  assert (forall (e:a).{:pattern (count e xs) \/ (count e ys)} count e (h::xs) == count e (h::ys))

unfold let swap_for (#a:eqtype) (xs:list a) = swap (length xs)
unfold let swaps_for (#a:eqtype) (xs:list a) = list (swap_for xs)

let rec append_swaps (#a:eqtype) (xs:list a) (ss1 ss2:swaps_for xs) : Lemma
  (ensures apply_swaps xs (ss1 @ ss2) == apply_swaps (apply_swaps xs ss1) ss2)
  (decreases ss1)
  =
  match ss1 with
  | [] -> ()
  | h::t -> append_swaps (apply_swap xs h) t ss2

let rec lift_swap_cons (#a:eqtype) (n:nat) (h:a) (xs:list a) (s:swap (length xs + n)) : Lemma
  (requires n <= s)
  (ensures apply_swap_aux n (h::xs) (s + 1) == h::(apply_swap_aux n xs s))
  (decreases xs)
val lift_swap_cons (#a: eqtype) (n: nat) (h: a) (xs: list a) (s: swap (length xs + n))
    : Lemma (requires n <= s)
      (ensures apply_swap_aux n (h :: xs) (s + 1) == h :: (apply_swap_aux n xs s))
      (decreases xs)

    n: Prims.nat ->
    h: a ->
    xs: Prims.list a ->
    s: FStar.Tactics.CanonCommSwaps.swap (FStar.List.Tot.Base.length xs + n)
  -> FStar.Pervasives.Lemma (requires n <= s)
      (ensures
        FStar.Tactics.CanonCommSwaps.apply_swap_aux n (h :: xs) (s + 1) ==
        h :: FStar.Tactics.CanonCommSwaps.apply_swap_aux n xs s)
      (decreases xs)