Cleanup: mostly moving lemmas to Util files, some moving lemmas to more general contexts.

13 files changed, 136 insertions, 166 deletions

diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v
index 84374fe8f..ab56cb711 100644
--- a/src/BaseSystemProofs.v
+++ b/src/BaseSystemProofs.v
@@ -17,6 +17,18 @@ Section BaseSystemProofs.
     unfold decode'; intros; f_equal; apply combine_truncate_l.
   Qed.
 
+  Lemma decode'_splice : forall xs ys bs,
+    decode' bs (xs ++ ys) = 
+    decode' (firstn (length xs) bs) xs + decode'  (skipn (length xs) bs) ys.
+  Proof.
+    unfold decode'.
+    induction xs; destruct ys, bs; boring.
+    + rewrite combine_truncate_r.
+      do 2 rewrite Z.add_0_r; auto.
+    + unfold accumulate.
+      apply Z.add_assoc.
+  Qed.
+
   Lemma add_rep : forall bs us vs, decode' bs (add us vs) = decode' bs us + decode' bs vs.
   Proof.
     unfold decode', accumulate; induction bs; destruct us, vs; boring; ring.
@@ -487,4 +499,5 @@ Section BaseSystemProofs.
     rewrite rev_length; omega.
   Qed.
 
+
 End BaseSystemProofs.
diff --git a/src/Encoding/ModularWordEncodingPre.v b/src/Encoding/ModularWordEncodingPre.v
index cb2f5a045..417344b43 100644
--- a/src/Encoding/ModularWordEncodingPre.v
+++ b/src/Encoding/ModularWordEncodingPre.v
@@ -3,8 +3,7 @@ Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Bedrock.Word.
 Require Import Crypto.Tactics.VerdiTactics.
-Require Import Crypto.Util.NatUtil.
-Require Import Crypto.Util.WordUtil.
+Require Import Crypto.Util.ZUtil Crypto.Util.WordUtil.
 Require Import Crypto.Spec.Encoding.
 
 Local Open Scope nat_scope.
@@ -21,45 +20,12 @@ Section ModularWordEncodingPre.
       else None
   .
 
-  (* TODO : move to ZUtil *)
-  Lemma bound_check_N : forall x : F m, (Z.to_N x < Npow2 sz)%N.
-  Proof.
-    intro.
-    pose proof (FieldToZ_range x m_pos) as x_range.
-    rewrite <- Nnat.N2Nat.id.
-    rewrite Npow2_nat.
-    replace (Z.to_N x) with (N.of_nat (Z.to_nat x)) by apply Z_nat_N.
-    apply (Nat2N_inj_lt _ (pow2 sz)).
-    rewrite Zpow_pow2.
-    destruct x_range as [x_low x_high].
-    apply Z2Nat.inj_lt in x_high; try omega.
-    rewrite <- ZUtil.pow_Z2N_Zpow by omega.
-    replace (Z.to_nat 2) with 2%nat by auto.
-    omega.
-  Qed.
-
-  (* TODO: move to WordUtil *)
-  Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N ->
-    wordToN (NToWord sz n) = n.
-  Proof.
-    intros.
-    rewrite wordToN_nat, NToWord_nat.
-    rewrite wordToNat_natToWord_idempotent; rewrite Nnat.N2Nat.id; auto.
-  Qed.
-
-  (* TODO: move to WordUtil *)
-  Lemma NToWord_wordToN : forall sz w, NToWord sz (wordToN w) = w.
-  Proof.
-    intros.
-    rewrite wordToN_nat, NToWord_nat, Nnat.Nat2N.id.
-    apply natToWord_wordToNat.
-  Qed.
-
   Lemma Fm_encoding_valid : forall x, Fm_dec (Fm_enc x) = Some x.
   Proof.
     unfold Fm_dec, Fm_enc; intros.
     pose proof (FieldToZ_range x m_pos).
-    rewrite wordToN_NToWord_idempotent by apply bound_check_N.
+    rewrite wordToN_NToWord_idempotent by (apply bound_check_nat_N;
+     assert (Z.to_nat x < Z.to_nat m) by (apply Z2Nat.inj_lt; omega); omega).
     rewrite Z2N.id by omega.
     rewrite ZToField_idempotent.
     break_if; auto; omega.
diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v
index 83f199d90..a74ccb522 100644
--- a/src/Encoding/ModularWordEncodingTheorems.v
+++ b/src/Encoding/ModularWordEncodingTheorems.v
@@ -1,10 +1,11 @@
 Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
 Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems.
 Require Import Bedrock.Word.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.Spec.Encoding.
+Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Spec.ModularWordEncoding.
 
 
@@ -47,29 +48,6 @@ Section SignBit.
     rewrite sign_bit_parity; auto.
   Qed.
 
-  (* TODO : move to ZUtil *)
-  Lemma Z_odd_mod : forall a b, (b <> 0)%Z ->
-    Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a.
-  Proof.
-    intros.
-    rewrite Zmod_eq_full by assumption.
-    rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul.
-    break_if; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r.
-  Qed.
-
-  (* TODO : move to ModularArithmeticTheorems *)
-  Lemma F_FieldToZ_add_opp : forall x : F m, x <> 0 -> (FieldToZ x + FieldToZ (opp x) = m)%Z.
-  Proof.
-    intros.
-    rewrite FieldToZ_opp.
-    rewrite Z_mod_nz_opp_full, mod_FieldToZ; try omega.
-    rewrite mod_FieldToZ.
-    replace 0%Z with (@FieldToZ m 0) by auto.
-    intro false_eq.
-    rewrite <-F_eq in false_eq.
-    congruence.
-  Qed.
-
   Lemma sign_bit_opp : forall (x : F m), x <> 0 -> negb (sign_bit x) = sign_bit (opp x).
   Proof.
     intros.
diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v
index 9b65d9819..e023da0ea 100644
--- a/src/Encoding/PointEncodingPre.v
+++ b/src/Encoding/PointEncodingPre.v
@@ -118,28 +118,6 @@ Section PointEncoding.
     | None => None
     end.
 
