diff options
Diffstat (limited to 'src/ModularArithmetic')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index d1bd49a55..3b50662a6 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -892,6 +892,24 @@ Section Canonicalization. : conditional_subtract_modulus_opt f cond = conditional_subtract_modulus f cond := Eval cbv [proj2_sig conditional_subtract_modulus_opt_sig] in proj2_sig (conditional_subtract_modulus_opt_sig f cond). + Definition ge_modulus_opt_sig (us : list Z) : + { b : bool | b = ModularBaseSystemList.ge_modulus us }. + Proof. + eexists. + cbv beta iota delta [ge_modulus ge_modulus']. + change length with length_opt. + change nth_default with @nth_default_opt. + change minus with minus_opt. + reflexivity. + Defined. + + Definition ge_modulus_opt us : bool + := Eval cbv [proj1_sig ge_modulus_opt_sig] in proj1_sig (ge_modulus_opt_sig us). + + Definition ge_modulus_opt_correct us : + ge_modulus_opt us = ge_modulus us + := Eval cbv [proj2_sig ge_modulus_opt_sig] in proj2_sig (ge_modulus_opt_sig us). + Definition freeze_opt_sig (us : list Z) : { b : list Z | length us = length limb_widths -> b = ModularBaseSystemList.freeze us }. |