diff options
Diffstat (limited to 'src/Algebra/Hierarchy.v')
| -rw-r--r-- | src/Algebra/Hierarchy.v | 161 |
1 files changed, 161 insertions, 0 deletions
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. |