Work-in-Progress: A Tactic for Pattern Matching in Autosubst

Technical Summary: A Tactic for Pattern Matching in Autosubst

Problem Statement
The paper addresses a specific limitation in the Autosubst framework, a code generator for the Rocq (formerly Coq) proof assistant that automates reasoning about de Bruijn terms and substitution via the $\sigma$-calculus. While Autosubst successfully automates equality checking for assumption-free goals using the asimpl tactic, it fails when users attempt to apply assumptions (e.g., typing rules or lemmas) to a goal via standard tactics like apply or eapply.

In these scenarios, the user must unify a goal with an assumption modulo $\sigma$-equivalence. However, Autosubst's automation is not designed for matching against assumptions. Consequently, users are forced to employ cumbersome workarounds, such as:

• Formulating rules in indirect forms (using fresh meta-variables instead of direct substitution terms).
• Introducing auxiliary lemmas to bridge the gap between the goal and the assumption.
• Manually transforming goals or explicitly instantiating existential variables during proofs.

The core difficulty lies in the fact that $\sigma$-matching (matching up to $\sigma$-equivalence) is not unique; a single matching problem may admit multiple solutions, not all of which satisfy the context's premises. Furthermore, second-order matching for the full $\lambda\sigma$-calculus is undecidable, and even without $\beta$-reduction, solutions are not necessarily unique.

Methodology
The authors propose a work-in-progress heuristic tactic named as_apply, implemented in Rocq's Ltac language, to automate pattern matching modulo $\sigma$-equivalence. The tactic operates in two primary phases:

1. Preprocessing:

   • Both the goal and the conclusion of the target assumption are normalized with respect to the $\sigma$-calculus using the existing asimpl tactic.
   • Quantified variables in the assumption are replaced with existential variables (evars).
   • The premises of the assumption are converted into subgoals to be solved after the matching phase.
   • The tactic handles conversions between explicit renaming operations (e.g., $s\langle\xi\rangle$) and instantiation operations ($s[\xi]$) using substify and renamify.

2. Matching Phase:

   • The tactic constructs a set of matching equations $M = \{s_i =_\sigma t_i\}$ between the goal terms and the instantiated assumption terms.
   • It processes equations from left to right using a partial procedure, $\sigma_{min}$, which attempts to match modulo the $\sigma_{min}$ fragment (a subset of $\sigma$-rules characterizing instantiation and compositionality).
   • Heuristics: If $\sigma_{min}$ fails to find a match, the tactic applies a set of heuristics capturing common patterns in formal developments. These include:
     • Handling equations of the form $s[t \cdot \sigma] =_\sigma ?s[t \cdot id]$ by instantiating the unknown with a lifted substitution ($?s \mapsto s[\Uparrow\sigma]$).
     • Handling cases involving identity substitutions or specific variable structures.
   • After applying substitutions, the tactic re-normalizes the assumption. Success is determined if the goal and the assumption become syntactically equal.

The tactic has been generalized to support the full input language of the Autosubst compiler, including multiple mutually inductive sorts, vector substitutions, and first-class renamings.

Key Contributions

1. Introduction of as_apply: A heuristic tactic designed to replace apply/eapply in Autosubst-based developments, enabling matching modulo $\sigma$-equivalence in the presence of assumptions.
2. Generalization: Extension of the matching logic to cover the full syntax supported by Autosubst, including complex binders and renaming operations.
3. Empirical Evaluation: Application of the tactic to standard benchmarks, specifically the POPLMark and POPLMark Reloaded challenges.

Results
The authors evaluated as_apply on the POPLMark (642 lines) and POPLMark Reloaded (683 lines) challenge solutions.

• Frequency of Use: The tactic was used 15 times in the POPLMark B solution and 10 times in the POPLMark Reloaded solution.
• Effectiveness: In all tested cases, as_apply successfully solved the intended goals.
• Simplification: The use of the tactic eliminated the need for the indirect rule formulations, auxiliary lemmas, and manual goal transformations that characterized previous solutions.
• Limitations: The authors acknowledge that as_apply is not $\sigma$-complete and is not a decider. Because $\sigma$-matching can have multiple solutions, the heuristic nature of the tactic means it could theoretically select an incorrect solution when a correct one exists, though no such failures were observed in the case studies.

Significance and Claims
The paper claims that while the theoretical problem of $\sigma$-matching is inherently difficult (non-unique solutions, undecidability in full $\lambda\sigma$), a pragmatic, heuristic approach can recover a high level of automation in practice. The significance lies in reducing the manual burden on users working with de Bruijn syntax, allowing them to state typing rules and lemmas in their direct, natural forms rather than in indirect forms tailored to the limitations of the proof assistant's unification engine.

The authors remain modest about the current state of the work, labeling it "Work-in-Progress." They note that the current tactic relies on heuristics due to the potential for infinite or multiple solutions. Future work aims to identify the largest fragment $\sigma'$ for which a uniqueness criterion holds, potentially leading to a matching tactic with proven guarantees.