\import Algebra.Algebra
\import Algebra.Group
\import Algebra.Group.Solver(NatData, CGroupData, GroupTerm)
\import Algebra.Linear.Solver
\import Algebra.Monoid
\import Algebra.Monoid.Solver
\import Algebra.StrictlyOrdered
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Solver
\import Algebra.Semiring
\import Algebra.Solver
\import Algebra.Solver.CGroup
\import Algebra.Solver.CMonoid
\import Algebra.Solver.CRing
\import Algebra.Solver.CSemiring
\import Algebra.Solver.Group
\import Algebra.Solver.Monoid
\import Algebra.Solver.Ring
\import Algebra.Solver.Semiring
\import Algebra.Ring.Boolean
\import Algebra.Solver.BooleanRing
\import Arith.Int
\import Arith.Nat
\import Arith.Rat
\import Category(Precat)
\import Category.Solver
\import Data.Bool
\import Data.List
\import Equiv
\import Order.Lattice
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Set
{- |
`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 `Algebra.Monoid.Monoid`, `Algebra.Monoid.AddMonoid`, or `Order.Lattice.TopMeetSemilattice`.
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.
-}
\meta equation => _ (Equiv, Map.A, Map.B, idEquiv, transEquiv, BaseSet.E, *>, Precat.Hom, Precat.o, Precat.id, AddMonoid.zro-right,
PseudoSemiring.zro_*-right, TopMeetSemilattice, BoundedDistributiveLattice, AddGroup.fromZero, AddGroup.toZero, List.nil,
List.::, Monoid, CMonoid, AddMonoid, AbMonoid, Ring, Semiring, Monoid.LDiv, Monoid.RDiv, AlgData.terms-equality,
CAlgData.terms-equality, CRingData.terms-equality, LatticeData.terms-equality, AlgData.interpret, gensZeroToIdealZero,
LatticeData, CRingData, RingData, CSemiringData, SemiringData, LatticeData.L, HData, MonoidData, CMonoidData, LData, LData.L,
MonoidData.interpretNF, MonoidData.interpretNF_++, MonoidData.normalize-consistent, MonoidData.terms-equality-conv,
LData.terms-equality, CMonoidData.terms-equality, MonoidData.terms-equality, CMonoidData.terms-equality-conv,
CMonoidData.sort-consistent, CMonoidData.replace-consistent, MonoidData.replace-consistent, MonoidTerm.var, MonoidTerm.:ide,
MonoidTerm.:*, HData.interpretNF, HData.interpretNF_++, HData.normalize-consistent, HData.terms-equality, CatTerm.var,
CatTerm.:id, CatTerm.:o, CatNF.:nil, CatNF.:cons, HData.H, HData.V, pmap, inv, NatSemiring, IntRing, BottomJoinSemilattice.bottom,
TopMeetSemilattice.top, JoinSemilattice.join, MeetSemilattice.meet, AddMonoid.+, Semigroup.*, Semiring.natCoef,
AddGroup.negative, AAlgebra.coefMap, Pointed.ide, AddPointed.zro, RingTerm.var, RingTerm.coef, RingTerm.:ide, RingTerm.:zro,
RingTerm.:negative, RingTerm.:*, RingTerm.:+, BaseData.R, MonoidData.vars)
\where {
{- |
The monoid solver solves goals of the form `e1 = {M} e2` for some monoid `M`.
If `e1` and `e2` represent the same word in the language of monoids, then the solver proves the equality immediately without any additional arguments.
For example, {monoid} proves the following equality: `(x * (ide * y)) * ((ide * z) * w) = x * ((y * (z * ide)) * w)`.
If the words represented by `e1` and `e2` are not the same, then {monoid} puts them in a canonical form and expects an argument that proves the equality of these normal forms.
For example, if the goal is `(x * (ide * y)) * ((ide * z) * w) = w * ((z * (y * ide)) * x)`, then the subgoal in `monoid {?}` is `x * (y * (z * w)) = w * (z * (y * x))`.
Conversely, if we have an expression of the type `e1 = {M} e2`, then we can transform it into a proof of the equality of canonical forms.
For example, if `(p : (x * (ide * y)) * ((ide * z) * w) = w * ((z * (y * ide)) * x))`, then `monoid in p` has type `x * (y * (z * w)) = w * (z * (y * x))`.
The monoid solver can also apply hypotheses to solve goals.
A hypothesis `h` is an expression of type `l = {M} r`.
Given such a hypothesis, `monoid {h}` replaces all occurrences of `l` with `r` in both `e1` and `e2`.
For example, if `p : x * y = ide` and the goal is `(z * x) * (y * w) = w * (x * (y * z))`, then the subgoal in `monoid {p} {?}` is `z * w = w * z`.
Several hypotheses are applied sequentially.
So, for example, if `p : x * y = ide` and the goal is `(x * x) * (y * y) = ide`, then `monoid {p,p}` proves the goal.
Finally, if we need to replace only one occurrence of the LHS of a hypothesis, then the number before the hypothesis indicates the position of the LHS that should be replaced.
For example, if `p : x = ide` and the goal is `x * y * x * y = x * y`, then we can eliminate only one `x` as follows:
* In `monoid { 1 p } {?}`, the subgoal is `y * (x * y) = x * y`.
* In `monoid { 2 p } {?}`, the subgoal is `x * (y * y) = x * y`.
* In `monoid { 3 p } {?}`, the subgoal is `x * (y * (x * y)) = y`.
-}
\meta monoid => _ (MonoidSolverModel, Monoid, Pointed.ide, Semigroup.*, SubstSolverModel.apply-axiom, List.::, List.nil,
MonoidSolverModel.Term.var, MonoidSolverModel.Term.:ide, MonoidSolverModel.Term.:*, SolverModel.terms-equality,
SolverModel.terms-equality-conv, inv, *>, BaseSet.E)
-- | The additive version of {equation.monoid}
\meta addMonoid => _ (AddMonoidSolverModel, AddMonoid, AddPointed.zro, AddMonoid.+, SubstSolverModel.apply-axiom, List.::, List.nil,
MonoidSolverModel.Term.var, MonoidSolverModel.Term.:ide, MonoidSolverModel.Term.:*, SolverModel.terms-equality,
SolverModel.terms-equality-conv, inv, *>, BaseSet.E)
{- |
The commutative monoid solver solves goals of the form `e1 = {M} e2` for some commutative monoid `M`.
If `e1` and `e2` represent the same word in the language of commutative monoids, then the solver proves the equality immediately without any additional arguments.
For example, {cMonoid} proves the following equality: `(w * (ide * x)) * ((ide * y) * z) = x * ((y * (z * ide)) * w)`.
If the words represented by `e1` and `e2` are not the same, then {cMonoid} puts them in a canonical form and expects an argument that proves the equality of these normal forms.
For example, if the goal is `(w * (ide * x)) * ((ide * x) * z) = x * ((y * (z * ide)) * w)`, then the subgoal in `cMonoid {?}` is `w * (x * (x * z)) = w * (x * (z * y))`.
Conversely, if we have an expression of the type `e1 = {M} e2`, then we can transform it into a proof of the equality of canonical forms.
For example, if `(p : (w * (ide * x)) * ((ide * x) * z) = x * ((y * (z * ide)) * w))`, then `cMonoid in p` has type `w * (x * (x * z)) = w * (x * (z * y))`.
The commutative monoid solver can also apply hypotheses to solve goals.
A hypothesis `h` is an expression of type `l = {M} r`.
Given such a hypothesis, `cMonoid {h}` replaces a single occurrence of `l` with `r` in both `e1` and `e2`.
For example, if `p : x = ide` and the goal is `(y * x) * (y * x)`, then the subgoal in `cMonoid {p} {?}` is `y * (y * x) = y`.
Several hypotheses are applied sequentially.
So, for example, if `p : x1 * y2 = y1 * x2`, `q : y1 * z2 = z1 * y2`, and the goal is `x1 * z2 * y2 = z1 * x2 * y2`, then `cMonoid {p,q}` proves the goal.
If we need to replace several occurrences of the LHS of a hypothesis, then the number before the hypothesis indicates the number of occurrences of the LHS that should be replaced.
A positive number indicates occurrences in `e1` and a negative number in `e2`.
* If `p : x = y`, `q : y * y = x`, and the goal is `x * x * x * x = x`, then `cMonoid { 4 p, 2 q, 2 p, q }` proves the goal.
* If `p : x * x = y`, `q : x * x * y = y`, and the goal is `x * x * y = x * x`, then `cMonoid { -1 p, q }` proves the goal.
-}
\meta cMonoid => _ (CMonoidSolverModel, CMonoid, Pointed.ide, Semigroup.*, CMonoidSolverModel.apply-axiom, List.::, List.nil,
MonoidSolverModel.Term.var, MonoidSolverModel.Term.:ide, MonoidSolverModel.Term.:*, SolverModel.terms-equality,
SolverModel.terms-equality-conv, inv, *>, BaseSet.E)
-- | The additive version of {equation.cMonoid}
\meta abMonoid => _ (AbMonoidSolverModel, AbMonoid, AddPointed.zro, AddMonoid.+, AbMonoidSolverModel.apply-axiom, List.::, List.nil,
MonoidSolverModel.Term.var, MonoidSolverModel.Term.:ide, MonoidSolverModel.Term.:*, SolverModel.terms-equality,
SolverModel.terms-equality-conv, inv, *>, BaseSet.E)
-- | TODO
\meta cMonoidAuto => _ (CMonoidSolverModel, CMonoid, Pointed.ide, Semigroup.*, CMonoidSolverModel.apply-axiom, List.::, List.nil,
MonoidSolverModel.Term.var, MonoidSolverModel.Term.:ide, MonoidSolverModel.Term.:*, SolverModel.terms-equality,
SolverModel.terms-equality-conv, inv, *>, BaseSet.E)
{- |
The group solver solves goals of the form `e1 = {G} e2` for some group `G`.
If `e1` and `e2` represent the same word in the language of groups, then the solver proves the equality immediately without any additional arguments.
For example, {group} proves the following equality: `(x * (z * inverse y)) * ((ide * y) * (ide * inverse z)) * w = x * ((ide * (y * ide)) * inverse y) * w`.
If the words represented by `e1` and `e2` are not the same, then {group} puts them in a canonical form and expects an argument that proves the equality of these normal forms.
For example, if the goal is `(x * (z * inverse y)) * ((ide * y) * (ide * inverse z)) * x = x * ((ide * (y * ide)) * inverse y) * inverse x`, then the subgoal in `group {?}` is `x * x = ide`.
Conversely, if we have an expression of the type `e1 = {G} e2`, then we can transform it into a proof of the equality of canonical forms.
For example, if `(p : (x * (z * inverse y)) * ((ide * y) * (ide * inverse z)) * x = x * ((ide * (y * ide)) * inverse y) * inverse x)`, then `group in p` has type `x * x = ide`.
-}
\meta group => _ (Group, Pointed.ide, Semigroup.*, Group.inverse, GroupSolverModel, SolverModel.terms-equality, SolverModel.terms-equality-conv,
GroupSolverModel.Term.var, GroupSolverModel.Term.:ide, GroupSolverModel.Term.:*, GroupSolverModel.Term.:inverse, inv, *>,
BaseSet.E)
-- | The additive version of {equation.group}
\meta addGroup => _ (AddGroup, AddPointed.zro, AddMonoid.+, AddGroup.negative, AddGroupSolverModel, SolverModel.terms-equality,
SolverModel.terms-equality-conv, GroupSolverModel.Term.var, GroupSolverModel.Term.:ide, GroupSolverModel.Term.:*,
GroupSolverModel.Term.:inverse, inv, *>, BaseSet.E)
{- |
The commutative group solver solves goals of the form `e1 = {G} e2` for some commutative group `G`.
If `e1` and `e2` represent the same word in the language of commutative groups, then the solver proves the equality immediately without any additional arguments.
For example, {cGroup} proves the following equality: `(x * (z * inverse y)) * ((ide * w) * (ide * inverse z)) * y = y * ((ide * (x * ide)) * inverse y) * w`.
If the words represented by `e1` and `e2` are not the same, then {cGroup} puts them in a canonical form and expects an argument that proves the equality of these normal forms.
For example, if the goal is `(x * (z * inverse y)) * ((ide * w) * (ide * inverse z)) * y * x = y * ((ide * (x * ide)) * inverse y) * inverse x`, then the subgoal in `cGroup {?}` is `x * (x * w) = ide`.
Conversely, if we have an expression of the type `e1 = {G} e2`, then we can transform it into a proof of the equality of canonical forms.
For example, if `(p : (x * (z * inverse y)) * ((ide * w) * (ide * inverse z)) * y * x = y * ((ide * (x * ide)) * inverse y) * inverse x)`, then `cGroup in p` has type `x * (x * w) = ide`.
The commutative group solver can also apply hypotheses to solve goals.
A hypothesis `h` is an expression of type `l = {G} r`.
Given such a hypothesis, `cGroup {h}` multiplies the goal by `inverse l * r`.
For example, if `p : y * x = ide` and the goal is `x * z = z * inverse y * w`, then {cGroup} simplifies the goal to `x * (y * inverse w) = ide` and the subgoal in `cGroup {p} {?}` is `inverse w = ide`.
If a hypothesis begins with a (positive or negative) number, then the solver raises it to the indicated power.
For example, if `p : z * z = inverse z * inverse y`, `q : x * z * z = ide`, and the goal is `x * inverse y * x = y * inverse x`, then `cGroup { 3 q, -2 p }` proves the goal.
-}
\meta cGroup => _ (CGroup, Pointed.ide, Semigroup.*, Group.inverse, CGroupSolverModel, CGroupSolverModel.terms-equality,
CGroupSolverModel.terms-equality-conv, CGroupSolverModel.apply-axioms, GroupSolverModel.Term.var,
GroupSolverModel.Term.:ide, GroupSolverModel.Term.:*, GroupSolverModel.Term.:inverse, inv, *>, BaseSet.E)
-- | The additive version of {equation.cGroup}
\meta abGroup => _ (AbGroup, AddPointed.zro, AddMonoid.+, AddGroup.negative, AbGroupSolverModel, AbGroupSolverModel.terms-equality,
AbGroupSolverModel.terms-equality-conv, AbGroupSolverModel.apply-axioms, GroupSolverModel.Term.var,
GroupSolverModel.Term.:ide, GroupSolverModel.Term.:*, GroupSolverModel.Term.:inverse, inv, *>, BaseSet.E)
{- |
The semiring solver solves goals of the form `e1 = {R} e2` for some semiring `R`.
If `e1` and `e2` represent the same word in the language of semirings, then the solver proves the equality immediately without any additional arguments.
For example, {semiring} proves the following equality: `(a + b) * (a + b) = a * a + a * b + b * a + b * b`.
If the words represented by `e1` and `e2` are not the same, then {semiring} puts them in a canonical form and expects an argument that proves the equality of these normal forms.
For example, if the goal is `a * (b + c) + a * b = 0`, then the subgoal in `semiring {?}` is `2 * (a * b) + a * c = 0`.
Conversely, if we have an expression of the type `e1 = {R} e2`, then we can transform it into a proof of the equality of canonical forms.
For example, if `(p : a * (b + c) + a * b = 0)`, then `semiring in p` has type `2 * (a * b) + a * c = 0`.
The semiring solver can also apply hypotheses to solve goals.
A hypothesis `h` is an expression of type `l = {R} r`.
Given such a hypothesis, `semiring {h}` replaces a single occurrence of `l` with `r` in both `e1` and `e2`.
Several hypotheses are applied sequentially.
For example, if `p : b * c = 0`, `q : a * d = 1`, and the goal is `(a + b) * (c + d) = a * c + b * d + 1`, then `semiring {p,q} {?}` proves the goal.
A (positive or negative) number before a hypothesis indicates the multiplicative factor applied to it.
If the number is positive, the hypothesis is applied to `e1`; otherwise it is applied to `e2`.
For example, if `p : 0 = a`, and the goal is `b = 0`, then
* In `semiring { p } {?}`, the subgoal is `b + a = a`.
* In `semiring { 1 p } {?}`, the subgoal is `b + a = 0`.
* In `semiring { -1 p } {?}`, the subgoal is `b = a`.
* In `semiring { 2 p } {?}`, the subgoal is `b + 2 * a = 0`.
* In `semiring { -2 p } {?}`, the subgoal is `b = 2 * a`.
-}
\meta semiring => _ (Semiring, SemiringSolverModel, SemiringSolverModel.apply-axiom, SolverModel.terms-equality, SolverModel.terms-equality-conv,
SemiringSolverModel.Term.:zro, SemiringSolverModel.Term.:ide, SemiringSolverModel.Term.:+, SemiringSolverModel.Term.:*,
SemiringSolverModel.Term.coef, SemiringSolverModel.Term.var, AddPointed.zro, Pointed.ide, AddMonoid.+, Semigroup.*,
Semiring.natCoef, List.::, List.nil, inv, *>, BaseSet.E)
{- |
The commutative semiring solver solves goals of the form `e1 = {R} e2` for some commutative semiring `R`.
If `e1` and `e2` represent the same word in the language of commutative semirings, then the solver proves the equality immediately without any additional arguments.
For example, {cSemiring} proves the following equality: `(a + b) * (a + b) = a * a + 2 * a * b + b * b`.
If the words represented by `e1` and `e2` are not the same, then {cSemiring} puts them in a canonical form and expects an argument that proves the equality of these normal forms.
For example, if the goal is `(a + 0) * (1 + b) = b * a`, then the subgoal in `cSemiring {?}` is `a + a * b = a * b`.
Conversely, if we have an expression of the type `e1 = {R} e2`, then we can transform it into a proof of the equality of canonical forms.
For example, if `(p : (a + 0) * (1 + b) = b * a)`, then `cSemiring in p` has type `a + a * b = a * b`.
The commutative semiring solver can also apply hypotheses to solve goals.
A hypothesis `h` is an expression of type `l = {R} r`.
Given such a hypothesis, `cSemiring {h}` replaces all occurrences of `l` with `r` in both `e1` and `e2`.
For example, if `p : a * b = 0`, `q : a * a = b * b`, and the goal is `(a + b) * (a + b) = 0`, then the subgoal in `cSemiring {p,q} {?}` is `2 * (b * b) = 0`.
A (positive or negative) number before a hypothesis indicates the multiplicative factor applied to it.
If the number is positive, the hypothesis is applied to `e1`; otherwise it is applied to `e2`.
For example, if `p : a = 0`, and the goal is `a + b = c + a`, then
* In `cSemiring { p } {?}`, the subgoal is `b = c`.
* In `semiring { 1 p } {?}`, the subgoal is `b = a + c`.
* In `semiring { -1 p } {?}`, the subgoal is `a + b = c`.
-}
\meta cSemiring => _ (CSemiring, CSemiringSolverModel, CSemiringSolverModel.apply-axiom, SolverModel.terms-equality,
SolverModel.terms-equality-conv, SemiringSolverModel.Term.:zro, SemiringSolverModel.Term.:ide, SemiringSolverModel.Term.:+,
SemiringSolverModel.Term.:*, SemiringSolverModel.Term.coef, SemiringSolverModel.Term.var, AddPointed.zro, Pointed.ide,
AddMonoid.+, Semigroup.*, Semiring.natCoef, List.::, List.nil, inv, *>, BaseSet.E)
{- |
The ring solver solves goals of the form `e1 = {R} e2` for some ring `R`.
If `e1` and `e2` represent the same word in the language of rings, then the solver proves the equality immediately without any additional arguments.
For example, {ring} proves the following equality: `(a + b) * (a - b) = a * a - a * b + b * a - b * b`.
If the words represented by `e1` and `e2` are not the same, then {ring} puts them in a canonical form and expects an argument that proves the equality of these normal forms.
For example, if the goal is `(a + b) * (a - b) = a * a - b * b`, then the subgoal in `ring {?}` is `negative (a * b) + b * a = 0`.
Conversely, if we have an expression of the type `e1 = {R} e2`, then we can transform it into a proof of the equality of canonical forms.
For example, if `(p : (a + b) * (a - b) = a * a - b * b)`, then `ring in p` has type `negative (a * b) + b * a = 0`.
The ring solver can also apply hypotheses to solve goals.
A hypothesis `h` is an expression of type `l = {R} r`.
Given such a hypothesis, `ring {h}` adds `r - l` to the goal.
For example, if `p : b * a = a * b` and the goal is `(a + b) * (a - b) = a * a - b * b`, then {ring} simplifies the goal to `negative (a * b) + b * a` and `ring {p}` proves the goal.
If a hypothesis begins with a (positive or negative) number, then the solver multiplies it by the indicated factor.
For example, if `p : b * a = a * b` and the goal is `(a + b) * (a - b) = a * a - b * b`, then `ring { -1 p }` proves the goal.
Several hypotheses can be applied at the same time.
For example, if `p : a * a = 0`, `q : b * b = 0`, and the goal is `(a + b) * (a - b) = b * a - a * b`, then `ring { p, -1 q }` proves the goal.
-}
\meta ring => _ (Ring, RingSolverModel, RingSolverModel.apply-axioms, RingSolverModel.terms-equality, RingSolverModel.terms-equality-conv,
AddGroup.negative, RingSolverModel.Term.:zro, RingSolverModel.Term.:ide, RingSolverModel.Term.:+, RingSolverModel.Term.:*,
RingSolverModel.Term.:negative, RingSolverModel.Term.coef, RingSolverModel.Term.var, AddPointed.zro, Pointed.ide,
AddMonoid.+, Semigroup.*, Semiring.natCoef, List.::, List.nil, inv, *>, BaseSet.E)
{- |
The commutative ring solver solves goals of the form `e1 = {R} e2` for some commutative ring `R`.
If `e1` and `e2` represent the same word in the language of commutative rings, then the solver proves the equality immediately without any additional arguments.
For example, {cRing} proves the following equality: `(a + b) * (a - b) = a * a - b * b`.
If the words represented by `e1` and `e2` are not the same, then {cRing} puts them in a canonical form and expects an argument that proves the equality of these normal forms.
For example, if the goal is `(a - b) * (a - b) = b * b`, then the subgoal in `cRing {?}` is `a * a - 2 * (a * b) = 0`.
Conversely, if we have an expression of the type `e1 = {R} e2`, then we can transform it into a proof of the equality of canonical forms.
For example, if `(p : (a - b) * (a - b) = b * b)`, then `cRing in p` has type `a * a - 2 * (a * b) = 0`.
The commutative ring solver can also apply hypotheses to solve goals.
A hypothesis `h` is an expression of type `l = {R} r`.
Given such a hypothesis, `cRing {h}` finds the largest word `w` such that `l * w` occurs in `e1 - e2` and replaces that subword with `r * w`.
For example, if `p : a * b = 0` and the goal is `(a + b) * (a + b) = a * a + b * b`, then `cRing {p}` proves the goal.
If a hypothesis begins with a (positive or negative) number, then the solver multiplies it by the indicated factor instead of the largest word `w`.
For example, if `p : a = b` and the goal is `a * c = 0`, then the subgoal in `cRing {?}` is `c * b = 0`, but the subgoal in `cRing { -1 p } {?}` is `a + (a * c - b) = 0`.
Several hypotheses are applied sequentially.
For example, if `p : a = b`, `q : b * c = 0`, and the goal is `a * c = 0`, then `cRing {p,q}` proves the goal.
-}
\meta cRing => _ (CRing, CRingSolverModel, CRingSolverModel.terms-equality, CRingSolverModel.terms-equality-conv,
CRingSolverModel.apply-axioms, AddGroup.negative, RingSolverModel.Term.:zro, RingSolverModel.Term.:ide,
RingSolverModel.Term.:+, RingSolverModel.Term.:*, RingSolverModel.Term.:negative, RingSolverModel.Term.coef,
RingSolverModel.Term.var, AddPointed.zro, Pointed.ide, AddMonoid.+, Semigroup.*, Semiring.natCoef, List.::, List.nil, inv, *>,
BaseSet.E)
-- | TODO
\meta cRingAuto => _ (AddGroup.negative, RingSolverModel.Term.:zro, RingSolverModel.Term.:ide, RingSolverModel.Term.:+,
RingSolverModel.Term.:negative, RingSolverModel.Term.:*, RingSolverModel.Term.coef, RingSolverModel.Term.var, CRing,
CRingSolverModel, CRingSolverModel.terms-equality, CRingSolverModel.terms-equality-conv, CRingSolverModel.apply-axioms,
AddPointed.zro, Pointed.ide, AddMonoid.+, Semigroup.*, Semiring.natCoef, List.::, List.nil, inv, *>, BaseSet.E)
{- |
The Boolean ring solver solves goals of the form `e1 = {B} e2` for some Boolean ring `B`.
If `e1` and `e2` represent the same word in the language of Boolean rings, then the solver proves the equality immediately without any additional arguments.
For example, {bRing} proves the following equality: `(a + b) * (a * b) = 0`.
If the words represented by `e1` and `e2` are not the same, then {cRing} puts them in a canonical form and expects an argument that proves the equality of these normal forms.
For example, if the goal is `(a - b) * (a ∨ b) = 0`, then the subgoal in `bRing {?}` is `a + b = 0`.
Conversely, if we have an expression of the type `e1 = {B} e2`, then we can transform it into a proof of the equality of canonical forms.
For example, if `(p : (a - b) * (a ∨ b) = 0)`, then `bRing in p` has type `a + b = 0`.
The Boolean ring solver can also apply hypotheses to solve goals.
A hypothesis `h` is an expression of type `l = {B} r`.
Given such a hypothesis, `bRing {h}` finds the largest word `w` such that `l * w` occurs in `e1 + e2` and replaces that subword with `r * w`.
For example, if `p : a + b = c` and the goal is `a * b + b = b * c`, then `bRing {p}` takes `w = b` and proves the goal.
If a hypothesis begins with a number, then the solver takes `w = 1`.
In other words, it just adds `l + r` to the equation `e1 + e2 = 0`, turning it into `e1 + e2 + l + r = 0`.
For example, if `p : a = a * b` and the goal is `a * b = 0`, then `bRing {?}` doesn't change the goal, but the subgoal in `bRing {1 p} {?}` is `a = 0`.
Several hypotheses are applied sequentially.
For example, if `p : a = b + c`, `q : b + b * c = c`, and the goal is `a * b = c`, then `bRing {p,q}` proves the goal.
-}
\meta bRing => _ (BooleanRing, AddPointed.zro, AddMonoid.+, Semigroup.*, AddGroup.negative, BooleanRingSolverModel.Term.:zro,
BooleanRingSolverModel.Term.:+, BooleanRingSolverModel.Term.:*, BooleanRingSolverModel.Term.:negative,
BooleanRingSolverModel.Term.var, BooleanRingSolverModel, BooleanRingSolverModel.terms-equality,
BooleanRingSolverModel.terms-equality-conv, BooleanRingSolverModel.apply-axioms, List.::, List.nil, true, false, inv, *>,
BaseSet.E)
}
-- | Solve systems of linear equations
\meta linarith => _ (Bool, Bool.true, zero<=_, pos<=pos, pos<pos, fromInt_<=, fromInt_<, Rat.fromInt, =_<=, OrderedAAlgebra.coef_<,
OrderedAAlgebra.coef_<=, LinearlyOrderedSemiring, OrderedRing, OrderedAddGroup.<, LinearOrder.<=, Preorder.<=, StrictPoset.<,
LinearRatAlgebraData, LinearRatData, LinearSemiringData, LinearRingData, LinearData.solveContrProblem,
LinearData.solve<=Problem, LinearData.solve<Problem, LinearData.solve=Problem, Operation.Less, Operation.LessOrEquals,
Operation.Equals, pmap, inv, NatSemiring, IntRing, BottomJoinSemilattice.bottom, TopMeetSemilattice.top, JoinSemilattice.join,
MeetSemilattice.meet, AddMonoid.+, Semigroup.*, Semiring.natCoef, AddGroup.negative, AAlgebra.coefMap, Pointed.ide,
AddPointed.zro, RingTerm.var, RingTerm.coef, RingTerm.:ide, RingTerm.:zro, RingTerm.:negative, RingTerm.:*, RingTerm.:+,
BaseData.R, MonoidData.vars)
-- | Proves an equality by congruence closure of equalities in the context. E.g. derives f a = g b from f = g and a = b
\meta cong => _ (inv, *>)
-- | Simplifies the expected type or the type of the argument if the expected type is unknown.
\meta simplify => _ (transport, *>, inv, Monoid, AddMonoid, Semiring, Ring, Group, CGroup, AddGroup, AbGroup, BaseSet.E, AddGroup.negative, Group.inverse,
Semigroup.*, AddMonoid.+, Pointed.ide, AddPointed.zro, AddGroup.negative-isInv, Group.inverse-isInv, Group.inverse_*,
AddGroup.negative_+, Ring.negative_*-left, Ring.negative_*-right, PseudoSemiring.zro_*-right, PseudoSemiring.zro_*-left,
AddMonoid.zro-left, AddMonoid.zro-right, Monoid.ide-left, Monoid.ide-right, AddGroup.toGroup, AbGroup.toCGroup,
AddGroup.negative_zro, Group.inverse_ide, NatData, CGroupData, GroupTerm.var, GroupTerm.:ide, GroupTerm.:*, GroupTerm.:inv,
CGroupData.simplify-correct, NatData.simplify-correct)
{- |
`rewriteEq (p : a = b) t : T` is similar to {rewrite}, but it finds and replaces occurrences of `a` up to algebraic equivalences.
For example, `rewriteEq (p : b * (c * id) = x) t : T` rewrites `(a * b) * (id * c)` as `a * x` in `T`.
Similarly to `rewrite` this meta allows specification of occurrence numbers.
Currently this meta supports noncommutative monoids and categories.
-}
\meta rewriteEq => _ (transport, transportInv, BaseSet.E, *>, Precat.Hom, Precat.o, Precat.id, AddMonoid.zro-right, PseudoSemiring.zro_*-right,
TopMeetSemilattice, BoundedDistributiveLattice, AddGroup.fromZero, AddGroup.toZero, List.nil, List.::, Monoid, CMonoid,
AddMonoid, AbMonoid, Ring, Semiring, Monoid.LDiv, Monoid.RDiv, AlgData.terms-equality, CAlgData.terms-equality,
CRingData.terms-equality, LatticeData.terms-equality, AlgData.interpret, gensZeroToIdealZero, LatticeData, CRingData,
RingData, CSemiringData, SemiringData, LatticeData.L, HData, MonoidData, CMonoidData, LData, LData.L, MonoidData.interpretNF,
MonoidData.interpretNF_++, MonoidData.normalize-consistent, MonoidData.terms-equality-conv, LData.terms-equality,
CMonoidData.terms-equality, MonoidData.terms-equality, CMonoidData.terms-equality-conv, CMonoidData.sort-consistent,
CMonoidData.replace-consistent, MonoidData.replace-consistent, MonoidTerm.var, MonoidTerm.:ide, MonoidTerm.:*,
HData.interpretNF, HData.interpretNF_++, HData.normalize-consistent, HData.terms-equality, CatTerm.var, CatTerm.:id,
CatTerm.:o, CatNF.:nil, CatNF.:cons, HData.H, HData.V, pmap, inv, NatSemiring, IntRing, BottomJoinSemilattice.bottom,
TopMeetSemilattice.top, JoinSemilattice.join, MeetSemilattice.meet, AddMonoid.+, Semigroup.*, Semiring.natCoef,
AddGroup.negative, AAlgebra.coefMap, Pointed.ide, AddPointed.zro, RingTerm.var, RingTerm.coef, RingTerm.:ide, RingTerm.:zro,
RingTerm.:negative, RingTerm.:*, RingTerm.:+, BaseData.R, MonoidData.vars)