Tactic |
Description |
Integers, Nats |
|
lia |
Solve the goal using Coq's Linear Integer Arithmetic procedure |
Reals |
|
R_field_simplify |
Simplify the goal using field axioms |
R_field |
Solve the goal using field axioms |
lra |
Solve the goal using Coq's Linear Real Arithmetic procedure |
Complex |
|
C_field_simplify |
Simplify the goal using field axioms |
C_field |
Solve the goal using field axioms |
lca |
Solve the goal using Coq's Linear Real Arithmetic procedure (indirectly) |
Matrix |
|
Msimpl |
Simplify the goal using standard matrix equalities |
by_cell |
Reduce m × n matrix equality to m∗n complex number equalities |
lma |
Solve the goal using Coq's Linear Real Arithmetic procedure (indirectly) |
Quantum Matrices |
|
qubit_simplify |
Simplify quantum expressions in Dirac notation |