Stream: Coq users

Topic: Simple inequality between sum of monomes


view this post on Zulip 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 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).

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Andrej Dudenhefner (Dec 11 2020 at 13:20):

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

view this post on Zulip 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...)

view this post on Zulip Andrej Dudenhefner (Dec 11 2020 at 13:23):

Ah yes, should have tried this first.

view this post on Zulip 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"?

view this post on Zulip 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.

view this post on Zulip 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: Mar 28 2024 at 23:01 UTC