Add prod_rect rewrite rule for saturated arithmetic

For #1609
mit-plv · Dec 9, 2023 · 7ad7c2d · 7ad7c2d
1 parent 652fc80
commit 7ad7c2d
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 3 deletions.
diff --git a/src/Rewriter/Rules.v b/src/Rewriter/Rules.v
@@ -56,6 +56,7 @@ Definition nbe_rewrite_rulesT : list (bool * Prop)
             ; (forall P t f, @Thunked.bool_rect P t f true = t tt)
             ; (forall P t f, @Thunked.bool_rect P t f false = f tt)
             ; (forall A B C f x y, @prod_rect A B (fun _ => C) f (x, y) = f x y)
+            ; (forall A B C f p, @prod_rect A B (fun _ : A * B => C) f p = dlet p := p in f (fst p) (snd p))
 
             ; (forall A x n,
                   @List.repeat A x ('n)

diff --git a/src/Rewriter/RulesProofs.v b/src/Rewriter/RulesProofs.v
@@ -65,6 +65,7 @@ Require Crypto.Util.PrimitiveHList.
 Require Import Crypto.Language.PreExtra.
 Require Import Crypto.CastLemmas.
 Require Import Crypto.Rewriter.Rules.
+Require Import Rewriter.Util.Prod.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Notations.
@@ -82,6 +83,7 @@ Local Ltac start_proof :=
   repeat apply PrimitiveProd.Primitive.pair; try exact tt.
 
 Local Hint Resolve
+      prod_rect_nodep_eta
       eq_repeat_nat_rect
       eq_app_list_rect
       eq_combine_list_rect
@@ -90,6 +92,9 @@ Local Hint Resolve
       eq_update_nth_nat_rect
   : core.
 
+(* to catch [prod_rect] and not just [prod_rect_nodep] *)
+Local Hint Extern 0 (prod_rect _ _ _ = _)  => solve [ apply prod_rect_nodep_eta ] : core.
+
 Lemma nbe_rewrite_rules_proofs
   : PrimitiveHList.hlist (@snd bool Prop) nbe_rewrite_rulesT.
 Proof using Type. start_proof; auto. Qed.
@@ -598,17 +603,17 @@ Proof.
       -- rewrite <- Z.mod_divide_full. assumption.
     + rewrite H2. apply Ones.Z.ones_nonneg. remember (Z.log2_nonneg (upper)). lia.
     + lia.
-    + rewrite H2. apply Ones.Z.ones_nonneg. remember (Z.log2_nonneg (upper)). lia.  
+    + rewrite H2. apply Ones.Z.ones_nonneg. remember (Z.log2_nonneg (upper)). lia.
 Qed.
-      
+
 Lemma arith_with_relaxed_casts_rewrite_rules_proofs
   : PrimitiveHList.hlist (@snd bool Prop) arith_with_relaxed_casts_rewrite_rulesT.
 Proof using Type.
   start_proof; auto; intros; try lia.
   - apply relaxed_rules_work; assumption.
   - rewrite Z.land_comm. apply relaxed_rules_work; assumption.
 Qed.
-      
+
 Lemma strip_literal_casts_rewrite_rules_proofs
   : PrimitiveHList.hlist (@snd bool Prop) strip_literal_casts_rewrite_rulesT.
 Proof using Type.