diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-12 16:31:41 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-12 16:31:41 -0500 |
| commit | 3d3b942308e09a678641005eabdc2f3761f0edae (patch) | |
| tree | 13739d3afa192ce6439d0a8a696518dc26c7d537 /src | |
| parent | 86ebe2d8218eb5d3559a3c17cbd2652636d4d564 (diff) | |
Work around bug #5198 (broken tc resolution)
This is https://coq.inria.fr/bugs/show_bug.cgi?id=5198, Inlining lets
breaks typechecking of [Definition]s
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/SC25519.v | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/src/Specific/SC25519.v b/src/Specific/SC25519.v index 9ce1213c0..9d8e7caee 100644 --- a/src/Specific/SC25519.v +++ b/src/Specific/SC25519.v @@ -105,11 +105,16 @@ Section Z. { reflexivity. } Qed. Definition SRepAdd : SRep -> SRep -> SRep - := Eval srep in fun x y => barrett_reduce_function_bundled (snd (ZBounded.CarryAdd x y)). + := Eval srep in + let work_around_bug_5198 + := fun x y => barrett_reduce_function_bundled (snd (ZBounded.CarryAdd x y)) + in work_around_bug_5198. Lemma SRepAdd_Correct : forall x y : ModularArithmetic.F.F l, SRepEq (S2Rep (ModularArithmetic.F.add x y)) (SRepAdd (S2Rep x) (S2Rep y)). Proof. intros x y; unfold SRepEq, S2Rep, b in *; simpl. - transitivity_refl (barrett_reduce_function_bundled (snd (ZBounded.CarryAdd (F.to_Z x) (F.to_Z y)))). + transitivity_refl (let work_around_bug_5198 + := fun x y => barrett_reduce_function_bundled (snd (ZBounded.CarryAdd x y)) + in work_around_bug_5198 (F.to_Z x) (F.to_Z y)). pose proof (ModularArithmeticTheorems.F.to_Z_range x). pose proof (ModularArithmeticTheorems.F.to_Z_range y). unfold l in *; specialize_by auto using modulusv_pos. @@ -124,11 +129,16 @@ Section Z. Global Instance SRepAdd_Proper : Proper (SRepEq ==> SRepEq ==> SRepEq) SRepAdd. Proof. unfold SRepEq; repeat intro; subst; reflexivity. Qed. Definition SRepMul : SRep -> SRep -> SRep - := Eval srep in fun x y => barrett_reduce_function_bundled (ZBounded.Mul x y). + := Eval srep in + let work_around_bug_5198 + := fun x y => barrett_reduce_function_bundled (ZBounded.Mul x y) + in work_around_bug_5198. Lemma SRepMul_Correct : forall x y : ModularArithmetic.F.F l, SRepEq (S2Rep (ModularArithmetic.F.mul x y)) (SRepMul (S2Rep x) (S2Rep y)). Proof. intros x y; unfold SRepEq, S2Rep, b in *; simpl. - transitivity_refl (barrett_reduce_function_bundled (ZBounded.Mul (F.to_Z x) (F.to_Z y))). + transitivity_refl (let work_around_bug_5198 + := fun x y => barrett_reduce_function_bundled (ZBounded.Mul x y) + in work_around_bug_5198 (F.to_Z x) (F.to_Z y)). pose proof (ModularArithmeticTheorems.F.to_Z_range x). pose proof (ModularArithmeticTheorems.F.to_Z_range y). unfold l in *; specialize_by auto using modulusv_pos. |