diff options
Diffstat (limited to 'src/Compilers/Z/ArithmeticSimplifierInterp.v')
| -rw-r--r-- | src/Compilers/Z/ArithmeticSimplifierInterp.v | 64 |
1 files changed, 56 insertions, 8 deletions
diff --git a/src/Compilers/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v index 6eec2f2a4..1f638c076 100644 --- a/src/Compilers/Z/ArithmeticSimplifierInterp.v +++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v @@ -10,6 +10,7 @@ Require Import Crypto.Compilers.Z.ArithmeticSimplifier. Require Import Crypto.Compilers.Z.ArithmeticSimplifierUtil. Require Import Crypto.Compilers.Z.Syntax.Equality. Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.AddGetCarry. Require Import Crypto.Util.Option. Require Import Crypto.Util.Prod. Require Import Crypto.Util.Sum. @@ -36,6 +37,7 @@ Local Ltac break_t_step := | progress inversion_prod | progress inversion_inverted_expr | progress inversion_flat_type + | progress subst_prod | progress destruct_head'_and | progress destruct_head'_prod | progress eliminate_hprop_eq @@ -72,6 +74,12 @@ Proof. | progress invert_op ]. } Qed. +Local Ltac rewrite_interp_as_expr_or_const_correct_base _ := + match goal with + | [ |- context[interpf _ ?e] ] + => erewrite !(@interp_as_expr_or_const_correct_base _ e) by eassumption; cbv beta iota + end. + Lemma interp_as_expr_or_const_correct_prod_base {A B} e (v : _ * _) : @interp_as_expr_or_const interp_base_type (Prod (Tbase A) (Tbase B)) e = Some v -> interpf interp_op e = (match fst v with @@ -90,9 +98,48 @@ Proof. | progress simpl in * | progress intros | break_t_step - | erewrite !interp_as_expr_or_const_correct_base by eassumption; cbv beta iota ]. + | rewrite_interp_as_expr_or_const_correct_base () ]. +Qed. + +Local Ltac rewrite_interp_as_expr_or_const_correct_prod_base _ := + match goal with + | [ |- context[interpf _ ?e] ] + => erewrite !(@interp_as_expr_or_const_correct_prod_base _ _ e) by eassumption; cbv beta iota + end. + +Lemma interp_as_expr_or_const_correct_prod3_base {A B C} e (v : _ * _ * _) + : @interp_as_expr_or_const interp_base_type (Prod (Prod (Tbase A) (Tbase B)) (Tbase C)) e = Some v + -> interpf interp_op e = (match fst (fst v) with + | const_of z => cast_const (t1:=TZ) z + | gen_expr e => interpf interp_op e + | neg_expr e => interpf interp_op (Op (Opp _ _) e) + end, + match snd (fst v) with + | const_of z => cast_const (t1:=TZ) z + | gen_expr e => interpf interp_op e + | neg_expr e => interpf interp_op (Op (Opp _ _) e) + end, + match snd v with + | const_of z => cast_const (t1:=TZ) z + | gen_expr e => interpf interp_op e + | neg_expr e => interpf interp_op (Op (Opp _ _) e) + end). +Proof. + invert_expr; + repeat first [ fin_t + | progress simpl in * + | progress intros + | break_t_step + | rewrite_interp_as_expr_or_const_correct_base () + | rewrite_interp_as_expr_or_const_correct_prod_base () ]. Qed. +Local Ltac rewrite_interp_as_expr_or_const_correct_prod3_base _ := + match goal with + | [ |- context[interpf _ ?e] ] + => erewrite !(@interp_as_expr_or_const_correct_prod3_base _ _ _ e) by eassumption; cbv beta iota + end. + Local Arguments Z.mul !_ !_. Local Arguments Z.add !_ !_. Local Arguments Z.sub !_ !_. @@ -104,17 +151,18 @@ Proof. apply InterpRewriteOp; intros; unfold simplify_op_expr. break_innermost_match; repeat first [ fin_t + | progress cbv [LetIn.Let_In] | progress simpl in * | progress subst - | erewrite !interp_as_expr_or_const_correct_prod_base by eassumption; cbv beta iota - | erewrite !interp_as_expr_or_const_correct_base by eassumption; cbv beta iota - | match goal with - | [ |- context[interpf _ ?e] ] - => erewrite !(@interp_as_expr_or_const_correct_base _ e) by eassumption; cbv beta iota - end + | progress subst_prod + | rewrite_interp_as_expr_or_const_correct_base () + | rewrite_interp_as_expr_or_const_correct_prod_base () + | rewrite_interp_as_expr_or_const_correct_prod3_base () | progress unfold interp_op, lift_op | progress Z.ltb_to_lt - | progress rewrite ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_0_l, ?Z.lor_0_r ]. + | progress rewrite ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_0_l, ?Z.lor_0_r + | rewrite !Z.sub_with_borrow_to_add_get_carry + | progress autorewrite with zsimplify_fast ]. Qed. Hint Rewrite @InterpSimplifyArith : reflective_interp. |