Simple inequality between sum of monomes · Coq users

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 zifyes 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):

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

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.

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

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

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

Stream: Coq users

Topic: Simple inequality between sum of monomes

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