rename-everything

9 files changed, 350 insertions, 27 deletions

diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v
index e71b24018..7270f6018 100644
--- a/src/Algebra/Field.v
+++ b/src/Algebra/Field.v
@@ -2,7 +2,7 @@ Require Import Crypto.Util.Relations Crypto.Util.Notations.
 Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Tactics.DebugPrint.
 Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms.
-Require Import Crypto.Algebra Crypto.Algebra.Ring Crypto.Algebra.IntegralDomain.
+Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Ring Crypto.Algebra.IntegralDomain.
 Require Coq.setoid_ring.Field_theory.
 
 Section Field.
@@ -215,14 +215,14 @@ End Homomorphism_rev.
 
 Ltac guess_field :=
   match goal with
-  | |- ?eq _ _ =>  constr:(_:Algebra.field (eq:=eq))
-  | |- not (?eq _ _) =>  constr:(_:Algebra.field (eq:=eq))
-  | [H: ?eq _ _ |- _ ] =>  constr:(_:Algebra.field (eq:=eq))
-  | [H: not (?eq _ _) |- _] =>  constr:(_:Algebra.field (eq:=eq))
+  | |- ?eq _ _ =>  constr:(_:Hierarchy.field (eq:=eq))
+  | |- not (?eq _ _) =>  constr:(_:Hierarchy.field (eq:=eq))
+  | [H: ?eq _ _ |- _ ] =>  constr:(_:Hierarchy.field (eq:=eq))
+  | [H: not (?eq _ _) |- _] =>  constr:(_:Hierarchy.field (eq:=eq))
   end.
 
 Ltac goal_to_field_equality fld :=
-  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
+  let eq := match type of fld with Hierarchy.field(eq:=?eq) => eq end in
   match goal with
   | [ |- eq _ _] => idtac
   | [ |- not (eq ?x ?y) ] => apply not_exfalso; intro; goal_to_field_equality fld
@@ -234,10 +234,10 @@ Ltac goal_to_field_equality fld :=
   end.
 
 Ltac inequalities_to_inverse_equations fld :=
-  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
-  let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in
-  let div := match type of fld with Algebra.field(div:=?div) => div end in
-  let sub := match type of fld with Algebra.field(sub:=?sub) => sub end in
+  let eq := match type of fld with Hierarchy.field(eq:=?eq) => eq end in
+  let zero := match type of fld with Hierarchy.field(zero:=?zero) => zero end in
+  let div := match type of fld with Hierarchy.field(div:=?div) => div end in
+  let sub := match type of fld with Hierarchy.field(sub:=?sub) => sub end in
   repeat match goal with
          | [H: not (eq _ _) |- _ ] =>
            lazymatch type of H with
@@ -258,8 +258,8 @@ Ltac unique_pose_implication pf :=
   end.
 
 Ltac inverses_to_conditional_equations fld :=
-  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
-  let inv := match type of fld with Algebra.field(inv:=?inv) => inv end in
+  let eq := match type of fld with Hierarchy.field(eq:=?eq) => eq end in
+  let inv := match type of fld with Hierarchy.field(inv:=?inv) => inv end in
   repeat match goal with
          | |- context[inv ?d] =>
            unique_pose_implication constr:(right_multiplicative_inverse(H:=fld) d)
@@ -268,15 +268,15 @@ Ltac inverses_to_conditional_equations fld :=
          end.
 
 Ltac clear_hypotheses_with_nonzero_requirements fld :=
-  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
-  let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in
+  let eq := match type of fld with Hierarchy.field(eq:=?eq) => eq end in
+  let zero := match type of fld with Hierarchy.field(zero:=?zero) => zero end in
   repeat match goal with
            [H: not (eq _ zero) -> _ |- _ ] => clear H
          end.
 
 Ltac forward_nonzero fld solver_tac :=
-  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
-  let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in
+  let eq := match type of fld with Hierarchy.field(eq:=?eq) => eq end in
+  let zero := match type of fld with Hierarchy.field(zero:=?zero) => zero end in
   repeat match goal with
          | [H: not (eq ?x zero) -> _ |- _ ]
            => let H' := fresh in
diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v
index 0743729c2..59ca72c6b 100644
--- a/src/Algebra/Field_test.v
+++ b/src/Algebra/Field_test.v
@@ -4,7 +4,7 @@ Require Import Crypto.Algebra.Ring Crypto.Algebra.Field.
 Module _fsatz_test.
   Section _test.
     Context {F eq zero one opp add sub mul inv div}
