Skip to content

Commit

Permalink
Add prod_rect rewrite rule for saturated arithmetic (#1780)
Browse files Browse the repository at this point in the history
For #1609
  • Loading branch information
JasonGross authored Dec 9, 2023
1 parent 864ea40 commit 2964ff0
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 3 deletions.
1 change: 1 addition & 0 deletions src/Rewriter/Rules.v
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
11 changes: 8 additions & 3 deletions src/Rewriter/RulesProofs.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand Down

0 comments on commit 2964ff0

Please sign in to comment.