diff options
| -rw-r--r-- | src/Algebra.v | 50 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 6 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 2 |
3 files changed, 29 insertions, 29 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 2ce0183ca..f083b06da 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -771,11 +771,11 @@ Ltac set_nonfraction_pieces := ltac:(fun T' => change T'); deduplicate_nonfraction_pieces mul end. -Ltac default_conservative_common_denominator_nonzero_tac := +Ltac default_common_denominator_nonzero_tac := repeat apply conj; try first [ assumption | intro; field_nonzero_mul_split; tauto ]. -Ltac conservative_common_denominator_in H := +Ltac common_denominator_in H := idtac; let fld := guess_field in let div := lazymatch type of fld with @@ -787,11 +787,11 @@ Ltac conservative_common_denominator_in H := => set_nonfraction_pieces_in H; field_simplify_eq_if_div_in H; [ - | default_conservative_common_denominator_nonzero_tac.. ]; + | default_common_denominator_nonzero_tac.. ]; repeat match goal with H := _ |- _ => subst H end | ?T => fail 0 "no division in" H ":" T end. -Ltac conservative_common_denominator := +Ltac common_denominator := idtac; let fld := guess_field in let div := lazymatch type of fld with @@ -803,12 +803,12 @@ Ltac conservative_common_denominator := => set_nonfraction_pieces; field_simplify_eq_if_div; [ - | default_conservative_common_denominator_nonzero_tac.. ]; + | default_common_denominator_nonzero_tac.. ]; repeat match goal with H := _ |- _ => subst H end | |- ?G => fail 0 "no division in goal" G end. -Ltac conservative_common_denominator_inequality_in H := +Ltac common_denominator_inequality_in H := let HT := type of H in lazymatch HT with | not (?R _ _) => idtac @@ -823,8 +823,8 @@ Ltac conservative_common_denominator_inequality_in H := cut (not HT'); subst HT'; [ intro H; clear H' | let H'' := fresh in - intro H''; apply H'; conservative_common_denominator; [ eexact H'' | .. ] ]. -Ltac conservative_common_denominator_inequality := + intro H''; apply H'; common_denominator; [ eexact H'' | .. ] ]. +Ltac common_denominator_inequality := let G := get_goal in lazymatch G with | not (?R _ _) => idtac @@ -838,37 +838,37 @@ Ltac conservative_common_denominator_inequality := assert (H' : not HT'); subst HT'; [ | let HG := fresh in - intros HG; apply H'; conservative_common_denominator_in HG; [ eexact HG | .. ] ]. + intros HG; apply H'; common_denominator_in HG; [ eexact HG | .. ] ]. -Ltac conservative_common_denominator_hyps := +Ltac common_denominator_hyps := try match goal with | [H: _ |- _ ] - => progress conservative_common_denominator_in H; - [ conservative_common_denominator_hyps + => progress common_denominator_in H; + [ common_denominator_hyps | .. ] end. -Ltac conservative_common_denominator_inequality_hyps := +Ltac common_denominator_inequality_hyps := try match goal with | [H: _ |- _ ] - => progress conservative_common_denominator_inequality_in H; - [ conservative_common_denominator_inequality_hyps + => progress common_denominator_inequality_in H; + [ common_denominator_inequality_hyps | .. ] end. -Ltac conservative_common_denominator_all := - try conservative_common_denominator; - [ try conservative_common_denominator_hyps +Ltac common_denominator_all := + try common_denominator; + [ try common_denominator_hyps | .. ]. -Ltac conservative_common_denominator_inequality_all := - try conservative_common_denominator_inequality; - [ try conservative_common_denominator_inequality_hyps +Ltac common_denominator_inequality_all := + try common_denominator_inequality; + [ try common_denominator_inequality_hyps | .. ]. -Ltac conservative_common_denominator_equality_inequality_all := - conservative_common_denominator_all; - [ conservative_common_denominator_inequality_all +Ltac common_denominator_equality_inequality_all := + common_denominator_all; + [ common_denominator_inequality_all | .. ]. Inductive field_simplify_done {T} : T -> Type := @@ -1042,7 +1042,7 @@ Ltac super_nsatz_internal nsatz_alternative := prensatz_contradict; (* Each goal left over by [prensatz_contradict] is separate (and there might not be any), so we handle them all separately *) - [ try conservative_common_denominator_equality_inequality_all; + [ try common_denominator_equality_inequality_all; [ try nsatz_inequality_to_equality; try first [ nsatz; (* [nstaz] might leave over side-conditions; we handle them if they are inequalities *) diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 66dbf86da..a160d8dab 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -55,7 +55,7 @@ Module E. let Hx := fresh "H" in intro Hx; apply H; - try conservative_common_denominator; + try common_denominator; [rewrite <-Hx; ring | ..]. Ltac bash_step := @@ -82,7 +82,7 @@ Module E. => apply_field_nonzero (addCompleteMinus _ _ _ _ A (addOnCurve (_, _) (_, _) B C)) || apply_field_nonzero (addCompletePlus _ _ _ _ A (addOnCurve (_, _) (_, _) B C)) | |- ?x <> 0 => let H := fresh "H" in assert (x = 1) as H by ring; rewrite H; exact one_neq_zero - | |- Feq _ _ => progress conservative_common_denominator + | |- Feq _ _ => progress common_denominator | |- Feq _ _ => nsatz | |- _ => exact _ (* typeclass instances *) end. @@ -120,7 +120,7 @@ Module E. Lemma solve_correct : forall x y, onCurve (x, y) <-> (x^2 = solve_for_x2 y). Proof. unfold solve_for_x2; simpl; split; intros; - (conservative_common_denominator_all; [nsatz | auto using a_d_y2_nonzero]). + (common_denominator_all; [nsatz | auto using a_d_y2_nonzero]). Qed. End PointCompression. End CompleteEdwardsCurveTheorems. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index a83c85b02..c74e9a321 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -67,7 +67,7 @@ Section Pre. onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). Proof. unfold onCurve, unifiedAdd'; intros [x1 y1] [x2 y2] ? ?. - conservative_common_denominator; [ | auto using edwardsAddCompleteMinus, edwardsAddCompletePlus..]. + common_denominator; [ | auto using edwardsAddCompleteMinus, edwardsAddCompletePlus..]. nsatz. Qed. End Pre. |