Add remaining rewrite rules for saturated arithmetic

For mit-plv#1609
JasonGross · Dec 9, 2023 · 968ddba · 968ddba
1 parent 652fc80
commit 968ddba
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
@@ -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
@@ -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