From 411cff37fd1b17aa032ea2364e9b2142d9b0ecbb Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Wed, 9 Dec 2015 21:28:30 -0500 Subject: Remove redundancy in lemma statement --- src/Specific/GF25519.v | 118 ++++++++++++++++++++++++++++++------------------- 1 file changed, 73 insertions(+), 45 deletions(-) (limited to 'src') diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 7d44addc4..d30d1f7fe 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -134,46 +134,16 @@ Section GF25519Base25Point5Formula. Import GF. Lemma GF25519Base25Point5_mul_reduce_formula : - forall f g - f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 - g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 - (Hf: rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] f) - (Hg: rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g), - let h0 := (f0*g0 + 38*f9*g1 + 19*f8*g2 + 38*f7*g3 + 19*f6*g4 + 38*f5*g5 + 19*f4*g6 + 38*f3*g7 + 19*f2*g8 + 38*f1*g9) in - let h1 := (f1*g0 + f0*g1 + 19*f9*g2 + 19*f8*g3 + 19*f7*g4 + 19*f6*g5 + 19*f5*g6 + 19*f4*g7 + 19*f3*g8 + 19*f2*g9) in - let h2 := (f2*g0 + 2*f1*g1 + f0*g2 + 38*f9*g3 + 19*f8*g4 + 38*f7*g5 + 19*f6*g6 + 38*f5*g7 + 19*f4*g8 + 38*f3*g9) in - let h3 := (f3*g0 + f2*g1 + f1*g2 + f0*g3 + 19*f9*g4 + 19*f8*g5 + 19*f7*g6 + 19*f6*g7 + 19*f5*g8 + 19*f4*g9) in - let h4 := (f4*g0 + 2*f3*g1 + f2*g2 + 2*f1*g3 + f0*g4 + 38*f9*g5 + 19*f8*g6 + 38*f7*g7 + 19*f6*g8 + 38*f5*g9) in - let h5 := (f5*g0 + f4*g1 + f3*g2 + f2*g3 + f1*g4 + f0*g5 + 19*f9*g6 + 19*f8*g7 + 19*f7*g8 + 19*f6*g9) in - let h6 := (f6*g0 + 2*f5*g1 + f4*g2 + 2*f3*g3 + f2*g4 + 2*f1*g5 + f0*g6 + 38*f9*g7 + 19*f8*g8 + 38*f7*g9) in - let h7 := (f7*g0 + f6*g1 + f5*g2 + f4*g3 + f3*g4 + f2*g5 + f1*g6 + f0*g7 + 19*f9*g8 + 19*f8*g9) in - let h8 := (f8*g0 + 2*f7*g1 + f6*g2 + 2*f5*g3 + f4*g4 + 2*f3*g5 + f2*g6 + 2*f1*g7 + f0*g8 + 38*f9*g9) in - let h9 := (f9*g0 + f8*g1 + f7*g2 + f6*g3 + f5*g4 + f4*g5 + f3*g6 + f2*g7 + f1*g8 + f0*g9) in - let h0c := Z.land h0 67108863 in - let h1c := (Z.shiftr h0 26 + h1)%Z in - let h2c := (Z.shiftr h1c 25 + h2)%Z in - let h3c := (Z.shiftr h2c 26 + h3)%Z in - let h4c := (Z.shiftr h3c 25 + h4)%Z in - let h5c := (Z.shiftr h4c 26 + h5)%Z in - let h6c := (Z.shiftr h5c 25 + h6)%Z in - let h7c := (Z.shiftr h6c 26 + h7)%Z in - let h8c := (Z.shiftr h7c 25 + h8)%Z in - let h9c := (Z.shiftr h8c 26 + h9)%Z in - let r0' := (19 * Z.shiftr h9c 25 + h0c)%Z in - let r0 := Z.land r0' 67108863 in - let r1' := Z.land h1c 33554431 in - let r1 := (Z.shiftr r0' 26 + r1')%Z in - let r2 := Z.land h2c 67108863 in - let r3 := Z.land h3c 33554431 in - let r4 := Z.land h4c 67108863 in - let r5 := Z.land h5c 33554431 in - let r6 := Z.land h6c 67108863 in - let r8 := Z.land h8c 67108863 in - let r7 := Z.land h7c 33554431 in - let r9 := Z.land h9c 33554431 in - rep [r0;r1;r2;r3;r4;r5;r6;r7;r8;r9] (f*g)%GF. + forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 + g0 g1 g2 g3 g4 g5 g6 g7 g8 g9, + {ls | forall f g, rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] f + -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g + -> rep ls (f*g)%GF}. Proof. intros. + eexists. + intros f g Hf Hg. + pose proof (mul_rep _ _ _ _ Hf Hg) as HmulRef. remember (GF25519Base25Point5.mul [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9]) as h. unfold @@ -306,12 +276,70 @@ Section GF25519Base25Point5Formula. remember (Z.ones 26) as m26 in *. compute in Heqm26. subst m26. unfold GF25519Base25Point5Params.c in *. - replace ([r0; r1; r2; r3; r4; r5; r6; r7; r8; r9]) with r; unfold rep; auto; subst r. + (* This tactic takes in [r], a variable that we want to use to instantiate an existential. + * We find one other variable mentioned in [r], with its own equality in the hypotheses. + * That equality is then switched into a [let] in [r]'s defining equation. *) + Ltac letify r := + match goal with + | [ H : ?x = ?e |- _ ] => + is_var x; + match goal with + | [ H' : r = _ |- _ ] => + pattern x in H'; + match type of H' with + | (fun z => r = @?e' z) x => + let H'' := fresh "H" in assert (H'' : r = let x := e in e' x) by congruence; + clear H'; subst x; rename H'' into H'; cbv beta in H' + end + end + end. - Ltac rsubstBoth := repeat (match goal with [ |- ?a = ?b] => subst a; subst b; repeat progress f_equal || reflexivity end). - Ltac t := f_equal; [abstract rsubstBoth|try t]. - t. - f_equal. - rsubstBoth. - Qed. + (* To instantiate an existential, give a variable with a defining equation to this tactic. + * We instantiate with a [let]-ified version of that equation. *) + Ltac existsFromEquations r := repeat letify r; + match goal with + | [ _ : r = ?e |- context[?u] ] => unify u e + end. + + clear HmulRef Hh Hf Hg. + existsFromEquations r. + split; auto; congruence. + + (* Here's the tactic code I added at this point at the end of the old version. + * Erase after reading, since it isn't needed anymore. + + replace ([r0; r1; r2; r3; r4; r5; r6; r7; r8; r9]) with r; unfold rep; auto. + + subst r. + + Ltac rsubstBoth := repeat (match goal with [ |- ?a = ?b] => subst a; subst b; repeat progress f_equal || reflexivity end). + Ltac t := f_equal; abstract rsubstBoth || (try t). + + Time t. + + + (* But there's a nicer way! *) + Undo 2. + + (* This tactic finds an [x := e] hypothesis and adds a matching [x = e] hypothesis. *) + Ltac letToEquality := + match goal with + | [ x := ?e |- _ ] => + match goal with + | [ _ : x = e |- _ ] => fail 1 (* To avoid infinite loop, make sure we didn't already do this one! *) + | _ => assert (x = e) by reflexivity + end + end. + + (* Repeated introduction of those equalities enables [congruence] to solve the goal. *) + Ltac smarter_congruence := repeat letToEquality; congruence. + + Time smarter_congruence.*) + Defined. End GF25519Base25Point5Formula. + +Extraction "/tmp/test.ml" GF25519Base25Point5_mul_reduce_formula. +(* It's easy enough to use extraction to get the proper nice-looking formula. + * More Ltac acrobatics will be needed to get out that formula for further use in Coq. + * The easiest fix will be to make the proof script above fully automated, + * using [abstract] to contain the proof part. *) -- cgit v1.2.3