v1.10.0

• Tactics:

  • assumption meta
  • in meta
  • defaultImpl meta

• Sets and logic:

  • Pigeonhole principle
  • Kuratowski-finite sets
  • "The following are equivalent" proofs
  • Countable sets
  • Subset operations
  • Simplified syntax for quantifiers
  • Partial elements

• Algebra:

  • Graded rings homogeneous ideals homogeneous localizations, Proj construction
  • Lagrange's theorem
  • Dimension of a ring, a characterization of zero-dimensional rings, zero-dimensional local rings, and von Neumann regular rings
  • A characterization of Smith rings
  • PIDs are Smith domains
  • PIDs are 1-dimensional
  • Euclidean domains are PIDs
  • Polynomial division
  • Matrix ring
  • Various definitions of determinant and a proof that they are equivalent
  • Various properties of determinant
  • Symmetric group, its cardinality, sign homomorphism
  • Characteristic polynomial of a matrix and a proof that eigenvalues are its roots
  • Integral elements and extensions, a characterization of finitely generated integral extensions
  • Monoid rings and multivariate polynomials
  • Valuation rings
  • Factor rings and factor fields
  • Nakayama's lemma
  • The minimal polynomial of an element of a ring extension
  • A proof that a finitely generated extension is integral if and only if it is zero-dimensional
  • The Chinese remainder theorem
  • Dimension of a finite free module
  • Independent sets, bases, and their various properties
  • The image and the kernel of a linear map between finite modules over a Smith domain are finite
  • Linear dependency is decidable in a finite module over a Smith domain
  • Splitting fields of polynomials over countable fields
  • Rank of a matrix over a Smith domain
  • Surjective linear endomaps on a finitely generated module are bijective
  • Cayley-Hamilton theorem
  • Direct limits of algebraic structures over semilattices
  • Algebraically closed fields and the algebraic closure of a countable field
  • The absolute value for linearly ordered abelian groups
  • Group actions
  • First isomorphism theorem

• Topology:

  • Cover spaces
  • Completion of cover spaces
  • Uniform spaces and their completion
  • Metric spaces and their completion
  • Equivalence between appropriate subcategories of complete cover spaces and regular locales
  • Topological abeliean groups and their completion
  • Normed abelian groups, normed rings, Banach spaces
  • Products of topological spaces, cover spaces, uniform spaces, and topological abelian groups
  • Normed abelian group of real numbers
  • Compact spaces and a characteriization of cover maps
  • Cover space structure on directed sets

• Analysis:

  • Limit of a function on a directed set
  • Uniform convergence
  • Series and various convergence tests
  • Power series and their radius of convergence

• Real and complex numbers:

  • The field of real numbers
  • The field of complex numbers
  • The exponential function on real numbers

• Categories:

  • Heyting algebras
  • Cartesian closed categories
  • Elementary topoi

v1.9.0

• The definion of modules, algebras, strict domains, polynomials, and various structures on them
• A synthetic definition of a derivative and its basic properties
• The definition of real numbers and the construction of the structure of an ordered field on them (except for multiplication).
• A tactic for solving systems of linear equations
• The definition of schemes, affine schemes, and a prove that affine schemes are schemes.
• A partial prove of the univalence for the precategory of ringed locales.

v1.8.0

• New and improved metas:
  • Improved Exists meta and new metas Given and Forall.
  • Improved contradiction meta. Now, it can derive contradictions from transitive closure of <, <=, and =.
  • New simplify meta.
• Locales:
  • The definition of discrete locales and the embedding of rationals into reals.
  • The definition of overt locales and open maps.
  • The construction of dense-closed and strongly dense-weakly closed factorization systems on the category of locales.
  • A proof that nuclei form a frame.
  • Limits and colimits of locales.
  • A characterization of embeddings of locales: a map of locales is a regular monomorphism if and only if the left adjoint is surjective.
  • The definition of (weakly) regular locales and a proof that the locale of reals is regular.
  • The definition of Hausdorff locales and a proof that regular locales are Hausdorff.
  • The definition of uniform locales and the construction of their completion.
• The definition of abstract reduction systems, second-order term rewriting systems, and a proof that the disjoint union of confluent left-linear systems is confluent.
• The definition of algebraic theories, the category of its models, and a proof that it has all small limits and colimits.
• The preorder of subobjects and regular subobjects.
• The construction of the structure sheaf on the spectrum of a ring.

v1.7.0

• The locale of real numbers
• Compactness of the interval and local compactness of reals
• Spectrum of a ring
• Sheaves
• rewriteEq meta

v1.6.0.1

• A few bug fixes
• Non-unital presentations of frames
• Definition of adjoint functors

v1.6.0

• Locales and topological spaces
• Functor category
• Euclidean domains and (extended) Euclidean algorithm
• The quotient ring Z/nZ and the field structure on it for prime n
• Solvers for commutative monoids and rings are implemented in the equation meta
• Extensionality meta
• Structure identity principle meta
• simp_coe meta
• cases meta and improved mcases meta
• unfold and unfold_let metas

v1.5.0

• Debug metas (println, random, time)
• Congruence closure
• Insertion and tree sort functions
• Meta mcases

v1.4.1

• Implemented at meta.
• Improved contradiction meta.
• Removed unnecessary implicit arguments.

v1.4.0

Updates:

• Refine and 'replace with constructor' goal solvers
• Level prover for non-recursive data types
• 'contradiction' meta
• Transitive and equivalence closure
• 'using' and 'hiding' meta definitions
• 'equation' meta
• Construction of K(G,1)

v1.3.0

Implemented a few tactics: rewrite, repeat, apply, solver for monoids.