diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-09-17 11:45:17 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-09-17 11:45:17 -0400 |
commit | fa0db09b0d91a76eec2f77bbb50815516feaf864 (patch) | |
tree | b6614585475ce9855604f12e4f263b5c86771921 /src/ModularArithmetic | |
parent | ea4c038614a2eba5e637d1ccd3d087fafd79eb7b (diff) |
deduplicate Let_In into src/Util/LetIn.v
Diffstat (limited to 'src/ModularArithmetic')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 24 |
1 files changed, 2 insertions, 22 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 2d4bb525f..eda2a584d 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -11,6 +11,7 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystem. Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. Require Import Coq.Lists.List. Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.AdditionChainExponentiation. Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil Crypto.Util.NatUtil Crypto.Util.CaseUtil. Import ListNotations. @@ -54,9 +55,6 @@ Definition zeros_opt := Eval compute in (@zeros). Definition bit_index_opt := Eval compute in bit_index. Definition digit_index_opt := Eval compute in digit_index. -Definition Let_In {A P} (x : A) (f : forall y : A, P y) - := let y := x in f y. - (* Some automation that comes in handy when constructing base parameters *) Ltac opt_step := match goal with @@ -160,23 +158,6 @@ Ltac kill_precondition H := forward H; [abstract (try exact eq_refl; clear; cbv; intros; repeat break_or_hyp; intuition)|]; subst_precondition. -Lemma Let_In_push : forall {A B C} (g : A -> B) (f : B -> C) x, - f (Let_In x g) = Let_In x (fun y => f (g y)). -Proof. - intros. - cbv [Let_In]. - reflexivity. -Qed. - -Lemma Let_In_ext : forall {A B} (f g : A -> B) x, - (forall x, f x = g x) -> - Let_In x g = Let_In x f. -Proof. - intros. - cbv [Let_In]. - congruence. -Qed. - Section Carries. Context `{prm : PseudoMersenneBaseParams} (* allows caller to precompute k and c *) @@ -680,7 +661,7 @@ Proof. + destruct a. apply IHy1. econstructor; try assumption. - apply H0; rewrite H; reflexivity. + apply H0; eapply Proper_nth_default; eauto; reflexivity. Qed. Section PowInv. @@ -748,7 +729,6 @@ Section PowInv. Definition inv_opt_correct x : eq (inv_opt x) (inv chain chain_correct x) := Eval cbv [proj2_sig inv_opt_sig] in (proj2_sig (inv_opt_sig x)). - End PowInv. Section Conversion. |