-            {fld:@Algebra.field F eq zero one opp add sub mul inv div}
+            {fld:@Hierarchy.field F eq zero one opp add sub mul inv div}
             {eq_dec:DecidableRel eq}.
     Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
     Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v
index 64e378281..8ce3e2a91 100644
--- a/src/Algebra/Group.v
+++ b/src/Algebra/Group.v
@@ -1,5 +1,5 @@
 Require Import Coq.Classes.Morphisms Crypto.Util.Relations (*Crypto.Util.Tactics*).
-Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult.
+Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult.
 
 Section BasicProperties.
   Context {T eq op id inv} `{@group T eq op id inv}.
diff --git a/src/Algebra/Hierarchy.v b/src/Algebra/Hierarchy.v
new file mode 100644
index 000000000..342e9feaa
--- /dev/null
+++ b/src/Algebra/Hierarchy.v
@@ -0,0 +1,161 @@
+Require Export Crypto.Util.FixCoqMistakes.
+Require Export Crypto.Util.Decidable.
+
+Require Coq.PArith.BinPos.
+Require Import Coq.Classes.Morphisms.
+
+Require Coq.Numbers.Natural.Peano.NPeano.
+Require Coq.Lists.List.
+
+Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope.
+
+Section Algebra.
+  Context {T:Type} {eq:T->T->Prop}.
+  Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+
+  Section SingleOperation.
+    Context {op:T->T->T}.
+
+    Class is_associative := { associative : forall x y z, op x (op y z) = op (op x y) z }.
+
+    Context {id:T}.
+
+    Class is_left_identity := { left_identity : forall x, op id x = x }.
+    Class is_right_identity := { right_identity : forall x, op x id = x }.
+
+    Class monoid :=
+      {
+        monoid_is_associative : is_associative;
+        monoid_is_left_identity : is_left_identity;
+        monoid_is_right_identity : is_right_identity;
+
+        monoid_op_Proper: Proper (respectful eq (respectful eq eq)) op;
+        monoid_Equivalence : Equivalence eq
+      }.
+    Global Existing Instance monoid_is_associative.
+    Global Existing Instance monoid_is_left_identity.
+    Global Existing Instance monoid_is_right_identity.
+    Global Existing Instance monoid_Equivalence.
+    Global Existing Instance monoid_op_Proper.
+
+    Context {inv:T->T}.
+    Class is_left_inverse := { left_inverse : forall x, op (inv x) x = id }.
+    Class is_right_inverse := { right_inverse : forall x, op x (inv x) = id }.
+
+    Class group :=
+      {
+        group_monoid : monoid;
+        group_is_left_inverse : is_left_inverse;
+        group_is_right_inverse : is_right_inverse;
+
+        group_inv_Proper: Proper (respectful eq eq) inv
+      }.
+    Global Existing Instance group_monoid.
+    Global Existing Instance group_is_left_inverse.
+    Global Existing Instance group_is_right_inverse.
+    Global Existing Instance group_inv_Proper.
+
+    Class is_commutative := { commutative : forall x y, op x y = op y x }.
+
+    Record abelian_group :=
+      {
+        abelian_group_group : group;
+        abelian_group_is_commutative : is_commutative
+      }.
+    Existing Class abelian_group.
+    Global Existing Instance abelian_group_group.
+    Global Existing Instance abelian_group_is_commutative.
+  End SingleOperation.
+
+  Section AddMul.
+    Context {zero one:T}. Local Notation "0" := zero. Local Notation "1" := one.
+    Context {opp:T->T}. Local Notation "- x" := (opp x).
+    Context {add:T->T->T} {sub:T->T->T} {mul:T->T->T}.
+    Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul.
+
+    Class is_left_distributive := { left_distributive : forall a b c, a * (b + c) =  a * b + a * c }.
+    Class is_right_distributive := { right_distributive : forall a b c, (b + c) * a = b * a + c * a }.
+
+
+    Class ring :=
+      {
+        ring_abelian_group_add : abelian_group (op:=add) (id:=zero) (inv:=opp);
+        ring_monoid_mul : monoid (op:=mul) (id:=one);
+        ring_is_left_distributive : is_left_distributive;
+        ring_is_right_distributive : is_right_distributive;
+
+        ring_sub_definition : forall x y, x - y = x + opp y;
+
+        ring_mul_Proper : Proper (respectful eq (respectful eq eq)) mul;
+        ring_sub_Proper : Proper(respectful eq (respectful eq eq)) sub
+      }.
+    Global Existing Instance ring_abelian_group_add.
+    Global Existing Instance ring_monoid_mul.
+    Global Existing Instance ring_is_left_distributive.
+    Global Existing Instance ring_is_right_distributive.
+    Global Existing Instance ring_mul_Proper.
+    Global Existing Instance ring_sub_Proper.
+
+    Class commutative_ring :=
+      {
+        commutative_ring_ring : ring;
+        commutative_ring_is_commutative : is_commutative (op:=mul)
+      }.
+    Global Existing Instance commutative_ring_ring.
+    Global Existing Instance commutative_ring_is_commutative.
+
+    Class is_zero_product_zero_factor :=
+      { zero_product_zero_factor : forall x y, x*y = 0 -> x = 0 \/ y = 0 }.
+
+    Class is_zero_neq_one := { zero_neq_one : zero <> one }.
+
+    Class integral_domain :=
+      {
+        integral_domain_commutative_ring : commutative_ring;
+        integral_domain_is_zero_product_zero_factor : is_zero_product_zero_factor;
+        integral_domain_is_zero_neq_one : is_zero_neq_one
+      }.
+    Global Existing Instance integral_domain_commutative_ring.
+    Global Existing Instance integral_domain_is_zero_product_zero_factor.
+    Global Existing Instance integral_domain_is_zero_neq_one.
+
+    Context {inv:T->T} {div:T->T->T}.
+    Class is_left_multiplicative_inverse := { left_multiplicative_inverse : forall x, x<>0 -> (inv x) * x = 1 }.
+
+    Class field :=
+      {
+        field_commutative_ring : commutative_ring;
+        field_is_left_multiplicative_inverse : is_left_multiplicative_inverse;
+        field_is_zero_neq_one : is_zero_neq_one;
+
+        field_div_definition : forall x y , div x y = x * inv y;
+
+        field_inv_Proper : Proper (respectful eq eq) inv;
+        field_div_Proper : Proper (respectful eq (respectful eq eq)) div
+      }.
+    Global Existing Instance field_commutative_ring.
+    Global Existing Instance field_is_left_multiplicative_inverse.
+    Global Existing Instance field_is_zero_neq_one.
+    Global Existing Instance field_inv_Proper.
+    Global Existing Instance field_div_Proper.
+  End AddMul.
+
+  Definition char_ge (zero:T) (inj:BinPos.positive->T) C := forall p, BinPos.Pos.lt p C -> not (eq (inj p) zero).
+  Existing Class char_ge.
+  Lemma char_ge_weaken id of_pos C
+        (HC:@char_ge id of_pos C) c (Hc:BinPos.Pos.le c C)
+    : @char_ge id of_pos c.
+  Proof. intros ??; eauto using BinPos.Pos.lt_le_trans. Qed.
+  (* TODO: make a typeclass instance that applies this lemma
+  automatically using [vm_decide] for the inequality if both
+  characteristics are literal constants. *)
+End Algebra.
+
+Section ZeroNeqOne.
+  Context {T eq zero one} `{@is_zero_neq_one T eq zero one} `{Equivalence T eq}.
+
+  Lemma one_neq_zero : not (eq one zero).
+  Proof using Type*.
+    intro HH; symmetry in HH. auto using zero_neq_one.
+  Qed.
+End ZeroNeqOne.
diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v
index 4ab50c6e3..c52b4ce87 100644
--- a/src/Algebra/IntegralDomain.v
+++ b/src/Algebra/IntegralDomain.v
@@ -1,7 +1,7 @@
 Require Coq.setoid_ring.Integral_domain.
-Require Crypto.Tactics.Algebra_syntax.Nsatz.
+Require Crypto.Algebra.Nsatz.
 Require Import Crypto.Util.Factorize.
-Require Import Crypto.Algebra Crypto.Algebra.Ring.
+Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Ring.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Tactics.BreakMatch.
 
@@ -23,8 +23,8 @@ Module IntegralDomain.
     Section ReflectiveNsatzSideConditionProver.
       Import BinInt BinNat BinPos.
       Context {R eq zero one opp add sub mul}
-              {ring:@Algebra.ring R eq zero one opp add sub mul}
-              {zpzf:@Algebra.is_zero_product_zero_factor R eq zero mul}.
+              {ring:@Hierarchy.ring R eq zero one opp add sub mul}
+              {zpzf:@Hierarchy.is_zero_product_zero_factor R eq zero mul}.
       Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
       Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
       Local Infix "+" := add.  Local Infix "-" := sub. Local Infix "*" := mul.
@@ -198,4 +198,4 @@ Ltac dropRingSyntax :=
         Ncring.opp_notation
         Ncring.eq_notation
     ] in *.
-Ltac nsatz := Algebra_syntax.Nsatz.nsatz; dropRingSyntax.
+Ltac nsatz := Algebra.Nsatz.nsatz; dropRingSyntax.
diff --git a/src/Algebra/Monoid.v b/src/Algebra/Monoid.v
index bd15290c7..470e8df40 100644
--- a/src/Algebra/Monoid.v
+++ b/src/Algebra/Monoid.v
@@ -1,6 +1,6 @@
 Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Util.Tactics.RewriteHyp.
-Require Import Crypto.Algebra.
+Require Import Crypto.Algebra.Hierarchy.
 
 Section Monoid.
   Context {T eq op id} {monoid:@monoid T eq op id}.
diff --git a/src/Algebra/Nsatz.v b/src/Algebra/Nsatz.v
new file mode 100644
index 000000000..2a65e7d82
--- /dev/null
+++ b/src/Algebra/Nsatz.v
@@ -0,0 +1,162 @@
+(* This is a rewrite of the Ltac parts of standard library nsatz. We should
+  periodically check whether we still need it -- once enough bugs get fixed
+  in mailine, we hope to drop this implementation *)
+
+Require Coq.nsatz.Nsatz.
+Require Import Coq.Lists.List.
+
+Generalizable All Variables.
+Lemma cring_sub_diag_iff {R zero eq sub} `{cring:Cring.Cring (R:=R) (ring0:=zero) (ring_eq:=eq) (sub:=sub)}
+  : forall x y, eq (sub x y) zero <-> eq x y.
+Proof.
+  split;intros Hx.
+  { eapply Nsatz.psos_r1b. eapply Hx. }
+  { eapply Nsatz.psos_r1. eapply Hx. }
+Qed.
+
+Ltac get_goal := lazymatch goal with |- ?g => g end.
+
+Ltac nsatz_equation_implications_to_list eq zero g :=
+  lazymatch g with
+  | eq ?p zero => constr:(p::nil)
+  | eq ?p zero -> ?g => let l := nsatz_equation_implications_to_list eq zero g in constr:(p::l)
+  end.
+
+Ltac nsatz_reify_equations eq zero :=
+  let g := get_goal in
+  let lb := nsatz_equation_implications_to_list eq zero g in
+  lazymatch (eval red in (Ncring_tac.list_reifyl (lterm:=lb))) with
+    (?variables, ?le) =>
+    lazymatch (eval compute in (List.rev le)) with
+    | ?reified_goal::?reified_givens => constr:((variables, reified_givens, reified_goal))
+    end
+  end.
+
+Ltac nsatz_get_free_variables reified_package :=
+  lazymatch reified_package with (?fv, _, _) => fv end.
+
+Ltac nsatz_get_reified_givens reified_package :=
+  lazymatch reified_package with (_, ?givens, _) => givens end.
+
+Ltac nsatz_get_reified_goal reified_package :=
+  lazymatch reified_package with (_, _, ?goal) => goal end.
+
+Require Import Coq.setoid_ring.Ring_polynom.
+(* Kludge for 8.4/8.5 compatibility *)
+Module Import mynsatz_compute.
+  Import Nsatz.
+  Global Ltac mynsatz_compute x := nsatz_compute x.
+End mynsatz_compute.
+Ltac nsatz_compute x := mynsatz_compute x.
+
+Ltac nsatz_compute_to_goal sugar nparams reified_goal power reified_givens :=
+  nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens).
+
+Ltac nsatz_compute_get_leading_coefficient :=
+  lazymatch goal with
+    |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => a
+  end.
+
+Ltac nsatz_compute_get_certificate :=
+  lazymatch goal with
+    |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:((c,b))
+  end.
+
+Ltac nsatz_rewrite_and_revert domain :=
+  lazymatch type of domain with
+  | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
+    lazymatch goal with
+    | |- eq _ zero => idtac
+    | |- eq _ _ => rewrite <-(cring_sub_diag_iff (cring:=FCring))
+    end;
+    repeat match goal with
+           | [H : eq _ zero |- _ ] => revert H
+           | [H : eq _ _ |- _ ] => rewrite <-(cring_sub_diag_iff (cring:=FCring)) in H; revert H
+           end
+  end.
+
+(** As per https://coq.inria.fr/bugs/show_bug.cgi?id=4851, [nsatz]
+    cannot handle duplicate hypotheses.  So we clear them. *)
+Ltac nsatz_clear_duplicates_for_bug_4851 domain :=
+  lazymatch type of domain with
+  | @Integral_domain.Integral_domain _ _ _ _ _ _ _ ?eq _ _ _ =>
+    repeat match goal with
+           | [ H : eq ?x ?y, H' : eq ?x ?y |- _ ] => clear H'
+           end
+  end.
+
+Ltac nsatz_nonzero :=
+  try solve [apply Integral_domain.integral_domain_one_zero
+            |apply Integral_domain.integral_domain_minus_one_zero
+            |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 *)
+  lazymatch type of domain with
+  | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
+    nsatz_clear_duplicates_for_bug_4851 domain;
+    nsatz_rewrite_and_revert domain;
+    let reified_package := nsatz_reify_equations eq zero in
+    let fv := nsatz_get_free_variables reified_package in
+    let interp := constr:(@Nsatz.PEevalR _ _ _ _ _ _ _ _ Fops fv) in
+    let reified_givens := nsatz_get_reified_givens reified_package in
+    let reified_goal := nsatz_get_reified_goal reified_package in
+    nsatz_compute_to_goal sugar nparams reified_goal power reified_givens;
+    let a := nsatz_compute_get_leading_coefficient in
+    let crt := nsatz_compute_get_certificate in
+    intros _ (* discard [nsatz_compute] output *); intros;
+    apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond));
+    [ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS]
+    | solve [vm_compute; exact (eq_refl true)] (* exact_no_check (eq_refl true) *)
+    | solve [repeat (split; [assumption|]); exact I] ]
+  end.
+
+Ltac nsatz_guess_domain :=
+  match goal with
+  | |- ?eq _ _ => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
+  | |- not (?eq _ _) =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
+  | [H: ?eq _ _ |- _ ] =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
+  | [H: not (?eq _ _) |- _] =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
+  end.
+
+Ltac nsatz_sugar_power sugar power :=
+  let domain := nsatz_guess_domain in
+  nsatz_domain_sugar_power domain sugar power.
+
+Ltac nsatz_power power :=
+  let power_N := (eval compute in (BinNat.N.of_nat power)) in
+  nsatz_sugar_power BinInt.Z0 power_N.
+
+Ltac nsatz := nsatz_power 1%nat.
+
+Tactic Notation "nsatz" := nsatz.
+Tactic Notation "nsatz" constr(n) := nsatz_power n.
+
+(** If the goal is of the form [?x <> ?y] and assuming [?x = ?y]
+    contradicts any hypothesis of the form [?x' <> ?y'], we turn this
+    problem about inequalities into one about equalities and give it
+    to [nsatz]. *)
+Ltac nsatz_contradict_single_hypothesis domain :=
+  lazymatch type of domain with
+  | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
+    unfold not in *;
+    match goal with
+    | [ H : eq _ _ -> False |- eq _ _ -> False ]
+      => intro; apply H; nsatz
+    | [ H : eq _ _ -> False |- False ]
+      => apply H; nsatz
+    end
+  end.
+
+Ltac nsatz_contradict :=
+  let domain := nsatz_guess_domain in
+  nsatz_contradict_single_hypothesis domain
+  || (unfold not;
+      intros;
+      lazymatch type of domain with
+      | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
+        assert (eq one zero) as Hbad;
+        [nsatz; nsatz_nonzero
+        |destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)]
+      end).
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v
index cff27bdb3..406706988 100644
--- a/src/Algebra/Ring.v
+++ b/src/Algebra/Ring.v
@@ -4,7 +4,7 @@ Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.OnSubterms.
 Require Import Crypto.Util.Tactics.Revert.
-Require Import Crypto.Algebra Crypto.Algebra.Group Crypto.Algebra.Monoid.
+Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Group Crypto.Algebra.Monoid.
 Require Coq.ZArith.ZArith Coq.PArith.PArith.
 
 
@@ -420,7 +420,7 @@ End of_Z.
 Definition char_ge
            {R eq zero one opp add} {sub:R->R->R} {mul:R->R->R}
            C :=
-  @Algebra.char_ge R eq zero (fun p => (@of_Z R zero one opp add) (BinInt.Z.pos p)) C.
+  @Hierarchy.char_ge R eq zero (fun p => (@of_Z R zero one opp add) (BinInt.Z.pos p)) C.
 Existing Class char_ge.
 
 (*** Tactics for ring equations *)
diff --git a/src/Algebra/ScalarMult.v b/src/Algebra/ScalarMult.v
index 5c17a6bb5..f52fc93ee 100644
--- a/src/Algebra/ScalarMult.v
+++ b/src/Algebra/ScalarMult.v
@@ -1,5 +1,5 @@
 Require Import Coq.Classes.Morphisms.
-Require Import Crypto.Algebra Crypto.Algebra.Monoid.
+Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Monoid.
 
 Module Import ModuloCoq8485.
   Import NPeano Nat.