diff options
| -rw-r--r-- | src/Algebra.v | 24 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 16 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 13 | ||||
| -rw-r--r-- | src/Spec/CompleteEdwardsCurve.v | 5 | ||||
| -rw-r--r-- | src/WeierstrassCurve/Pre.v | 3 |
5 files changed, 19 insertions, 42 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 9f53c0613..f2c47b081 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -984,26 +984,6 @@ Ltac neq01 := |apply one_neq_zero |apply Group.opp_one_neq_zero]. -Ltac conservative_field_algebra := - intros; - conservative_common_denominator_all; - try nsatz; - repeat (apply conj); - try solve - [neq01 - |trivial - |apply Ring.opp_nonzero_nonzero;trivial]. - -Ltac field_algebra := - intros; - common_denominator_all; - try nsatz; - repeat (apply conj); - try solve - [neq01 - |trivial - |apply Ring.opp_nonzero_nonzero;trivial]. - Ltac combine_field_inequalities_step := match goal with | [ H : not (?R ?x ?zero), H' : not (?R ?x' ?zero) |- _ ] @@ -1184,10 +1164,10 @@ Section Example. Add Field _ExampleField : (Field.field_theory_for_stdlib_tactic (T:=F)). Example _example_nsatz x y : 1+1 <> 0 -> x + y = 0 -> x - y = 0 -> x = 0. - Proof. field_algebra. Qed. + Proof. intros. nsatz. Qed. Example _example_field_nsatz x y z : y <> 0 -> x/y = z -> z*y + y = x + y. - Proof. intros; subst; field_algebra. Qed. + Proof. intros. super_nsatz. Qed. Example _example_nonzero_nsatz_contradict x y : x * y = 1 -> not (x = 0). Proof. intros. intro. nsatz_contradict. Qed. diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 263582508..d8efb82f3 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -33,6 +33,7 @@ Module Extended. Create HintDb bash discriminated. Local Hint Unfold E.eq fst snd fieldwise fieldwise' coordinates E.coordinates proj1_sig Pre.onCurve : bash. Ltac bash := + pose proof E.char_gt_2; repeat match goal with | |- Proper _ _ => intro | _ => progress intros @@ -43,15 +44,11 @@ Module Extended. | |- _ /\ _ => split | _ => solve [neq01] | _ => solve [eauto] - | _ => solve [intuition] + | _ => solve [intuition eauto] | _ => solve [etransitivity; eauto] - | |- Feq _ _ => field_algebra - | |- _ <> 0 => apply mul_nonzero_nonzero - | [ H : _ <> 0 |- _ <> 0 ] => - intro; apply H; - field_algebra; - solve [ apply Ring.opp_nonzero_nonzero, E.char_gt_2 - | apply E.char_gt_2] + | |- _*_ <> 0 => apply mul_nonzero_nonzero + | [H: _ |- _ ] => solve [intro; apply H; super_nsatz] + | |- Feq _ _ => super_nsatz end. Obligation Tactic := bash. @@ -63,8 +60,7 @@ Module Extended. (let '(X,Y,Z,T) := coordinates P in ((X/Z), (Y/Z))) _. Definition eq (P Q:point) := E.eq (to_twisted P) (to_twisted Q). - Global Instance DecidableRel_eq : Decidable.DecidableRel eq. - Proof. typeclasses eauto. Qed. + Global Instance DecidableRel_eq : Decidable.DecidableRel eq := _. Local Hint Unfold from_twisted to_twisted eq : bash. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index 432e834aa..a83c85b02 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -50,24 +50,25 @@ Section Pre. => apply d_nonsquare with (sqrt_d:= (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) /(f (sqrt_a * x2) y2 * x1 * y1 )) | _ => apply a_nonzero - end; field_algebra; auto using Ring.opp_nonzero_nonzero; nsatz_contradict. + end; super_nsatz. Qed. Lemma edwardsAddCompletePlus x1 y1 x2 y2 : onCurve (x1, y1) -> onCurve (x2, y2) -> (1 + d*x1*x2*y1*y2) <> 0. - Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed. + Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); super_nsatz. Qed. Lemma edwardsAddCompleteMinus x1 y1 x2 y2 : onCurve (x1, y1) -> onCurve (x2, y2) -> (1 - d*x1*x2*y1*y2) <> 0. - Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed. + Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); super_nsatz. Qed. - Lemma zeroOnCurve : onCurve (0, 1). Proof. simpl. field_algebra. Qed. + Lemma zeroOnCurve : onCurve (0, 1). Proof. simpl. super_nsatz. Qed. Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). Proof. - unfold onCurve, unifiedAdd'; intros [x1 y1] [x2 y2] H1 H2. - field_algebra; auto using edwardsAddCompleteMinus, edwardsAddCompletePlus. + unfold onCurve, unifiedAdd'; intros [x1 y1] [x2 y2] ? ?. + conservative_common_denominator; [ | auto using edwardsAddCompleteMinus, edwardsAddCompletePlus..]. + nsatz. Qed. End Pre. diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index f6db1c14f..16a1217ce 100644 --- a/src/Spec/CompleteEdwardsCurve.v +++ b/src/Spec/CompleteEdwardsCurve.v @@ -29,8 +29,9 @@ Module E. Definition coordinates (P:point) : (F*F) := proj1_sig P. (** The following points are indeed on the curve -- see [CompleteEdwardsCurve.Pre] for proof *) - Local Obligation Tactic := intros; apply Pre.zeroOnCurve - || apply (Pre.unifiedAdd'_onCurve (char_gt_2:=char_gt_2) (d_nonsquare:=nonsquare_d) + Local Obligation Tactic := intros; + apply (Pre.zeroOnCurve(a_nonzero:=nonzero_a)(char_gt_2:=char_gt_2)) || + apply (Pre.unifiedAdd'_onCurve (char_gt_2:=char_gt_2) (d_nonsquare:=nonsquare_d) (a_nonzero:=nonzero_a) (a_square:=square_a) _ _ (proj2_sig _) (proj2_sig _)). Program Definition zero : point := (0, 1). diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v index 71a970b7d..b140e95b5 100644 --- a/src/WeierstrassCurve/Pre.v +++ b/src/WeierstrassCurve/Pre.v @@ -51,7 +51,6 @@ Section Pre. onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). Proof. unfold onCurve, unifiedAdd'; intros [[x1 y1]|] [[x2 y2]|] H1 H2; - break_match; trivial; setoid_subst_rel eq; only_two_square_roots; - field_algebra; nsatz_contradict. + break_match; trivial; setoid_subst_rel eq; only_two_square_roots; super_nsatz. Qed. End Pre. |