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

1 files changed, 64 insertions, 15 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.