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?

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.

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

Guillaume Melquiond (Apr 07 2023 at 15:43):

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

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.
  now rewrite Nat.add_assoc.
Qed.

Last updated: Oct 04 2023 at 23:01 UTC