Basic manipulation of algebraic expressions

user_4453951 0
Viewed 52

I'm still missing the basic technique to manipulate algebraic expressions by adding the same value to both sides. For instance, if the present goal is a + b < a + 5, how do I transform it to b < 5 as one would do in a pen-paper proof? Thanks for any help.

coq
2 Answers

For this kind of things, you need to use the lemmata that already prove this. Most of these are proven in Arith. If you type

From Coq Require Import Arith.
Search "+" "<".

Coq will tell you of lemmata that talk about both addition and the 'lower than' relation. In particular you will find

plus_lt_compat_l: forall n m p : nat, n < m -> p + n < p + m

So that

Goal forall a b, a + b < a + 5.
  intros a b.
  apply plus_lt_compat_l.

will indeed leave you to prove b < 5.

More often than not, you do not really want to go through the search and instead use some automation. For this lia is recommended.

From Coq Require Import Lia.

Goal forall a b, a + b < a + 5.
  intros a b.
  cut (b < 5).
  { lia. }
  (* The remaining goal is b < 5 *)

lia is a tactic that solves many arithmetic problems like those.

user_12759750

Ok, let's set up this goal. Although nat and < are predefined, you need Require Import Arith for many basic theorems about arithmetic.

Require Import Arith.
Goal forall a b : nat, b < 5 -> a + b < a + 5.
  intros.

First let's see how to find the right lemma from the library manually. We can search the available lemmas whose conclusion has the right shape.

SearchPattern (_+_ < _+_).

This returns many lemmas, one of which happens to have the right shape (were the left-hand sides of the + operator are the same on both sides): plus_lt_compat_l. So we can apply this lemma.

  apply plus_lt_compat_l.
  assumption.
Qed.

Note that sometimes there might be a lemma with < but not one with <=, and SearchPattern won't find that. In such cases, unfold lt in *. to expand all uses of < to <= might help, possibly followed by additional rewriting to move the S around.

Of course finding the right lemma each time is tedious, so there are ways to automate this search. One of the ways is to use a hint database. There's a built-in database called arith, which includes this lemma. auto with arith tries to apply any combination of lemmas from the arith database up to a certain depth. The variant eauto with arith, not needed here, would also try to invent intermediate variables.

Require Import Arith.
Goal forall a b : nat, b < 5 -> a + b < a + 5.
  intros.
  auto with arith.
Qed.

For arithmetic specifically, there are “just solve this” targets, such as lia (or omega in older versions of Coq), which can solve any inequation involving additions of variables and constants.

Require Import Omega.
Goal forall a b : nat, b < 5 -> a + b < a + 5.
  intros.
  omega.
Qed.
user_3870760
Related