Library multi_int
Require Import ssreflect ssrbool eqtype.
Require Import ZArith_ext Lists_ext.
Local Open Scope zarith_ext_scope.
Require Import machine_int.
Import MachineInt.
Require Import ZArith_ext Lists_ext.
Local Open Scope zarith_ext_scope.
Require Import machine_int.
Import MachineInt.
a multi_int is a list of (int n) that represents an unsigned integer in base 2^n, LSW first
expected: length l = n * k
the input list l is with MSb first, the output list is a multi_int
Fixpoint listbit_to_ints (n k:nat) (l:list bool) {struct k} : list (int n) :=
match k with
| O => nil
| S k' => let (one, two) := split_n l n in
listbit_to_ints n k' two ++ bits2u n one :: nil
end.
Lemma length_listbit_to_ints : forall k n l, length l = (k * n)%nat ->
length (listbit_to_ints n k l) = k.
match k with
| O => nil
| S k' => let (one, two) := split_n l n in
listbit_to_ints n k' two ++ bits2u n one :: nil
end.
Lemma length_listbit_to_ints : forall k n l, length l = (k * n)%nat ->
length (listbit_to_ints n k l) = k.
Z2ints: turn a Z into a multi_int
Definition adjust_to_ints (n k:nat) (l:list bool) : list (int n) :=
listbit_to_ints n k (listbit.ListBit.adjust_ulist l (k * n)).
Definition Z2ints n k z : list (int n) :=
match z with
| Zpos p => adjust_to_ints n k (rev (listbit_correct.pos2lst p))
| Zneg p => adjust_to_ints n k (rev (listbit_correct.pos2lst p))
| _ => rep (Z2u n 0) k
end.
Lemma Z2ints_0 : forall n x, Z2ints n 0 x = List.nil.
Lemma len_Z2ints : forall k n z, length (Z2ints n k z) = k.
sum_k k lst sum the list elements of indices 0,k-1
Fixpoint sum_k k (lst : list (int n)) :=
match lst with
| nil => 0
| hd :: tl => match k with
| O => u2Z hd
| S k' => u2Z hd + 2 ^^ n * sum_k k' tl
end
end.
Lemma sum_k_nil : forall k, sum_k k (@nil (int n)) = 0.
Lemma sum_k_0 : forall (h : int n) t, sum_k 0 (h :: t) = u2Z h.
Lemma sum_k_S : forall k (h : int n) t, sum_k (S k) (h :: t) = u2Z h + 2 ^^ n * sum_k k t.
match lst with
| nil => 0
| hd :: tl => match k with
| O => u2Z hd
| S k' => u2Z hd + 2 ^^ n * sum_k k' tl
end
end.
Lemma sum_k_nil : forall k, sum_k k (@nil (int n)) = 0.
Lemma sum_k_0 : forall (h : int n) t, sum_k 0 (h :: t) = u2Z h.
Lemma sum_k_S : forall k (h : int n) t, sum_k (S k) (h :: t) = u2Z h + 2 ^^ n * sum_k k t.
sum the first k list members (with k>=1)
Definition Sum k (lst : list (int n)) := match k with O => 0 | S k' => sum_k k' lst end.
Lemma Sum_nil : forall k, Sum k (@nil (int n)) = 0.
Lemma Sum_S : forall k (h : int n) t, Sum (S k) (h :: t) = u2Z h + 2 ^^ n * Sum k t.
Lemma min_Sum : forall (lst : list (int n)) k, 0 <= Sum k lst.
Lemma Sum_max : forall k (lst : list (int n)), Sum k lst < 2 ^^ (k * n).
Lemma Sum_inj : forall k (l1 l2 : list (int n)), length l1 = k -> length l2 = k ->
Sum k l1 = Sum k l2 -> l1 = l2.
Lemma Sum_head_swap : forall k h h' (tl : list (int n)), (k > 0)%nat ->
Sum k (h :: tl) + u2Z h' = Sum k (h' :: tl) + u2Z h.
Lemma Sum_nil : forall k, Sum k (@nil (int n)) = 0.
Lemma Sum_S : forall k (h : int n) t, Sum (S k) (h :: t) = u2Z h + 2 ^^ n * Sum k t.
Lemma min_Sum : forall (lst : list (int n)) k, 0 <= Sum k lst.
Lemma Sum_max : forall k (lst : list (int n)), Sum k lst < 2 ^^ (k * n).
Lemma Sum_inj : forall k (l1 l2 : list (int n)), length l1 = k -> length l2 = k ->
Sum k l1 = Sum k l2 -> l1 = l2.
Lemma Sum_head_swap : forall k h h' (tl : list (int n)), (k > 0)%nat ->
Sum k (h :: tl) + u2Z h' = Sum k (h' :: tl) + u2Z h.
(0 a_0 ... a{k-1}) + z = (z a_0 ... a{k-1})
beta * (a_0 ... a{k-1}) = (0 a_0...a{k-1})
Lemma Sum_Zpower_Zmult : forall k lst, 2 ^^ n * Sum k lst = Sum (S k) (Z2u n 0 :: lst).
Lemma Sum_1 : forall lst, Sum 1 lst = u2Z (nth 0 lst (Z2u n 0)).
Lemma Sum_rep_0 : forall k k', Sum k (rep (Z2u n 0) k') = 0.
Lemma Sum_0_inv_new : forall k (l : list (int n)), (k <= length l)%nat ->
Sum k l = 0 -> firstn k l = rep (Z2u n 0) k.
Lemma Sum_0_inv : forall len (l : list (int n)), length l = len -> Sum len l = 0 ->
l = rep (Z2u n 0) len.
Lemma Sum_remove_last' : forall K (lst : list (int n)) k, length lst = K ->
Sum (S k) lst = Sum k lst + 2 ^^ (k * n) * u2Z (nth k lst (Z2u n 0)).
Lemma Sum_remove_last : forall (lst : list (int n)) k,
Sum (S k) lst = Sum k lst + 2 ^^ (k * n) * u2Z (nth k lst (Z2u n 0)).
Lemma Sum_cut : forall k1 (l1 : list (int n)),
length l1 = k1 ->
forall k l l2,
length l = k ->
l = l1 ++ l2 ->
Sum k (l1 ++ l2) = Sum k1 l1 + 2 ^^ (k1 * n) * Sum (k - k1) l2.
Lemma Sum_cut_last : forall k (l : list (int n)) last, length (l ++ last :: nil) = k ->
Sum k (l ++ last :: nil) = Sum (k - 1) l + 2 ^^ ((k - 1) * n) * u2Z last.
Lemma Sum_beyond : forall k (l : list (int n)), length l = k ->
forall l', Sum k l = Sum k (l ++ l').
Lemma Sum_beyond_idx : forall (k : nat) (l : list (int n)), length l = k ->
forall k', Sum (k + k') l = Sum k l.
Lemma Sum_cut_last_beyond : forall k (l : list (int n)),
(0 < k)%nat -> length l = k ->
Sum k l = Sum (k - 1) l + 2 ^^ ((k - 1) * n) * u2Z (nth (k - 1) l (Z2u n 0)).
Lemma Sum_beyond_inv : forall len (lst: list (int n)) len',
length lst = len ->
(len' < len)%nat ->
Sum len lst < 2 ^^ (len' * n) ->
lst = firstn len' lst ++ rep (Z2u n 0) (len - len').
Lemma Sum_update_list : forall (lst : list (int n)) k m,
Sum k lst = Sum k (update_list lst k m).
Lemma Sum_update_list2 : forall k (lst : list (int n)) i z,
length lst = k ->
(i < k)%nat ->
Sum k lst - u2Z (nth i lst (Z2u n 0)) * 2 ^^ (i * n) + u2Z z * 2 ^^ (i * n) = Sum k (update_list lst i z).
Lemma Sum_skipn : forall l (A B : list (int n)) m k, length A = l -> length B = l ->
Sum (k - m) (skipn m A) < Sum (k - m) (skipn m B) ->
Sum k A < Sum k B.
Lemma Sum_positive_to_ints : forall k l, length l = (k * n)%nat ->
Sum k (listbit_to_ints n k l) = listbit_correct.ulst2Z l.
Lemma Sum_Z2ints : forall len z, Zabs z < 2 ^^ (len * n) ->
Sum len (Z2ints n len z) = Zabs z.
Lemma Sum_Z2ints_pos : forall len z, 0 <= z /\ z < 2 ^^ (len * n) ->
Sum len (Z2ints n len z) = z.
Lemma Z2ints_Sum : forall k lst, k = length lst ->
lst = Z2ints n k (Sum k lst).
Lemma Sum_1 : forall lst, Sum 1 lst = u2Z (nth 0 lst (Z2u n 0)).
Lemma Sum_rep_0 : forall k k', Sum k (rep (Z2u n 0) k') = 0.
Lemma Sum_0_inv_new : forall k (l : list (int n)), (k <= length l)%nat ->
Sum k l = 0 -> firstn k l = rep (Z2u n 0) k.
Lemma Sum_0_inv : forall len (l : list (int n)), length l = len -> Sum len l = 0 ->
l = rep (Z2u n 0) len.
Lemma Sum_remove_last' : forall K (lst : list (int n)) k, length lst = K ->
Sum (S k) lst = Sum k lst + 2 ^^ (k * n) * u2Z (nth k lst (Z2u n 0)).
Lemma Sum_remove_last : forall (lst : list (int n)) k,
Sum (S k) lst = Sum k lst + 2 ^^ (k * n) * u2Z (nth k lst (Z2u n 0)).
Lemma Sum_cut : forall k1 (l1 : list (int n)),
length l1 = k1 ->
forall k l l2,
length l = k ->
l = l1 ++ l2 ->
Sum k (l1 ++ l2) = Sum k1 l1 + 2 ^^ (k1 * n) * Sum (k - k1) l2.
Lemma Sum_cut_last : forall k (l : list (int n)) last, length (l ++ last :: nil) = k ->
Sum k (l ++ last :: nil) = Sum (k - 1) l + 2 ^^ ((k - 1) * n) * u2Z last.
Lemma Sum_beyond : forall k (l : list (int n)), length l = k ->
forall l', Sum k l = Sum k (l ++ l').
Lemma Sum_beyond_idx : forall (k : nat) (l : list (int n)), length l = k ->
forall k', Sum (k + k') l = Sum k l.
Lemma Sum_cut_last_beyond : forall k (l : list (int n)),
(0 < k)%nat -> length l = k ->
Sum k l = Sum (k - 1) l + 2 ^^ ((k - 1) * n) * u2Z (nth (k - 1) l (Z2u n 0)).
Lemma Sum_beyond_inv : forall len (lst: list (int n)) len',
length lst = len ->
(len' < len)%nat ->
Sum len lst < 2 ^^ (len' * n) ->
lst = firstn len' lst ++ rep (Z2u n 0) (len - len').
Lemma Sum_update_list : forall (lst : list (int n)) k m,
Sum k lst = Sum k (update_list lst k m).
Lemma Sum_update_list2 : forall k (lst : list (int n)) i z,
length lst = k ->
(i < k)%nat ->
Sum k lst - u2Z (nth i lst (Z2u n 0)) * 2 ^^ (i * n) + u2Z z * 2 ^^ (i * n) = Sum k (update_list lst i z).
Lemma Sum_skipn : forall l (A B : list (int n)) m k, length A = l -> length B = l ->
Sum (k - m) (skipn m A) < Sum (k - m) (skipn m B) ->
Sum k A < Sum k B.
Lemma Sum_positive_to_ints : forall k l, length l = (k * n)%nat ->
Sum k (listbit_to_ints n k l) = listbit_correct.ulst2Z l.
Lemma Sum_Z2ints : forall len z, Zabs z < 2 ^^ (len * n) ->
Sum len (Z2ints n len z) = Zabs z.
Lemma Sum_Z2ints_pos : forall len z, 0 <= z /\ z < 2 ^^ (len * n) ->
Sum len (Z2ints n len z) = z.
Lemma Z2ints_Sum : forall k lst, k = length lst ->
lst = Z2ints n k (Sum k lst).
Sum_hole
Definition Sum_hole len hole (l : list (int n)) := Sum (len - 1) (idel hole l).
Lemma Sum_hole_last : forall (l : list (int n)) k, length l = k ->
Sum_hole k (k - 1)%nat l = Sum (k - 1)%nat l.
Lemma Sum_hole_last' : forall (l : list (int n)) k, length l = k ->
Sum_hole k 0 l = Sum (k - 1)%nat (tail l).
Lemma Sum_hole_update_list : forall l (lst : list (int n)) k m, length lst = l ->
Sum_hole l k lst = Sum_hole l k (update_list lst k m).
Lemma Sum_hole_shift : forall k (l : list (int n)), length l = k ->
forall j, (j < k)%nat ->
Sum_hole k j l + u2Z (nth j l (Z2u n 0)) * 2 ^^ (n * (j - 1)) =
Sum_hole k (j - 1) l + u2Z (nth (j - 1) l (Z2u n 0)) * 2 ^^ (n * (j - 1)).
End sum_section.
Implicit Arguments sum_k [n].
Implicit Arguments Sum [n].
Implicit Arguments min_Sum [n].
Implicit Arguments Sum_1 [n].
Implicit Arguments Sum_cut [n].
Implicit Arguments Sum_cut_last [n].
Implicit Arguments Sum_cut_last_beyond [n].
Implicit Arguments Sum_update_list2 [n].
Implicit Arguments Sum_skipn [n].
Implicit Arguments Sum_rep_0 [n].
Implicit Arguments Sum_Z2ints [n].
Implicit Arguments Sum_Z2ints_pos [n].
Implicit Arguments Z2ints_Sum [n].
Implicit Arguments Sum_hole.
Implicit Arguments Sum_hole_last [n].
Implicit Arguments Sum_hole_last' [n].
Implicit Arguments Sum_hole_update_list [n].
Implicit Arguments Sum_hole_shift [n].
Lemma Zodd_Sum : forall n (lst : list (int (S n))) len, Zodd (Sum len lst) ->
Zodd (u2Z (nth 0 lst (Z2u (S n) 0))).
Lemma Zeven_Sum : forall n (l : list (int (S n))) len, (0 < len)%nat ->
Zeven (Sum len l) -> Zeven (u2Z (nth 0 l (Z2u (S n) 0))).
Lemma Z2ints_inj : forall n k x x',
0 <= x < 2 ^^ (k * n) -> 0 <= x' < 2 ^^ (k * n) ->
Z2ints n k x = Z2ints n k x' -> x = x'.