how to simplify basic arithmetic in more complex goals

Question

Here's a minimal example of my problem

Lemma arith: forall T (G: seq T), (size G + 1 + 1).+1 = (size G + 3).

I would like to be able to reduce this to forall T (G: seq T), (size G + 2).+1 = (size G + 3).

by the simplest possible means. Trying simpl or auto immediately does nothing.

If I rewrite with associativity first, that is,

intros. rewrite - addnA. simpl. auto.,

simpl and auto still do nothing. I am left with a goal of

(size G + (1 + 1)).+1 = size G + 3

I guess the .+1 is "in the way" of simpl and auto working on the (1+1) somehow. It seems like I must first remove the .+1 before I can simplify the 1+1.

However, in my actual proof, there is a lot more stuff than the .+1 "in the way" and I would really like to simplify my copious amount of +1s first. As a hack, I'm using 'replace' on individual occurrences but this feels very clumsy (and there are a lot of different arithmetic expressions to replace). Is there any better way to do this?

I am using the ssrnat library.

Thanks.

Answer 1

Coq has a ring and ring_simplify tactic for this kind of work. Sorry for my ssreflect ignorant intros, but this works:

From mathcomp Require Import all_ssreflect.

Lemma arith: forall T (G: seq T), (size G + 1 + 1).+1 = (size G + 3).
Proof.
  intros.
  ring.
Qed.

There is also a field and field_simplify. For inequalities there are lia and lra, but I am not sure if these work in mathcomp - for lia you might need this (https://github.com/math-comp/mczify) but it might be integrated meanwhile.

Answer 2

There are many lemmas in ssrnat to reason about addition. One possible solution to your problem is the following:

From mathcomp Require Import all_ssreflect.

Lemma arith: forall T (G: seq T), (size G + 1 + 1).+1 = (size G + 3).
Proof. by move=> T G; rewrite !addn1 addn3. Qed.

where

addn1 : forall n, n + 1 = n.+1
addn3 : forall n, n + 3 = n.+3 (* := n.+1.+1.+1 *)

You can use the Search command to look for lemmas related to certain term patterns. For instance, Search (_ + 1) returns, among other things, addn1.