From 968ddbafe0bcc089922256cde4c06dee6e340de6 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 7 Dec 2023 21:56:26 -0500
Subject: [PATCH] Add remaining rewrite rules for saturated arithmetic

For https://github.com/mit-plv/fiat-crypto/pull/1609
---
 src/Rewriter/Rules.v       | 7 +++++++
 src/Rewriter/RulesProofs.v | 7 +++++++
 2 files changed, 14 insertions(+)

diff --git a/src/Rewriter/Rules.v b/src/Rewriter/Rules.v
index dee627c7418..8f40742ac89 100644
--- a/src/Rewriter/Rules.v
+++ b/src/Rewriter/Rules.v
@@ -182,6 +182,13 @@ Definition nbe_rewrite_rulesT : list (bool * Prop)
                             end)
                         ('n)
                         xs)
+              ; typeof! @unfold1_nat_rect_fbb_b
+              ; typeof! @unfold1_nat_rect_fbb_b_b
+              ; typeof! @unfold1_list_rect_fbb_b
+              ; typeof! @unfold1_list_rect_fbb_b_b
+              ; typeof! @unfold1_list_rect_fbb_b_b_b
+              ; typeof! @unfold1_list_rect_fbb_b_b_b_b
+              ; typeof! @unfold1_list_rect_fbb_b_b_b_b_b
              ]
         ].
 
diff --git a/src/Rewriter/RulesProofs.v b/src/Rewriter/RulesProofs.v
index 6e7cc2dddd6..edd2fb13fe1 100644
--- a/src/Rewriter/RulesProofs.v
+++ b/src/Rewriter/RulesProofs.v
@@ -88,6 +88,13 @@ Local Hint Resolve
       eq_firstn_nat_rect
       eq_skipn_nat_rect
       eq_update_nth_nat_rect
+      unfold1_nat_rect_fbb_b
+      unfold1_nat_rect_fbb_b_b
+      unfold1_list_rect_fbb_b
+      unfold1_list_rect_fbb_b_b
+      unfold1_list_rect_fbb_b_b_b
+      unfold1_list_rect_fbb_b_b_b_b
+      unfold1_list_rect_fbb_b_b_b_b_b
   : core.
 
 Lemma nbe_rewrite_rules_proofs