val permute_via_swaps_correct_aux
      (#b: Type)
      (p: permute b)
      (pvs: permute_via_swaps p)
      (#a: Type)
      (m: cm a)
      (vm: vmap a b)
      (xs: list var)
    : Lemma (xsdenote m vm xs == xsdenote m vm (p a vm xs))
let permute_via_swaps_correct_aux
  (#b:Type) (p:permute b) (pvs:permute_via_swaps p)
  (#a:Type) (m:cm a) (vm:vmap a b)  (xs:list var) :
    Lemma (xsdenote m vm xs == xsdenote m vm (p a vm xs)) =
  pvs vm xs;
  assert(exists ss. p a vm xs == apply_swaps xs ss);
  exists_elim (xsdenote m vm xs == xsdenote m vm (p a vm xs))
    (() <: squash (exists ss. p a vm xs == apply_swaps xs ss))
    (fun ss -> apply_swaps_correct m vm xs ss)
val permute_via_swaps_correct_aux
      (#b: Type)
      (p: permute b)
      (pvs: permute_via_swaps p)
      (#a: Type)
      (m: cm a)
      (vm: vmap a b)
      (xs: list var)
    : Lemma (xsdenote m vm xs == xsdenote m vm (p a vm xs))
let permute_via_swaps_correct_aux
      (#b: Type)
      (p: permute b)
      (pvs: permute_via_swaps p)
      (#a: Type)
      (m: cm a)
      (vm: vmap a b)
      (xs: list var)
    : Lemma (xsdenote m vm xs == xsdenote m vm (p a vm xs)) =
pvs vm xs;
assert (exists ss. p a vm xs == apply_swaps xs ss);
exists_elim (xsdenote m vm xs == xsdenote m vm (p a vm xs))
  (() <: squash (exists ss. p a vm xs == apply_swaps xs ss))
  (fun ss -> apply_swaps_correct m vm xs ss)
FStar.Tactics.CanonCommMonoid.fst.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Util.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSwaps.fst.checked FStar.Reflection.V2.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Order.fst.checked FStar.List.Tot.Properties.fst.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.List.fst.checked FStar.Classical.fsti.checked FStar.Algebra.CommMonoid.fst.checked
FStar.Tactics.CanonCommMonoid.fst
FStar.Tactics.CanonCommMonoid.permute FStar.Tactics.CanonCommMonoid.permute_via_swaps FStar.Algebra.CommMonoid.cm FStar.Tactics.CanonCommMonoid.vmap Prims.list FStar.Tactics.CanonCommMonoid.var FStar.Classical.exists_elim Prims.eq2 FStar.Tactics.CanonCommMonoid.xsdenote FStar.Tactics.CanonCommSwaps.swap FStar.List.Tot.Base.length FStar.Tactics.CanonCommSwaps.apply_swaps Prims.squash Prims.l_Exists FStar.Tactics.CanonCommMonoid.apply_swaps_correct Prims.unit Prims._assert Prims.l_True 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.CanonCommMonoid

open FStar.Algebra.CommMonoid
open FStar.List
open FStar.Reflection.V2
open FStar.Tactics.V2
open FStar.Classical
open FStar.Tactics.CanonCommSwaps

(* An expression canonizer for commutative monoids.
   Inspired by:
   - http://adam.chlipala.net/cpdt/html/Cpdt.Reflection.html
   - http://poleiro.info/posts/2015-04-13-writing-reflective-tactics.html
*)

(* Only dump when debugging is on *)
private let dump m = if debugging () then dump m

(***** Expression syntax *)

let var : eqtype = nat

type exp : Type =
  | Unit : exp
  | Var : var -> exp
  | Mult : exp -> exp -> exp

let rec exp_to_string (e:exp) : string =
  match e with
  | Unit -> "Unit"
  | Var x -> "Var " ^ string_of_int (x <: var)
  | Mult e1 e2 -> "Mult (" ^ exp_to_string e1
                   ^ ") (" ^ exp_to_string e2 ^ ")"

(***** Expression denotation *)

// Use a map that stores for each variable
// (1) its denotation that should be treated abstractly (type a) and
// (2) user-specified extra information depending on its term (type b)

let vmap (a b:Type) = list (var * (a*b)) * (a * b)
let const (#a #b:Type) (xa:a) (xb:b) : vmap a b = [], (xa,xb)
let select (#a #b:Type) (x:var) (vm:vmap a b) : Tot a =
  match assoc #var #(a * b) x (fst vm) with
  | Some (a, _) -> a
  | _ -> fst (snd vm)
let select_extra (#a #b:Type) (x:var) (vm:vmap a b) : Tot b =
  match assoc #var #(a * b) x (fst vm) with
  | Some (_, b) -> b
  | _ -> snd (snd vm)
let update (#a #b:Type) (x:var) (xa:a) (xb:b) (vm:vmap a b) : vmap a b =
  (x, (xa, xb))::fst vm, snd vm

let rec mdenote (#a #b:Type) (m:cm a) (vm:vmap a b) (e:exp) : Tot a =
  match e with
  | Unit -> CM?.unit m
  | Var x -> select x vm
  | Mult e1 e2 -> CM?.mult m (mdenote m vm e1) (mdenote m vm e2)

let rec xsdenote (#a #b:Type) (m:cm a) (vm:vmap a b) (xs:list var) : Tot a =
  match xs with
  | [] -> CM?.unit m
  | [x] -> select x vm
  | x::xs' -> CM?.mult m (select x vm) (xsdenote m vm xs')

(***** Flattening expressions to lists of variables *)

let rec flatten (e:exp) : list var =
  match e with
  | Unit -> []
  | Var x -> [x]
  | Mult e1 e2 -> flatten e1 @ flatten e2

let rec flatten_correct_aux (#a #b:Type) (m:cm a) (vm:vmap a b)
                                                  (xs1 xs2:list var) :
    Lemma (xsdenote m vm (xs1 @ xs2) == CM?.mult m (xsdenote m vm xs1)
                                                   (xsdenote m vm xs2)) =
  match xs1 with
  | [] -> CM?.identity m (xsdenote m vm xs2)
  | [x] -> if (Nil? xs2) then right_identity m (select x vm)
  | x::xs1' -> (CM?.associativity m (select x vm)
                      (xsdenote m vm xs1') (xsdenote m vm xs2);
                flatten_correct_aux m vm xs1' xs2)

let rec flatten_correct (#a #b:Type) (m:cm a) (vm:vmap a b) (e:exp) :
    Lemma (mdenote m vm e == xsdenote m vm (flatten e)) =
  match e with
  | Unit | Var _ -> ()
  | Mult e1 e2 -> flatten_correct_aux m vm (flatten e1) (flatten e2);
                  flatten_correct m vm e1; flatten_correct m vm e2

(***** Permuting the lists of variables
       by swapping adjacent elements *)

(* The user has control over the permutation. He can store extra
   information in the vmap and use that for choosing the
   permutation. This means that permute has access to the vmap. *)

let permute (b:Type) = a:Type -> vmap a b -> list var -> list var

// high-level correctness criterion for permutations
let permute_correct (#b:Type) (p:permute b) =
  #a:Type -> m:cm a -> vm:vmap a b -> xs:list var ->
    Lemma (xsdenote m vm xs == xsdenote m vm (p a vm xs))

// sufficient condition:
// permutation has to be expressible as swaps of adjacent list elements

let rec apply_swap_aux_correct (#a #b:Type) (n:nat) (m:cm a) (vm:vmap a b)
                           (xs:list var) (s:swap (length xs + n)) :
    Lemma (requires True)
      (ensures (xsdenote m vm xs == xsdenote m vm (apply_swap_aux n xs s)))
      (decreases xs) =
  match xs with
  | [] | [_] -> ()
  | x1 :: x2 :: xs' ->
      if n = (s <: nat)
      then (// x1 + (x2 + xs') =a (x1 + x2) + xs'
            //                 =c (x2 + x1) + xs' = a x2 + (x1 + xs')
           let a = CM?.associativity m in
           a (select x1 vm) (select x2 vm) (xsdenote m vm xs');
           a (select x2 vm) (select x1 vm) (xsdenote m vm xs');
           CM?.commutativity m (select x1 vm) (select x2 vm))
      else apply_swap_aux_correct (n+1) m vm (x2 :: xs') s

let apply_swap_correct (#a #b:Type) (m:cm a) (vm:vmap a b)
                           (xs:list var) (s:swap (length xs)):
    Lemma (requires True)
          (ensures (xsdenote m vm xs == xsdenote m vm (apply_swap xs s)))
          (decreases xs) = apply_swap_aux_correct 0 m vm xs s

let rec apply_swaps_correct (#a #b:Type) (m:cm a) (vm:vmap a b)
                            (xs:list var) (ss:list (swap (length xs))):
    Lemma (requires True)
      (ensures (xsdenote m vm xs == xsdenote m vm (apply_swaps xs ss)))
      (decreases ss) =
  match ss with
  | [] -> ()
  | s::ss' -> apply_swap_correct m vm xs s;
              apply_swaps_correct m vm (apply_swap xs s) ss'

let permute_via_swaps (#b:Type) (p:permute b) =
  (#a:Type) -> (vm:vmap a b) -> xs:list var ->
    Lemma (exists ss. p a vm xs == apply_swaps xs ss)

let permute_via_swaps_correct_aux
  (#b:Type) (p:permute b) (pvs:permute_via_swaps p)
  (#a:Type) (m:cm a) (vm:vmap a b)  (xs:list var) :
val permute_via_swaps_correct_aux
      (#b: Type)
      (p: permute b)
      (pvs: permute_via_swaps p)
      (#a: Type)
      (m: cm a)
      (vm: vmap a b)
      (xs: list var)
    : Lemma (xsdenote m vm xs == xsdenote m vm (p a vm xs))

    p: FStar.Tactics.CanonCommMonoid.permute b ->
    pvs: FStar.Tactics.CanonCommMonoid.permute_via_swaps p ->
    m: FStar.Algebra.CommMonoid.cm a ->
    vm: FStar.Tactics.CanonCommMonoid.vmap a b ->
    xs: Prims.list FStar.Tactics.CanonCommMonoid.var
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Tactics.CanonCommMonoid.xsdenote m vm xs ==
      FStar.Tactics.CanonCommMonoid.xsdenote m vm (p a vm xs))