val lemma_and_ones (a:poly) (n:nat) : Lemma
  (requires degree a < n)
  (ensures poly_and a (ones n) == a /\ poly_and (ones n) a == a)
let lemma_and_ones a n =
  lemma_bitwise_all ();
  lemma_equal (poly_and a (ones n)) a;
  lemma_equal (poly_and (ones n) a) a;
  ()
val lemma_and_ones (a:poly) (n:nat) : Lemma
  (requires degree a < n)
  (ensures poly_and a (ones n) == a /\ poly_and (ones n) a == a)
let lemma_and_ones a n =
lemma_bitwise_all ();
lemma_equal (poly_and a (ones n)) a;
lemma_equal (poly_and (ones n) a) a;
()
Vale.Math.Poly2.Lemmas.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.List.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.Math.Poly2.Lemmas.fst
Vale.Math.Poly2_s.poly Prims.nat Prims.unit Vale.Math.Poly2.lemma_equal Vale.Math.Poly2.poly_and Vale.Math.Poly2.ones Vale.Math.Poly2.Lemmas.lemma_bitwise_all
module Vale.Math.Poly2.Lemmas
open FStar.Mul

let lemma_pointwise_equal a b pf =
  FStar.Classical.forall_intro pf;
  lemma_equal a b

let lemma_index a =
  FStar.Classical.forall_intro (lemma_index_i a)

let lemma_index_all () =
  FStar.Classical.forall_intro_2 lemma_index_i

let lemma_zero_define () =
  FStar.Classical.forall_intro lemma_zero_define_i

let lemma_one_define () =
  FStar.Classical.forall_intro lemma_one_define_i

let lemma_monomial_define n =
  FStar.Classical.forall_intro (lemma_monomial_define_i n)

let lemma_monomial_define_all () =
  FStar.Classical.forall_intro_with_pat (fun n -> monomial n) lemma_monomial_define

let lemma_ones_define n =
  FStar.Classical.forall_intro (lemma_ones_define_i n)

let lemma_ones_define_all () =
  FStar.Classical.forall_intro_with_pat (fun n -> ones n) lemma_ones_define

let lemma_shift_define p n =
  FStar.Classical.forall_intro (lemma_shift_define_i p n)

let lemma_shift_define_forward p n =
  lemma_shift_define p n

let lemma_shift_define_all () =
  FStar.Classical.forall_intro_2_with_pat (fun p n -> shift p n) lemma_shift_define

let lemma_and_define a b =
  FStar.Classical.forall_intro (lemma_and_define_i a b)

let lemma_and_define_all () =
  FStar.Classical.forall_intro_2_with_pat (fun a b -> poly_and a b) lemma_and_define

let lemma_or_define a b =
  FStar.Classical.forall_intro (lemma_or_define_i a b)

let lemma_or_define_all () =
  FStar.Classical.forall_intro_2_with_pat (fun a b -> poly_or a b) lemma_or_define

let lemma_mask_define p n =
  FStar.Classical.forall_intro (lemma_mask_define_i p n);
  ()

let lemma_mask_define_all () =
  FStar.Classical.forall_intro_2_with_pat (fun p n -> mask p n) lemma_mask_define

let lemma_reverse_define p n =
  FStar.Classical.forall_intro (lemma_reverse_define_i p n)

let lemma_reverse_define_all () =
  FStar.Classical.forall_intro_2 lemma_reverse_define

let lemma_degree_negative a =
  let f (i:int) : Lemma (not a.[i]) =
    lemma_index_i a i
    in
  FStar.Classical.forall_intro f;
  lemma_zero_define ();
  lemma_equal a zero

let lemma_degree_is a n =
  lemma_index a;
  lemma_index_i a n;
  lemma_degree a

let lemma_zero_degree =
  lemma_degree zero;
  lemma_zero_define ()

let lemma_one_degree =
  lemma_one_define ();
  lemma_degree_is one 0

