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.
lia resolved the whole thing.
Any idea how a more 'manual' proof can turn out?
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
Goal forall n:nat, S n * S n = n * n + 2 * n + 1.
How can we solve this without
Natural numbers aren't rings, but under what circumstances can we use the
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
ring, you can prove the property by sufficiently many applications of a few rewriting rules like
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)?
(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: )
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: Oct 04 2023 at 23:01 UTC