val lemma_sum_join (i j k: int) (f: (int -> bool))
    : Lemma (requires i <= j /\ j <= k)
      (ensures sum_of_bools i k f == (sum_of_bools i j f <> sum_of_bools j k f))
      (decreases (k - j))
let rec lemma_sum_join (i j k:int) (f:int -> bool) : Lemma
  (requires i <= j /\ j <= k)
  (ensures sum_of_bools i k f == (sum_of_bools i j f <> sum_of_bools j k f))
  (decreases (k - j))
  =
  if j < k then lemma_sum_join i j (k - 1) f
val lemma_sum_join (i j k: int) (f: (int -> bool))
    : Lemma (requires i <= j /\ j <= k)
      (ensures sum_of_bools i k f == (sum_of_bools i j f <> sum_of_bools j k f))
      (decreases (k - j))
let rec lemma_sum_join (i j k: int) (f: (int -> bool))
    : Lemma (requires i <= j /\ j <= k)
      (ensures sum_of_bools i k f == (sum_of_bools i j f <> sum_of_bools j k f))
      (decreases (k - j)) =
if j < k then lemma_sum_join i j (k - 1) f
Vale.Math.Poly2.Defs.fst.checked
Vale.Math.Poly2.Defs_s.fst.checked Vale.Def.Prop_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.Classical.fsti.checked
Vale.Math.Poly2.Defs.fst
Prims.int Prims.bool Prims.op_LessThan Vale.Math.Poly2.Defs.lemma_sum_join Prims.op_Subtraction Prims.unit Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.squash Prims.eq2 Vale.Math.Poly2.Defs_s.sum_of_bools Prims.op_disEquality Prims.Nil FStar.Pervasives.pattern
module Vale.Math.Poly2.Defs
open FStar.Mul
open Vale.Def.Prop_s
open FStar.Seq
open Vale.Math.Poly2.Defs_s
unfold let max = FStar.Math.Lib.max

#reset-options "--z3rlimit 10"

let poly_equal (a b:poly) : prop0 =
  (forall (i:nat).{:pattern a.[i] \/ b.[i]} a.[i] == b.[i])

unfold let ( =. ) = poly_equal
unfold let ( +. ) = add
unfold let ( *. ) = mul
unfold let ( /. ) = div
unfold let ( %. ) = mod

let lemma_poly_equal_elim (a b:poly) : Lemma
  (requires a =. b)
  (ensures a == b)
  (decreases (length a + length b))
  [SMTPat (poly_equal a b)]
  =
  let len = max (length a) (length b) in
  assert (len > 0 ==> a.[len - 1] == b.[len - 1]);
  assert (length a == length b);
  assert (forall (i:nat).{:pattern (index a i) \/ (index b i)} a.[i] == b.[i]);
  assert (equal a b)

let lemma_pointwise_equal (a b:poly) (pf:(i:int -> Lemma (a.[i] == b.[i]))) : Lemma (a == b) =
  FStar.Classical.forall_intro pf;
  lemma_poly_equal_elim a b


// ADDITION

let lemma_add_zero (a:poly) : Lemma ((a +. zero) =. a) = ()
let lemma_add_cancel (a:poly) : Lemma ((a +. a) =. zero) = ()
let lemma_add_cancel_eq (a b:poly) : Lemma (requires (a +. b) == zero) (ensures a =. b) = ()
let lemma_add_commute (a b:poly) : Lemma ((a +. b) =. (b +. a)) = ()
let lemma_add_associate (a b c:poly) : Lemma ((a +. (b +. c)) =. ((a +. b) +. c)) = ()

let lemma_add_move (a b:poly) : Lemma (ensures a == (a +. b) +. b) =
  lemma_add_associate a b b;
  lemma_add_cancel b;
  lemma_add_zero a


// SUMMATION

let lemma_sum_empty (j:int) (f:int -> bool) : Lemma
  (requires True)
  (ensures not (sum_of_bools j j f))
  [SMTPat (sum_of_bools j j f)]
  =
  ()

let rec lemma_sum_of_zero (j k:int) (f:int -> bool) : Lemma
  (requires (forall (i:int).{:pattern (f i)} j <= i /\ i < k ==> not (f i)))
  (ensures not (sum_of_bools j k f))
  (decreases (k - j))
  =
  if j < k then lemma_sum_of_zero j (k - 1) f

let rec lemma_sum_join (i j k:int) (f:int -> bool) : Lemma
  (requires i <= j /\ j <= k)
  (ensures sum_of_bools i k f == (sum_of_bools i j f <> sum_of_bools j k f))
  (decreases (k - j))
val lemma_sum_join (i j k: int) (f: (int -> bool))
    : Lemma (requires i <= j /\ j <= k)
      (ensures sum_of_bools i k f == (sum_of_bools i j f <> sum_of_bools j k f))
      (decreases (k - j))
i: Prims.int -> j: Prims.int -> k: Prims.int -> f: (_: Prims.int -> Prims.bool)
  -> FStar.Pervasives.Lemma (requires i <= j /\ j <= k)
      (ensures
        Vale.Math.Poly2.Defs_s.sum_of_bools i k f ==
        (Vale.Math.Poly2.Defs_s.sum_of_bools i j f <> Vale.Math.Poly2.Defs_s.sum_of_bools j k f))
      (decreases k - j)