I was trying to prove that the sum of the first n natural numbers is n*(n+1)/2 and in between thought having this lemma would help:

```
Lemma helper: forall n:nat,
(S n) * (S n) = n*n + 2*n + 1.
Proof.
intros n.
induction n.
- reflexivity.
- rewrite IHn.
lia.
Qed.
```

Using `lia`

resolved the whole thing.

Any idea how a more 'manual' proof can turn out?

Before `lia`

, the goal was:

```
n : nat
IHn : S n * S n = n * n + 2 * n + 1
========================= (1 / 1)
S (S n) * S (S n) = n * n + 2 * n + 1 + 2 * S n + 1
```

As in:

```
Goal
forall n:nat,
S n * S n = n * n + 2 * n + 1.
```

How can we solve this without `lia`

?

Natural numbers aren't rings, but under what circumstances can we use the `ring`

tactic?

Because it had worked for:

```
Require Import Arith.
Goal forall a b:nat,
(a+b)*(a+b) = (a*a)+2*a*b+(b*b).
Proof.
intros.
ring.
Qed.
```

Regarding not using `lia`

or `ring`

, you can prove the property by sufficiently many applications of a few rewriting rules like `plus_assoc`

and `plus_comm`

.

`ring`

works for semirings as well: https://coq.inria.fr/refman/addendum/ring.html

Too many such rewrites for us to write them manually?

The proof term made with `lia`

looked quite big with many `Z`

(as in integer) functions coming in.

And which rewrite rule can I use to break up `S (S n) * S (S n)`

?

`simpl`

(In other words, you do not need a rewriting rule. It is by definition.)

Thanks. How can we make `simpl`

affect only the LHS?

(I tried using `Nat.add_1_r`

instead of `simpl`

earlier so that RHS would remain untouched... :sweat_smile: )

Stupid option: `rewrite (ltac:(reflexivity) : S (S n) * S (S n) = S (S n) + S n * S (S n))`

. I hope there's a better option.

The SSReflect plugin provides a pattern language to select a subterm (e.g., to simplify or to rewrite). `rewrite [LHS]/=`

would do `simpl`

only for the LHS. This `LHS`

is the notation defined here: https://github.com/coq/coq/blob/master/theories/ssrmatching/ssrmatching.v#L32

you generally shouldn't need to simpl before reflexivity

```
Require Import Arith.
Lemma helper: forall n:nat,
(S n) * (S n) = n*n + 2*n + 1.
Proof.
intros n.
induction n.
- reflexivity.
- rewrite IHn.
simpl.
rewrite <-!plus_n_Sm.
rewrite <-!plus_n_O.
simpl.
do 4 apply f_equal with (f := S).
rewrite Nat.add_assoc, Nat.add_comm.
apply f_equal2 with (f := Nat.add); auto.
rewrite !Nat.mul_succ_r.
now rewrite Nat.add_assoc.
Qed.
```

I would expect the proof to be much simpler if you do it directly rather than going through an induction.

```
Require Import Arith.
Lemma helper: forall n:nat,
(S n) * (S n) = n*n + 2*n + 1.
Proof.
intros n.
simpl.
rewrite <- plus_n_Sm.
rewrite <-!plus_n_O.
rewrite plus_comm.
rewrite Nat.mul_succ_r.
now rewrite Nat.add_assoc.
Qed.
```

Last updated: Jun 25 2024 at 15:02 UTC