prove-plus-comm

name	prove-plus-comm
description	Guidance for proving mathematical properties in Coq using induction, specifically addition commutativity and similar arithmetic lemmas. This skill should be used when working with Coq proof assistants to complete induction proofs, fill in proof cases, or apply standard library lemmas like plus_n_O and plus_n_Sm.

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

For induction proofs on natural numbers:

Base Case (n = 0):

• After simpl, determine what the goal simplifies to
• Common pattern: proving m = m + 0 requires the plus_n_O lemma
• The plus_n_O lemma states: forall n, n = n + 0

Inductive Case (n = S n'):

• Identify the inductive hypothesis (IH) available in context
• After simpl, the goal typically involves S (...) on both sides
• Common pattern: proving S (n' + m) = m + S n' requires:
  • Rewriting with the inductive hypothesis
  • Applying plus_n_Sm lemma: forall n m, S (n + m) = n + S m

Step 3: Apply Tactics

Common tactics for arithmetic proofs:

Tactic	Usage
simpl	Simplify expressions using definitions
rewrite <- lemma	Rewrite goal right-to-left using lemma
rewrite -> lemma	Rewrite goal left-to-right using lemma
rewrite IHn	Apply inductive hypothesis
reflexivity	Prove goal when both sides are identical
apply lemma	Apply a lemma directly to the goal

Step 4: Verify with Compilation

After completing the proof:

1. Compile the file with coqc filename.v
2. Successful compilation produces a .vo file
3. If compilation fails, read error messages to identify issues

Verification Strategies

Incremental Verification

Compile after each significant edit rather than completing all cases first. This prevents cascading errors and simplifies debugging.

Check Goal States

When uncertain about what a tactic produces, consider:

• Using Show to display the current goal
• Running Coq interactively with coqtop to step through proofs
• Checking goal state after simpl before applying lemmas

Library Verification

Verify lemma availability before use:

• Use Search command to find relevant lemmas: Search ((_ + 0) = _).
• Use Print to view lemma statements: Print plus_n_O.
• Confirm the Arith library is imported for standard arithmetic lemmas

Common Pitfalls

Direction of Rewriting

The <- and -> arrows in rewrite matter:

• rewrite <- plus_n_O rewrites n to n + 0
• rewrite -> plus_n_O rewrites n + 0 to n

Incorrect direction causes the tactic to fail or produce an incorrect goal.

Missing Library Imports

Standard arithmetic lemmas require Require Import Arith. Without this import, lemmas like plus_n_O and plus_n_Sm are unavailable.

Assuming Lemma Existence

Do not assume lemmas exist without verification. For non-standard proofs, explore the library using Search before relying on specific lemmas.

Coq Version Compatibility

Tactics and lemma names may differ between Coq versions. If a tactic fails unexpectedly, verify the Coq version and check documentation for version-specific syntax.

Key Lemmas for Addition Proofs

Lemma	Statement	Usage
plus_n_O	forall n, n = n + 0	Base case: 0 + m = m simplifies to m = m + 0
plus_n_Sm	forall n m, S (n + m) = n + S m	Inductive case: relates S (n' + m) to m + S n'
plus_comm	forall n m, n + m = m + n	The commutativity property itself (if already proven)
plus_assoc	forall n m p, n + (m + p) = (n + m) + p	Associativity for rearranging terms

Example Pattern: Completing Commutativity Proof

For a proof structured as:

Theorem plus_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n m.
  induction n as [| n' IHn'].
  - (* Base case: n = 0 *)
    simpl.
    (* Goal: m = m + 0 *)
    (* TODO: complete this case *)
  - (* Inductive case: n = S n' *)
    simpl.
    (* Goal: S (n' + m) = m + S n' *)
    (* IHn': n' + m = m + n' *)
    (* TODO: complete this case *)
Qed.

Base case solution:

rewrite <- plus_n_O. reflexivity.

Inductive case solution:

rewrite IHn'. rewrite plus_n_Sm. reflexivity.