Add remaining rewrite rules for saturated arithmetic

For #1609
mit-plv · Dec 23, 2023 · 1588b10 · 1588b10
1 parent 69a1b5f
commit 1588b10
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/src/Rewriter/Rules.v b/src/Rewriter/Rules.v
@@ -183,6 +183,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
@@ -90,6 +90,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.
 
 (* to catch [prod_rect] and not just [prod_rect_nodep] *)