diff options
| -rw-r--r-- | src/Arithmetic/Saturated/MontgomeryAPI.v | 31 | ||||
| -rw-r--r-- | src/Compilers/MultiSizeTest.v | 2 | ||||
| -rw-r--r-- | src/Compilers/Wf.v | 4 |
3 files changed, 1 insertions, 36 deletions
diff --git a/src/Arithmetic/Saturated/MontgomeryAPI.v b/src/Arithmetic/Saturated/MontgomeryAPI.v index 092630eab..e84c8d083 100644 --- a/src/Arithmetic/Saturated/MontgomeryAPI.v +++ b/src/Arithmetic/Saturated/MontgomeryAPI.v @@ -383,23 +383,9 @@ Section API. eauto using small_add, small_join0. Qed. - Lemma small_add_S2 n a b : - (2 <= bound) -> - small a -> small b -> small (@add_S2 n a b). - Proof. - intros. pose_all. - cbv [add_cps add add_S2 Let_In]. - autorewrite with uncps push_id. - (*apply Positional.small_sat_add.*) - Admitted. - Lemma small_left_tl n (v:T (S n)) : small v -> small (left_tl v). Proof. cbv [small]. auto using Tuple.In_to_list_left_tl. Qed. - Lemma small_divmod n (p: T (S n)) (Hsmall : small p) : - left_hd p = eval p / uweight bound n /\ eval (left_tl p) = eval p mod (uweight bound n). - Admitted. - Lemma eval_drop_high n v : small v -> eval (@drop_high n v) = eval v mod (uweight bound n). Proof. @@ -482,21 +468,6 @@ Section API. apply small_drop_high, @B.Positional.small_sat_add; omega. Qed. - (* TODO : remove if unneeded when all admits are proven - Lemma small_highest_zero_iff {n} (p: T (S n)) (Hsmall : small p) : - (left_hd p = 0 <-> eval p < uweight bound n). - Proof. - destruct (small_divmod _ p Hsmall) as [Hdiv Hmod]. - pose proof Hsmall as Hsmalltl. apply eval_small in Hsmall. - apply small_left_tl, eval_small in Hsmalltl. rewrite Hdiv. - rewrite (Z.div_small_iff (eval p) (uweight bound n)) - by auto using uweight_nonzero. - split; [|intros; left; omega]. - let H := fresh "H" in intro H; destruct H; [|omega]. - omega. - Qed. - *) - Lemma map2_zselect n cond x y : Tuple.map2 (n:=n) (Z.zselect cond) x y = if dec (cond = 0) then x else y. Proof. @@ -632,4 +603,4 @@ Section API. Qed. End Proofs. End API. -Hint Rewrite nonzero_id join0_id divmod_id drop_high_id scmul_id add_id add_S1_id add_S2_id sub_then_maybe_add_id conditional_sub_id : uncps.
\ No newline at end of file +Hint Rewrite nonzero_id join0_id divmod_id drop_high_id scmul_id add_id add_S1_id add_S2_id sub_then_maybe_add_id conditional_sub_id : uncps. diff --git a/src/Compilers/MultiSizeTest.v b/src/Compilers/MultiSizeTest.v index fab0c65d8..c31127126 100644 --- a/src/Compilers/MultiSizeTest.v +++ b/src/Compilers/MultiSizeTest.v @@ -82,8 +82,6 @@ Definition typeD (t : type) : Type := | Word9 => word9 end. -Axiom admit : forall T, T. - Theorem O_lt_S : forall n, O < S n. Proof. intros; omega. diff --git a/src/Compilers/Wf.v b/src/Compilers/Wf.v index a56d3bbdd..85c24886b 100644 --- a/src/Compilers/Wf.v +++ b/src/Compilers/Wf.v @@ -59,12 +59,8 @@ Section language. End with_var. Definition Wf {t} (E : @Expr t) := forall var1 var2, wf (E var1) (E var2). - - Axiom Wf_admitted : forall {t} (E:Expr t), @Wf t E. End language. -Ltac admit_Wf := apply Wf_admitted. - Global Arguments wff {_ _ _ _} G {t} _ _. Global Arguments wf {_ _ _ _ t} _ _. Global Arguments Wf {_ _ t} _. |