From 03403f0a6c9bcb610de0a82419f13105e82824b2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 18 Oct 2016 18:26:10 -0400 Subject: Define carry_opp in terms of carry_sub --- src/ModularArithmetic/ModularBaseSystem.v | 2 +- src/ModularArithmetic/ModularBaseSystemOpt.v | 23 +++++++---------------- 2 files changed, 8 insertions(+), 17 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index ff2c23ab8..5c0d143c2 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -74,7 +74,7 @@ Section ModularBaseSystem. Definition carry_opp (carry_chain : list nat) (modulus_multiple : digits) (modulus_multiple_correct : decode modulus_multiple = 0%F) (x : digits) : digits := - carry_ carry_chain (opp modulus_multiple modulus_multiple_correct x). + carry_sub carry_chain modulus_multiple modulus_multiple_correct zero x. Definition rep (us : digits) (x : F modulus) := decode us = x. Local Notation "u ~= x" := (rep u x). diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index f1b8c601b..ff1dd87dd 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -533,29 +533,20 @@ Section Subtraction. : opp_opt us = opp coeff coeff_mod us := proj2_sig (opp_opt_sig us). - Definition carry_opp_opt_sig {T} (f:digits -> T) - (us : digits) : { x | x = f (carry_opp carry_chain coeff coeff_mod us) }. + Definition carry_opp_opt_sig (us : digits) : { b : digits | b = carry_opp carry_chain coeff coeff_mod us }. Proof. eexists. cbv [carry_opp]. - rewrite <-carry__opt_cps_correct, <-opp_opt_correct. - cbv [carry_sequence_opt_cps carry__opt_cps opp_opt opp sub_opt]. - rewrite to_list_from_list. + rewrite <-carry_sub_opt_correct. reflexivity. Defined. - Definition carry_opp_opt_cps {T} (f:digits -> T) (us : digits) : T - := Eval cbv [proj1_sig carry_opp_opt_sig] in proj1_sig (carry_opp_opt_sig f us). - - Definition carry_opp_opt_cps_correct {T} (f:digits -> T) (us : digits) - : carry_opp_opt_cps f us = f (carry_opp carry_chain coeff coeff_mod us) - := proj2_sig (carry_opp_opt_sig f us). - - Definition carry_opp_opt := carry_opp_opt_cps id. + Definition carry_opp_opt (us : digits) : digits + := Eval cbv [proj1_sig carry_opp_opt_sig] in proj1_sig (carry_opp_opt_sig us). - Definition carry_opp_opt_correct (us : digits) - : carry_opp_opt us = carry_opp carry_chain coeff coeff_mod us := - carry_opp_opt_cps_correct id us. + Definition carry_opp_opt_correct us + : carry_opp_opt us = carry_opp carry_chain coeff coeff_mod us + := proj2_sig (carry_opp_opt_sig us). End Subtraction. -- cgit v1.2.3