From 65dad95295378962770304dbf4368975fe46c7dc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 24 Jun 2016 17:37:06 -0700 Subject: Various nsatz and field tactic improvements After | File Name | Before || Change ------------------------------------------------------------------------------------ 2m29.81s | Total | 2m34.05s || -0m04.23s ------------------------------------------------------------------------------------ 0m11.98s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m15.22s || -0m03.24s 0m29.71s | ModularArithmetic/ModularBaseSystemProofs | 0m30.05s || -0m00.33s 0m29.12s | Specific/GF25519 | 0m29.12s || +0m00.00s 0m21.50s | Experiments/SpecEd25519 | 0m21.43s || +0m00.07s 0m18.20s | CompleteEdwardsCurve/ExtendedCoordinates | 0m18.24s || -0m00.03s 0m07.36s | Specific/GF1305 | 0m07.33s || +0m00.03s 0m06.66s | Experiments/GenericFieldPow | 0m06.89s || -0m00.22s 0m03.84s | ModularArithmetic/ModularBaseSystemOpt | 0m03.84s || +0m00.00s 0m03.82s | ModularArithmetic/Tutorial | 0m03.88s || -0m00.06s 0m03.74s | CompleteEdwardsCurve/Pre | 0m03.81s || -0m00.06s 0m02.30s | ModularArithmetic/ModularArithmeticTheorems | 0m02.27s || +0m00.02s 0m02.11s | ModularArithmetic/PrimeFieldTheorems | 0m02.05s || +0m00.06s 0m01.93s | Algebra | 0m02.06s || -0m00.13s 0m01.17s | Experiments/DerivationsOptionRectLetInEncoding | 0m01.19s || -0m00.02s 0m01.13s | ModularArithmetic/ExtendedBaseVector | 0m01.18s || -0m00.05s 0m01.01s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m01.07s || -0m00.06s 0m00.61s | Encoding/ModularWordEncodingTheorems | 0m00.64s || -0m00.03s 0m00.61s | Spec/EdDSA | 0m00.62s || -0m00.01s 0m00.57s | Encoding/ModularWordEncodingPre | 0m00.62s || -0m00.05s 0m00.56s | Spec/ModularWordEncoding | 0m00.59s || -0m00.02s 0m00.55s | ModularArithmetic/ModularBaseSystem | 0m00.59s || -0m00.03s 0m00.52s | ModularArithmetic/PseudoMersenneBaseRep | 0m00.52s || +0m00.00s 0m00.41s | Tactics/Nsatz | 0m00.41s || +0m00.00s 0m00.38s | Spec/CompleteEdwardsCurve | 0m00.40s || -0m00.02s 0m00.03s | Util/Tactics | 0m00.03s || +0m00.00s --- src/Algebra.v | 79 +++++++++++++++++++++++++++++++++++++++++++---------- src/Tactics/Nsatz.v | 3 +- src/Util/Tactics.v | 7 +++++ 3 files changed, 73 insertions(+), 16 deletions(-) diff --git a/src/Algebra.v b/src/Algebra.v index 99fb2deb8..7f4fe06cc 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -580,6 +580,10 @@ Ltac field_nonzero_mul_split := repeat match goal with | [ H : ?R (?mul ?x ?y) ?zero |- _ ] => apply IntegralDomain.mul_nonzero_nonzero_cases in H; destruct H + | [ |- not (?R (?mul ?x ?y) ?zero) ] + => apply IntegralDomain.mul_nonzero_nonzero_iff; split + | [ H : not (?R (?mul ?x ?y) ?zero) |- _ ] + => apply IntegralDomain.mul_nonzero_nonzero_iff in H; destruct H end. Ltac common_denominator := @@ -607,6 +611,28 @@ Ltac common_denominator_all := repeat match goal with [H: _ |- _ _ _ ] => progress common_denominator_in H end. (** Now we have more conservative versions that don't simplify non-division structure. *) +Ltac deduplicate_nonfraction_pieces mul := + repeat match goal with + | [ x0 := ?v, x1 := context[?v] |- _ ] + => progress change v with x0 in x1 + | [ x := mul ?a ?b |- _ ] + => not is_var a; + let a' := fresh x in + pose a as a'; change a with a' in x + | [ x := mul ?a ?b |- _ ] + => not is_var b; + let b' := fresh x in + pose b as b'; change b with b' in x + | [ x0 := ?v, x1 := ?v |- _ ] + => change x1 with x0 in *; clear x1 + | [ x := ?v |- _ ] + => is_var v; subst x + | [ x0 := mul ?a ?b, x1 := mul ?a ?b' |- _ ] + => subst x0 x1 + | [ x0 := mul ?a ?b, x1 := mul ?a' ?b |- _ ] + => subst x0 x1 + end. + Ltac set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac cont := idtac; let one_arg_recr := @@ -656,7 +682,8 @@ Ltac set_nonfraction_pieces_in_by H nonzero_tac := => let T := type of H in set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac - ltac:(fun T' => change T' in H) + ltac:(fun T' => change T' in H); + deduplicate_nonfraction_pieces mul end. Ltac set_nonfraction_pieces_by nonzero_tac := idtac; @@ -666,31 +693,53 @@ Ltac set_nonfraction_pieces_by nonzero_tac := => let T := get_goal in set_nonfraction_pieces_on T eq zero opp add sub mul inv div nonzero_tac - ltac:(fun T' => change T') + ltac:(fun T' => change T'); + deduplicate_nonfraction_pieces mul end. Ltac set_nonfraction_pieces_in H := set_nonfraction_pieces_in_by H ltac:(try (intro; field_nonzero_mul_split; try tauto)). Ltac set_nonfraction_pieces := set_nonfraction_pieces_by ltac:(try (intro; field_nonzero_mul_split; tauto)). Ltac conservative_common_denominator_in H := - set_nonfraction_pieces_in H; - [ .. - | common_denominator_in H; - [ repeat split; try assumption.. - | ] ]; - repeat match goal with H := _ |- _ => subst H end. + idtac; + let fld := guess_field in + let div := lazymatch type of fld with + | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div + => div + end in + lazymatch type of H with + | appcontext[div] + => set_nonfraction_pieces_in H; + [ .. + | common_denominator_in H; + [ repeat split; try assumption.. + | ] ]; + repeat match goal with H := _ |- _ => subst H end + | ?T => fail 0 "no division in" H ":" T + end. Ltac conservative_common_denominator := - set_nonfraction_pieces; - [ .. - | common_denominator; - [ repeat split; try assumption.. - | ] ]; - repeat match goal with H := _ |- _ => subst H end. + idtac; + let fld := guess_field in + let div := lazymatch type of fld with + | @field ?T ?eq ?zero ?one ?opp ?add ?sub ?mul ?inv ?div + => div + end in + lazymatch goal with + | |- appcontext[div] + => set_nonfraction_pieces; + [ .. + | common_denominator; + [ repeat split; try assumption.. + | ] ]; + repeat match goal with H := _ |- _ => subst H end + | |- ?G + => fail 0 "no division in goal" G + end. Ltac conservative_common_denominator_all := try conservative_common_denominator; [ .. - | repeat match goal with [H: _ |- _ _ _ ] => progress conservative_common_denominator_in H; [] end ]. + | repeat match goal with [H: _ |- _ ] => progress conservative_common_denominator_in H; [] end ]. Inductive field_simplify_done {T} : T -> Type := Field_simplify_done : forall H, field_simplify_done H. diff --git a/src/Tactics/Nsatz.v b/src/Tactics/Nsatz.v index 84d472e54..04f35c200 100644 --- a/src/Tactics/Nsatz.v +++ b/src/Tactics/Nsatz.v @@ -85,7 +85,8 @@ Ltac nsatz_clear_duplicates_for_bug_4851 domain := Ltac nsatz_nonzero := try solve [apply Integral_domain.integral_domain_one_zero |apply Integral_domain.integral_domain_minus_one_zero - |trivial]. + |trivial + |assumption]. Ltac nsatz_domain_sugar_power domain sugar power := let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *) diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index e8876fee2..2324e1b34 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -111,3 +111,10 @@ Ltac destruct_trivial_step := | [ H : True |- _ ] => clear H || destruct H end. Ltac destruct_trivial := repeat destruct_trivial_step. + +Ltac clear_duplicates_step := + match goal with + | [ H : ?T, H' : ?T |- _ ] => clear H' + | [ H := ?T, H' := ?T |- _ ] => clear H' + end. +Ltac clear_duplicates := repeat clear_duplicates_step. -- cgit v1.2.3