From c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 6 Apr 2017 22:53:07 -0400 Subject: rename-everything --- src/Algebra/Field.v | 32 ++++----- src/Algebra/Field_test.v | 2 +- src/Algebra/Group.v | 2 +- src/Algebra/Hierarchy.v | 161 ++++++++++++++++++++++++++++++++++++++++++ src/Algebra/IntegralDomain.v | 10 +-- src/Algebra/Monoid.v | 2 +- src/Algebra/Nsatz.v | 162 +++++++++++++++++++++++++++++++++++++++++++ src/Algebra/Ring.v | 4 +- src/Algebra/ScalarMult.v | 2 +- 9 files changed, 350 insertions(+), 27 deletions(-) create mode 100644 src/Algebra/Hierarchy.v create mode 100644 src/Algebra/Nsatz.v (limited to 'src/Algebra') 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. -- cgit v1.2.3