diff options
| author |  jadep <jadep@mit.edu> | 2019-02-15 14:56:22 -0500 |
|---|---|---|
| committer |  jadephilipoom <jade.philipoom@gmail.com> | 2019-02-21 11:10:12 -0500 |
| commit | 9025014cf7b64082d0bfed93dd76ba99ab9bb72b (patch) | |
| tree | 9ef8dd60ee34fe50335b53b1b57f56bf39f84d47 /src | |
| parent | a1f9d9ee2c662790b43bf56df58121a390efbe7c (diff) | |
Make Qed not take forever
Diffstat (limited to 'src')
| -rw-r--r-- | src/PushButtonSynthesis/BarrettReduction.v | 1 | ||||
| -rw-r--r-- | src/PushButtonSynthesis/MontgomeryReduction.v | 7 |
2 files changed, 5 insertions, 3 deletions
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 |