Stream: Coq users

Topic: Tiny proof without lia


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Julin S (Apr 07 2023 at 15:35):

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

view this post on Zulip Julin S (Apr 07 2023 at 15:37):

Too many such rewrites for us to write them manually?

view this post on Zulip 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.

view this post on Zulip Julin S (Apr 07 2023 at 15:40):

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

view this post on Zulip Guillaume Melquiond (Apr 07 2023 at 15:43):

simpl

view this post on Zulip Guillaume Melquiond (Apr 07 2023 at 15:44):

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

view this post on Zulip Julin S (Apr 07 2023 at 15:46):

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

view this post on Zulip 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: )

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Apr 07 2023 at 15:55):

you generally shouldn't need to simpl before reflexivity

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Mar 29 2024 at 10:01 UTC