Add tactics to simplify repeated conditions

After    | File Name                                         | Before   || Change
------------------------------------------------------------------------------------
2m39.26s | Total                                             | 2m42.89s || -0m03.62s
------------------------------------------------------------------------------------
0m34.94s | CompleteEdwardsCurve/ExtendedCoordinates          | 0m38.79s || -0m03.85s
0m13.94s | Experiments/SpecEd25519                           | 0m15.81s || -0m01.87s
0m16.65s | ModularArithmetic/ModularBaseSystemProofs         | 0m16.38s || +0m00.26s
0m15.26s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m15.33s || -0m00.07s
0m14.57s | Specific/GF25519                                  | 0m14.49s || +0m00.08s
0m05.97s | Algebra                                           | 0m06.01s || -0m00.04s
0m05.93s | Experiments/GenericFieldPow                       | 0m05.73s || +0m00.19s
0m04.65s | WeierstrassCurve/Pre                              | 0m04.58s || +0m00.07s
0m04.17s | ModularArithmetic/Pow2BaseProofs                  | 0m04.26s || -0m00.08s
0m03.68s | ModularArithmetic/Montgomery/ZProofs              | 0m03.59s || +0m00.09s
0m03.62s | ModularArithmetic/Tutorial                        | 0m03.51s || +0m00.11s
0m03.59s | Experiments/SpecificCurve25519                    | 0m03.29s || +0m00.29s
0m03.42s | CompleteEdwardsCurve/Pre                          | 0m03.42s || +0m00.00s
0m02.57s | ModularArithmetic/BarrettReduction/ZHandbook      | 0m02.51s || +0m00.06s
0m02.16s | Experiments/EdDSARefinement                       | 0m01.80s || +0m00.36s
0m02.12s | ModularArithmetic/ModularBaseSystemOpt            | 0m02.05s || +0m00.07s
0m02.08s | Specific/GF1305                                   | 0m02.15s || -0m00.06s
0m02.08s | ModularArithmetic/BarrettReduction/ZGeneralized   | 0m02.06s || +0m00.02s
0m01.94s | ModularArithmetic/ModularArithmeticTheorems       | 0m01.91s || +0m00.03s
0m01.48s | Encoding/PointEncodingPre                         | 0m01.51s || -0m00.03s
0m01.44s | ModularArithmetic/BarrettReduction/Z              | 0m01.20s || +0m00.24s
0m01.21s | Experiments/DerivationsOptionRectLetInEncoding    | 0m00.86s || +0m00.35s
0m01.11s | ModularArithmetic/ExtendedBaseVector              | 0m01.10s || +0m00.01s
0m01.02s | ModularArithmetic/PrimeFieldTheorems              | 0m01.04s || -0m00.02s
0m00.91s | ModularArithmetic/ModularBaseSystemField          | 0m00.91s || +0m00.00s
0m00.85s | ModularArithmetic/ModularBaseSystemListProofs     | 0m00.80s || +0m00.04s
0m00.69s | Util/IterAssocOp                                  | 0m00.68s || +0m00.00s
0m00.69s | Encoding/ModularWordEncodingTheorems              | 0m00.66s || +0m00.02s
0m00.65s | ModularArithmetic/ExtPow2BaseMulProofs            | 0m00.65s || +0m00.00s
0m00.64s | ModularArithmetic/ModularBaseSystemList           | 0m00.67s || -0m00.03s
0m00.64s | Spec/ModularWordEncoding                          | 0m00.55s || +0m00.08s
0m00.64s | Testbit                                           | 0m00.61s || +0m00.03s
0m00.63s | Util/AdditionChainExponentiation                  | 0m00.68s || -0m00.05s
0m00.61s | ModularArithmetic/ModularBaseSystem               | 0m00.61s || +0m00.00s
0m00.61s | ModularArithmetic/PseudoMersenneBaseParamProofs   | 0m00.59s || +0m00.02s
0m00.60s | Encoding/ModularWordEncodingPre                   | 0m00.62s || -0m00.02s
0m00.59s | Spec/EdDSA                                        | 0m00.60s || -0m00.01s
0m00.45s | Spec/WeierstrassCurve                             | 0m00.44s || +0m00.01s
0m00.43s | Spec/CompleteEdwardsCurve                         | 0m00.39s || +0m00.03s
0m00.04s | Util/Tactics                                      | 0m00.05s || -0m00.01s

1 files changed, 17 insertions, 0 deletions

diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 8ddfecb5f..cca98c471 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -342,3 +342,20 @@ Ltac revert_last_nondep :=
   end.
 
 Ltac reverse_nondep := repeat revert_last_nondep.
+
+Ltac simplify_repeated_ifs_step :=
+  match goal with
+  | [ |- context G[if ?b then ?x else ?y] ]
+    => let x' := match x with
+                 | context x'[b] => let x'' := context x'[true] in x''
+                 end in
+       let G' := context G[if b then x' else y] in
+       cut G'; [ destruct b; exact (fun z => z) | cbv iota ]
+  | [ |- context G[if ?b then ?x else ?y] ]
+    => let y' := match y with
+                 | context y'[b] => let y'' := context y'[false] in y''
+                 end in
+       let G' := context G[if b then x else y'] in
+       cut G'; [ destruct b; exact (fun z => z) | cbv iota ]
+  end.
+Ltac simplify_repeated_ifs := repeat simplify_repeated_ifs_step.