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

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' *)
assert (S a' + c = S (a' + c)) as H.
{
}
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?

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.


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.
$$$$
`