Pseudize Lemmas for Dual Operations

1 files changed, 44 insertions, 0 deletions

diff --git a/src/Assembly/Vectorize.v b/src/Assembly/Vectorize.v
index aeb47f960..d2fca3ce6 100644
--- a/src/Assembly/Vectorize.v
+++ b/src/Assembly/Vectorize.v
@@ -2,6 +2,11 @@ Require Export Bedrock.Word Bedrock.Nomega.
 Require Import NPeano NArith PArith Ndigits Compare_dec Arith.
 Require Import ProofIrrelevance Ring List Omega.
 
+Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x :=
+  let y := x in f y.
+
+Notation "'plet' x := y 'in' z" := (Let_In y (fun x => z)) (at level 60).
+
 Section Vector.
   Import ListNotations.
 
@@ -62,6 +67,45 @@ Section Vector.
   Defined.
 End Vector.
 
+Section Vectorization.
+  Import ListNotations.
+
+  Lemma detuple_let: forall {A B C} (y0: A) (y1: B) (z: (A * B) -> C),
+      Let_In (y0, y1) z =
+        Let_In y0 (fun x0 =>
+          Let_In y1 (fun x1 =>
+            z (x0, x1))).
+  Proof. intros; unfold Let_In; cbv zeta; intuition. Qed.
+
+  Lemma listize_let: forall {A B} (y d: A) (z: A -> B),
+      Let_In y z = Let_In [y] (fun x => z (nth 0 x d)).
+  Proof. intros; unfold Let_In; cbv zeta; intuition. Qed.
+
+  Lemma combine_let_lists: forall {A B} (a: list A) (b: list A) (d: A) (z: list A -> list A -> B),
+      Let_In a (fun x => Let_In b (z x)) =
+        Let_In (a ++ b) (fun x => z (firstn (length a) x) (skipn (length a) x)).
+  Proof.
+
+    intros; unfold Let_In; cbv zeta.
+
+    assert (forall b0, firstn (length a) (a ++ b0) = a) as HA. {
+      induction a; intros; simpl; try reflexivity.
+      apply f_equal; apply IHa.
+    }
+
+    assert (forall b0, skipn (length a) (a ++ b0) = b0) as HB. {
+      induction a; intros; simpl; try reflexivity.
+      apply IHa; intro; simpl in HA.
+      pose proof (HA b1) as HA'; inversion HA' as [HA''].
+      rewrite HA''.
+      assumption.
+    }
+
+    rewrite HA, HB; reflexivity.
+  Qed.
+
+End Vectorization.
+
 Ltac vectorize :=
   repeat match goal with
    | [ |- context[?a - 1] ] =>