Automation For Rocq

Tactics Manipulate Proof Terms

• Transform proof state by manipulating proof terms with holes.

• Simple tactics (e.g., intros) are straightforward.

• Powerful tactics (e.g., ring, lia, auto) use automated reasoning.

Automated Theorem Proving Strategies

• Identify decidable fragment and create decision procedure.

• Embrace undecidability for heuristic proof search.

• First approach guarantees validity; second is heuristic.

Decidable Fragment Definition

• Restricted language for which validity is decidable.
• Always terminates with yes/no.
• Examples: propositional logic, linear arithmetic, arrays.

Equality and Uninterpreted Functions (EUF)

• Decidable fragment with equations and no quantifiers.
• Functions treated as uninterpreted symbols.
• Solved by congruence closure algorithm.

Congruence Closure Algorithm

• Assign each term to a congruence class.
• Merge classes for equal terms and propagate merges.
• Achieves closure properties plus function congruence.

SMT Solvers

• Satisfiability Modulo Theories (e.g., Z3, cvc5).
• Implement decision procedures for many decidable fragments.
• Combine theories: linear arithmetic, arrays, bitvectors.

Undecidable Problem Approach

• Use heuristic proof search if outside decidable fragment.
• Techniques include backward and forward chaining.
• No guarantees of termination or completeness.

Backward Chaining

• Start from goal and work backwards to premises.
• Uses inference rules in reverse.
• Employed by auto tactic and Prolog.

Forward Chaining

• Start from premises and derive consequences.
• Works forward until the goal is reached.
• Complements backward chaining.

auto Tactic

• Rocq tactic using backward chaining with hints.
• Applies lemmas automatically to goals.
• Partial automation for undecidable problems.

lia Tactic

• Decision procedure for linear integer arithmetic.
• Decidable fragment: linear equations/inequalities.
• Utilizes Fourier-Motzkin elimination.

ring Tactic

• Proves equalities in ring structures (+, *, 0, 1).
• Uses canonical forms for decision procedure.
• Focus on polynomial equations.

congruence Tactic

• Implements congruence closure for EUF fragment.
• Proves equalities with uninterpreted functions.
• Uses graph merging algorithms.