let lemma_monomial_degree n =
  lemma_monomial_define n;
  lemma_degree_is (monomial n) n

let lemma_ones_degree n =
  lemma_ones_define n;
  lemma_degree_is (ones n) (n - 1)

let lemma_shift_degree a n =
  lemma_index a;
  lemma_degree a;
  lemma_shift_define a n;
  lemma_zero_define ();
  if degree a < 0 || degree a + n < 0 then
  (
    lemma_equal zero (shift a n);
    lemma_degree_negative (shift a n)
  )
  else
    lemma_degree_is (shift a n) (degree a + n)

let lemma_and_degree a b =
  lemma_and_define a b;
  lemma_index_all ();
  lemma_degree a;
  lemma_degree b;
  lemma_degree (poly_and a b)

let lemma_or_degree a b =
  lemma_or_define a b;
  lemma_index_all ();
  lemma_degree a;
  lemma_degree b;
  lemma_degree_is (poly_or a b) (FStar.Math.Lib.max (degree a) (degree b))

let lemma_mask_degree a n =
  lemma_mask_define a n;
  lemma_degree (mask a n)

let lemma_reverse_degree a n =
  lemma_index a;
  lemma_reverse_define a n;
  lemma_degree (reverse a n)

let lemma_of_list_degree l =
  let len = List.length l in
  let s = seq_of_list l in
  let a = of_seq s in
  assert (forall (i:nat).{:pattern (index s i)} i < len ==> index s i == List.index l i);
  lemma_index a;
  lemma_degree a;
  lemma_zero_define ();
  if len > 0 then
    lemma_degree_is a (len - 1)
  else
    assert (not a.[degree a])

let lemma_add_define a b =
  FStar.Classical.forall_intro (lemma_add_define_i a b)

let lemma_add_define_all () =
  FStar.Classical.forall_intro_2_with_pat (fun a b -> (a +. b)) lemma_add_define

let lemma_add_zero_right = lemma_add_zero
let lemma_add_zero_left a = lemma_add_zero a; lemma_add_commute a zero

let lemma_add_all () =
  FStar.Classical.forall_intro_with_pat (fun a -> a +. zero) lemma_add_zero;
  FStar.Classical.forall_intro_with_pat (fun a -> a +. a) lemma_add_cancel;
  FStar.Classical.forall_intro_2_with_pat (fun a b -> a +. b) lemma_add_commute;
  FStar.Classical.forall_intro_3_with_pat (fun a b c -> a +. (b +. c)) lemma_add_associate

let lemma_bitwise_all () =
  lemma_index_all ();
  lemma_zero_define ();
  lemma_one_define ();
  lemma_monomial_define_all ();
  lemma_ones_define_all ();
  lemma_shift_define_all ();
  lemma_and_define_all ();
  lemma_or_define_all ();
  lemma_mask_define_all ();
  lemma_reverse_define_all ();
  lemma_add_define_all ();
  ()

let lemma_monomial_add_degree n a =
  lemma_bitwise_all ();
  lemma_degree_is (monomial n +. a) n;
  lemma_degree_is (a +. monomial n) n;
  ()

let lemma_and_zero a =
  lemma_bitwise_all ();
  lemma_equal (poly_and a zero) zero;
  lemma_equal (poly_and zero a) zero;
  ()
val lemma_and_ones (a:poly) (n:nat) : Lemma
  (requires degree a < n)
  (ensures poly_and a (ones n) == a /\ poly_and (ones n) a == a)
a: Vale.Math.Poly2_s.poly -> n: Prims.nat
  -> FStar.Pervasives.Lemma (requires Vale.Math.Poly2_s.degree a < n)
      (ensures
        Vale.Math.Poly2.poly_and a (Vale.Math.Poly2.ones n) == a /\
        Vale.Math.Poly2.poly_and (Vale.Math.Poly2.ones n) a == a)