| 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 |