短(er)证明'forall nk,(forall q,n <> q*3) - > n + n <> k*3

Question

在一个证明中我需要表明"如果n不是三的倍数,那么n + n也不是三的倍数." 我认为我的证据太长而且不太优雅.是否有一些更漂亮的写作方式？有没有ssreflect？(我确定在ssreflect中有一个oneliner :)).

我的证据n以三步为单位进行归纳.

Require Import Omega.
Lemma math_helper n: forall k, (forall q, n <> q * 3) ->  n + n <> k * 3.
  (* name the predicate Q and strengthen induction hypothesis *)
  pattern n; match goal with [ _:_ |- ?P ?n] => let X := fresh Q in remember P as X end.
  enough (Q n /\ Q (1+n) /\ Q (2+n)) by tauto.
  induction n; subst Q;
    [| destruct IHn as [IH1 [IH2 IH3]]];
    repeat split; simpl; intros; auto; try omega.
  intro C; assert (k>=2) by omega; do 2 (try destruct k); try omega.
  assert (n+n = k*3) by omega.
  apply (IH1 k); auto; intros q HH; eapply (H (1+q)); subst n; omega.
Qed.

Answer 1

通常情况下,答案是ssreflect one-liner:

From mathcomp Require Import ssreflect ssrbool ssrnat div.

Lemma math_helper n : 3 %| n.*2 -> 3 %| n.
Proof. by rewrite -muln2 Gauss_dvdl. Qed.

好吧,我作弊了一点,因为我改变了定理的陈述.这是您实际要求的证明.

Lemma math_helper n k : (forall q, n <> q * 3) -> n + n <> k * 3.
Proof.
rewrite addnn -mul2n mulnC => h1 h2.
suff/dvdnP [q /h1]: 3 %| n by [].
by rewrite -(@Gauss_dvdl _ _ 2) //; apply/dvdnP; eauto.
Qed.

Answer 2

有一个更简单的解决方案,只依靠分裂,并让欧米茄做推理.

Lemma math_helper2 n : forall k, (forall q, n <> q * 3) ->  n + n <> k * 3.
Proof.
intros k kq A.
assert (k = 2 * (k / 2) + k mod 2) by (apply Nat.div_mod; omega).
assert (k mod 2 < 2) by (apply (Nat.mod_bound_pos k 2); omega).
apply (kq (k/2)); omega.
Qed.

Answer 3

这也可以使用标准库中的高斯引理在vanilla Coq中解决(因此以下仅仅是对Arthur已经展示的内容的重新表述):

Require Import Coq.Numbers.Natural.Peano.NPeano.

Lemma math_helper n k : (forall q, n <> q * 3) -> n + n <> k * 3.
Proof.
  fold (Nat.double n); rewrite Nat.double_twice, (Nat.mul_comm k 3); intros H1 H2.
  assert (3 | 2 * n) as H3 by (rewrite H2; apply Nat.divide_factor_l).
  apply Nat.gauss in H3 as [x contra]; auto.
  apply (H1 _ contra).
Qed.