Generating laws from equations
The invariants defined in this chapter are properties of the syntax of the equations being considered. In other words, they are properties of the laws associated with the equations, rather than of the equations themselves. Proving non-implications using invariants requires a way to operate on the syntax of the equations and then translate the reasoning back to results about the original equations.
A magma law can be generated from an equation by accessing the syntax used in its definition and converting it to a declaration representing a magma law through metaprogramming. There is a choice in the variable set of the magma law – one one hand, it can be a finite set whose size matches the number of variables, and on the other hand, it can be the set of natural numbers. The advantage of the former is that one can generate proofs that the satisfiability of the magma law is equivalent to the satisfiability of the original equation (this only needs to be done for variable sets of size up to six, since that is the maximum size currently being considered in the project; it's convenient to prove individual lemmata for each variable set size establishing this equivalence). The advantage of the latter is that it bypasses the need to cast between various finite sets while constructing a model as a counter-example.
One approach is to generate both forms of the law, using the first to establish the equisatisfiability of the law and the equation and then transporting this result to the second form of the law. The conversion from the first form to the second is summarised in the lemma below.
Lemmacompatibility-between-magma-laws#
[Compatibility between magma laws over finite sets and the natural numbers] Let \(E\) be a magma law defined over \(n\) variables and let \(\tilde{E}\) be the same equation with variables ranging over the natural numbers (formally, \(\tilde{E}\) is the image of \(E\) under the canonical map from the finite set with \(n\) elements to the natural numbers). Then any magma \(M\) satisfies \(E\) if and only if it satisfies \(\tilde{E}\).
Proof
In the forward direction, suppose \(\phi : \mathbb{N} \to M\) is a substitution. Then the restriction of \(\phi\) to the first \(n\) natural numbers is a substitution for the variables of \(E\), and since \(M\) satisfies \(E\), the law \(E\) is true in \(M\) under this substitution. Since \(\tilde{E}\) is the same as \(E\) under the substitution \(\phi\), \(M\) satisfies \(\tilde{E}\).
In the reverse direction, suppose \(\phi : \{0, 2, \ldots, n-1\} \to M\) is a substitution. Then \(\phi\) can be extended to a substitution \(\tilde{\phi} : \mathbb{N} \to M\) by setting \(\tilde{\phi}(i) = \phi(i)\) for \(i \leq n\) and \(\tilde{\phi}(i) = 0\) for \(i \geq n\). Since \(M\) satisfies \(\tilde{E}\) under the substitution \(\tilde{\phi}\), it satisfies \(E\) under the restriction of \(\tilde{\phi}\) to the first \(n\) natural numbers, which is precisely \(\phi\). The special case where \(n = 0\) is in fact impossible, since there cannot be an expression with no variables.
Lean
Stated as Law.satisfies_fin_satisfies_nat; the blueprint marks no proof of it as formalized.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.