08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
75 lines
2.5 KiB
Text
75 lines
2.5 KiB
Text
class Semigroup (α : Type u) extends Mul α where
|
||
mul_assoc (a b c : α) : a * b * c = a * (b * c)
|
||
|
||
class CommSemigroup (α : Type u) extends Semigroup α where
|
||
mul_comm (a b : α) : a * b = b * a
|
||
|
||
class Monoid (α : Type u) extends Semigroup α, One α where
|
||
one_mul (a : α) : 1 * a = a
|
||
mul_one (a : α) : a * 1 = a
|
||
|
||
class CommMonoid (α : Type u) extends Monoid α, CommSemigroup α
|
||
|
||
set_option pp.all true
|
||
#check CommMonoid.mk
|
||
#print CommMonoid.toCommSemigroup
|
||
|
||
class Group (α : Type u) extends Monoid α, Inv α where
|
||
mul_left_inv (a : α) : a⁻¹ * a = 1
|
||
|
||
class CommGroup (α : Type u) extends Group α, CommMonoid α
|
||
|
||
#check CommGroup.mk
|
||
#print CommGroup.toCommMonoid
|
||
|
||
class AddSemigroup (α : Type u) extends Add α where
|
||
add_assoc (a b c : α) : a + b + c = a + (b + c)
|
||
|
||
class AddCommSemigroup (α : Type u) extends AddSemigroup α where
|
||
add_comm (a b : α) : a + b = b + a
|
||
|
||
class AddMonoid (α : Type u) extends AddSemigroup α, Zero α where
|
||
zero_add (a : α) : 0 + a = a
|
||
add_zero (a : α) : a + 0 = a
|
||
|
||
class AddCommMonoid (α : Type u) extends AddMonoid α, AddCommSemigroup α
|
||
|
||
class AddGroup (α : Type u) extends AddMonoid α, Neg α where
|
||
add_left_neg (a : α) : -a + a = 0
|
||
|
||
class AddCommGroup (α : Type u) extends AddGroup α, AddCommMonoid α
|
||
|
||
class Distrib (α : Type u) extends Mul α, Add α where
|
||
left_distrib ( a b c : α) : a * (b + c) = (a * b) + (a * c)
|
||
right_distrib (a b c : α) : (a + b) * c = (a * c) + (b * c)
|
||
|
||
class MulZero (α : Type u) extends Mul α, Zero α where
|
||
zero_mul (a : α) : 0 * a = 0
|
||
mul_zero (a : α) : a * 0 = 0
|
||
|
||
class ZeroNeOne (α : Type u) extends Zero α, One α where
|
||
zero_ne_one : (0:α) ≠ 1
|
||
|
||
class Semiring (α : Type u) extends AddCommMonoid α, Monoid α, Distrib α, MulZero α
|
||
|
||
class CommSemiring (α : Type u) extends Semiring α, CommMonoid α
|
||
|
||
class Ring (α : Type u) extends AddCommGroup α, Monoid α, Distrib α
|
||
|
||
class CommRing (α : Type u) extends Ring α, CommSemigroup α
|
||
|
||
class NoZeroDivisors (α : Type u) extends Mul α, Zero α where
|
||
eq_zero_or_eq_zero_of_mul_eq_zero (a b : α) : a * b = 0 → a = 0 ∨ b = 0
|
||
|
||
class IntegralDomain (α : Type u) extends CommRing α, NoZeroDivisors α, ZeroNeOne α
|
||
|
||
class DivisionRing (α : Type u) extends Ring α, Inv α, ZeroNeOne α where
|
||
mul_inv_cancel {a : α} : a ≠ 0 → a * a⁻¹ = 1
|
||
inv_mul_cancel {a : α} : a ≠ 0 → a⁻¹ * a = 1
|
||
|
||
class Field (α : Type u) extends DivisionRing α, CommRing α
|
||
|
||
set_option pp.all false in
|
||
#check Field.mk
|
||
#print Field.toDivisionRing
|
||
#print Field.toCommRing
|