## Stream: Coq users

### Topic: Tiny proof without lia

#### Julin S (Apr 07 2023 at 15:16):

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`?

#### Julin S (Apr 07 2023 at 15:34):

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

``````Require Import Arith.

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

#### Guillaume Melquiond (Apr 07 2023 at 15:35):

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

#### Julin S (Apr 07 2023 at 15:35):

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

#### Julin S (Apr 07 2023 at 15:37):

Too many such rewrites for us to write them manually?

#### Julin S (Apr 07 2023 at 15:37):

The proof term made with `lia` looked quite big with many `Z` (as in integer) functions coming in.

#### Julin S (Apr 07 2023 at 15:40):

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

`simpl`

#### Guillaume Melquiond (Apr 07 2023 at 15:44):

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

#### Julin S (Apr 07 2023 at 15:46):

Thanks. How can we make `simpl` affect only the LHS?

#### Julin S (Apr 07 2023 at 15:49):

(I tried using `Nat.add_1_r` instead of `simpl` earlier so that RHS would remain untouched... :sweat_smile: )

#### Huỳnh Trần Khanh (Apr 07 2023 at 15:54):

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.

#### Kazuhiko Sakaguchi (Apr 07 2023 at 15:54):

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

#### Gaëtan Gilbert (Apr 07 2023 at 15:55):

you generally shouldn't need to simpl before reflexivity

#### Laurent Théry (Apr 07 2023 at 16:18):

``````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).
apply f_equal2 with (f := Nat.add); auto.
rewrite !Nat.mul_succ_r.
Qed.
``````

#### Guillaume Melquiond (Apr 07 2023 at 16:20):

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

#### Laurent Théry (Apr 07 2023 at 16:24):

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