prove foldIRT/unfoldIRT isomorphism

for GaloisInc/heapster-saw#74
GaloisInc · Feb 25, 2021 · 7e098d5 · 7e098d5
1 parent da0f8fd
commit 7e098d5
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCorePreludeExtra.v
@@ -59,3 +59,13 @@ Proof.
     intuition.
   }
 Qed.
+
+Theorem fold_unfold_IRT As Ds D : forall x, foldIRT As Ds D (unfoldIRT As Ds D x) = x.
+Proof.
+  induction x; simpl; unfold uncurry; now f_equal.
+Qed.
+
+Theorem unfold_fold_IRT As Ds D : forall u, unfoldIRT As Ds D (foldIRT As Ds D u) = u.
+Proof.
+  revert Ds; induction D; try destruct u; simpl; now f_equal.
+Qed.