Stream: Coq users

Topic: ✔ Why lia won't solve this goal?

view this post on Zulip Felipe Lisboa Malaquias (Jan 05 2023 at 14:14):

Hi, I don't quite get why lia fails for this goal:

Lemma test (t y x : N) :
        (2 * (t - (y - x) - 1) + 1)%N = (2 * t - (2 * y - 2 * x) - 1)%N.

Can anyone enlighten me?

view this post on Zulip Guillaume Melquiond (Jan 05 2023 at 14:21):

Counterexample: t = x = y = 0.

view this post on Zulip Felipe Lisboa Malaquias (Jan 05 2023 at 14:34):

Thanks. Indeed, adding (t > (y - x)) as precondition does the job.

view this post on Zulip Notification Bot (Jan 05 2023 at 14:34):

Felipe Lisboa Malaquias has marked this topic as resolved.

view this post on Zulip Mukesh Tiwari (Jan 07 2023 at 04:42):

@Guillaume Melquiond It would be nice to have if lia produces a counter example, when it fails.

view this post on Zulip Ali Caglayan (Jan 07 2023 at 21:16):

@Mukesh Tiwari Open a feature request issue on Github!

view this post on Zulip Michael Soegtrop (Jan 09 2023 at 09:33):

Mukesh Tiwari said:

Guillaume Melquiond It would be nice to have if lia produces a counter example, when it fails.

I am using QuickChick for this purpose:

Require Import QuickChick.QuickChick.
Require Import NArith.
Conjecture test: forall (t y x : N),
        (2 * (t - (y - x) - 1) + 1)%N = (2 * t - (2 * y - 2 * x) - 1)%N.
QuickCheck test.

results in:

QuickChecking test
0
0
0
*** Failed after 1 tests and 0 shrinks. (0 discards)

The 0 0 0 are the counter example values for the variables in order they are given. QuickChick has the advantage that it is very generic and can handle e.g. goals lia can't handle. In my experience it is very worthwhile to get used to it. But indeed having counter examples from lia would be nice!

view this post on Zulip Mukesh Tiwari (Jan 10 2023 at 10:08):

@Michael Soegtrop Very nice! I never used QuickChick but I think I should start using it.

view this post on Zulip Karl Palmskog (Jan 10 2023 at 17:25):

model finding and QuickCheck-like testing are two almost (theoretically) disjoint ways to find counterexamples

view this post on Zulip Karl Palmskog (Jan 10 2023 at 17:27):

I think Isabelle is the only system that has them under a single roof with Nitpick et al.

view this post on Zulip Michael Soegtrop (Jan 11 2023 at 09:04):

I am already quite happy that I can formulate a statement once and then use quite different tools, like QuickChick, Lia, manual proofs, ... to work on it.

Last updated: Oct 13 2024 at 01:02 UTC