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?

(And is `/\`

commutative?)

try `p = 0`

and `q = 1`

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`

.

Concerning your original goal, you will have `Nat.Even (n - m)`

as soon as `n < m`

since then `n - m = 0`

.

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

For Z instead of nat, this holds, btw.

With an additional hypothesis, it's OK.

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

Last updated: Jan 29 2023 at 06:02 UTC