diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-14 00:34:52 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-14 00:45:47 -0400 |
commit | d5bfa641ac3269b90bf8fd23511d110b99b3f5fb (patch) | |
tree | 39fa098cc8126229dbd3adde774004923e178ec9 /src/Compilers/Z/ArithmeticSimplifierWf.v | |
parent | a0e2a43ddba56a58673c1acffe6fd179f78255ee (diff) |
Rework and speed up arithmetic simplifier proofs
Induction is so much faster than brute force.
After | File Name | Before || Change
--------------------------------------------------------------------------------
6m15.02s | Total | 7m14.18s || -0m59.15s
--------------------------------------------------------------------------------
0m11.62s | Compilers/Z/ArithmeticSimplifierWf | 0m42.97s || -0m31.35s
0m06.52s | Compilers/Z/ArithmeticSimplifierInterp | 0m34.28s || -0m27.76s
2m47.55s | Specific/IntegrationTestLadderstep | 2m48.14s || -0m00.58s
1m09.50s | Specific/IntegrationTestKaratsubaMul | 1m08.86s || +0m00.64s
1m03.53s | Specific/IntegrationTestLadderstep130 | 1m04.05s || -0m00.51s
0m16.39s | Specific/IntegrationTestFreeze | 0m16.29s || +0m00.10s
0m13.60s | Specific/IntegrationTestMul | 0m13.60s || +0m00.00s
0m11.58s | Specific/IntegrationTestSub | 0m11.36s || +0m00.22s
0m09.79s | Specific/IntegrationTestSquare | 0m09.71s || +0m00.07s
0m03.64s | Compilers/Z/Bounds/Pipeline/Definition | 0m03.54s || +0m00.10s
0m00.75s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.80s || -0m00.05s
0m00.55s | Compilers/Z/Bounds/Pipeline | 0m00.58s || -0m00.02s
Diffstat (limited to 'src/Compilers/Z/ArithmeticSimplifierWf.v')
-rw-r--r-- | src/Compilers/Z/ArithmeticSimplifierWf.v | 247 |
1 files changed, 103 insertions, 144 deletions
diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v index 176301e06..33f3c3335 100644 --- a/src/Compilers/Z/ArithmeticSimplifierWf.v +++ b/src/Compilers/Z/ArithmeticSimplifierWf.v @@ -1,4 +1,5 @@ Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Wf. Require Import Crypto.Compilers.WfInversion. Require Import Crypto.Compilers.TypeInversion. @@ -8,6 +9,7 @@ Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.OpInversion. Require Import Crypto.Compilers.Z.ArithmeticSimplifier. Require Import Crypto.Compilers.Z.Syntax.Equality. +Require Import Crypto.Compilers.Z.Syntax.Util. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Option. Require Import Crypto.Util.Sum. @@ -99,130 +101,55 @@ Local Ltac pret_step := => is_var e; destruct (interp_as_expr_or_const e) eqn:? end ]. -Lemma wff_interp_as_expr_or_const_base {var1 var2 t} {G e1 e2 v1 v2} - (Hwf : @wff var1 var2 G (Tbase t) e1 e2) - : @interp_as_expr_or_const var1 (Tbase t) e1 = Some v1 - -> @interp_as_expr_or_const var2 (Tbase t) e2 = Some v2 - -> match v1, v2 with - | const_of z1, const_of z2 => z1 = z2 - | gen_expr e1, gen_expr e2 - | neg_expr e1, neg_expr e2 - => wff G e1 e2 - | const_of _, _ - | gen_expr _, _ - | neg_expr _, _ - => False - end. -Proof. - invert_one_expr e1; intros; break_innermost_match; intros; - try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in - invert_one_expr e2); intros; - repeat first [ fin_t - | progress simpl in * - | progress intros - | break_t_step - | match goal with - | [ H : wff _ _ ?e |- _ ] => is_var e; invert_one_expr e - end ]. -Qed. - -Local Ltac pose_wff_base := - match goal with - | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] - => pose proof (wff_interp_as_expr_or_const_base Hwf H1 H2); clear H1 H2 - end. - -Lemma wff_interp_as_expr_or_const_prod_base {var1 var2 A B} {G e1 e2} {v1 v2 : _ * _} - (Hwf : wff G e1 e2) - : @interp_as_expr_or_const var1 (Prod (Tbase A) (Tbase B)) e1 = Some v1 - -> @interp_as_expr_or_const var2 (Prod (Tbase A) (Tbase B)) e2 = Some v2 - -> match fst v1, fst v2 with - | const_of z1, const_of z2 => z1 = z2 - | gen_expr e1, gen_expr e2 - | neg_expr e1, neg_expr e2 - => wff G e1 e2 - | const_of _, _ - | gen_expr _, _ - | neg_expr _, _ - => False - end - /\ match snd v1, snd v2 with - | const_of z1, const_of z2 => z1 = z2 - | gen_expr e1, gen_expr e2 - | neg_expr e1, neg_expr e2 - => wff G e1 e2 - | const_of _, _ - | gen_expr _, _ - | neg_expr _, _ - => False - end. -Proof. - invert_one_expr e1; intros; break_innermost_match; intros; try exact I; - try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in - invert_one_expr e2); - intros; break_innermost_match; intros; try exact I; - repeat first [ pret_step - | pose_wff_base - | break_t_step - | apply conj ]. -Qed. - -Local Ltac pose_wff_prod := - match goal with - | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] - => pose proof (wff_interp_as_expr_or_const_prod_base Hwf H1 H2); clear H1 H2 - end. +Fixpoint wff_as_expr_or_const {var1 var2} G {t} + : interp_flat_type (@inverted_expr var1) t + -> interp_flat_type (@inverted_expr var2) t + -> Prop + := match t with + | Tbase T + => fun z1 z2 => match z1, z2 return Prop with + | const_of z1, const_of z2 => z1 = z2 + | gen_expr e1, gen_expr e2 + | neg_expr e1, neg_expr e2 + => wff G e1 e2 + | const_of _, _ + | gen_expr _, _ + | neg_expr _, _ + => False + end + | Unit => fun _ _ => True + | Prod A B => fun a b : interp_flat_type _ A * interp_flat_type _ B + => and (@wff_as_expr_or_const var1 var2 G A (fst a) (fst b)) + (@wff_as_expr_or_const var1 var2 G B (snd a) (snd b)) + end. -Lemma wff_interp_as_expr_or_const_prod3_base {var1 var2 A B C} {G e1 e2} {v1 v2 : _ * _ * _} - (Hwf : wff G e1 e2) - : @interp_as_expr_or_const var1 (Prod (Prod (Tbase A) (Tbase B)) (Tbase C)) e1 = Some v1 - -> @interp_as_expr_or_const var2 (Prod (Prod (Tbase A) (Tbase B)) (Tbase C)) e2 = Some v2 - -> match fst (fst v1), fst (fst v2) with - | const_of z1, const_of z2 => z1 = z2 - | gen_expr e1, gen_expr e2 - | neg_expr e1, neg_expr e2 - => wff G e1 e2 - | const_of _, _ - | gen_expr _, _ - | neg_expr _, _ - => False - end - /\ match snd (fst v1), snd (fst v2) with - | const_of z1, const_of z2 => z1 = z2 - | gen_expr e1, gen_expr e2 - | neg_expr e1, neg_expr e2 - => wff G e1 e2 - | const_of _, _ - | gen_expr _, _ - | neg_expr _, _ - => False - end - /\ match snd v1, snd v2 with - | const_of z1, const_of z2 => z1 = z2 - | gen_expr e1, gen_expr e2 - | neg_expr e1, neg_expr e2 - => wff G e1 e2 - | const_of _, _ - | gen_expr _, _ - | neg_expr _, _ - => False - end. +Lemma wff_interp_as_expr_or_const {var1 var2 t} {G e1 e2 v1 v2} + (Hwf : @wff var1 var2 G t e1 e2) + : @interp_as_expr_or_const var1 t e1 = Some v1 + -> @interp_as_expr_or_const var2 t e2 = Some v2 + -> wff_as_expr_or_const G v1 v2. Proof. - invert_one_expr e1; intros; break_innermost_match; intros; try exact I; - try (let e2 := match goal with Hwf : wff ?G ?e1 ?e2 |- _ => e2 end in - invert_one_expr e2); - intros; break_innermost_match; intros; try exact I; - repeat first [ pret_step - | pose_wff_base - | pose_wff_prod - | break_t_step - | apply conj ]. + induction Hwf; + repeat first [ progress subst + | progress inversion_option + | progress simpl in * + | progress cbn [wff_as_expr_or_const] + | reflexivity + | break_innermost_match_hyps_step + | intro + | match goal with + | [ H : forall z, Some _ = Some z -> _ |- _ ] => specialize (H _ eq_refl) + | [ |- context[match ?e with _ => _ end] ] + => is_var e; invert_one_op e + end + | break_innermost_match_step + | solve [ auto with wf ] ]. Qed. -Local Ltac pose_wff_prod3 := +Local Ltac pose_wff _ := match goal with | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] - => pose proof (wff_interp_as_expr_or_const_prod3_base Hwf H1 H2); clear H1 H2 + => pose proof (wff_interp_as_expr_or_const Hwf H1 H2); clear H1 H2 end. Lemma Wf_SimplifyArith {convert_adc_to_sbb} {t} (e : Expr t) @@ -230,32 +157,64 @@ Lemma Wf_SimplifyArith {convert_adc_to_sbb} {t} (e : Expr t) : Wf (SimplifyArith convert_adc_to_sbb e). Proof. apply Wf_RewriteOp; [ | assumption ]. - intros ???????? Hwf'; unfold simplify_op_expr; - repeat match goal with - | [ H : ?T |- ?T ] => exact H - | [ H : False |- _ ] => exfalso; assumption - | [ H : false = true |- _ ] => exfalso; clear -H; discriminate - | [ H : true = false |- _ ] => exfalso; clear -H; discriminate - | _ => pose_wff_base - | _ => pose_wff_prod - | _ => pose_wff_prod3 - | _ => progress destruct_head'_and - | _ => progress subst - | _ => inversion_base_type_constr_step - | [ H1 : _ = Some _, H2 : _ = None, Hwf : wff _ _ _ |- _ ] - => pose proof (interp_as_expr_or_const_Some_None Hwf H1 H2); clear H1 H2 - | [ H1 : _ = None, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] - => pose proof (interp_as_expr_or_const_None_Some Hwf H1 H2); clear H1 H2 - | [ |- wff _ (Op _ _) (LetIn _ _) ] => exfalso - | [ |- wff _ (LetIn _ _) (Op _ _) ] => exfalso - | [ |- wff _ (Pair _ _) (LetIn _ _) ] => exfalso - | [ |- wff _ (LetIn _ _) (Pair _ _) ] => exfalso - | [ |- wff _ _ _ ] => constructor; intros - | [ |- List.In _ _ ] => progress (simpl; auto) - | _ => rewrite FixedWordSizesEquality.ZToWord_wordToZ - | _ => rewrite FixedWordSizesEquality.ZToWord_wordToZ_ZToWord by reflexivity - | _ => break_innermost_match_step; simpl in * - end. + intros ???????? Hwf'; unfold simplify_op_expr. + repeat match goal with + | [ H : ?T |- ?T ] => exact H + | [ H : False |- _ ] => exfalso; assumption + | [ |- True ] => exact I + | [ H : false = true |- _ ] => exfalso; clear -H; discriminate + | [ H : true = false |- _ ] => exfalso; clear -H; discriminate + | [ H : None = Some _ |- _ ] => exfalso; clear -H; discriminate + | [ H : Some _ = None |- _ ] => exfalso; clear -H; discriminate + | [ H : TT = Op _ _ |- _ ] => exfalso; clear -H; discriminate + | [ H : invert_Op ?e = None, H' : wff _ (Op ?opc _) ?e |- _ ] + => progress (exfalso; clear -H H'; generalize dependent opc; intros; try (is_var e; destruct e)) + | [ H : invert_Op ?e = None, H' : wff _ ?e (Op ?opc _) |- _ ] + => progress (exfalso; clear -H H'; generalize dependent opc; intros; try (is_var e; destruct e)) + | _ => progress destruct_head'_and + | _ => progress subst + | _ => progress destruct_head'_prod + | _ => progress destruct_head'_sig + | _ => progress destruct_head'_sigT + | _ => inversion_base_type_constr_step + | _ => inversion_wf_step_constr + | _ => progress invert_expr_subst + | _ => progress rewrite_eta_match_base_type_impl + | [ H : ?x = ?x |- _ ] => clear H || (progress eliminate_hprop_eq) + | [ H : match ?e with @const_of _ _ _ => _ = _ | _ => _ end |- _ ] + => is_var e; destruct e + | [ H : match ?e with @const_of _ _ _ => False | _ => _ end |- _ ] + => is_var e; destruct e + | [ H1 : _ = Some _, H2 : _ = None, Hwf : wff _ _ _ |- _ ] + => pose proof (interp_as_expr_or_const_Some_None Hwf H1 H2); clear H1 H2 + | [ H1 : _ = None, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] + => pose proof (interp_as_expr_or_const_None_Some Hwf H1 H2); clear H1 H2 + | [ |- wff _ (Op _ _) (LetIn _ _) ] => exfalso + | [ |- wff _ (LetIn _ _) (Op _ _) ] => exfalso + | [ |- wff _ (Pair _ _) (LetIn _ _) ] => exfalso + | [ |- wff _ (LetIn _ _) (Pair _ _) ] => exfalso + | _ => pose_wff () + | _ => progress cbn [fst snd projT1 projT2 interp_flat_type wff_as_expr_or_const eq_rect invert_Op] in * + | [ |- wff _ _ _ ] => constructor; intros + | [ H : match ?e with @const_of _ _ _ => _ | _ => _ end |- _ ] + => is_var e; destruct e + | [ |- context[match @interp_as_expr_or_const ?var ?t ?e with _ => _ end] ] + => destruct (@interp_as_expr_or_const var t e) eqn:? + | [ |- context[match base_type_eq_semidec_transparent ?t1 ?t2 with _ => _ end] ] + => destruct (base_type_eq_semidec_transparent t1 t2) + | [ |- context[match @invert_Op ?base_type ?op ?var ?t ?e with _ => _ end] ] + => destruct (@invert_Op base_type op var t e) eqn:? + | [ |- context[if BinInt.Z.eqb ?x ?y then _ else _] ] + => destruct (BinInt.Z.eqb x y) eqn:? + | [ |- context[if BinInt.Z.ltb ?x ?y then _ else _] ] + => destruct (BinInt.Z.ltb x y) eqn:? + | [ |- context[match ?e with @OpConst _ _ => _ | _ => _ end] ] + => is_var e; destruct e + | [ |- context[match ?e with @OpConst _ _ => _ | _ => _ end] ] + => is_var e; invert_one_op e; try exact I; break_innermost_match_step; intros + | [ |- List.In _ _ ] => progress (simpl; auto) + | _ => break_innermost_match_step + end. Qed. Hint Resolve Wf_SimplifyArith : wf. |