From 715389d71c2188b05a746cf41b1e48c0fd853a6d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 13 Dec 2017 10:21:11 -0500 Subject: clean up src/Curves/Montgomery/XZProofs.v --- src/Curves/Montgomery/XZProofs.v | 157 ++++++++++++--------------------------- 1 file changed, 46 insertions(+), 111 deletions(-) (limited to 'src/Curves') diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v index 71d30919c..404913df9 100644 --- a/src/Curves/Montgomery/XZProofs.v +++ b/src/Curves/Montgomery/XZProofs.v @@ -38,114 +38,59 @@ Module M. Local Notation boringladderstep := (M.boringladderstep(ap2d4:=ap2d4)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)). Local Notation to_xz := (M.to_xz(Fzero:=Fzero)(Fone:=Fone)(Feq:=Feq)(Fadd:=Fadd)(Fmul:=Fmul)(a:=a)(b:=b)). + (* TODO(#152): deduplicate between curves files *) + Ltac prept_step := + match goal with + | _ => progress intros + | _ => progress autounfold with points_as_coordinates in * + | _ => progress destruct_head' @unit + | _ => progress destruct_head' @bool + | _ => progress destruct_head' @prod + | _ => progress destruct_head' @sig + | _ => progress destruct_head' @sum + | _ => progress destruct_head' @and + | _ => progress destruct_head' @or + | H: context[dec ?P] |- _ => destruct (dec P) + | |- context[dec ?P] => destruct (dec P) + | |- ?P => lazymatch type of P with Prop => split end + end. + Ltac prept := repeat prept_step. + Ltac t := prept; trivial; try contradiction; fsatz. + + Create HintDb points_as_coordinates discriminated. + Hint Unfold Proper respectful Reflexive Symmetric Transitive : points_as_coordinates. + Hint Unfold Let_In : points_as_coordinates. + Hint Unfold fst snd proj1_sig : points_as_coordinates. + Hint Unfold fieldwise fieldwise' : points_as_coordinates. + Hint Unfold M.add M.opp M.point M.coordinates M.xzladderstep M.donnaladderstep M.boringladderstep M.to_xz : points_as_coordinates. + Lemma donnaladderstep_ok x1 Q Q' : - let eq := fieldwise (n:=2) (fieldwise (n:=2) Feq) in - eq (xzladderstep x1 Q Q') (donnaladderstep x1 Q Q'). - Proof. cbv; break_match; repeat split; fsatz. Qed. + fieldwise (n:=2) (fieldwise (n:=2) Feq) + (xzladderstep x1 Q Q') + (donnaladderstep x1 Q Q'). + Proof. t. Qed. Lemma boringladderstep_ok x1 Q Q' : - let eq := fieldwise (n:=2) (fieldwise (n:=2) Feq) in - eq (xzladderstep x1 Q Q') (boringladderstep x1 Q Q'). - Proof. cbv; break_match; repeat split; fsatz. Qed. + fieldwise (n:=2) (fieldwise (n:=2) Feq) + (xzladderstep x1 Q Q') + (boringladderstep x1 Q Q'). + Proof. t. Qed. Definition projective (P:F*F) := if dec (snd P = 0) then fst P <> 0 else True. Definition eq (P Q:F*F) := fst P * snd Q = fst Q * snd P. - Local Ltac do_unfold := - cbv [eq projective fst snd M.coordinates M.add M.zero M.eq M.opp proj1_sig xzladderstep M.to_xz Let_In Proper respectful] in *. - - Ltac t_step _ := - match goal with - | _ => solve [ contradiction | trivial ] - | _ => progress intros - | _ => progress subst - | _ => progress specialize_by_assumption - | [ H : ?x = ?x |- _ ] => clear H - | [ H : ?x <> ?x |- _ ] => specialize (H (reflexivity _)) - | [ H0 : ?T, H1 : ~?T -> _ |- _ ] => clear H1 - | _ => progress destruct_head'_prod - | _ => progress destruct_head'_and - | _ => progress Sum.inversion_sum - | _ => progress Prod.inversion_prod - | _ => progress cbv [fst snd proj1_sig projective eq] in * |- - | _ => progress cbn [to_xz M.coordinates proj1_sig] in * |- - | _ => progress destruct_head' @M.point - | _ => progress destruct_head'_sum - | [ H : context[dec ?T], H' : ~?T -> _ |- _ ] - => let H'' := fresh in - destruct (dec T) as [H''|H'']; [ clear H' | specialize (H' H'') ] - | _ => progress break_match_hyps - | _ => progress break_match - | |- _ /\ _ => split - | _ => progress do_unfold - end. - Ltac t := repeat t_step (). + Hint Unfold projective eq : points_as_coordinates. (* happens if u=0 in montladder, all denominators remain 0 *) Lemma add_0_numerator_r A B C D : snd (fst (xzladderstep 0 (pair C 0) (pair 0 A))) = 0 /\ snd (snd (xzladderstep 0 (pair D 0) (pair 0 B))) = 0. - Proof. t; fsatz. Qed. + Proof. t. Qed. Lemma add_0_denominators A B C D : snd (fst (xzladderstep 0 (pair A 0) (pair C 0))) = 0 /\ snd (snd (xzladderstep 0 (pair B 0) (pair D 0))) = 0. - Proof. t; fsatz. Qed. - - (** This tactic is to work around deficiencies in the Coq 8.6 - (released) version of [nsatz]; it has some heuristics for - clearing hypotheses and running [exfalso], and then tries to - solve the goal with [tac]. If [tac] fails on a goal, this - tactic does nothing. *) - Local Ltac exfalso_smart_clear_solve_by tac := - try lazymatch goal with - | [ fld : Hierarchy.field (T:=?F) (eq:=?Feq), Feq_dec : DecidableRel ?Feq |- _ ] - => lazymatch goal with - | [ H : ?x * 1 = ?y * ?z, H' : ?x <> 0, H'' : ?z = 0 |- _ ] - => clear -H H' H'' fld Feq_dec; exfalso; tac - | [ H : ?x * 0 = 1 * ?y, H' : ?y <> 0 |- _ ] - => clear -H H' fld Feq_dec; exfalso; tac - | _ - => match goal with - | [ H : ?b * ?lhs = ?rhs, H' : ?b * ?lhs' = ?rhs', Heq : ?x = ?y, Hb : ?b <> 0 |- _ ] - => exfalso; - repeat match goal with H : Ring.char_ge _ |- _ => revert H end; - let rhs := match (eval pattern x in rhs) with ?f _ => f end in - let rhs' := match (eval pattern y in rhs') with ?f _ => f end in - unify rhs rhs'; - match goal with - | [ H'' : ?x = ?Fopp ?x, H''' : ?x <> ?Fopp (?Fopp ?y) |- _ ] - => let lhs := match (eval pattern x in lhs) with ?f _ => f end in - let lhs' := match (eval pattern y in lhs') with ?f _ => f end in - unify lhs lhs'; - clear -H H' Heq H'' H''' Hb fld Feq_dec; intros - | [ H'' : ?x <> ?Fopp ?y, H''' : ?x <> ?Fopp (?Fopp ?y) |- _ ] - => let lhs := match (eval pattern x in lhs) with ?f _ => f end in - let lhs' := match (eval pattern y in lhs') with ?f _ => f end in - unify lhs lhs'; - clear -H H' Heq H'' H''' Hb fld Feq_dec; intros - end; - tac - | [ H : ?x * (?y * ?z) = 0 |- _ ] - => exfalso; - repeat match goal with - | [ H : ?x * 1 = ?y * ?z |- _ ] - => is_var x; is_var y; is_var z; - revert H - end; - generalize fld; - let lhs := match type of H with ?lhs = _ => lhs end in - repeat match goal with - | [ x : F |- _ ] => lazymatch type of H with - | context[x] => fail - | _ => clear dependent x - end - end; - intros _; intros; - tac - end - end - end. + Proof. t. Qed. Lemma to_xz_add (x1:F) (xz x'z':F*F) (Hxz:projective xz) (Hz'z':projective x'z') @@ -158,11 +103,7 @@ Module M. : eq (to_xz (Madd Q Q )) (fst (xzladderstep x1 xz xz)) /\ eq (to_xz (Madd Q Q')) (snd (xzladderstep x1 xz x'z')) /\ projective (snd (xzladderstep x1 xz x'z')). - Proof. - fsatz_prepare_hyps. - Time t. - Time par: abstract (exfalso_smart_clear_solve_by fsatz || fsatz). - Time Qed. + Proof. Time prept. Time par : abstract t. Time Qed. Context {a2m4_nonsquare:forall r, r*r <> a*a - (1+1+1+1)}. @@ -170,10 +111,10 @@ Module M. : projective (fst (xzladderstep x1 Q Q)). Proof. specialize (a2m4_nonsquare (fst Q/snd Q - fst Q/snd Q)). - destruct (dec (snd Q = 0)); t; specialize_by assumption; fsatz. + destruct (dec (snd Q = 0)); t. Qed. - Let a2m4_nz : a*a - (1+1+1+1) <> 0. + Local Definition a2m4_nz : a*a - (1+1+1+1) <> 0. Proof. specialize (a2m4_nonsquare 0). fsatz. Qed. Lemma difference_preserved Q Q' : @@ -219,7 +160,7 @@ Module M. split; [|split; [|split;[|split]]]; eauto. { pose proof projective_fst_xzladderstep x1 xz Hxz. - destruct_head prod. + destruct_head prod. cbv [projective fst xzladderstep] in *; eauto. } { pose proof difference_preserved Q Q' as HQQ; @@ -233,29 +174,23 @@ Module M. Definition to_x (xz:F*F) : F := if dec (snd xz = 0) then 0 else fst xz / snd xz. + Hint Unfold to_x : points_as_coordinates. Lemma to_x_to_xz Q : to_x (to_xz Q) = match M.coordinates Q with | ∞ => 0 | (x,y) => x end. - Proof. - cbv [to_x]; t; fsatz. - Qed. + Proof. t. Qed. Lemma proper_to_x_projective xz x'z' (Hxz:projective xz) (Hx'z':projective x'z') (H:eq xz x'z') : Feq (to_x xz) (to_x x'z'). - Proof. - destruct (dec (snd xz = 0)), (dec(snd x'z' = 0)); - cbv [to_x]; t; - specialize_by (assumption||reflexivity); - try fsatz. - Qed. + Proof. destruct (dec (snd xz = 0)), (dec(snd x'z' = 0)); t. Qed. Lemma to_x_zero x : to_x (pair x 0) = 0. - Proof. cbv; t; fsatz. Qed. + Proof. t. Qed. Lemma projective_to_xz Q : projective (to_xz Q). - Proof. t; fsatz. Qed. + Proof. t. Qed. End MontgomeryCurve. End M. -- cgit v1.2.3