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).
```

(well, `leq_crossout`

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

not sure if relevant but `easy`

automatically tries `inversion`

(which produces somewhat big proof terms), unlike e.g. ssreflect/stdpp's done

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.

@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.
```

Maybe with an better `aux`

the rewrite with `add_assoc`

is not necessary.

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...)

Ah yes, should have tried this first.

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

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.

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: Jan 29 2023 at 01:02 UTC