Stream: Coq users

Topic: lia shows error.


view this post on Zulip 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?

view this post on Zulip Julin S (Sep 15 2022 at 12:34):

(And is /\ commutative?)

view this post on Zulip Olivier Laurent (Sep 15 2022 at 12:38):

try p = 0 and q = 1

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Michael Soegtrop (Sep 15 2022 at 12:45):

For Z instead of nat, this holds, btw.

view this post on Zulip Pierre Castéran (Sep 15 2022 at 13:56):

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