Julin S (Sep 15 2022 at 12:34): 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