-  (* TODO : move *)
-  Lemma sqrt_mod_q_0 : forall x : F q, sqrt_mod_q x = 0 -> x = 0.
-  Proof.
-    unfold sqrt_mod_q; intros.
-    break_if.
-    - match goal with [ H : ?sqrt_x ^ 2 = x, H' : ?sqrt_x = 0 |- _ ] => rewrite <-H, H' end.
-      ring.
-    - match goal with
-      | [H : sqrt_minus1 * _ = 0 |- _ ]=>
-         apply Fq_mul_zero_why in H; destruct H as [sqrt_minus1_zero | ? ];
-         [ | eapply Fq_root_zero; eauto ]
-      end.
-      unfold sqrt_minus1 in sqrt_minus1_zero.
-      rewrite sqrt_minus1_zero in sqrt_minus1_valid.
-      exfalso.
-      pose proof (@F_opp_spec q 1) as opp_spec_1.
-      rewrite <-sqrt_minus1_valid in opp_spec_1.
-      assert (((1 + 0 ^ 2) : F q) = (1 : F q)) as ring_subst by ring.
-      rewrite ring_subst in *.
-      apply Fq_1_neq_0; assumption.
-  Qed.
-
   Lemma point_coordinates_encoding_canonical : forall w p,
     point_dec_coordinates sign_bit w = Some p -> point_enc_coordinates p = w.
   Proof.
@@ -151,7 +129,7 @@ Section PointEncoding.
       do 2 (break_if; try congruence); inversion coord_dec_Some; subst.
     + destruct (F_eq_dec (sqrt_mod_q (E.solve_for_x2 f1)) 0%F) as [sqrt_0 | ?].
       - rewrite sqrt_0 in *.
-        apply sqrt_mod_q_0 in sqrt_0.
+        apply sqrt_mod_q_root_0 in sqrt_0; try assumption.
         rewrite sqrt_0 in *.
         break_if; [symmetry; auto using Bool.eqb_prop | ].
         rewrite sign_bit_zero in *.
@@ -195,19 +173,6 @@ Proof.
   exact (encoding_valid y).
 Qed.
 
-(*
-Lemma wordToN_enc_neq_opp : forall x, x <> 0 -> (wordToN (enc (opp x)) <> wordToN (enc x))%N.
-Proof.
-  intros x x_nonzero.
-  intro false_eq.
-  apply x_nonzero.
-  apply F_eq_opp_zero; try apply two_lt_q.
-  apply wordToN_inj in false_eq.
-  apply encoding_inj in false_eq.
-  auto.
-Qed.
-*)
-
 Lemma sign_bit_opp_eq_iff : forall x y, y <> 0 ->
   (sign_bit x <> sign_bit y <-> sign_bit x = sign_bit (opp y)).
 Proof.
@@ -242,25 +207,6 @@ Proof.
     reflexivity.
 Qed.
 
-(* TODO : move *)
-Lemma sqrt_mod_q_of_0 : @sqrt_mod_q q 0 = 0.
-Proof.
-  unfold sqrt_mod_q.
-  rewrite !Fq_pow_zero.
-  break_if; ring.
-
-  congruence.
-  intro false_eq.
-  SearchAbout Z.to_N.
-  rewrite <-(N2Z.id 0) in false_eq.
-  rewrite N2Z.inj_0 in false_eq.
-  pose proof (prime_ge_2 q prime_q).
-  apply Z2N.inj in false_eq; zero_bounds.
-  assert (0 < q / 8 + 1)%Z.
-  apply Z.add_nonneg_pos; zero_bounds.
-  omega.
-Qed.
-
 Lemma point_encoding_coordinates_valid : forall p, E.onCurve p ->
    point_dec_coordinates sign_bit (point_enc_coordinates p) = Some p.
 Proof.
@@ -277,7 +223,7 @@ Proof.
     rewrite !Fq_pow_zero, sqrt_mod_q_of_0, Fq_pow_zero by congruence.
     rewrite if_F_eq_dec_if_F_eqb, sign_bit_zero. 
     reflexivity.
-  + assert (sqrt_mod_q (x ^ 2) <> 0) by (intro false_eq; apply sqrt_mod_q_0 in false_eq;
+  + assert (sqrt_mod_q (x ^ 2) <> 0) by (intro false_eq; apply sqrt_mod_q_root_0 in false_eq; try assumption;
       apply Fq_root_zero in false_eq; rewrite false_eq, F_eqb_refl in eqb_x_0; congruence).
     replace (F_eqb (sqrt_mod_q (x ^ 2)) 0) with false by (symmetry;
         apply F_eqb_neq_complete; assumption).
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 954fac15d..8b1ae9f93 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -697,4 +697,17 @@ Section VariousModulo.
     replace y with ((y - b) + b) by ring.
     rewrite Hxayb; ring.
   Qed.
+
+  Lemma F_FieldToZ_add_opp : forall x : F m, x <> 0 -> (FieldToZ x + FieldToZ (opp x) = m)%Z.
+  Proof.
+    intros.
+    rewrite FieldToZ_opp.
+    rewrite Z_mod_nz_opp_full, mod_FieldToZ; try omega.
+    rewrite mod_FieldToZ.
+    replace 0%Z with (@FieldToZ m 0) by auto.
+    intro false_eq.
+    rewrite <-F_eq in false_eq.
+    congruence.
+  Qed.
+
 End VariousModulo.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index f39f32ea5..2989bfa12 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -178,20 +178,6 @@ Section PseudoMersenneProofs.
     }
   Qed.
 
-  (* TODO: move to BaseSystemProofs *)
-  Lemma decode'_splice : forall xs ys bs,
-    BaseSystem.decode' bs (xs ++ ys) = 
-    BaseSystem.decode' (firstn (length xs) bs) xs + 
-    BaseSystem.decode'  (skipn (length xs) bs) ys.
-  Proof.
-    unfold BaseSystem.decode'.
-    induction xs; destruct ys, bs; boring.
-    + rewrite combine_truncate_r.
-      do 2 rewrite Z.add_0_r; auto.
-    + unfold BaseSystem.accumulate.
-      apply Z.add_assoc.
-  Qed.
-
   Lemma set_nth_sum : forall n x us, (n < length us)%nat ->
     BaseSystem.decode base (set_nth n x us) = 
     (x - nth_default 0 us n) * nth_default 0 base n + BaseSystem.decode base us.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 759085dc6..8a69a0c54 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -472,6 +472,44 @@ Section SquareRootsPrime5Mod8.
     field.
   Qed.
 
+  Lemma sqrt_mod_q_of_0 : sqrt_mod_q 0 = 0.
+  Proof.
+    unfold sqrt_mod_q.
+    rewrite !Fq_pow_zero.
+    break_if; ring.
+
+    congruence.
+    intro false_eq.
+    rewrite <-(N2Z.id 0) in false_eq.
+    rewrite N2Z.inj_0 in false_eq.
+    pose proof (prime_ge_2 q prime_q).
+    apply Z2N.inj in false_eq; zero_bounds.
+    assert (0 < q / 8 + 1)%Z.
+    apply Z.add_nonneg_pos; zero_bounds.
+    omega.
+  Qed.
+
+  Lemma sqrt_mod_q_root_0 : forall x : F q, sqrt_mod_q x = 0 -> x = 0.
+  Proof.
+    unfold sqrt_mod_q; intros.
+    break_if.
+    - match goal with [ H : ?sqrt_x ^ 2 = x, H' : ?sqrt_x = 0 |- _ ] => rewrite <-H, H' end.
+      ring.
+    - match goal with
+      | [H : sqrt_minus1 * _ = 0 |- _ ]=>
+         apply Fq_mul_zero_why in H; destruct H as [sqrt_minus1_zero | ? ];
+         [ | eapply Fq_root_zero; eauto ]
+      end.
+      unfold sqrt_minus1 in sqrt_minus1_zero.
+      rewrite sqrt_minus1_zero in sqrt_minus1_valid.
+      exfalso.
+      pose proof (@F_opp_spec q 1) as opp_spec_1.
+      rewrite <-sqrt_minus1_valid in opp_spec_1.
+      assert (((1 + 0 ^ 2) : F q) = (1 : F q)) as ring_subst by ring.
+      rewrite ring_subst in *.
+      apply Fq_1_neq_0; assumption.
+  Qed.
+
 End SquareRootsPrime5Mod8.
 
 Local Open Scope F_scope.
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index 0a58c81d2..1a7b3316e 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -89,26 +89,6 @@ Section PseudoMersenneBaseParamProofs.
       - rewrite IHl by auto; ring.
   Qed.
 
-  (* TODO : move to LsitUtil *)
-  Lemma fold_right_invariant : forall {A} P (f: A -> A -> A) l x,
-    P x -> (forall y, In y l -> forall z, P z -> P (f y z)) ->
-    P (fold_right f x l).
-  Proof.
-    induction l; intros ? ? step; auto.
-    simpl.
-    apply step; try apply in_eq.
-    apply IHl; auto.
-    intros y in_y_l.
-    apply (in_cons a) in in_y_l.
-    auto.
-  Qed.
-
-  (* TODO : move to ListUtil *)
-  Lemma In_firstn : forall {T} n l (x : T), In x (firstn n l) -> In x l.
-  Proof.
-    induction n; destruct l; boring.
-  Qed.
-
   Lemma sum_firstn_limb_widths_nonneg : forall n, 0 <= sum_firstn limb_widths n.
   Proof.
     unfold sum_firstn; intros.
@@ -163,16 +143,6 @@ Section PseudoMersenneBaseParamProofs.
     rewrite two_p_correct in nth_err_x.
     congruence.
   Qed.
- 
-
-  (* TODO : move to ZUtil *)
-  Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0.
-  Proof.
-    intros.
-    replace b with (b - c + c) by ring.
-    rewrite Z.pow_add_r by omega.
-    apply Z_mod_mult.
-  Qed.
 
   Lemma base_matches_modulus: forall i j,
     (i   <  length base)%nat ->
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index 505797987..9ae03dcd5 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -146,8 +146,8 @@ Qed.
 Lemma b_minus1_nonzero : 0 < b - 1. Proof. cbv. omega. Qed.
 
 Definition PointEncoding : encoding of E.point as (word b) :=
-  (@point_encoding _ _ b_minus1_nonzero b_valid q_5mod8 sqrt_minus1_valid FqEncoding
-  (@sign_bit _ prime_q two_lt_q _ b_valid) sign_bit_zero sign_bit_opp).
+  (@point_encoding curve25519params (b - 1) q_5mod8 sqrt_minus1_valid FqEncoding
+  (@sign_bit _ prime_q two_lt_q (b - 1) b_valid) sign_bit_zero sign_bit_opp).
 
 Definition H : forall n : nat, word n -> word (b + b). Admitted.
 Definition B : E.point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *)
diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v
index 3668632f4..484c5f0df 100644
--- a/src/Spec/PointEncoding.v
+++ b/src/Spec/PointEncoding.v
@@ -33,10 +33,10 @@ Section PointEncoding.
   Definition point_dec := Eval hnf in (proj1_sig point_dec_with_spec).
 
    Definition point_encoding_valid : forall p : E.point, point_dec (point_enc p) = Some p :=
-     @PointEncodingPre.point_encoding_valid _ _ sz_nonzero bound_check q_5mod8 sqrt_minus1_valid _ _ sign_bit_zero sign_bit_opp.
+     @PointEncodingPre.point_encoding_valid _ _ q_5mod8 sqrt_minus1_valid _ _ sign_bit_zero sign_bit_opp.
 
    Definition point_encoding_canonical : forall x_enc x, point_dec x_enc = Some x -> point_enc x = x_enc :=
-     PointEncodingPre.point_encoding_canonical . 
+     PointEncodingPre.point_encoding_canonical.
 
   Instance point_encoding : encoding of E.point as (Word.word (S sz)) := {
     enc := point_enc;
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index b640fb8e8..36d8a3ad3 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -563,4 +563,22 @@ Proof.
   induction l; intros; simpl; try tauto.
   rewrite <- IHl.
   intuition (subst; auto).
-Qed. 
\ No newline at end of file
+Qed.
+
+Lemma fold_right_invariant : forall {A} P (f: A -> A -> A) l x,
+  P x -> (forall y, In y l -> forall z, P z -> P (f y z)) ->
+  P (fold_right f x l).
+Proof.
+  induction l; intros ? ? step; auto.
+  simpl.
+  apply step; try apply in_eq.
+  apply IHl; auto.
+  intros y in_y_l.
+  apply (in_cons a) in in_y_l.
+  auto.
+Qed.
+
+Lemma In_firstn : forall {T} n l (x : T), In x (firstn n l) -> In x l.
+Proof.
+  induction n; destruct l; boring.
+Qed.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 17d04c60a..d655d046d 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -1,5 +1,6 @@
 Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.NatUtil.
 Require Import Bedrock.Word.
 
 Local Open Scope nat_scope.
@@ -21,6 +22,30 @@ Proof.
   auto.
 Qed.
 
+Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N ->
+  wordToN (NToWord sz n) = n.
+Proof.
+  intros.
+  rewrite wordToN_nat, NToWord_nat.
+  rewrite wordToNat_natToWord_idempotent; rewrite Nnat.N2Nat.id; auto.
+Qed.
+
+Lemma NToWord_wordToN : forall sz w, NToWord sz (wordToN w) = w.
+Proof.
+  intros.
+  rewrite wordToN_nat, NToWord_nat, Nnat.Nat2N.id.
+  apply natToWord_wordToNat.
+Qed.
+
+Lemma bound_check_nat_N : forall x n, (Z.to_nat x < 2 ^ n)%nat -> (Z.to_N x < Npow2 n)%N.
+Proof.
+  intros x n bound_nat.
+  rewrite <- Nnat.N2Nat.id, Npow2_nat.
+  replace (Z.to_N x) with (N.of_nat (Z.to_nat x)) by apply Z_nat_N.
+  apply (Nat2N_inj_lt _ (pow2 n)).
+  rewrite pow2_id; assumption.
+Qed.
+
 Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n.
   refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with
                             | eq_refl => w
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 9f7b1d645..bc7e9d740 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -280,6 +280,23 @@ Proof.
   assumption.
 Qed.
 
+Lemma Z_odd_mod : forall a b, (b <> 0)%Z ->
+  Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a.
+Proof.
+  intros.
+  rewrite Zmod_eq_full by assumption.
+  rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul.
+  case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r.
+Qed.
+
+Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0.
+Proof.
+  intros.
+  replace b with (b - c + c) by ring.
+  rewrite Z.pow_add_r by omega.
+  apply Z_mod_mult.
+Qed.
+
 (* prove that known nonnegative numbers are nonnegative *)
 Ltac zero_bounds' :=
   repeat match goal with