How do I approach the final step in proving the cancellation law in Coq?

Question

I'm trying to prove the cancellation law for natural numbers. This is my proof so far:

Proposition add_cancellation : forall a b c : nat,
    a + b = a + c -> b = c.
Proof.
    intros a b c. induction a as [| a' IHa' ].
    - (* a = 0 *)
        simpl. symmetry. rewrite -> H. reflexivity.
    - (* a = S n' *) 
        rewrite -> add_comm, S_assoc, add_comm.
        assert (S a' + c = S (a' + c)) as H.
        {
            rewrite -> add_comm, S_assoc, add_comm. reflexivity.
        }
        rewrite -> H.

The current state of the proof is

a', b, c: nat
IHa': a' + b = a' + c -> b = c
H: S a' + c = S (a' + c)
---------------------------------
1/1
S (a' + b) = S (a' + c) -> b = c

This is largely following Terence Tao's proof for the law:

where Axiom 2.4 can be written as:

Theorem S_n_eq_S_m_if_n_eq_m : forall n m : nat,
    (S n = S m) -> n = m.

It's clear how 2.4 is supposed to apply here: S(a' + b) = S(a' + c) should simplify to a' + b = a' + c. However it doesn't, and this is where I'm getting stuck. Why can't I apply axiom 2.4 here?

Answer 1

You can prove your theorem S_n_eq_S_m_if_n_eq_m by congruence:

Theorem S_n_eq_S_m_if_n_eq_m : forall n m : nat,
    (S n = S m) -> n = m.
Proof.
  congruence.
Qed.

Another way to do it is to apply the predecessor function on both sides, and that will cancel the S out. In fact, your original cancellation problem can be shown in a similar way (first prove a + b - b = a then apply function on both sides, something like that).

I noticed that you were trying to show S n + m is S (n + m). You can do this by simpl., because that's by definition of +.

The current state of the proof is

The proof state you have shown does not seem well -- you need to show S ... = S ... implies b = c, but you've shown the premise to be true. This will not help you -- it should be part of the assumptions! So at least your direction is not going well. Using congruence can solve your problem.

Here's a completed and simplified proof:

Axiom add_comm : forall a b : nat, a + b = b + a.

Proposition add_cancellation : forall a b c : nat,
    a + b = a + c -> b = c.
Proof.
    intros a b c. induction a as [| a' IHa' ].
    - simpl. trivial.
    - simpl. intros. apply IHa'.
      congruence.
Qed.

Answer 2

Here is a proof without congruence, closer to your paper proof. What you want is probably the injection tactic, more about injection below.

(* By definition of +, forall n, m,
   - 0 + m = m
   - (S n) + m = S (n + m). *)
Proposition add_cancellation : forall a b c : nat,
    a + b = a + c -> b = c.
Proof.
    intros a b c. induction a as [| a' IHa'].
    - (* by computation, 0 + b = b and 0 + c = c*)
      simpl.
      (* assume H : b = c *)
      intros H.
      (* Then, b = c *)
      exact H.
    - (* by computation, (S a') + b = S (a' + b) and (S a') + c = S (a' + c). *)
      simpl.
      (* assume H : S (a' + b) = S (a' +  c) *)
      intros H.
      (* in coq, constructors of inductive types are injective (same as axiom
         2.4 in your paper proof) *)
      injection H as H. (* H : a' + b = a' + c *)
      (* by (IHa), to prove b = c, it suffices to prove a' + b = a' + c *)
      apply IHa'.
      (* but this is exactly H *)
      exact H.
Qed.

What makes injection possible is the fact that one can define functions by pattern matching over inductive types, such as nat here:

Definition prd (n : nat) :=
  match n with
    0 => 0 (* arbitrary *)
  | S n' => n'
  end.

Theorem prd_succ_id : forall n, prd (S n) = n.
Proof.
  intros n.
  (* By computation, prd (S n) = n *)
  simpl.
  reflexivity.
Qed.

Theorem S_n_eq_S_m_if_n_eq_m : forall n m : nat, (S n = S m) -> n = m.
Proof.
  intros n m H.
  (* replace n with prd (S n) and m with prd (S m) *)
  rewrite <-(prd_succ_id n), <-(prd_succ_id m).
  rewrite H.
  reflexivity.
Qed.
```