Proving Addition Commutativity in Coq

Overview

This skill provides guidance for completing induction proofs in Coq, particularly proofs involving arithmetic properties like addition commutativity (n + m = m + n). It covers the workflow for understanding incomplete proofs, identifying required lemmas, and verifying correctness through compilation.

Workflow for Completing Coq Proofs

Step 1: Understand the Proof Structure

Before making any edits, read and understand the existing proof file:

1. Identify the theorem statement and what needs to be proved
2. Locate incomplete cases marked with admit, Admitted, or placeholder tactics
3. Understand the induction structure (base case vs inductive case)
4. Note which libraries are imported (e.g., Require Import Arith)

Step 2: Analyze Each Case