prove-plus-comm（证明加上通讯）

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:

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

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.