Rebase + remove WordizeUtil dependency from Z/Interpretations

4 files changed, 118 insertions, 9 deletions

diff --git a/src/Util/HList.v b/src/Util/HList.v
index aacefe8f3..ec9dcdd7b 100644
--- a/src/Util/HList.v
+++ b/src/Util/HList.v
@@ -88,6 +88,18 @@ Proof.
   destruct n; [ constructor | apply hlist'_impl ].
 Defined.
 
+Local Arguments Tuple.map : simpl never.
+Lemma hlist_map {n A B F} {f:A -> B} (xs:tuple A n)
+  : hlist F (Tuple.map f xs) = hlist (fun x => F (f x)) xs.
+Proof.
+  destruct n as [|n]; [ reflexivity | ].
+  induction n; [ reflexivity | ].
+  specialize (IHn (fst xs)).
+  destruct xs; rewrite Tuple.map_S.
+  simpl @hlist in *; rewrite <- IHn.
+  reflexivity.
+Qed.
+
 Module Tuple.
   Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n)
   : hlist (fun x => f x = x) xs -> Tuple.map f xs = xs.
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 4d97c7857..79747ec2d 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -20,6 +20,42 @@ Definition tuple T n : Type :=
   | S n' => tuple' T n'
   end.
 
+(** right-associated tuples *)
+Fixpoint rtuple' T n : Type :=
+  match n with
+  | O => T
+  | S n' => (T * rtuple' T n')%type
+  end.
+
+Definition rtuple T n : Type :=
+  match n with
+  | O => unit
+  | S n' => rtuple' T n'
+  end.
+
+Fixpoint rsnoc' T n {struct n} : forall (x : rtuple' T n) (y : T), rtuple' T (S n)
+  := match n return forall (x : rtuple' T n) (y : T), rtuple' T (S n) with
+     | O => fun x y => (x, y)
+     | S n' => fun x y => (fst x, @rsnoc' T n' (snd x) y)
+     end.
+Global Arguments rsnoc' {T n} _ _.
+
+Fixpoint assoc_right' {n T} {struct n}
+  : tuple' T n -> rtuple' T n
+  := match n return tuple' T n -> rtuple' T n with
+     | 0 => fun x => x
+     | S n' => fun ts => let xs := @assoc_right' n' T (fst ts) in
+                         let x := snd ts in
+                         rsnoc' xs x
+     end.
+
+Definition assoc_right {n T}
+  : tuple T n -> rtuple T n
+  := match n with
+     | 0 => fun x => x
+     | S n' => @assoc_right' n' T
+     end.
+
 Definition tl' {T n} : tuple' T (S n) -> tuple' T n := @fst _ _.
 Definition tl {T n} : tuple T (S n) -> tuple T n :=
   match n with
@@ -168,6 +204,11 @@ Definition on_tuple2 {A B C} (f : list A -> list B -> list C) {a b c : nat}
 Definition map2 {n A B C} (f:A -> B -> C) (xs:tuple A n) (ys:tuple B n) : tuple C n
   := on_tuple2 (map2 f) (fun la lb pfa pfb => eq_trans (@map2_length _ _ _ _ la lb) (eq_trans (f_equal2 _ pfa pfb) (Min.min_idempotent _))) xs ys.
 
+Lemma map2_S {n A B C} (f:A -> B -> C) (xs:tuple' A n) (ys:tuple' B n) (x:A) (y:B)
+  : map2 (n:=S (S n)) f (xs, x) (ys, y) = (map2 (n:=S n) f xs ys, f x y).
+Proof.
+Admitted.
+
 Lemma map_map2 {n A B C D} (f:A -> B -> C) (g:C -> D) (xs:tuple A n) (ys:tuple B n)
   : map g (map2 f xs ys) = map2 (fun a b => g (f a b)) xs ys.
 Proof.
@@ -193,6 +234,23 @@ Lemma map_id_ext {n A} (f : A -> A) (xs:tuple A n)
 Proof.
 Admitted.
 
+Lemma map2_map {n A B C A' B'} (f:A -> B -> C) (g:A' -> A) (h:B' -> B) (xs:tuple A' n) (ys:tuple B' n)
+  : map2 f (map g xs) (map h ys) = map2 (fun a b => f (g a) (h b)) xs ys.
+Proof.
+Admitted.
+
+Lemma map2_map_fst {n A B C A'} (f:A -> B -> C) (g:A' -> A) (xs:tuple A' n) (ys:tuple B n)
+  : map2 f (map g xs) ys = map2 (fun a b => f (g a) b) xs ys.
+Proof.
+  rewrite <- (map2_map f g (fun x => x)), map_id; reflexivity.
+Qed.
+
+Lemma map2_map_snd {n A B C B'} (f:A -> B -> C) (g:B' -> B) (xs:tuple A n) (ys:tuple B' n)
+  : map2 f xs (map g ys) = map2 (fun a b => f a (g b)) xs ys.
+Proof.
+  rewrite <- (map2_map f (fun x => x) g), map_id; reflexivity.
+Qed.
+
 Lemma map_map {n A B C} (g : B -> C) (f : A -> B) (xs:tuple A n)
   : map g (map f xs) = map (fun x => g (f x)) xs.
 Proof.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 4c74fe9b4..f0e6ef335 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -1,5 +1,6 @@
 Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith.
+Require Import Coq.NArith.NArith.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Bedrock.Word.
@@ -51,6 +52,32 @@ Proof.
   auto.
 Qed.
 
+Lemma Npow2_gt0 : forall x, (0 < Npow2 x)%N.
+Proof.
+  intros; induction x.
+
+  - simpl; apply N.lt_1_r; intuition.
+
+  - replace (Npow2 (S x)) with (2 * (Npow2 x))%N by intuition.
+      apply (N.lt_0_mul 2 (Npow2 x)); left; split; apply N.neq_0_lt_0.
+
+    + intuition; inversion H.
+
+    + apply N.neq_0_lt_0 in IHx; intuition.
+Qed.
+
+Lemma Npow2_N: forall n, Npow2 n = (2 ^ N.of_nat n)%N.
+Proof.
+  induction n.
+
+  - simpl; intuition.
+
+  - rewrite Nat2N.inj_succ.
+    rewrite N.pow_succ_r; try apply N_ge_0.
+    rewrite <- IHn.
+    simpl; intuition.
+Qed.
+
 Lemma Npow2_Zlog2 : forall x n,
     (Z.log2 (Z.of_N x) < Z.of_nat n)%Z
  -> (x < Npow2 n)%N.
@@ -243,16 +270,26 @@ Ltac wordsize_eq_tac := cbv beta delta [wordsize_eq] in *; omega*.
 Ltac gt84_abstract t := t. (* TODO: when we drop Coq 8.4, use [abstract] here *)
 Hint Extern 100 (wordsize_eq _ _) => gt84_abstract wordsize_eq_tac : typeclass_instances.
 
-Program Fixpoint cast_word {n m} : forall {pf:wordsize_eq n m}, word n -> word m :=
-  match n, m return wordsize_eq n m -> word n -> word m with
-  | O, O => fun _ _ => WO
-  | S n', S m' => fun _ w => WS (whd w) (@cast_word _ _ _ (wtl w))
-  | _, _ => fun _ _ => !
+Fixpoint correct_wordsize_eq (x y : nat) : wordsize_eq x y -> x = y
+  := match x, y with
+     | O, O => fun _ => eq_refl
+     | S x', S y' => fun pf => f_equal S (correct_wordsize_eq x' y' (f_equal pred pf))
+     | _, _ => fun x => x
+     end.
+
+Lemma correct_wordsize_eq_refl n pf : correct_wordsize_eq n n pf = eq_refl.
+Proof.
+  induction n; [ reflexivity | simpl ].
+  rewrite IHn; reflexivity.
+Qed.
+
+Definition cast_word {n m} {pf:wordsize_eq n m} : word n -> word m :=
+  match correct_wordsize_eq n m pf in _ = y return word n -> word y with
+  | eq_refl => fun w => w
   end.
-Global Arguments cast_word {_ _ _} _. (* 8.4 does not pick up the forall braces *)
 
 Lemma cast_word_refl {n} pf (w:word n) : @cast_word n n pf w = w.
-Proof. induction w; simpl; auto using f_equal. Qed.
+Proof. unfold cast_word; rewrite correct_wordsize_eq_refl; reflexivity. Qed.
 
 Lemma wordToNat_cast_word {n} (w:word n) m pf :
   wordToNat (@cast_word n m pf w) = wordToNat w.
@@ -721,4 +758,4 @@ Axiom winit : forall sz, word (sz+1) -> word sz. Arguments winit {_} _.
 Axiom combine_winit_wlast : forall {sz} a b (c:word (sz+1)),
     @combine sz a 1 b = c <-> a = winit c /\ b = (WS (wlast c) WO).
 Axiom winit_combine : forall sz a b, @winit sz (combine a b) = a.
-Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
\ No newline at end of file
+Axiom wlast_combine : forall sz a b, @wlast sz (combine a (WS b WO)) = b.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 17e8d62bf..42e88e8c4 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -944,6 +944,7 @@ Module Z.
       rewrite Z.ones_succ by assumption.
       zero_bounds.
   Qed.
+  Hint Resolve ones_nonneg : zarith.
 
   Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i.
   Proof.
@@ -953,6 +954,7 @@ Module Z.
     apply Z.lt_succ_lt_pred.
     apply Z.pow_gt_1; omega.
   Qed.
+  Hint Resolve ones_pos_pos : zarith.
 
   Lemma pow2_mod_id_iff : forall a n, 0 <= n ->
                                       (Z.pow2_mod a n = a <-> 0 <= a < 2 ^ n).
@@ -2128,7 +2130,7 @@ Module Z.
   Qed.
   Hint Resolve log2_ones_lt_nonneg : zarith.
 
-  Lemma log2_lt_pow2_alt a b : 0 < b -> a < 2^b <-> Z.log2 a < b.
+  Lemma log2_lt_pow2_alt a b : 0 < b -> (a < 2^b <-> Z.log2 a < b).
   Proof.
     destruct (Z_lt_le_dec 0 a); auto using Z.log2_lt_pow2; [].
     rewrite Z.log2_nonpos by omega.