rename-everything

1 files changed, 0 insertions, 161 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
deleted file mode 100644
index 342e9feaa..000000000
--- a/src/Algebra.v
+++ /dev/null
@@ -1,161 +0,0 @@
-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.