From 9025014cf7b64082d0bfed93dd76ba99ab9bb72b Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 15 Feb 2019 14:56:22 -0500 Subject: Make Qed not take forever --- src/PushButtonSynthesis/BarrettReduction.v | 1 + src/PushButtonSynthesis/MontgomeryReduction.v | 7 ++++--- 2 files changed, 5 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v index bc525412a..224584c4a 100644 --- a/src/PushButtonSynthesis/BarrettReduction.v +++ b/src/PushButtonSynthesis/BarrettReduction.v @@ -96,6 +96,7 @@ Section rbarrett_red. prefix "barrett_red" barrett_red (fun _ _ _ => @nil string). + Local Strategy -100 [barrett_red]. (* Probably needed to make Qed not take forever *) (* TODO: Replace the following lemmas with a new-glue-style correctness lemma, like << Lemma barrett_red_correct res diff --git a/src/PushButtonSynthesis/MontgomeryReduction.v b/src/PushButtonSynthesis/MontgomeryReduction.v index 1387cad36..d4399a743 100644 --- a/src/PushButtonSynthesis/MontgomeryReduction.v +++ b/src/PushButtonSynthesis/MontgomeryReduction.v @@ -183,7 +183,8 @@ Lemma montred_correct res | rewrite Z.div_add' by lia | rewrite Z.div_small by lia | progress Z.rewrite_mod_small ]. - + + Local Strategy -100 [montred]. (* needed for making Qed not take forever *) Lemma montred_correct res (Hres : montred = Success res) : montred_correct N R R' (expr.Interp (@ident.gen_interp cast_oor) res). Proof using n nout curve_good. @@ -195,7 +196,7 @@ Lemma montred_correct res rewrite Bool.andb_true_iff, !Z.leb_le. lia. } { cbv [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by bound is_bounded_by_bool value_range upper lower]. rewrite Bool.andb_true_iff, !Z.leb_le. lia. } - Admitted. + Qed. End rmontred. -(* TODO: get Barrett to this same point, even if Qed slow, and then use these lemmas in the specific files *) \ No newline at end of file +(* TODO: get Barrett to this same point, and then use these lemmas in the specific files *) \ No newline at end of file -- cgit v1.2.3