val fold_equality (#c:_) (#eq:_) (cm: CE.cm c eq) 
                  (a: int) (b: not_less_than a) 
                  (expr1 expr2: (ifrom_ito a b) -> c)
  : Lemma (requires (forall (i: ifrom_ito a b). expr1 i == expr2 i))
          (ensures fold cm a b expr1 == fold cm a b expr2)
let rec fold_equality #c #eq (cm: CE.cm c eq) 
  (a: int) (b: not_less_than a) 
  (expr1 expr2: (ifrom_ito a b) -> c)
  : Lemma (requires (forall (i: ifrom_ito a b). expr1 i == expr2 i))
          (ensures fold cm a b expr1 == fold cm a b expr2)
          (decreases b - a) = 
  if b > a then fold_equality cm a (b - 1) expr1 expr2
val fold_equality (#c:_) (#eq:_) (cm: CE.cm c eq) 
                  (a: int) (b: not_less_than a) 
                  (expr1 expr2: (ifrom_ito a b) -> c)
  : Lemma (requires (forall (i: ifrom_ito a b). expr1 i == expr2 i))
          (ensures fold cm a b expr1 == fold cm a b expr2)
let rec fold_equality
      #c
      #eq
      (cm: CE.cm c eq)
      (a: int)
      (b: not_less_than a)
      (expr1: ((ifrom_ito a b) -> c))
      (expr2: ((ifrom_ito a b) -> c))
    : Lemma (requires (forall (i: ifrom_ito a b). expr1 i == expr2 i))
      (ensures fold cm a b expr1 == fold cm a b expr2)
      (decreases b - a) =
if b > a then fold_equality cm a (b - 1) expr1 expr2
FStar.Algebra.CommMonoid.Fold.fst.checked
prims.fst.checked FStar.Seq.Properties.fsti.checked FStar.Seq.Permutation.fsti.checked FStar.Seq.Base.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.IntegerIntervals.fst.checked FStar.Algebra.CommMonoid.Equiv.fst.checked
FStar.Algebra.CommMonoid.Fold.fst
FStar.Algebra.CommMonoid.Equiv.equiv FStar.Algebra.CommMonoid.Equiv.cm Prims.int FStar.IntegerIntervals.not_less_than FStar.IntegerIntervals.ifrom_ito Prims.op_GreaterThan FStar.Algebra.CommMonoid.Fold.fold_equality Prims.op_Subtraction Prims.bool Prims.unit Prims.l_Forall Prims.eq2 Prims.squash FStar.Algebra.CommMonoid.Fold.fold Prims.Nil FStar.Pervasives.pattern
(*
   Copyright 2008-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.

   Author: A. Rozanov
*)

module FStar.Algebra.CommMonoid.Fold
module CE = FStar.Algebra.CommMonoid.Equiv

open FStar.Seq.Base
open FStar.Seq.Properties 
open FStar.Seq.Permutation

open FStar.IntegerIntervals

(* Here we define the notion for big sums and big products for 
   arbitrary commutative monoids. We construct the folds from 
   an integer range and a function, then calculate the fold --
   a sum or a product, depending on the monoid operation. *)
 
(* We refine multiplication a bit to make proofs smoothier *)

open FStar.Mul  

let rec fold #c #eq 
             (cm: CE.cm c eq) 
             (a: int) (b: not_less_than a) 
             (expr: (ifrom_ito a b) -> c) 
  // some of the lemmas want (ensures (fun (x:c) -> ((nk = n0) ==> (x == expr nk)))) 
  : Tot (c) (decreases b-a) 
  = if b = a then expr b
    else (fold cm a (b-1) expr) `cm.mult` expr b

let rec fold_equality #c #eq (cm: CE.cm c eq) 
  (a: int) (b: not_less_than a) 
  (expr1 expr2: (ifrom_ito a b) -> c)
  : Lemma (requires (forall (i: ifrom_ito a b). expr1 i == expr2 i))
          (ensures fold cm a b expr1 == fold cm a b expr2)
val fold_equality (#c:_) (#eq:_) (cm: CE.cm c eq) 
                  (a: int) (b: not_less_than a) 
                  (expr1 expr2: (ifrom_ito a b) -> c)
  : Lemma (requires (forall (i: ifrom_ito a b). expr1 i == expr2 i))
          (ensures fold cm a b expr1 == fold cm a b expr2)

    cm: FStar.Algebra.CommMonoid.Equiv.cm c eq ->
    a: Prims.int ->
    b: FStar.IntegerIntervals.not_less_than a ->
    expr1: (_: FStar.IntegerIntervals.ifrom_ito a b -> c) ->
    expr2: (_: FStar.IntegerIntervals.ifrom_ito a b -> c)
  -> FStar.Pervasives.Lemma
      (requires forall (i: FStar.IntegerIntervals.ifrom_ito a b). expr1 i == expr2 i)
      (ensures
        FStar.Algebra.CommMonoid.Fold.fold cm a b expr1 ==
        FStar.Algebra.CommMonoid.Fold.fold cm a b expr2)
      (decreases b - a)