\module Algebra.Meta

equation

equation a_1 … a_n proves an equation a_0 = a_{n+1} using a_1, … a_n as intermediate steps. A proof of a_i = a_{i+1} can be specified as implicit arguments between them. using, usingOnly, and hiding with a single argument can be used instead of a proof to control the context. The first implicit argument can be either a universe or a subclass of either Monoid, AddMonoid, or Order.Lattice.Bounded.MeetSemilattice. In the former case, the meta will prove an equality in a type without using any additional structure on it. In the latter case, the meta will prove an equality using only structure available in the specified class.

cong

This meta implements the congruence closure algorithm. For example, given assumptions x = x’ and y = y’, it can prove f x y = f x’ y’.

linarith

This meta solves systems of linear equations in ordered rings using Fourier–Motzkin elimination.