## Stream: Coq users

### Topic: lia shows error.

#### Julin S (Sep 15 2022 at 12:34):

I was trying to prove that addition/subtraction of an odd and even nat would be an odd number.

So I tried:

``````Definition even_odd : forall n m:nat,
(Nat.Even n) /\ (Nat.Odd m)
-> Nat.Odd (n+m) /\ Nat.Odd (n-m).
Proof.
intros n m [[p Hp] [q Hq]].
unfold Nat.Odd.
rewrite Hp.
rewrite Hq.
split.
- exists (p+q).
lia.
- exists (p-q-1).
``````

At this point the goal was:

``````1 subgoal (ID 64)

n, m, p : nat
Hp : n = 2 * p
q : nat
Hq : m = 2 * q + 1
============================
2 * p - (2 * q + 1) = 2 * (p - q - 1) + 1
``````

This equality holds, right?

But when I tried `lia` after this, it said:

``````Error: Tactic failure:  Cannot find witness.
``````

What am I missing here?

#### Julin S (Sep 15 2022 at 12:34):

(And is `/\` commutative?)

#### Olivier Laurent (Sep 15 2022 at 12:38):

try `p = 0` and `q = 1`

#### James Wood (Sep 15 2022 at 12:38):

Set `p := q := 0`. Then, the LHS is `0 - 1`, which is `0`, while the RHS is `2 * (0 - 0 - 1) + 1`, which is `2 * 0 + 1`, which is `1`.

#### Olivier Laurent (Sep 15 2022 at 12:40):

Concerning your original goal, you will have `Nat.Even (n - m)` as soon as `n < m` since then `n - m = 0`.

#### Michael Soegtrop (Sep 15 2022 at 12:44):

I ask QuickChick such "why" questions:

``````From QuickChick Require Import QuickChick.
Import QcNotation.

Conjecture test: forall p q,  2 * p - (2 * q + 1) = 2 * (p - q - 1) + 1.

QuickChick test.
``````

results in

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

Indeed for p=q=0 the left hand side is 0 (observe that 0-1=0 for nat). The right hand side is 1 (for the same reason).

#### Michael Soegtrop (Sep 15 2022 at 12:45):

For Z instead of nat, this holds, btw.

#### Pierre Castéran (Sep 15 2022 at 13:56):

With an additional hypothesis, it's OK.

``````Lemma even_odd : forall n m:nat,
Nat.Even n -> Nat.Odd m ->
Nat.Odd (n+m) /\ (n <= m -> Nat.Odd (m-n)).
Proof.
intros n m  [p Hp] [q Hq]; subst; split.
- exists (p+q); lia.
- intro Hle; exists (q-p); lia.
Qed.
``````

Last updated: Oct 03 2023 at 21:01 UTC