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?

Counterexample: t = x = y = 0.

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

Felipe Lisboa Malaquias has marked this topic as resolved.

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

@Mukesh Tiwari Open a feature request issue on Github!

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!

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

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

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

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