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?
p = 0 and
q = 1
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
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.
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 : 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