如何使用ssreflect以更优雅的方式证明目标？

Question

看来我的 coq 证明比预期更长、更难看，尽管我尝试了，但我无法在其中实现 ssreflect 优势。我想我错过了一些关键点。或者也许我只是需要了解更多策略。

这是我想出的一些证据。请帮助我找到并修复我做出的错误路线或决定。我用评论指出了我怀疑的线条。关于证据或知识来源的建议也很有用。

(* SSReflect proof language requires these libraries to be loaded and options to be set. *)
From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
From Coq Require Import Nat Arith Lia.

Lemma L1: forall A B C, A -> (A -> B /\ C) -> C.
Proof.
move => A B C H1 H2.
(* Seems like there is a way to apply H2 in H1 without moving them from goal. *)
apply H2 in H1. 
destruct H1 as [H3 Goal].
done.
Qed.

Lemma L2: forall A Q, (forall x, (exists y, x + y = y + x) -> A) -> Q -> A.
Proof.
move => A _ T _.
(* I think there is a better way then coming up with this "H" or smth. *)
assert (H: exists y, 2 + y = y + 2) by (exists 0; lia).
(* Again, there should be the way to do apply via ssreflect. *)
apply (T 2) in H.
done.
Qed.

Lemma divides_by_2_by_3_means_by_6 : 
        forall z p q, z = 2 * p -> z = 3 * q -> exists n, z = 6 * n. 
Proof.
move => a b c P Q.
(* Which way is better to create a subgoal? *)
assert (odd_or_even: forall n, (exists k, n = 2 * k) \/ (exists k, n = 2 * k + 1)). {
  induction n.
  - left. exists 0. lia.
  - destruct IHn as [[x H] | [x H]].
    + right; exists x; lia.
    + left; exists (x + 1); lia.
}
(* How can I add new fact in context? I found this way, but there should be the right one. *)
move : (odd_or_even c) => H.
destruct H as [[x H] | [x H]].
- exists x; lia.
- lia.
Qed.

Answer 1

如果您想充分利用

ssreflect

，您还可以考虑使用完整的数学组件库。但现在，我只说明策略，而不是定理。我是

ssreflect

和数学组件的频繁用户，因此这还将包含此库中强制执行的一些风格习惯（例如缩进约定，即 2 * (n - 1) 个空格，其中 n 是数字开放目标），以及在每行开头添加“by”以完成证明的习惯。

From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
From Coq Require Import Nat Arith Lia.

Lemma L1: forall A B C, A -> (A -> B /\ C) -> C.
Proof.
by move=> A B C /[swap] /[apply] - [].
Qed.

\[swap]

和

\[apply]

介绍模式是该语言最近添加的内容。

Lemma L2: forall A Q, (forall x, (exists y, x + y = y + x) -> A) -> Q -> A.
Proof.
by move=> A _ + _ => /(_ 2); apply; exists 0; lia.
Qed.

在此示例中，请注意使用

+

来表示该假设保留在目标中，而下一个假设则被

_

丢弃。

无参数的

apply

策略将其参数作为目标中箭头左侧的第一个命题。

Lemma divides_by_2_by_3_means_by_6 : 
  forall z p q, z = 2 * p -> z = 3 * q -> exists n, z = 6 * n. 
Proof.
move=> a b c.
have odd_or_even : forall n, (exists k, n = 2 * k) \/
  (exists k, n = 2 * k + 1).
  elim=> [ | n [[k kP] | [k kP]]]; first by left; exists 0.
    by right; exists k; lia.
  by left; exists (k + 1); lia.
move=> a b c P Q; move: (odd_or_even c)=> [[x H] | [x H]].
  by exists x; lia.
by lia.
Qed.

这里

elim

策略的行为类似于前面示例中的

apply

策略：它将其参数作为目标上最左边的普遍量化（或前提）。引入模式直接用于破坏作为析取或存在陈述的假设。

直到最近，数学组件还很少使用

lia

，因此这不是完全惯用的 ssreflect 代码，但它确实有效。就我个人而言，我对

lia

设法解决最后一个目标感到有点困惑。

Answer 2

只是为了好玩，这里是基于 Yves 想法的最后一个目标的可能的非基于 lia 的解决方案：

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma divides_by_2_by_3_means_by_6 : 
  forall z p q, z = 2 * p -> z = 3 * q -> exists n, z = 6 * n. 
Proof.
move=> a b c.
have odd_or_even : forall n, (exists k, n = 2 * k) \/
  (exists k, n = 2 * k + 1).
  elim=> [ | n [[k kP] | [k kP]]]; first by left; exists 0.
    by right; exists k; rewrite kP addn1.
  by left; exists (k + 1); rewrite kP -addnS mulnDr muln1.
move=> P Q; move: (odd_or_even c) => [[x H] | [x H]].
  by exists x; rewrite Q H mulnA; congr (_ * _).
move: P.
rewrite Q H => /eqP.
have -> : 3 * (2 * x + 1) = 2 * (3 * x + 1) + 1.
  by rewrite 2!mulnDr !mulnA mulnC -addnA; congr (_ + _).
have -> // : forall n m, (2 * n + 1 == 2 * m) = false.
  by move=> n m; rewrite !mul2n addn1 eqn_leq leq_Sdouble ltn_double ltnNge andNb.
Qed.

请注意，要证明的最后一个子目标（

exists n : nat, a = 6 * n

）是通过显示上下文是矛盾的来解决的，这是 lia 能够处理的。