2 Reflection by Inference

2.1 Representation Inference

Lean’s type-class inference is a powerful tool for automatically constructing instances of a parameterized type. Our approach to proof-by-reflection, which we will call reflection by inference, employs type-class inference to construct computable representations of target properties. First, we will briefly discuss type-class inference. Instance declarations are the blueprint for this process; each declaration states the parameter of the type it instantiates, admits any type class instances it requires as input, and specifies how to construct the target instance from these inputs. As displayed in Figure 2, type-class inference is a depth-first search which, at each step, checks all instance declarations that match the current goal. For more details on type-class inference, consult the Theorem Proving in Lean 4 handbook [ 13 ] .

Lean’s type-class inference is central to our reflection model and we will refer to it as the inference procedure. In our case, the types we will construct are of computable representations of the target properties parameterized over polynomials. We will refer to these computable representions as representations and the type classes that contain instances of them as reflection classes. As addressed in Figure 1, reflection classes are generic to the representations they contain. It follows that the inference procedure is generic to computable representations of the target properties. We will refer to instance declarations for reflection classes as inference rules. Once the reflection classes and inference rules are declared, we may implement tactics that perform the inference procedure to resolve goals. These tactics rewrite the target property as the constructed computable representation so that the goal can be resolved by last-mile automation tactics. Recall that the LeanSSR project [ 3 ] discusses last-mile automation.

2.2 Reflection Model

The reflection-by-inference model in Figure 1 guides our implementation of the system for polynomials. We ensure levels of modularity with respect to the target property and the representation of that property by specifying three levels of abstraction: The signature declares inference rules for generic reflection classes. The interface extends multiple signatures with a specified reflection class that asserts the target property. At this level, tactics may be implemented for generic representations. The implementation instantiates an interface with a specified representation of the target property and implements the rules declared in the signatures.

2.3 Sensitive Inference Procedure

Although the inference procedure is effective for target properties with inference rules that require only the simple input instances without extra conditions, it is limited for properties that require extra assumptions at each step. For example, inference for exact degrees and leading coefficients requires that leading terms do not cancel at each +, *, or ^ step. To address this issue, we implement the sensitive inference procedure which is invoked by Tactic 2.1.

open Nat

class IsDouble (n : ℕ) where
  m : ℕ
  h : n = 2 * m

instance (h : n % 2 = 0) : IsDouble n :=
  ⟨n / 2, (Nat.mul_div_cancel' (dvd_of_mod_eq_zero h)).symm⟩

example : IsDouble 4 := by infer_instance_trying <:> decide