## Stream: Coq users

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

#### 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?

#### Guillaume Melquiond (Jan 05 2023 at 14:21):

Counterexample: t = x = y = 0.

#### Felipe Lisboa Malaquias (Jan 05 2023 at 14:34):

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

#### Notification Bot (Jan 05 2023 at 14:34):

Felipe Lisboa Malaquias has marked this topic as resolved.

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

#### Ali Caglayan (Jan 07 2023 at 21:16):

@Mukesh Tiwari Open a feature request issue on Github!

#### 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!

#### Mukesh Tiwari (Jan 10 2023 at 10:08):

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

#### Karl Palmskog (Jan 10 2023 at 17:25):

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

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

#### 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: Jun 18 2024 at 07:01 UTC