## Stream: Coq users

### Topic: Simple inequality between sum of monomes

#### Fabian Kunze (Dec 11 2020 at 12:40):

Does anyone have an Idea how to solve this kind of goals, inequalities over nat where all parts of the sum on the LHS appear syntactically in the sum on the RHS, fast and automatic?

``````Import Nat.
Require Import Lia.
Goal forall maxPro maxVar maxDepth n c' c'' n0 n1 n2 n3,

n3 + n2 + n1 + n0 + c'' + 1 <=
n3 * n + n3 + n2 * n + n2 + n1 * n + n1 + n0 * n + n0 + c'' * n + c'' +
n * c' * maxVar + n * c' + n * maxPro + n * maxDepth + n +
c' * maxVar + c' + maxPro + maxDepth + 1.
Proof.
Fail timeout 10 lia.
Qed.
``````

(Lia fails probably because it `zify`es first and introduces a lot of inequalities.

I have a tactic that finds and "removes" matching items. It is very fast, but diverges at QED time (related: coq/coq#8044 ):

``````Require Import ZArith.
Ltac leq_crossout :=
try zify;try apply Zle_0_minus_le; ring_simplify;
repeat eapply Z.add_nonneg_nonneg;try now (repeat eapply Z.mul_nonneg_nonneg;easy).
``````

#### Fabian Kunze (Dec 11 2020 at 12:41):

(well, `leq_crossout` maybe does not diverge, but takes more than 38 seconds to qed, which i find unacceptable.)

#### Paolo Giarrusso (Dec 11 2020 at 12:52):

not sure if relevant but `easy` automatically tries `inversion` (which produces somewhat big proof terms), unlike e.g. ssreflect/stdpp's done

#### Fabian Kunze (Dec 11 2020 at 13:01):

And `try now (...;easy)` is also a bit redundant, but sadly/luckily this is not the source of slowness.
Maybe i should generalize over all products, as there might be irrelevant case distinctions on the sign of the two sides of the product.

#### Andrej Dudenhefner (Dec 11 2020 at 13:19):

@Fabian Kunze For your very particular goal, here is one somewhat fast solution:

``````Import Nat.
Require Import Lia.

Lemma aux {m n k} : m <= k - n -> n <= k -> n + m <= k.
Proof. lia. Qed.

Goal forall maxPro maxVar maxDepth n c' c'' n0 n1 n2 n3,

n3 + n2 + n1 + n0 + c'' + 1 <=
n3 * n + n3 + n2 * n + n2 + n1 * n + n1 + n0 * n + n0 + c'' * n + c'' +
n * c' * maxVar + n * c' + n * maxPro + n * maxDepth + n +
c' * maxVar + c' + maxPro + maxDepth + 1.
Proof.
intros *. repeat (rewrite <- PeanoNat.Nat.add_assoc).
do 5 (apply aux; [|lia]).
lia.
Qed.
``````

#### Andrej Dudenhefner (Dec 11 2020 at 13:20):

Maybe with an better `aux` the rewrite with `add_assoc` is not necessary.

#### Fabian Kunze (Dec 11 2020 at 13:21):

Thanks
Or why not this:

``````Import Nat.
Require Import Lia.

Goal forall maxPro maxVar maxDepth n c' c'' n0 n1 n2 n3,

n3 + n2 + n1 + n0 + c'' + 1 <=
n3 * n + n3 + n2 * n + n2 + n1 * n + n1 + n0 * n + n0 + c'' * n + c'' +
n * c' * maxVar + n * c' + n * maxPro + n * maxDepth + n +
c' * maxVar + c' + maxPro + maxDepth + 1.
Proof.
intros *. repeat (rewrite <- PeanoNat.Nat.add_assoc). lia.
Qed.
``````

(Yes, this is instantanious...)

#### Andrej Dudenhefner (Dec 11 2020 at 13:23):

Ah yes, should have tried this first.

#### Fabian Kunze (Dec 11 2020 at 13:23):

are you joking or do you have an idea why this works faster, expect because "it is somehow fragile"?

#### Andrej Dudenhefner (Dec 11 2020 at 13:25):

are you joking

a little of both, I also have long experience with trying to get `lia` to do it's job in a reasonable time and associativity is useful for this.

#### Andrej Dudenhefner (Dec 11 2020 at 13:30):

Here is a somewhat related `nia` puzzle: Find a term `SOLUTION` that makes the following work (fast)

``````Require Import Lia.

(* injective pairing *)
Definition enc_pair '(x, y) : nat := SOLUTION.

Lemma enc_pair_inj {xy x'y'} : enc_pair xy = enc_pair x'y' -> xy = x'y'.
Proof.
destruct xy as [x y]. destruct x'y' as [x' y']. cbn.
rewrite pair_equal_spec. nia.
Qed.
``````

Mathematically, `SOLUTION` = `(x + y) * (x + y) + y` suffices, but `nia` fails unless one adds `assert (x + y <> x' + y' \/ x + y = x' + y') by lia. destruct H; nia.`.

Last updated: Oct 01 2023 at 18:01 UTC